-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
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))))))
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))))))),
    IsMaxRank u ↔ FiniteIndex (Subgroup.closure (Set.range u))
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))))))
have₃ 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))))))),
    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)))))))
    (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₆ :
  ∀
    (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
⊢ IsMaxRank u ↔ FiniteIndex (Subgroup.closure (Set.range 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

Premises used: 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