-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) σ
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) :=
  ((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
          (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
        ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
      (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
    (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ hσ)
this_1 : CharP (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) p
this : Finite.{u_1 + 1} (𝓞 K ⧸ P)
i : ℕ
hi :
  ∀ (x : 𝓞 K ⧸ P),
    (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) x = x ^ Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i
h₀ : IsPrimitiveRoot (M := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) n
h₁ :
  Eq (α := 𝓞 K ⧸ P)
    (((((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
                    (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
                  ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
                (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
              (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x)
                σ hσ) :
            Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
          (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P)
        ((algebraMap (𝓞 K ⧸ P) (𝓞 K ⧸ P) : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P)
          ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger)) :
      𝓞 K ⧸ P)
    ((algebraMap (𝓞 K ⧸ P) (𝓞 K ⧸ P) : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P)
        ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P)
          ((↑(Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ
                  hσ) :
              Gal(K/ℚ)) •
            hζ.toInteger)) :
      𝓞 K ⧸ P)
⊢ Eq (α := (ZMod n)ˣ) ((fun (x : ℤ) ↦ ZMod.unitOfCoprime p hn ^ x) (↑i : ℤ) : (ZMod n)ˣ)
    (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ : (ZMod n)ˣ)
have h₂ : Eq (α := 𝓞 K ⧸ P)
  (((((IsFractionRing.stabilizerHom (A := ℤ) Gal(K/ℚ) (span {(↑p : ℤ)}) P
                  (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) (𝓞 K ⧸ P) :
                ↥(stabilizer Gal(K/ℚ) P) →* Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
              (a : ↥(stabilizer Gal(K/ℚ) P)) → Gal((𝓞 K ⧸ P)/ℤ ⧸ span {(↑p : ℤ)}))
            (Subtype.mk (p := fun (x : Gal(K/ℚ)) ↦ Membership.mem (γ := Subgroup Gal(K/ℚ)) (stabilizer Gal(K/ℚ) P) x) σ
              hσ) :
          Gal((𝓞 K ⧸ P)/HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))) :
        (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P)
      ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger) :
    𝓞 K ⧸ P)
  ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) (σ • hζ.toInteger) : 𝓞 K ⧸ P)
Tactic: simp only [Algebra.algebraMap_self, RingHomCompTriple.comp_apply] at h₁
Cleared hypotheses: h₁