-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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 : ℕ
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)
        ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger) :
      𝓞 K ⧸ P)
    ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) (σ • hζ.toInteger) : 𝓞 K ⧸ P)
hi :
  (τ : (a : 𝓞 K ⧸ P) → 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger) =
    HPow.hPow (α := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P)
      (Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i)
rwa :
  ∀
    (hi :
      (Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) (σ • hζ.toInteger) =
        HPow.hPow (α := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P)
          (Nat.card (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)})) ^ i)),
    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)ˣ)
rwa₁ :
  ∀
    (hi :
      (Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) (σ • hζ.toInteger) =
        HPow.hPow (α := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) (p ^ i)),
    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)ˣ)
rwa₂ :
  ∀
    (hi :
      (Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P)
          (hζ.toInteger ^
            ZMod.val (n := n)
              (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) =
        HPow.hPow (α := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) (p ^ i)),
    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)ˣ)
rwa₃ :
  ∀
    (hi :
      HPow.hPow (α := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P)
          (ZMod.val (n := n)
            (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) =
        HPow.hPow (α := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) (p ^ i)),
    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)ˣ)
rwa₄ :
  ∀
    (hi :
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) %
          orderOf (G := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) hζ.toInteger : 𝓞 K ⧸ P) =
        p ^ i % orderOf (G := 𝓞 K ⧸ P) ((Ideal.Quotient.mk P : (a : 𝓞 K) → 𝓞 K ⧸ P) 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)ˣ)
rwa₅ :
  ∀
    (hi :
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) % n =
        p ^ i % n),
    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)ˣ)
rwa₆ :
  ∀
    (hi :
      Eq (α := ZMod n)
        (↑(ZMod.val (n := n)
              (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
          ZMod n)
        (↑(p ^ i) : ZMod n)),
    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)ˣ)
rwa₇ :
  ∀
    (hi :
      (↑(ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
          ZMod n) =
        HPow.hPow (α := ZMod n) (↑p : ZMod n) i),
    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)ˣ)
rwa₈ :
  ∀
    (hi :
      (↑(ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
          ZMod n) =
        (↑(ZMod.unitOfCoprime p hn) : ZMod n) ^ i),
    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)ˣ)
rwa₉ :
  ∀
    (hi :
      (↑(ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
          ZMod n) =
        (↑(ZMod.unitOfCoprime p hn ^ i) : ZMod n)),
    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)ˣ)
rwa₁₀ :
  ∀
    (hi :
      (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n) =
        (↑(ZMod.unitOfCoprime p hn ^ i) : ZMod n)),
    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)ˣ)
rwa₁₁ :
  ∀ (hi : ((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ = ZMod.unitOfCoprime p hn ^ i),
    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)ˣ)
rwa₁₂ rwa₁₃ rwa₁₄ rwa₁₅ :
  ∀ (hi : ZMod.unitOfCoprime p hn ^ i = ((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ),
    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)ˣ)
⊢ 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)ˣ)

Tactic:
rwa [h₁, Int.card_ideal_quot, galEquivZMod_smul_of_pow_eq n _ _
    (hζ.toInteger_isPrimitiveRoot.pow_eq_one), map_pow, (h₀.isOfFinOrder (NeZero.ne _)).pow_inj_mod,
    ← h₀.eq_orderOf, ← ZMod.natCast_eq_natCast_iff', Nat.cast_pow, ← ZMod.coe_unitOfCoprime p hn,
    ← Units.val_pow_eq_pow_val, ZMod.natCast_zmod_val, ← Units.ext_iff, eq_comm] at hi

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot, IsPrimitiveRoot.eq_orderOf, Units.ext_iff, Int.card_ideal_quot, ZMod.natCast_eq_natCast_iff', map_pow, eq_comm, ZMod.natCast_zmod_val, IsOfFinOrder.pow_inj_mod, IsPrimitiveRoot.isOfFinOrder, ZMod.coe_unitOfCoprime, Nat.cast_pow, Units.val_pow_eq_pow_val, IsPrimitiveRoot.pow_eq_one, NeZero.ne, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq