-- 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)ˣ
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))))))
⊢ IsMaxRank u ↔ FiniteIndex (Subgroup.closure (Set.range 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))
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