Physlib.Units.UnitDependent

Physlib
Units
UnitDependent

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Units.Basic
public import Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Types which depend on dimensions

In addition to types which carry a dimension, we also have types whose elements depend on a choice of a units. For example a function f : M1 → M2 between two types M1 and M2 which carry dimensions does not itself carry a dimensions, but is dependent on a choice of units.

We define three versions

UnitDependent M having a function scaleUnit : LTMCTUnitChoices → LTMCTUnitChoices → M → M subject to two conditions scaleUnit_trans and scaleUnit_id

LinearUnitDependent M extends UnitDependent M with additional linearity conditions on scaleUnit.

ContinuousLinearUnitDependent M extends LinearUnitDependent M with an additional continuity condition on scaleUnit.

@[expose] public section

A type carries the instance UnitDependent M if it depends on a choice of units. This dependence is manifested in scaleUnit u1 u2 which describes how elements of M change under a scaling of units which would take u1 to u2.

This type is used for functions, and propositions etc.

scaleUnit u1 u2 is the map transforming elements of M under a scaling of units which would take the unit u1 to the unit u2. This is not to say that in scaleUnit u1 u2 m that m should be interpreted as being in the units u1, although this is often the case.

class UnitDependent (M : Type) where

  scaleUnit : LTMCTUnitChoices → LTMCTUnitChoices → M → M
  scaleUnit_trans : ∀ u1 u2 u3 m, scaleUnit u2 u3 (scaleUnit u1 u2 m) = scaleUnit u1 u3 m
  scaleUnit_trans' : ∀ u1 u2 u3 m, scaleUnit u1 u2 (scaleUnit u2 u3 m) = scaleUnit u1 u3 m
  scaleUnit_id : ∀ u m, scaleUnit u u m = m

A type M with an instance of UnitDependent M such that scaleUnit u1 u2 is compatible with the MulAction ℝ≥0 M instance on M.

class MulUnitDependent (M : Type) [MulAction ℝ≥0 M] extends
    UnitDependent M where
  scaleUnit_mul : ∀ u1 u2 (r : ℝ≥0) m,
    scaleUnit u1 u2 (r • m) = r • scaleUnit u1 u2 m

A type M with an instance of UnitDependent M such that scaleUnit u1 u2 is compatible with the Module ℝ M instance on M.

class LinearUnitDependent (M : Type) [AddCommMonoid M] [Module ℝ M] extends UnitDependent M where
  scaleUnit_add : ∀ u1 u2 m1 m2,
    scaleUnit u1 u2 (m1 + m2) = scaleUnit u1 u2 m1 + scaleUnit u1 u2 m2
  scaleUnit_smul : ∀ u1 u2 (r : ℝ) m,
    scaleUnit u1 u2 (r • m) = r • scaleUnit u1 u2 m

A type M with an instance of UnitDependent M such that scaleUnit u1 u2 is compatible with the Module ℝ M instance on M, and is continuous.

class ContinuousLinearUnitDependent (M : Type) [AddCommMonoid M] [Module ℝ M]
    [TopologicalSpace M] extends LinearUnitDependent M where
  scaleUnit_cont : ∀ u1 u2, Continuous (scaleUnit u1 u2)

## Basic properties of scaleUnit



@[simp]
lemma UnitDependent.scaleUnit_symm_apply {M : Type} [UnitDependent M]
    (u1 u2 : LTMCTUnitChoices) (m : M) :
    scaleUnit u2 u1 (scaleUnit u1 u2 m) = m := byM:Typeinst✝:UnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesm:M⊢ scaleUnit u2 u1 (scaleUnit u1 u2 m) = m
  rw [scaleUnit_trans,M:Typeinst✝:UnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesm:M⊢ scaleUnit u1 u1 m = mAll goals completed! 🐙 scaleUnit_idM:Typeinst✝:UnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesm:M⊢ m = mAll goals completed! 🐙]All goals completed! 🐙

