awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : Fin (rank K)
x : { w : InfinitePlace K // w ≠ w₀ }
a :
  Eq (α := ℝ) ((basisOfIsMaxRank ⋯ : (a : Fin (rank K)) → logSpace K) i x)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) i) : logSpace K) x)
a₁ :
  Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K i) : Additive (𝓞 K)ˣ) x)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) i) : logSpace K) x)
⊢ Eq (α := ℝ) ((basisOfIsMaxRank ⋯ : (a : Fin (rank K)) → logSpace K) i x : ℝ)
    (((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : Basis (Fin (rank K)) ℝ (logSpace K)) :
          (a : Fin (rank K)) → logSpace K)
        i x :
      ℝ)
have a₂ : Eq (α := ℝ) ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) i) : logSpace K) x)
  ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) i) : logSpace K) x)
Tactic: rw [Basis.ofZLatticeBasis_apply, basisOfIsMaxRank_apply, logEmbedding_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ regulator K = regOfFamily (fundSystem K)
have rw : regulator K =
  ZLattice.covolume (E := logSpace K)
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank sorry) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  regulator K =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regulator K = regOfFamily (fundSystem K)
have rw₁ : ZLattice.covolume.{u_1} (E := logSpace K) (unitLattice K) (volume : Measure (logSpace K)) =
  ZLattice.covolume (E := logSpace K)
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank sorry) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  regulator K =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₁ :
  ZLattice.covolume.{u_1} (E := logSpace K) (unitLattice K) (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regulator K = regOfFamily (fundSystem K)
have rw₂ : ZLattice.covolume.{u_1} (E := logSpace K)
    (span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K)) =
  ZLattice.covolume (E := logSpace K)
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank sorry) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  regulator K =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₁ :
  ZLattice.covolume.{u_1} (E := logSpace K) (unitLattice K) (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₂ :
  ZLattice.covolume.{u_1} (E := logSpace K)
      (span ℤ
        (Set.range (ι := Fin (rank K))
          (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regulator K = regOfFamily (fundSystem K)
have rw₃ : ZLattice.covolume.{u_1} (E := logSpace K)
    (span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K)) =
  ZLattice.covolume.{u_1} (E := logSpace K)
    (span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : Basis (Fin (rank K)) ℝ (logSpace K)) :
          (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ regulator K = regOfFamily (fundSystem K)
have rw : regulator K =
  ZLattice.covolume (E := logSpace K)
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank sorry) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: classical
  rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  regulator K =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regulator K = regOfFamily (fundSystem K)
have rw₁ : ZLattice.covolume.{u_1} (E := logSpace K) (unitLattice K) (volume : Measure (logSpace K)) =
  ZLattice.covolume (E := logSpace K)
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank sorry) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: classical
  rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  regulator K =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₁ :
  ZLattice.covolume.{u_1} (E := logSpace K) (unitLattice K) (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regulator K = regOfFamily (fundSystem K)
have rw₂ : ZLattice.covolume.{u_1} (E := logSpace K)
    (span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K)) =
  ZLattice.covolume (E := logSpace K)
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank sorry) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: classical
  rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  regulator K =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₁ :
  ZLattice.covolume.{u_1} (E := logSpace K) (unitLattice K) (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₂ :
  ZLattice.covolume.{u_1} (E := logSpace K)
      (span ℤ
        (Set.range (ι := Fin (rank K))
          (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regulator K = regOfFamily (fundSystem K)
have rw₃ : ZLattice.covolume.{u_1} (E := logSpace K)
    (span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K)) =
  ZLattice.covolume.{u_1} (E := logSpace K)
    (span ℤ
      (Set.range (ι := Fin (rank K))
        (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : Basis (Fin (rank K)) ℝ (logSpace K)) :
          (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: classical
  rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ regulator K =
    |Matrix.det (n := { w : InfinitePlace K // w ≠ w₀ })
        ((Matrix.of :
              (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) →
                Matrix { w : InfinitePlace K // w ≠ w₀ } { w : InfinitePlace K // w ≠ w₀ } ℝ)
            fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
            (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
              ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
                  (fundSystem K
                    (((Equiv.symm (equivFinRank K) : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      i)) :
                Additive (𝓞 K)ˣ) :
          Matrix { w : InfinitePlace K // w ≠ w₀ } { w : InfinitePlace K // w ≠ w₀ } ℝ)|
have rw : regOfFamily (fundSystem K) =
  |Matrix.det (n := { w : InfinitePlace K // w ≠ w₀ })
      ((Matrix.of :
            (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) →
              Matrix { w : InfinitePlace K // w ≠ w₀ } { w : InfinitePlace K // w ≠ w₀ } ℝ)
          fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
          (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
                (fundSystem K
                  (((Equiv.symm (equivFinRank K) : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                      (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                    i)) :
              Additive (𝓞 K)ˣ) :
        Matrix { w : InfinitePlace K // w ≠ w₀ } { w : InfinitePlace K // w ≠ w₀ } ℝ)|
Tactic: rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w' : InfinitePlace K
e : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
⊢ regulator K =
    |Matrix.det (n := { w : InfinitePlace K // w ≠ w' })
        ((Matrix.of :
              (a : { w : InfinitePlace K // w ≠ w' } → { w : InfinitePlace K // w ≠ w' } → ℝ) →
                Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)
            fun (i w : { w : InfinitePlace K // w ≠ w' }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)|
have rw : regOfFamily (fundSystem K) =
  |Matrix.det (n := { w : InfinitePlace K // w ≠ w' })
      ((Matrix.of :
            (a : { w : InfinitePlace K // w ≠ w' } → { w : InfinitePlace K // w ≠ w' } → ℝ) →
              Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)
          fun (i w : { w : InfinitePlace K // w ≠ w' }) ↦
          (↑(↑w : InfinitePlace K).mult : ℝ) *
            Real.log
              (((↑w : InfinitePlace K) : (a : K) → ℝ)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                    (↑(fundSystem K ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K)) i)) : 𝓞 K) :
                  K)) :
        Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)|
Tactic: rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w' : InfinitePlace K
e : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
⊢ (↑(finrank ℚ K) : ℝ) * regulator K =
    |Matrix.det (n := InfinitePlace K)
        ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            fun (i w : InfinitePlace K) ↦
            if h : i = w' then (↑w.mult : ℝ)
            else
              (↑w.mult : ℝ) *
                Real.log
                  ((w : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(fundSystem K
                              ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                          𝓞 K) :
                      K)) :
          Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
have rw : (↑(finrank ℚ K) : ℝ) * regOfFamily (fundSystem K) =
  |Matrix.det (n := InfinitePlace K)
      ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          fun (i w : InfinitePlace K) ↦
          if h : i = w' then (↑w.mult : ℝ)
          else
            (↑w.mult : ℝ) *
              Real.log
                ((w : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                              (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                        𝓞 K) :
                    K)) :
        Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
Tactic: rw [regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
have pos : ∀ (hu : IsMaxRank u),
  regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
Tactic: by_cases hu : IsMaxRank u
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
pos :
  ∀ (hu : IsMaxRank u),
    regOfFamily u / regOfFamily v =
      (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
have neg : ∀ (hu : ¬IsMaxRank u),
  regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
Tactic: by_cases hu : IsMaxRank u
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ LE.le (α := Submodule ℤ (logSpace K))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K)))
have rw : LE.le (α := AddSubgroup (logSpace K))
  (AddSubgroup.map (logEmbedding K)
    ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
      (Subgroup.closure (Set.range u) ⊔ torsion K)))
  (AddSubgroup.map (logEmbedding K)
    ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
      (Subgroup.closure (Set.range v) ⊔ torsion K)))
Tactic: rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,
        ← SupHomClass.map_sup, ← SupHomClass.map_sup]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
have this : LE.le (α := Submodule ℤ (logSpace K))
  (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
  (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K)))
Tactic: have : span ℤ (Set.range (basisOfIsMaxRank hu)) ≤ span ℤ (Set.range (basisOfIsMaxRank hv)) := by
      rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,
        ← SupHomClass.map_sup, ← SupHomClass.map_sup]
      exact AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this :
  LE.le (α := Submodule ℤ (logSpace K))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K)))
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
have pos : ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) /
    regOfFamily v =
  (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
Tactic: rw [regOfFamily_of_isMaxRank hu, regOfFamily_of_isMaxRank hv,
      covolume_div_covolume_eq_relIndex _ _ this, span_basisOfIsMaxRank hu,
      span_basisOfIsMaxRank hv, AddSubgroup.relIndex_map_map, logEmbedding_ker,
      ← OrderIso.map_sup, ← OrderIso.map_sup, ← Subgroup.relIndex_toAddSubgroup]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this :
  LE.le (α := Submodule ℤ (logSpace K))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K)))
pos :
  ZLattice.covolume (E := logSpace K)
        (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
        (volume : Measure (logSpace K)) /
      regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
have pos₁ : ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) /
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) =
  (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
Tactic: rw [regOfFamily_of_isMaxRank hu, regOfFamily_of_isMaxRank hv,
      covolume_div_covolume_eq_relIndex _ _ this, span_basisOfIsMaxRank hu,
      span_basisOfIsMaxRank hv, AddSubgroup.relIndex_map_map, logEmbedding_ker,
      ← OrderIso.map_sup, ← OrderIso.map_sup, ← Subgroup.relIndex_toAddSubgroup]