-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
h :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    Membership.mem (α := Kˣ) A.principalUnitGroup ((A.unitGroup.subtype : (a : ↥A.unitGroup) → Kˣ) x : Kˣ)
h₁ : x ∈ A.unitGroupToResidueFieldUnits.ker ↔ (↑x : Kˣ) ∈ A.principalUnitGroup
h₂ :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
      (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
      ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)
h₃ :
  x ∈
      MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (MonoidHom.comp
          (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
          A.unitGroupMulEquiv.toMonoidHom) ↔
    Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
      (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
      ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)
h₄ :
  x ∈
      MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (MonoidHom.comp
          (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
          A.unitGroupMulEquiv.toMonoidHom) ↔
    Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
      (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* IsLocalRing.ResidueField ↥A)))
      ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)
h₅ :
  x ∈
      MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (MonoidHom.comp
          (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
          A.unitGroupMulEquiv.toMonoidHom) ↔
    Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
      (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* IsLocalRing.ResidueField ↥A)))
      ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)
h₆ :
  Membership.mem (γ := Subgroup ↥A.unitGroup)
      (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (MonoidHom.comp
          (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
          (↑A.unitGroupMulEquiv : ↥A.unitGroup →* (↥A)ˣ)))
      x ↔
    Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
      (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* IsLocalRing.ResidueField ↥A)))
      ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)
⊢ x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
have h₇ : Eq (α := (IsLocalRing.ResidueField ↥A)ˣ)
    ((MonoidHom.comp
            (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
            (↑A.unitGroupMulEquiv : ↥A.unitGroup →* (↥A)ˣ) :
          (a : ↥A.unitGroup) → (IsLocalRing.ResidueField ↥A)ˣ)
        x :
      (IsLocalRing.ResidueField ↥A)ˣ)
    (1 : (IsLocalRing.ResidueField ↥A)ˣ) ↔
  Eq (α := (IsLocalRing.ResidueField ↥A)ˣ)
    ((Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* IsLocalRing.ResidueField ↥A) :
          (a : (↥A)ˣ) → (IsLocalRing.ResidueField ↥A)ˣ)
        ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) :
      (IsLocalRing.ResidueField ↥A)ˣ)
    (1 : (IsLocalRing.ResidueField ↥A)ˣ)
Tactic: simp_rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff,
    unitGroupToResidueFieldUnits, IsLocalRing.residue, RingHom.toMonoidHom_eq_coe,
    MulEquiv.toMonoidHom_eq_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, MonoidHom.coe_coe,
    Function.comp_apply]