awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ 0 <
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))

Tactic:
ZLattice.covolume_pos _ volume

Premises used: MeasureTheory.MeasureSpace.volume, ZLattice.covolume_pos
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ 0 <
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))

Tactic:
exact ZLattice.covolume_pos _ volume

Premises used: MeasureTheory.MeasureSpace.volume, ZLattice.covolume_pos
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
rw rw₁ rw₂ :
  0 <
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ 0 < regOfFamily u

Tactic:
classical
  rw [regOfFamily_of_isMaxRank hu]
  exact ZLattice.covolume_pos _ volume

Premises used: NumberField.Units.regOfFamily_of_isMaxRank, MeasureTheory.MeasureSpace.volume, ZLattice.covolume_pos
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ regOfFamily u ≠ 0

Tactic:
(regOfFamily_pos hu).ne'

Premises used: LT.lt.ne', NumberField.Units.regOfFamily_pos
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ regOfFamily u ≠ 0 → IsMaxRank u

Tactic:
simpa using (fun hu ↦ regOfFamily_eq_zero hu).mt

Premises used: Function.mt, NumberField.Units.regOfFamily_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
pos :
  ∀ (hu : IsMaxRank u),
    regOfFamily u =
      |det (n := { w : InfinitePlace K // w ≠ w₀ })
          ((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)ˣ)
                    (u
                      (((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₀ } ℝ)|
neg :
  ∀ (hu : ¬IsMaxRank u),
    regOfFamily u =
      |det (n := { w : InfinitePlace K // w ≠ w₀ })
          ((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)ˣ)
                    (u
                      (((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₀ } ℝ)|
⊢ regOfFamily u =
    |det (n := { w : InfinitePlace K // w ≠ w₀ })
        ((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)ˣ)
                  (u
                    (((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:
by_cases hu : IsMaxRank u

Premises used: NumberField.Units.IsMaxRank
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
i x : { w : InfinitePlace K // w ≠ w₀ }
⊢ Eq (α := ℝ)
    (Function.comp (β :=
      ↥(span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
      (Subtype.val (p := fun (x : { w : InfinitePlace K // w ≠ w₀ } → ℝ) ↦
        Membership.mem (γ := Submodule ℤ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ))
          (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))) x))
      (Function.comp (β := Fin (rank K))
        (⇑(Basis.restrictScalars ℤ (basisOfIsMaxRank hu)) :
          (a : Fin (rank K)) → ↥(span ℤ (Set.range (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
        (⇑(Equiv.symm (equivFinRank K)) : (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K)))
      i x)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (u
            (((Equiv.symm (equivFinRank K) : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
              i)) :
        Additive (𝓞 K)ˣ)
      x)

Tactic:
simp [basisOfIsMaxRank_apply hu]

Premises used: NumberField.Units.basisOfIsMaxRank_apply
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
neg :
  ¬LinearIndependent ℝ (M := { w : InfinitePlace K // w ≠ w₀ } → ℝ) fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
      (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)ˣ)
                (u
                  (((Equiv.symm (equivFinRank K) : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                      (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                    i)) :
              Additive (𝓞 K)ˣ))
        i
⊢ regOfFamily u =
    |det (n := { w : InfinitePlace K // w ≠ w₀ })
        ((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)ˣ)
                  (u
                    (((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 [regOfFamily_eq_zero hu, det_eq_zero_of_not_linearIndependent_rows, abs_zero]

Premises used: abs_zero, NumberField.Units.regOfFamily_eq_zero, Matrix.det_eq_zero_of_not_linearIndependent_rows
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w : InfinitePlace K // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w : InfinitePlace K // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K :=
  Equiv.trans (finSuccEquiv (rank K))
    (↑((Equiv.symm (Equiv.optionSubtype w₁) :
            (a : Fin (rank K) ≃ { y : InfinitePlace K // y ≠ w₁ }) →
              { e : Option (Fin (rank K)) ≃ InfinitePlace K //
                (e : (a : Option (Fin (rank K))) → InfinitePlace K) none = w₁ })
          e₁.symm) :
      Option (Fin (rank K)) ≃ InfinitePlace K)
x : InfinitePlace K
⊢ x ≠ w₂ ↔
    Ne (α := Fin (rank K + 1)) ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) x : Fin (rank K + 1))
      ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂ : Fin (rank K + 1))

Tactic:
simp [f]
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w : InfinitePlace K // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w : InfinitePlace K // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K :=
  Equiv.trans (finSuccEquiv (rank K))
    (↑((Equiv.symm (Equiv.optionSubtype w₁) :
            (a : Fin (rank K) ≃ { y : InfinitePlace K // y ≠ w₁ }) →
              { e : Option (Fin (rank K)) ≃ InfinitePlace K //
                (e : (a : Option (Fin (rank K))) → InfinitePlace K) none = w₁ })
          e₁.symm) :
      Option (Fin (rank K)) ≃ InfinitePlace K)
g : { w : InfinitePlace K // w ≠ w₂ } ≃ Fin (rank K) :=
  Equiv.trans (β := { b : Fin (rank K + 1) // b ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂ })
    (f.symm.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ w₂) (q := fun (b : Fin (rank K + 1)) ↦
      b ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂) ⋯)
    (Equiv.symm (finSuccAboveEquiv ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂)))
⊢ |det (n := { w : InfinitePlace K // w ≠ w₂ })
        (submatrix (m := { w : InfinitePlace K // w ≠ w₂ })
            ((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)
                        (↑(u ((e₂ : (a : { w : InfinitePlace K // w ≠ w₂ }) → Fin (rank K)) i)) : 𝓞 K) :
                      K)))
            (⇑(g.trans e₂.symm) : (a : { w : InfinitePlace K // w ≠ w₂ }) → { w : InfinitePlace K // w ≠ w₂ }) id :
          Matrix { w : InfinitePlace K // w ≠ w₂ } { w : InfinitePlace K // w ≠ w₂ } ℝ)| =
    |HMul.hMul (α := ℝ)
        (↑(↑(((Equiv.Perm.sign : Equiv.Perm { w : InfinitePlace K // w ≠ w₂ } →* ℤˣ) :
                    (a : Equiv.Perm { w : InfinitePlace K // w ≠ w₂ }) → ℤˣ)
                  (g.trans e₂.symm)) :
              ℤ) :
          ℝ)
        (det (n := { w : InfinitePlace K // w ≠ w₂ })
          ((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)
                        (↑(u ((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:
have h_col := congr_arg abs <| det_permute (g.trans e₂.symm)
    (of fun i w : {w // w ≠ w₂} ↦ (mult w.val : ℝ) * (w.val (u (e₂ i) : K)).log)
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
⊢ regOfFamily u =
    |det (n := { w : InfinitePlace K // w ≠ w' })
        ((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)
                      (↑(u ((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:
simp [regOfFamily_eq_det', abs_det_eq_abs_det u e (equivFinRank K).symm, logEmbedding]

Premises used: NumberField.Units.equivFinRank, NumberField.Units.logEmbedding, NumberField.Units.abs_det_eq_abs_det, Equiv.symm, NumberField.Units.regOfFamily_eq_det'
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K :=
  Equiv.trans (finSuccEquiv (rank K))
    (↑((Equiv.symm (Equiv.optionSubtype w') :
            (a : Fin (rank K) ≃ { y : InfinitePlace K // y ≠ w' }) →
              { e : Option (Fin (rank K)) ≃ InfinitePlace K //
                (e : (a : Option (Fin (rank K))) → InfinitePlace K) none = w' })
          e.symm) :
      Option (Fin (rank K)) ≃ InfinitePlace K)
x : InfinitePlace K
⊢ x ≠ w' ↔
    Ne (α := Fin (rank K + 1)) ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) x : Fin (rank K + 1))
      ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w' : Fin (rank K + 1))

Tactic:
simp [f]
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K :=
  Equiv.trans (finSuccEquiv (rank K))
    (↑((Equiv.symm (Equiv.optionSubtype w') :
            (a : Fin (rank K) ≃ { y : InfinitePlace K // y ≠ w' }) →
              { e : Option (Fin (rank K)) ≃ InfinitePlace K //
                (e : (a : Option (Fin (rank K))) → InfinitePlace K) none = w' })
          e.symm) :
      Option (Fin (rank K)) ≃ InfinitePlace K)
g : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K) :=
  Equiv.trans (β := { b : Fin (rank K + 1) // b ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w' })
    (f.symm.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ w') (q := fun (b : Fin (rank K + 1)) ↦
      b ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') ⋯)
    (Equiv.symm (finSuccAboveEquiv ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w')))
simp_rw :
  ∀ (b : InfinitePlace K),
    ¬b = w' →
      Eq (α := ℝ)
        (if h : b = w' then ∑ x : InfinitePlace K, (↑x.mult : ℝ)
        else
          ∑ x : InfinitePlace K,
            (↑x.mult : ℝ) *
              Real.log
                ((x : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(u
                            ((e : (a : { w : InfinitePlace K // ¬w = w' }) → Fin (rank K))
                              (Subtype.mk (p := fun (w : InfinitePlace K) ↦ ¬w = w') b ⋯))) :
                        𝓞 K) :
                    K)))
        0
⊢ ∀ (i : Fin (rank K + 1)),
    i ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w' →
      Eq (α := ℝ)
        (∑ j : Fin (rank K + 1),
          ((reindex f.symm f.symm :
                Matrix (InfinitePlace K) (InfinitePlace K) ℝ ≃ Matrix (Fin (rank K + 1)) (Fin (rank K + 1)) ℝ) :
              (a : Matrix (InfinitePlace K) (InfinitePlace K) ℝ) → Matrix (Fin (rank K + 1)) (Fin (rank K + 1)) ℝ)
            ((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)
                          (↑(u
                                ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                                  (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                            𝓞 K) :
                        K)))
            i j)
        0

Tactic:
simp_rw [Equiv.forall_congr_left f, ← f.symm.sum_comp, reindex_apply, submatrix_apply,
      of_apply, f.symm_symm, f.apply_symm_apply, Finset.sum_dite_irrel, ne_eq,
      EmbeddingLike.apply_eq_iff_eq]

Premises used: Equiv.apply_symm_apply, Finset.sum_dite_irrel, Equiv.sum_comp, Equiv.forall_congr_left, Matrix.reindex_apply, Equiv.symm_symm, EmbeddingLike.apply_eq_iff_eq, Matrix.of_apply, ne_eq, Matrix.submatrix_apply, Equiv.symm
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K :=
  Equiv.trans (finSuccEquiv (rank K))
    (↑((Equiv.symm (Equiv.optionSubtype w') :
            (a : Fin (rank K) ≃ { y : InfinitePlace K // y ≠ w' }) →
              { e : Option (Fin (rank K)) ≃ InfinitePlace K //
                (e : (a : Option (Fin (rank K))) → InfinitePlace K) none = w' })
          e.symm) :
      Option (Fin (rank K)) ≃ InfinitePlace K)
g : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K) :=
  Equiv.trans (β := { b : Fin (rank K + 1) // b ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w' })
    (f.symm.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ w') (q := fun (b : Fin (rank K + 1)) ↦
      b ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') ⋯)
    (Equiv.symm (finSuccAboveEquiv ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w')))
b : InfinitePlace K
h : ¬b = w'
rw :
  Eq (α := ℝ)
    (∑ x : InfinitePlace K,
      (↑x.mult : ℝ) *
        Real.log
          ((x : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                (↑(u
                      ((e : (a : { w : InfinitePlace K // ¬w = w' }) → Fin (rank K))
                        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ ¬w = w') b ⋯))) :
                  𝓞 K) :
              K)))
    0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ)
    (if h : b = w' then ∑ x : InfinitePlace K, (↑x.mult : ℝ)
    else
      ∑ x : InfinitePlace K,
        (↑x.mult : ℝ) *
          Real.log
            ((x : (a : K) → ℝ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                  (↑(u
                        ((e : (a : { w : InfinitePlace K // ¬w = w' }) → Fin (rank K))
                          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ ¬w = w') b ⋯))) :
                    𝓞 K) :
                K)))
    0

Tactic:
rw [dif_neg h, sum_mult_mul_log]

Premises used: dif_neg, NumberField.Units.sum_mult_mul_log
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LinearIndependent.{0, 0, u_1} (ι := Fin (rank K)) ℝ (M := logSpace K)
    (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)

Tactic:
((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K)).linearIndependent

Premises used: NumberField.Units.basisUnitLattice, Real, Module.Basis.ofZLatticeBasis, NumberField.Units.unitLattice, Module.Basis.linearIndependent
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : Fin (rank K)),
    Eq (α := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K x) : Additive (𝓞 K)ˣ) :
        logSpace K)
      ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : (a : Fin (rank K)) → logSpace K) x : logSpace K)
⊢ IsMaxRank (fundSystem K)

Tactic:
convert! ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K)).linearIndependent

Premises used: NumberField.Units.basisUnitLattice, Real, Module.Basis.ofZLatticeBasis, NumberField.Units.unitLattice, Module.Basis.linearIndependent
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : Fin (rank K)
h :
  Eq.{u_1 + 1} (α := logSpace K)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) x) : logSpace K) : logSpace K)
    ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : (a : Fin (rank K)) → logSpace K) x : logSpace K)
h₁ h₂ :
  Eq.{u_1 + 1} (α := logSpace K) (↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) x) : logSpace K)
    (↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) x) : logSpace K)
⊢ Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K x) : Additive (𝓞 K)ˣ) :
      logSpace K)
    ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : (a : Fin (rank K)) → logSpace K) x : logSpace K)

Tactic:
rw [logEmbedding_fundSystem, Basis.ofZLatticeBasis_apply]

Premises used: NumberField.Units.logEmbedding_fundSystem, Module.Basis.ofZLatticeBasis_apply
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : Fin (rank K)),
    Eq (α := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K x) : Additive (𝓞 K)ˣ) :
        logSpace K)
      ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : (a : Fin (rank K)) → logSpace K) x : logSpace K)
⊢ IsMaxRank (fundSystem K)

Tactic:
classical
  convert! ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K)).linearIndependent
  rw [logEmbedding_fundSystem, Basis.ofZLatticeBasis_apply]

Premises used: NumberField.Units.logEmbedding_fundSystem, Real, Module.Basis.ofZLatticeBasis_apply, Module.Basis.ofZLatticeBasis, Module.Basis.linearIndependent
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a :
  ∀ (i : Fin (rank K)) (x : { w : InfinitePlace K // w ≠ w₀ }),
    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 :
        ℝ)
⊢ Eq (α := Basis (Fin (rank K)) ℝ (logSpace K)) (basisOfIsMaxRank ⋯)
    (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
ext