@[simp]
lemma UnitDependent.scaleUnit_injective {M : Type} [UnitDependent M]
    (u1 u2 : LTMCTUnitChoices) (m1 m2 : M) :
    scaleUnit u1 u2 m1 = scaleUnit u1 u2 m2 ↔ m1 = m2 :=
  ⟨fun h => byM:Typeinst✝:UnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesm1:Mm2:Mh:scaleUnit u1 u2 m1 = scaleUnit u1 u2 m2⊢ m1 = m2 simpa using congrArg (scaleUnit u2 u1) hAll goals completed! 🐙, congrArg (scaleUnit u1 u2)⟩

### Variations on the map scaleUnit

For an M with an instance of UnitDependent M, scaleUnit u1 u2 as an equivalence.

def UnitDependent.scaleUnitEquiv {M : Type} [UnitDependent M]
    (u1 u2 : LTMCTUnitChoices) : M ≃ M where
  toFun m := scaleUnit u1 u2 m
  invFun m := scaleUnit u2 u1 m
  right_inv m := byM:Typeinst✝:UnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesm:M⊢ (fun m => scaleUnit u1 u2 m) ((fun m => scaleUnit u2 u1 m) m) = m simpAll goals completed! 🐙
  left_inv m := byM:Typeinst✝:UnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesm:M⊢ (fun m => scaleUnit u2 u1 m) ((fun m => scaleUnit u1 u2 m) m) = m simpAll goals completed! 🐙

For an M with an instance of LinearUnitDependent M, scaleUnit u1 u2 as a linear map.

def LinearUnitDependent.scaleUnitLinear
    {M : Type} [AddCommMonoid M] [Module ℝ M] [LinearUnitDependent M]
    (u1 u2 : LTMCTUnitChoices) :
    M →ₗ[ℝ] M where
  toFun m := scaleUnit u1 u2 m
  map_add' m1 m2 := byM:Typeinst✝²:AddCommMonoid Minst✝¹:Module ℝ Minst✝:LinearUnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesm1:Mm2:M⊢ scaleUnit u1 u2 (m1 + m2) = scaleUnit u1 u2 m1 + scaleUnit u1 u2 m2 simp [LinearUnitDependent.scaleUnit_add]All goals completed! 🐙
  map_smul' r m2 := byM:Typeinst✝²:AddCommMonoid Minst✝¹:Module ℝ Minst✝:LinearUnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesr:ℝm2:M⊢ scaleUnit u1 u2 (r • m2) = (RingHom.id ℝ) r • scaleUnit u1 u2 m2 simp [LinearUnitDependent.scaleUnit_smul]All goals completed! 🐙

For an M with an instance of LinearUnitDependent M, scaleUnit u1 u2 as a linear equivalence.

def LinearUnitDependent.scaleUnitLinearEquiv {M : Type} [AddCommMonoid M]
    [Module ℝ M] [LinearUnitDependent M] (u1 u2 : LTMCTUnitChoices) :
    M ≃ₗ[ℝ] M :=
    LinearEquiv.ofLinear (scaleUnitLinear u1 u2) (scaleUnitLinear u2 u1)
    (byM:Typeinst✝²:AddCommMonoid Minst✝¹:Module ℝ Minst✝:LinearUnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnitLinear u1 u2 ∘ₗ scaleUnitLinear u2 u1 = LinearMap.id ext uM:Typeinst✝²:AddCommMonoid Minst✝¹:Module ℝ Minst✝:LinearUnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesu:M⊢ (scaleUnitLinear u1 u2 ∘ₗ scaleUnitLinear u2 u1) u = LinearMap.id u; simp [scaleUnitLinear]All goals completed! 🐙)
    (byM:Typeinst✝²:AddCommMonoid Minst✝¹:Module ℝ Minst✝:LinearUnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnitLinear u2 u1 ∘ₗ scaleUnitLinear u1 u2 = LinearMap.id ext uM:Typeinst✝²:AddCommMonoid Minst✝¹:Module ℝ Minst✝:LinearUnitDependent Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesu:M⊢ (scaleUnitLinear u2 u1 ∘ₗ scaleUnitLinear u1 u2) u = LinearMap.id u; simp [scaleUnitLinear]All goals completed! 🐙)

For an M with an instance of ContinuousLinearUnitDependent M, scaleUnit u1 u2 as a continuous linear map.

