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)ˣ
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
⊢ (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)))))))

Tactic:
rw [← AddSubgroup.index_ne_zero_iff_finite]

Premises used: AddSubgroup.index_ne_zero_iff_finite
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ 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))
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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)))
⊢ 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

Premises used: QuotientGroup.range_mk', Subgroup.index_top, mul_one, QuotientGroup.ker_mk'
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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
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
⊢ (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 [← 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]

Premises used: Set.range_comp, QuotientGroup.coe_mk', MonoidHom.map_closure, Submodule.span_int_eq_addSubgroupClosure, Subgroup.toAddSubgroup_closure, Subgroup.index_toAddSubgroup, Submodule.map_toAddSubgroup, Equiv.image_symm_eq_preimage, LinearEquiv.coe_coe
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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 ↥(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
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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))))))
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))
⊢ 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:
rw [← SetLike.isDiscrete_iff_discreteTopology]

Premises used: SetLike.isDiscrete_iff_discreteTopology
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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))

Tactic:
(inferInstance : DiscreteTopology (unitLattice K)).isDiscrete.mono ?_

Premises used: DiscreteTopology.isDiscrete, IsDiscrete.mono
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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))))))
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))
⊢ 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:
refine (inferInstance : DiscreteTopology (unitLattice K)).isDiscrete.mono ?_

Premises used: DiscreteTopology.isDiscrete, IsDiscrete.mono
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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))))))
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))
⊢ (↑(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:
rw [SetLike.coe_subset_coe, Submodule.span_le]

Premises used: SetLike.coe_subset_coe, Submodule.span_le
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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))))))
i : Fin (rank K)
⊢ (fun (i : Fin (rank K)) ↦
        ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ) :
          logSpace K))
      i ∈
    (↑(unitLattice K) : Set (logSpace K))

Tactic:
⟨Additive.ofMul (u i), mem_top, rfl⟩

Premises used: Set.Mem, setOf, Additive.ofMul, And.intro, Exists.intro, Set.image, DFunLike.coe, Submodule.mem_top, rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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))))))
i : Fin (rank K)
⊢ (fun (i : Fin (rank K)) ↦
        ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ) :
          logSpace K))
      i ∈
    (↑(unitLattice K) : Set (logSpace K))

Tactic:
exact ⟨Additive.ofMul (u i), mem_top, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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)ˣ)))

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⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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)ˣ)))
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
⊢ IsMaxRank u ↔ FiniteIndex (Subgroup.closure (Set.range u))

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]

Premises used: Real.finrank_eq_int_finrank_of_discrete, Submodule.finiteQuotient_iff, Set.finrank, eq_comm, Submodule.finrank_map_subtype_eq, NumberField.Units.unitLattice_rank, NumberField.Units.IsMaxRank, Submodule.map_span, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, Subgroup.finiteIndex_iff, Set.range_comp', linearIndependent_iff_card_eq_finrank_span
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
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)ˣ)))
⊢ 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:
simp
-- 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 :
  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
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ regOfFamily u = 0

Tactic:
rw [regOfFamily, dif_neg hu]

Premises used: dif_neg, NumberField.Units.regOfFamily
-- 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 :
  (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))
rw₁ 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))
⊢ 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))

Tactic:
rw [regOfFamily, dif_pos hu]

Premises used: dif_pos, NumberField.Units.regOfFamily
-- 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 :
  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:
rw [regOfFamily_of_isMaxRank hu]

Premises used: NumberField.Units.regOfFamily_of_isMaxRank