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
u : Fin (rank K) → (𝓞 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 : 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₀ } ℝ)|
have 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₀ } ℝ)|
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 : 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₀ } ℝ)|
⊢ 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₀ } ℝ)|
have 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₀ } ℝ)|
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 : Fin (rank K) → (𝓞 K)ˣ
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₀ } ℝ)|
have pos : Eq (α := ℝ)
  |det.{0, u_1} (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₀ } ℝ)
        (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)))))|
  |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_of_isMaxRank hu, ZLattice.covolume_eq_det _
      (((basisOfIsMaxRank hu).restrictScalars ℤ).reindex (equivFinRank K)), Basis.coe_reindex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
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₀ } ℝ)|
have 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
Tactic: rw [regOfFamily_eq_zero hu, det_eq_zero_of_not_linearIndependent_rows, abs_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
⊢ ¬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
have neg : ∀
  (hu :
    ¬LinearIndependent.{0, 0, u_1} ℝ (M := logSpace K) fun (i : Fin (rank K)) ↦
        (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ)),
  ¬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
Tactic: rwa [IsMaxRank, ← linearIndependent_equiv (equivFinRank K).symm] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
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')))
⊢ ∀ (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
have 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 sorry))) :
                      𝓞 K) :
                  K)))
      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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
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'
⊢ 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
have 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 sorry))) :
                𝓞 K) :
            K)))
  0
Tactic: rw [dif_neg h, sum_mult_mul_log]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
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
⊢ 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
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [dif_neg h, sum_mult_mul_log]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsMaxRank (fundSystem K)
have 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)
Tactic: convert! ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K)).linearIndependent
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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)
have 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)
Tactic: rw [logEmbedding_fundSystem, Basis.ofZLatticeBasis_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
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)
⊢ 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)
have 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)
Tactic: rw [logEmbedding_fundSystem, Basis.ofZLatticeBasis_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsMaxRank (fundSystem K)
have 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)
Tactic: classical
  convert! ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K)).linearIndependent
  rw [logEmbedding_fundSystem, Basis.ofZLatticeBasis_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Basis (Fin (rank K)) ℝ (logSpace K)) (basisOfIsMaxRank ⋯)
    (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
have a : ∀ (i : Fin (rank K)) (x : { w : InfinitePlace K // w ≠ w₀ }),
  Eq (α := ℝ) ((basisOfIsMaxRank sorry : (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 :
      ℝ)
Tactic: ext
-- 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₀ }
⊢ 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 (α := ℝ) ((basisOfIsMaxRank sorry : (a : Fin (rank K)) → logSpace K) i 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
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)
⊢ 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 (α := ℝ)
  ((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)
Tactic: rw [Basis.ofZLatticeBasis_apply, basisOfIsMaxRank_apply, logEmbedding_fundSystem]