def ContinuousLinearUnitDependent.scaleUnitContLinear {M : Type} [AddCommMonoid M] [Module ℝ M]
    [TopologicalSpace M] [ContinuousLinearUnitDependent M]
    (u1 u2 : LTMCTUnitChoices) : M →L[ℝ] M where
  toLinearMap := LinearUnitDependent.scaleUnitLinear u1 u2
  cont := ContinuousLinearUnitDependent.scaleUnit_cont u1 u2

For an M with an instance of ContinuousLinearUnitDependent M, scaleUnit u1 u2 as a continuous linear equivalence.

def ContinuousLinearUnitDependent.scaleUnitContLinearEquiv {M : Type} [AddCommMonoid M] [Module ℝ M]
    [TopologicalSpace M] [ContinuousLinearUnitDependent M]
    (u1 u2 : LTMCTUnitChoices) : M ≃L[ℝ] M :=
    ContinuousLinearEquiv.mk (LinearUnitDependent.scaleUnitLinearEquiv u1 u2)
    (ContinuousLinearUnitDependent.scaleUnit_cont u1 u2)
    (ContinuousLinearUnitDependent.scaleUnit_cont u2 u1)

@[simp]
lemma ContinuousLinearUnitDependent.scaleUnitContLinearEquiv_apply
    {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    [ContinuousLinearUnitDependent M]
    (u1 u2 : LTMCTUnitChoices) (m : M) :
    (ContinuousLinearUnitDependent.scaleUnitContLinearEquiv u1 u2) m =
      scaleUnit u1 u2 m := rfl

@[simp]
lemma ContinuousLinearUnitDependent.scaleUnitContLinearEquiv_symm_apply
    {M : Type} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M]
    [ContinuousLinearUnitDependent M]
    (u1 u2 : LTMCTUnitChoices) (m : M) :
    (ContinuousLinearUnitDependent.scaleUnitContLinearEquiv u1 u2).symm m =
      scaleUnit u2 u1 m := rfl

Instances of the type classes

We construct instance of the UnitDependent, LinearUnitDependent and ContinuousLinearUnitDependent type classes based on CarriesDimension and functions.

              @[simp]
lemma LTMCTUnitChoices.scaleUnit_apply_fst (u1 u2 : LTMCTUnitChoices) :
    (scaleUnit u1 u2 u1) = u2 := byu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnit u1 u2 u1 = u2
  extlengthu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).length = u2.lengthtimeu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).time = u2.timemassu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).mass = u2.masschargeu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).charge = u2.chargetemperatureu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).temperature = u2.temperature <;>lengthu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).length = u2.lengthtimeu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).time = u2.timemassu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).mass = u2.masschargeu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).charge = u2.chargetemperatureu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ (scaleUnit u1 u2 u1).temperature = u2.temperature simp [scaleUnit, LengthUnit.scale, TimeUnit.scale, MassUnit.scale, ChargeUnit.scale,
    TemperatureUnit.scale, LengthUnit.div_eq_val, TimeUnit.div_eq_val, MassUnit.div_eq_val,
    ChargeUnit.div_eq_val, TemperatureUnit.div_eq_val, toReal]All goals completed! 🐙@[simp]
lemma LTMCTUnitChoices.dimScale_scaleUnit {u1 u2 u : LTMCTUnitChoices}
    (d : Dimension LTMCTDimensionBase) :
    u.dimScale (scaleUnit u1 u2 u) d = u1.dimScale u2 d := byu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesu:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u.dimScale (scaleUnit u1 u2 u)) d = (u1.dimScale u2) d
  simp [dimScale, scaleUnit]u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesu:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ ⟨(↑(u2.length / u1.length))⁻¹, ⋯⟩ ^ ↑d.length * ⟨(↑(u2.time / u1.time))⁻¹, ⋯⟩ ^ ↑d.time *
        ⟨(↑(u2.mass / u1.mass))⁻¹, ⋯⟩ ^ ↑d.mass *
      ⟨(↑(u2.charge / u1.charge))⁻¹, ⋯⟩ ^ ↑d.charge *
    ⟨(↑(u2.temperature / u1.temperature))⁻¹, ⋯⟩ ^ ↑d.temperature =
  (u1.length / u2.length) ^ ↑d.length * (u1.time / u2.time) ^ ↑d.time * (u1.mass / u2.mass) ^ ↑d.mass *
      (u1.charge / u2.charge) ^ ↑d.charge *
    (u1.temperature / u2.temperature) ^ ↑d.temperature
  simp [LengthUnit.div_eq_val, TimeUnit.div_eq_val, MassUnit.div_eq_val, ChargeUnit.div_eq_val,
    TemperatureUnit.div_eq_val, toReal]All goals completed! 🐙

