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
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (s ⊔ torsion K) ≠ 0
have rw : s.relIndex (torsion K) ≠ 0
Tactic: rw [Subgroup.relIndex_sup_left]
-- 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)ˣ
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite.{u_1 + 1}
      (HasQuotient.Quotient ↥(Submodule.toAddSubgroup (unitLattice K)) (B :=
        AddSubgroup ↥(Submodule.toAddSubgroup (unitLattice K)))
        (Submodule.toAddSubgroup (module_M := AddCommGroup.toIntModule ↥(unitLattice K))
          (span ℤ
            (Set.range
              (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
                (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
                (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                  (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                  (QuotientGroup.mk ∘ u)))))))
have rw : (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
  AddSubgroup.index (G := ↥(Submodule.toAddSubgroup (unitLattice K)))
      (Submodule.toAddSubgroup (module_M := AddCommGroup.toIntModule ↥(unitLattice K))
        (span ℤ
          (Set.range
            (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
              (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
              (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                (QuotientGroup.mk ∘ u)))))) ≠
    0
Tactic: rw [← AddSubgroup.index_ne_zero_iff_finite]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    AddSubgroup.index (G := ↥(Submodule.toAddSubgroup (unitLattice K)))
        (Submodule.toAddSubgroup (module_M := AddCommGroup.toIntModule ↥(unitLattice K))
          (span ℤ
            (Set.range
              (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
                (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
                (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                  (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                  (QuotientGroup.mk ∘ u)))))) ≠
      0
have this : index (G := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
    (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))) =
  (Subgroup.closure (Set.range u) ⊔
        MonoidHom.ker (M := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
          (QuotientGroup.mk' (torsion K))).index *
    index (G := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
      (MonoidHom.range (QuotientGroup.mk' (torsion K)))
Tactic: have := index_map (closure (Set.range u)) (QuotientGroup.mk' (torsion K))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  index (G := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
      (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))) =
    (Subgroup.closure (Set.range u) ⊔
          MonoidHom.ker (M := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
            (QuotientGroup.mk' (torsion K))).index *
      index (G := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
        (MonoidHom.range (QuotientGroup.mk' (torsion K)))
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    AddSubgroup.index (G := ↥(Submodule.toAddSubgroup (unitLattice K)))
        (Submodule.toAddSubgroup (module_M := AddCommGroup.toIntModule ↥(unitLattice K))
          (span ℤ
            (Set.range
              (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
                (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
                (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                  (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                  (QuotientGroup.mk ∘ u)))))) ≠
      0
have this₁ : index (G := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
    (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))) =
  (Subgroup.closure (Set.range u) ⊔ torsion K).index
Tactic: rw [QuotientGroup.ker_mk', QuotientGroup.range_mk', index_top, mul_one] at this
Cleared hypotheses: this
-- 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)ˣ
this :
  index (G := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
      (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))) =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    AddSubgroup.index (G := ↥(Submodule.toAddSubgroup (unitLattice K)))
        (Submodule.toAddSubgroup (module_M := AddCommGroup.toIntModule ↥(unitLattice K))
          (span ℤ
            (Set.range
              (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
                (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
                (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                  (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                  (QuotientGroup.mk ∘ u)))))) ≠
      0
have rw : AddSubgroup.index.{u_1} (G := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
      ((Subgroup.toAddSubgroup : (a : Subgroup ((𝓞 K)ˣ ⧸ torsion K)) → AddSubgroup (Additive ((𝓞 K)ˣ ⧸ torsion K)))
        (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u)))) ≠
    0 ↔
  AddSubgroup.index (G := ↥(Submodule.toAddSubgroup (unitLattice K)))
      (Submodule.toAddSubgroup (module_M := AddCommGroup.toIntModule ↥(unitLattice K))
        (span ℤ
          (Set.range
            (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
              (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
              (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                (QuotientGroup.mk ∘ u)))))) ≠
    0
Tactic: rw [← this, ← index_toAddSubgroup, ← AddSubgroup.index_map_equiv
        _ (logEmbeddingEquiv K).toAddEquiv, Set.range_comp, ← LinearEquiv.coe_coe,
      ← map_span (logEmbeddingEquiv K).toLinearMap,
      map_toAddSubgroup, span_int_eq_addSubgroupClosure,
      MonoidHom.map_closure, toAddSubgroup_closure, Set.range_comp, Set.range_comp,
      QuotientGroup.coe_mk', ← Equiv.image_symm_eq_preimage]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ IsMaxRank u ↔ FiniteIndex (Subgroup.closure (Set.range u))
have h₁ : (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
  Finite.{u_1 + 1}
    (HasQuotient.Quotient ↥(unitLattice K) (B := Submodule ℤ ↥(unitLattice K))
      (span ℤ
        (Set.range
          (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
            (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
            (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
              (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
              (QuotientGroup.mk ∘ u))))))
Tactic: have h₁ : (closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
      Finite (unitLattice K ⧸ span ℤ (Set.range ((logEmbeddingEquiv K) ∘ Additive.toMul.symm ∘
        QuotientGroup.mk ∘ u))) := by
    change _ ↔ Finite ((unitLattice K).toAddSubgroup ⧸ (span ℤ (Set.range _)).toAddSubgroup)
    rw [← AddSubgroup.index_ne_zero_iff_finite]
    have := index_map (closure (Set.range u)) (QuotientGroup.mk' (torsion K))
    rw [QuotientGroup.ker_mk', QuotientGroup.range_mk', index_top, mul_one] at this
    rw [← this, ← index_toAddSubgroup, ← AddSubgroup.index_map_equiv
        _ (logEmbeddingEquiv K).toAddEquiv, Set.range_comp, ← LinearEquiv.coe_coe,
      ← map_span (logEmbeddingEquiv K).toLinearMap,
      map_toAddSubgroup, span_int_eq_addSubgroupClosure,
      MonoidHom.map_closure, toAddSubgroup_closure, Set.range_comp, Set.range_comp,
      QuotientGroup.coe_mk', ← Equiv.image_symm_eq_preimage]
    rfl
-- 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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite.{u_1 + 1}
      (HasQuotient.Quotient ↥(unitLattice K) (B := Submodule ℤ ↥(unitLattice K))
        (span ℤ
          (Set.range
            (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
              (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
              (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                (QuotientGroup.mk ∘ u))))))
⊢ DiscreteTopology.{u_1}
    ↥(span ℤ
        (Set.range fun (i : Fin (rank K)) ↦
          (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ)))
have rw : IsDiscrete
  (↑(span ℤ
        (Set.range fun (i : Fin (rank K)) ↦
          (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ))) :
    Set (logSpace K))
Tactic: rw [← SetLike.isDiscrete_iff_discreteTopology]
-- 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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite.{u_1 + 1}
      (HasQuotient.Quotient ↥(unitLattice K) (B := Submodule ℤ ↥(unitLattice K))
        (span ℤ
          (Set.range
            (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
              (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
              (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                (QuotientGroup.mk ∘ u))))))
⊢ IsDiscrete
    (↑(span ℤ
          (Set.range fun (i : Fin (rank K)) ↦
            (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
              ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ))) :
      Set (logSpace K))
have refine : (↑(span ℤ
        (Set.range fun (i : Fin (rank K)) ↦
          (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ))) :
    Set (logSpace K)) ⊆
  (↑(unitLattice K) : Set (logSpace K))
Tactic: refine (inferInstance : DiscreteTopology (unitLattice K)).isDiscrete.mono ?_
-- 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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite.{u_1 + 1}
      (HasQuotient.Quotient ↥(unitLattice K) (B := Submodule ℤ ↥(unitLattice K))
        (span ℤ
          (Set.range
            (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
              (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
              (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                (QuotientGroup.mk ∘ u))))))
⊢ (↑(span ℤ
          (Set.range fun (i : Fin (rank K)) ↦
            (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
              ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ))) :
      Set (logSpace K)) ⊆
    (↑(unitLattice K) : Set (logSpace K))
have rw : (Set.range fun (i : Fin (rank K)) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ)) ⊆
  (↑(unitLattice K) : Set (logSpace K))
Tactic: rw [SetLike.coe_subset_coe, Submodule.span_le]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite.{u_1 + 1}
      (HasQuotient.Quotient ↥(unitLattice K) (B := Submodule ℤ ↥(unitLattice K))
        (span ℤ
          (Set.range
            (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
              (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
              (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                (QuotientGroup.mk ∘ u))))))
⊢ IsMaxRank u ↔ FiniteIndex (Subgroup.closure (Set.range u))
have h₂ : DiscreteTopology.{u_1}
  ↥(span ℤ
      (Set.range fun (i : Fin (rank K)) ↦
        (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ)))
Tactic: have h₂ : DiscreteTopology
      (span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i)))) := by
    rw [← SetLike.isDiscrete_iff_discreteTopology]
    refine (inferInstance : DiscreteTopology (unitLattice K)).isDiscrete.mono ?_
    rw [SetLike.coe_subset_coe, Submodule.span_le]
    rintro _ ⟨i, rfl⟩
    exact ⟨Additive.ofMul (u i), mem_top, rfl⟩
-- 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)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite.{u_1 + 1}
      (HasQuotient.Quotient ↥(unitLattice K) (B := Submodule ℤ ↥(unitLattice K))
        (span ℤ
          (Set.range
            (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
              (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
              (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                (QuotientGroup.mk ∘ u))))))
h₂ :
  DiscreteTopology.{u_1}
    ↥(span ℤ
        (Set.range fun (i : Fin (rank K)) ↦
          (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ)))
⊢ IsMaxRank u ↔ FiniteIndex (Subgroup.closure (Set.range u))
have rw : finrank.{0, u_1} ℤ
      ↥(span ℤ
          (Set.range fun (i : Fin (rank K)) ↦
            (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
              ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ))) =
    Fintype.card (Fin (rank K)) ↔
  finrank.{0, u_1} ℤ
      ↥(span ℤ
          (Set.range fun (x : Fin (rank K)) ↦
            (Submodule.subtype (unitLattice K) : (a : ↥(unitLattice K)) → logSpace K)
              (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
                (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
                (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
                  (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
                  (QuotientGroup.mk ∘ u))
                x))) =
    rank K
Tactic: rw [finiteIndex_iff_sup_torsion_finiteIndex, finiteIndex_iff, h₁, finiteQuotient_iff,
    unitLattice_rank, ← Set.finrank, IsMaxRank, linearIndependent_iff_card_eq_finrank_span,
    Real.finrank_eq_int_finrank_of_discrete h₂, Set.finrank, Set.finrank, ← finrank_map_subtype_eq,
    map_span, ← Set.range_comp', eq_comm]
-- 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)ˣ
⊢ IsMaxRank u ↔ FiniteIndex (Subgroup.closure (Set.range u))
have have : (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
  Finite.{u_1 + 1}
    (HasQuotient.Quotient ↥(unitLattice K) (B := Submodule ℤ ↥(unitLattice K))
      (span ℤ
        (Set.range
          (Function.comp (β := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
            (⇑(logEmbeddingEquiv K) : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → ↥(unitLattice K))
            (Function.comp (β := HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
              (⇑(Equiv.symm Additive.toMul) : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
              (QuotientGroup.mk ∘ u))))))
Tactic: classical
  have h₁ : (closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
      Finite (unitLattice K ⧸ span ℤ (Set.range ((logEmbeddingEquiv K) ∘ Additive.toMul.symm ∘
        QuotientGroup.mk ∘ u))) := by
    change _ ↔ Finite ((unitLattice K).toAddSubgroup ⧸ (span ℤ (Set.range _)).toAddSubgroup)
    rw [← AddSubgroup.index_ne_zero_iff_finite]
    have := index_map (closure (Set.range u)) (QuotientGroup.mk' (torsion K))
    rw [QuotientGroup.ker_mk', QuotientGroup.range_mk', index_top, mul_one] at this
    rw [← this, ← index_toAddSubgroup, ← AddSubgroup.index_map_equiv
        _ (logEmbeddingEquiv K).toAddEquiv, Set.range_comp, ← LinearEquiv.coe_coe,
      ← map_span (logEmbeddingEquiv K).toLinearMap,
      map_toAddSubgroup, span_int_eq_addSubgroupClosure,
      MonoidHom.map_closure, toAddSubgroup_closure, Set.range_comp, Set.range_comp,
      QuotientGroup.coe_mk', ← Equiv.image_symm_eq_preimage]
    rfl
  have h₂ : DiscreteTopology
      (span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i)))) := by
    rw [← SetLike.isDiscrete_iff_discreteTopology]
    refine (inferInstance : DiscreteTopology (unitLattice K)).isDiscrete.mono ?_
    rw [SetLike.coe_subset_coe, Submodule.span_le]
    rintro _ ⟨i, rfl⟩
    exact ⟨Additive.ofMul (u i), mem_top, rfl⟩
  rw [finiteIndex_iff_sup_torsion_finiteIndex, finiteIndex_iff, h₁, finiteQuotient_iff,
    unitLattice_rank, ← Set.finrank, IsMaxRank, linearIndependent_iff_card_eq_finrank_span,
    Real.finrank_eq_int_finrank_of_discrete h₂, Set.finrank, Set.finrank, ← finrank_map_subtype_eq,
    map_span, ← Set.range_comp', eq_comm]
  simp
-- 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 = 0
have rw : Eq (α := ℝ)
  (if hu : IsMaxRank u then
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
  else 0)
  0
Tactic: rw [regOfFamily, dif_neg 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)ˣ
hu : ¬IsMaxRank u
rw :
  Eq (α := ℝ)
    (if hu : IsMaxRank u then
      ZLattice.covolume (E := logSpace K)
        (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
        (volume : Measure (logSpace K))
    else 0)
    0
⊢ regOfFamily u = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [regOfFamily, dif_neg 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)ˣ
hu : IsMaxRank u
⊢ regOfFamily u =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
have rw : (if hu : IsMaxRank u then
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
  else 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: rw [regOfFamily, dif_pos 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)ˣ
hu : IsMaxRank u
rw :
  (if hu : IsMaxRank u then
      ZLattice.covolume (E := logSpace K)
        (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
        (volume : Measure (logSpace K))
    else 0) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regOfFamily u =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
have rw₁ : 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 hu) : (a : Fin (rank K)) → logSpace K)))
    (volume : Measure (logSpace K))
Tactic: rw [regOfFamily, dif_pos 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)ˣ
hu : IsMaxRank u
⊢ 0 < regOfFamily u
have 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))
Tactic: rw [regOfFamily_of_isMaxRank 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)ˣ
hu : IsMaxRank u
⊢ 0 < regOfFamily u
have 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))
Tactic: classical
  rw [regOfFamily_of_isMaxRank hu]
  exact ZLattice.covolume_pos _ volume