-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this :
  LE.le (α := Submodule ℤ (logSpace K))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K)))
pos :
  ZLattice.covolume (E := logSpace K)
        (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
        (volume : Measure (logSpace K)) /
      regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
pos₁ :
  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 hv) : (a : Fin (rank K)) → logSpace K)))
        (volume : Measure (logSpace K)) =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
pos₂ :
  Eq (α := ℝ)
    (↑(AddSubgroup.relIndex (G := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
          (toAddSubgroup (module_M := AddCommGroup.toIntModule ({ w : InfinitePlace K // w ≠ w₀ } → ℝ))
            (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
          (toAddSubgroup (module_M := AddCommGroup.toIntModule ({ w : InfinitePlace K // w ≠ w₀ } → ℝ))
            (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K))))) :
      ℝ)
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
pos₃ :
  Eq (α := ℝ)
    (↑(AddSubgroup.relIndex (G := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
          (AddSubgroup.map (logEmbedding K)
            ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
              (Subgroup.closure (Set.range u))))
          (toAddSubgroup (module_M := AddCommGroup.toIntModule ({ w : InfinitePlace K // w ≠ w₀ } → ℝ))
            (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K))))) :
      ℝ)
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
have pos₄ : Eq (α := ℝ)
  (↑(AddSubgroup.relIndex (G := { w : InfinitePlace K // w ≠ w₀ } → ℝ)
        (AddSubgroup.map (logEmbedding K)
          ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
            (Subgroup.closure (Set.range u))))
        (AddSubgroup.map (logEmbedding K)
          ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
            (Subgroup.closure (Set.range v))))) :
    ℝ)
  (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
Tactic: rw [regOfFamily_of_isMaxRank hu, regOfFamily_of_isMaxRank hv,
      covolume_div_covolume_eq_relIndex _ _ this, span_basisOfIsMaxRank hu,
      span_basisOfIsMaxRank hv, AddSubgroup.relIndex_map_map, logEmbedding_ker,
      ← OrderIso.map_sup, ← OrderIso.map_sup, ← Subgroup.relIndex_toAddSubgroup]