lemma Dimensionful.of_scaleUnit {M : Type} [CarriesDimension M] {u1 u2 u : LTMCTUnitChoices}
    (c : Dimensionful M) :
    c.1 (scaleUnit u1 u2 u) =
    u1.dimScale u2 (dim M) • c.1 (u) := byM:Typeinst✝:CarriesDimension Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesu:LTMCTUnitChoicesc:Dimensionful M⊢ ↑c (scaleUnit u1 u2 u) = (u1.dimScale u2) (dim M) • ↑c u
  rw [c.2 u (scaleUnit u1 u2 u),M:Typeinst✝:CarriesDimension Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesu:LTMCTUnitChoicesc:Dimensionful M⊢ (u.dimScale (scaleUnit u1 u2 u)) (dim M) • ↑c u = (u1.dimScale u2) (dim M) • ↑c uAll goals completed! 🐙 LTMCTUnitChoices.dimScale_scaleUnitM:Typeinst✝:CarriesDimension Mu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesu:LTMCTUnitChoicesc:Dimensionful M⊢ (u1.dimScale u2) (dim M) • ↑c u = (u1.dimScale u2) (dim M) • ↑c uAll goals completed! 🐙]All goals completed! 🐙lemma HasDim.scaleUnit_apply {M : Type} [CarriesDimension M]
    (u1 u2 : LTMCTUnitChoices) (m : M) :
    scaleUnit u1 u2 m = (u1.dimScale u2 (dim M)) • m :=
  toDimensionful_apply_apply u1 u2 m

Functions

              @[simp]
lemma UnitDependent.scaleUnit_apply_fun_right {M1 M2 : Type} [UnitDependent M2]
    (u1 u2 : LTMCTUnitChoices) (f : M1 → M2) (m1 : M1) :
    scaleUnit u1 u2 f m1 = scaleUnit u1 u2 (f m1) := rfl@[simp]
lemma UnitDependent.scaleUnit_apply_fun_left {M1 M2 : Type} [UnitDependent M1]
    (u1 u2 : LTMCTUnitChoices) (f : M1 → M2) (m1 : M1) :
    scaleUnit u1 u2 f m1 = f (scaleUnit u2 u1 m1) := rfl@[simp]
lemma UnitDependent.scaleUnit_apply_fun {M1 M2 : Type} [UnitDependent M1]
    [UnitDependent M2] (u1 u2 : LTMCTUnitChoices) (f : M1 → M2) (m1 : M1) :
    scaleUnit u1 u2 f m1 = scaleUnit u1 u2 (f (scaleUnit u2 u1 m1)) := rfl@[simp]
lemma ContinuousLinearUnitDependent.scaleUnit_apply_fun {M1 M2 : Type}
    [AddCommGroup M1] [Module ℝ M1]
    [TopologicalSpace M1] [ContinuousLinearUnitDependent M1]
    [AddCommGroup M2] [Module ℝ M2] [TopologicalSpace M2] [ContinuousConstSMul ℝ M2]
    [IsTopologicalAddGroup M2]
    [ContinuousLinearUnitDependent M2]
    (u1 u2 : LTMCTUnitChoices) (f : M1 →L[ℝ] M2) (m1 : M1) :
    scaleUnit u1 u2 f m1 =
      scaleUnit u1 u2 (f (scaleUnit u2 u1 m1)) := rfl

isDimensionallyCorrect

A term of type M carrying an instance of UnitDependent M is said to be dimensionally correct if under a change of units it remains the same.

More colloquially, something is dimensionally correct if it (e.g. it's value or its truth for a proposition) does not depend on the units it is written in.

For the case of m : M with CarriesDimension M then IsDimensionallyCorrect m corresponds to the statement that m does not depend on units, e.g. is zero or the dimension of M is zero.

def IsDimensionallyCorrect {M : Type} [UnitDependent M] (m : M) : Prop :=
  ∀ u1 u2 : LTMCTUnitChoices, scaleUnit u1 u2 m = m

              lemma isDimensionallyCorrect_iff {M : Type} [UnitDependent M] (m : M) :
    IsDimensionallyCorrect m ↔ ∀ u1 u2 : LTMCTUnitChoices,
      scaleUnit u1 u2 m = m := byM:Typeinst✝:UnitDependent Mm:M⊢ IsDimensionallyCorrect m ↔ ∀ (u1 u2 : LTMCTUnitChoices), scaleUnit u1 u2 m = m rflAll goals completed! 🐙@[simp]
lemma isDimensionallyCorrect_fun_iff {M1 M2 : Type} [UnitDependent M1] [UnitDependent M2]
    {f : M1 → M2} :
    IsDimensionallyCorrect f ↔
    ∀ u1 u2 : LTMCTUnitChoices, ∀ m, scaleUnit u1 u2 (f (scaleUnit u2 u1 m)) = f m := byM1:TypeM2:Typeinst✝¹:UnitDependent M1inst✝:UnitDependent M2f:M1 → M2⊢ IsDimensionallyCorrect f ↔ ∀ (u1 u2 : LTMCTUnitChoices) (m : M1), scaleUnit u1 u2 (f (scaleUnit u2 u1 m)) = f m
  simp [IsDimensionallyCorrect, funext_iff]All goals completed! 🐙@[simp]
lemma isDimensionallyCorrect_fun_left {M1 M2 : Type} [UnitDependent M1]
    {f : M1 → M2} :
    IsDimensionallyCorrect f ↔
    ∀ u1 u2 : LTMCTUnitChoices, ∀ m, (f (scaleUnit u2 u1 m)) = f m := byM1:TypeM2:Typeinst✝:UnitDependent M1f:M1 → M2⊢ IsDimensionallyCorrect f ↔ ∀ (u1 u2 : LTMCTUnitChoices) (m : M1), f (scaleUnit u2 u1 m) = f m
  simp [IsDimensionallyCorrect, funext_iff]All goals completed! 🐙@[simp]
lemma isDimensionallyCorrect_fun_right {M1 M2 : Type} [UnitDependent M2]
    {f : M1 → M2} :
    IsDimensionallyCorrect f ↔
    ∀ u1 u2 : LTMCTUnitChoices, ∀ m, scaleUnit u1 u2 (f m) = f m := byM1:TypeM2:Typeinst✝:UnitDependent M2f:M1 → M2⊢ IsDimensionallyCorrect f ↔ ∀ (u1 u2 : LTMCTUnitChoices) (m : M1), scaleUnit u1 u2 (f m) = f m
  simp [IsDimensionallyCorrect, funext_iff]All goals completed! 🐙

Some type classes to help track dimensions

The multiplication of an element of M1 with an element of M2 to get an element of M3 in such a way that dimensions are preserved.

class DMul (M1 M2 M3 : Type) [CarriesDimension M1] [CarriesDimension M2] [CarriesDimension M3]
    extends HMul M1 M2 M3 where
  mul_dim : ∀ (m1 : Dimensionful M1) (m2 : Dimensionful M2),
    HasDimension (fun u => hMul (m1.1 u) (m2.1 u))

@[simp]
lemma DMul.hMul_scaleUnit {M1 M2 M3 : Type} [CarriesDimension M1] [CarriesDimension M2]
    [CarriesDimension M3]
    [DMul M1 M2 M3] (m1 : M1) (m2 : M2) (u1 u2 : LTMCTUnitChoices) :
    (scaleUnit u1 u2 m1) * (scaleUnit u1 u2 m2) =
    scaleUnit u1 u2 (m1 * m2) := byM1:TypeM2:TypeM3:Typeinst✝³:CarriesDimension M1inst✝²:CarriesDimension M2inst✝¹:CarriesDimension M3inst✝:DMul M1 M2 M3m1:M1m2:M2u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnit u1 u2 m1 * scaleUnit u1 u2 m2 = scaleUnit u1 u2 (m1 * m2)
  simpa [scaleUnit, toDimensionful] using
    DMul.mul_dim (M3 := M3) (toDimensionful u1 m1) (toDimensionful u1 m2) u1 u2All goals completed! 🐙

Dim Subtype

Given a type M that depends on units, e.g. the function type M1 → M2 between two types carrying a dimension, the subtype of M which scales according to the dimension d.

def DimSet (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension LTMCTDimensionBase) :
    Set M :=
  {m : M | ∀ u1 u2, scaleUnit u1 u2 m = (LTMCTUnitChoices.dimScale u1 u2 d) • m}

              

instance (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension LTMCTDimensionBase) :
    MulAction ℝ≥0 (DimSet M d) where
  smul a f := ⟨a • f.1, fun u1 u2 => byM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0f:↑(DimSet M d)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnit u1 u2 (a • ↑f) = (u1.dimScale u2) d • a • ↑f
    rw [smul_comm,M:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0f:↑(DimSet M d)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnit u1 u2 (a • ↑f) = a • (u1.dimScale u2) d • ↑fM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0f:↑(DimSet M d)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnit u1 u2 (a • ↑f) = a • scaleUnit u1 u2 ↑f ← f.2M:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0f:↑(DimSet M d)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnit u1 u2 (a • ↑f) = a • scaleUnit u1 u2 ↑fM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0f:↑(DimSet M d)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnit u1 u2 (a • ↑f) = a • scaleUnit u1 u2 ↑f]M:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0f:↑(DimSet M d)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ scaleUnit u1 u2 (a • ↑f) = a • scaleUnit u1 u2 ↑f
    rw [MulUnitDependent.scaleUnit_mulM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0f:↑(DimSet M d)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ a • scaleUnit u1 u2 ↑f = a • scaleUnit u1 u2 ↑fAll goals completed! 🐙]All goals completed! 🐙⟩
  one_smul f := byM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasef:↑(DimSet M d)⊢ 1 • f = f
    extM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasef:↑(DimSet M d)⊢ ↑(1 • f) = ↑f
    change (1 : ℝ≥0) • f.1 = f.1M:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasef:↑(DimSet M d)⊢ 1 • ↑f = ↑f
    simpAll goals completed! 🐙
  mul_smul a b f := byM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0b:ℝ≥0f:↑(DimSet M d)⊢ (a * b) • f = a • b • f
    extM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0b:ℝ≥0f:↑(DimSet M d)⊢ ↑((a * b) • f) = ↑(a • b • f)
    change (a * b) • f.1 = a • (b • f.1)M:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0b:ℝ≥0f:↑(DimSet M d)⊢ (a * b) • ↑f = a • b • ↑f
    rw [smul_smulM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasea:ℝ≥0b:ℝ≥0f:↑(DimSet M d)⊢ (a * b) • ↑f = (a * b) • ↑fAll goals completed! 🐙]All goals completed! 🐙instance (M : Type) [MulAction ℝ≥0 M] [MulUnitDependent M] (d : Dimension LTMCTDimensionBase) :
    CarriesDimension (DimSet M d) where
  d := d@[simp]
lemma scaleUnit_dimSet_val {M : Type} [MulAction ℝ≥0 M] [MulUnitDependent M]
    (d : Dimension LTMCTDimensionBase) (m : DimSet M d) (u1 u2 : LTMCTUnitChoices) :
    (scaleUnit u1 u2 m).1 = scaleUnit u1 u2 m.1 := (m.2 u1 u2).symmlemma DimSet.mem_iff {M : Type} [MulAction ℝ≥0 M] [MulUnitDependent M]
    (d : Dimension LTMCTDimensionBase) (m : M) :
    m ∈ DimSet M d ↔ ∀ u1 u2, scaleUnit u1 u2 m = (LTMCTUnitChoices.dimScale u1 u2 d) • m := byM:Typeinst✝¹:MulAction ℝ≥0 Minst✝:MulUnitDependent Md:Dimension LTMCTDimensionBasem:M⊢ m ∈ DimSet M d ↔ ∀ (u1 u2 : LTMCTUnitChoices), scaleUnit u1 u2 m = (u1.dimScale u2) d • m rflAll goals completed! 🐙