-- Mathlib/RingTheory/Frobenius.lean
lemma isArithFrobAt_localize [Q.IsPrime] : H.localize.IsArithFrobAt (maximalIdeal _)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
⊢ H.localize.IsArithFrobAt (maximalIdeal (Localization.AtPrime Q))

Tactic:
intro x

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : Localization.AtPrime Q
⊢ H.localize x - x ^ Nat.card (R ⧸ Ideal.under R (maximalIdeal (Localization.AtPrime Q))) ∈
    maximalIdeal (Localization.AtPrime Q)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : Localization.AtPrime Q
⊢ H.localize x - x ^ Nat.card (R ⧸ Ideal.under R (maximalIdeal (Localization.AtPrime Q))) ∈
    maximalIdeal (Localization.AtPrime Q)

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective Q.primeCompl x

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ H.localize (IsLocalization.mk' (Localization.AtPrime Q) x s) -
      IsLocalization.mk' (Localization.AtPrime Q) x s ^
        Nat.card (R ⧸ Ideal.under R (maximalIdeal (Localization.AtPrime Q))) ∈
    maximalIdeal (Localization.AtPrime Q)

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ φ x * ↑(s ^ Nat.card (R ⧸ Ideal.under R Q)) - x ^ Nat.card (R ⧸ Ideal.under R Q) * ↑⟨φ ↑s, ⋯⟩ ∈ Q

Tactic:
simp only [SubmonoidClass.coe_pow, ← Ideal.Quotient.eq_zero_iff_mem]

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ (Ideal.Quotient.mk Q) (φ x * ↑s ^ Nat.card (R ⧸ Ideal.under R Q) - x ^ Nat.card (R ⧸ Ideal.under R Q) * φ ↑s) = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)

Tactic:
congr 2

Result:
case e_α.e_b
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q)) = Ideal.under R Q

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime Q) (φ x) ⟨φ ↑s, ⋯⟩ -
      IsLocalization.mk' (Localization.AtPrime Q) (x ^ Nat.card (R ⧸ Ideal.under R Q))
        (s ^ Nat.card (R ⧸ Ideal.under R Q)) ∈
    maximalIdeal (Localization.AtPrime Q)

Tactic:
rw [← IsLocalization.mk'_sub,
  IsLocalization.AtPrime.mk'_mem_maximal_iff (Localization.AtPrime Q) Q]

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ φ x * ↑(s ^ Nat.card (R ⧸ Ideal.under R Q)) - x ^ Nat.card (R ⧸ Ideal.under R Q) * ↑⟨φ ↑s, ⋯⟩ ∈ Q

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ H.localize (IsLocalization.mk' (Localization.AtPrime Q) x s) -
      IsLocalization.mk' (Localization.AtPrime Q) x s ^
        Nat.card (R ⧸ Ideal.under R (maximalIdeal (Localization.AtPrime Q))) ∈
    maximalIdeal (Localization.AtPrime Q)

Tactic:
simp [localize, coe_mk, -mem_maximalIdeal, mem_nonunits_iff, Localization.localRingHom_mk',
  ← IsLocalization.mk'_pow, h]

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime Q) (φ x) ⟨φ ↑s, ⋯⟩ -
      IsLocalization.mk' (Localization.AtPrime Q) (x ^ Nat.card (R ⧸ Ideal.under R Q))
        (s ^ Nat.card (R ⧸ Ideal.under R Q)) ∈
    maximalIdeal (Localization.AtPrime Q)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ H.localize.IsArithFrobAt (maximalIdeal (Localization.AtPrime Q))

Tactic:
have h : Nat.card (R ⧸ (maximalIdeal _).comap (algebraMap R (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Q.under R) := by
  congr 2
  rw [IsScalarTower.algebraMap_eq R S (Localization.AtPrime Q), ← Ideal.comap_comap,
    Localization.AtPrime.comap_maximalIdeal]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
⊢ H.localize.IsArithFrobAt (maximalIdeal (Localization.AtPrime Q))

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ (Ideal.Quotient.mk Q) (φ x * ↑s ^ Nat.card (R ⧸ Ideal.under R Q) - x ^ Nat.card (R ⧸ Ideal.under R Q) * φ ↑s) = 0

Tactic:
simp [H.mk_apply]

Result:
no goals