-- Mathlib/RingTheory/Frobenius.lean
lemma conj (H : IsArithFrobAt R σ Q) (τ : G) : IsArithFrobAt R (τ * σ * τ⁻¹) (τ • Q)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this : Ideal.under R (Ideal.map (MulSemiringAction.toRingEquiv G S τ) Q) = Ideal.under R Q
⊢ (MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x - x ^ Nat.card (R ⧸ Ideal.under R (τ • Q)) ∈ τ • Q

Tactic:
rw [Ideal.pointwise_smul_eq_comap, Ideal.mem_comap]

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this : Ideal.under R (Ideal.map (MulSemiringAction.toRingEquiv G S τ) Q) = Ideal.under R Q
⊢ (RingEquiv.symm ((MulSemiringAction.toRingAut G S) τ))
      ((MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x -
        x ^ Nat.card (R ⧸ Ideal.under R (Ideal.comap (RingEquiv.symm ((MulSemiringAction.toRingAut G S) τ)) Q))) ∈
    Q

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
⊢ IsArithFrobAt R (τ * σ * τ⁻¹) (τ • Q)

Tactic:
intro x

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ (MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x - x ^ Nat.card (R ⧸ Ideal.under R (τ • Q)) ∈ τ • Q

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ Ideal.under R (Ideal.map (MulSemiringAction.toRingEquiv G S τ) Q) = Ideal.under R Q

Tactic:
rw [← Ideal.comap_symm, ← Ideal.comap_coe, Ideal.under, Ideal.comap_comap]

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ Ideal.comap ((↑(MulSemiringAction.toRingEquiv G S τ).symm).comp (algebraMap R S)) Q = Ideal.under R Q

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this : Ideal.under R (Ideal.map (MulSemiringAction.toRingEquiv G S τ) Q) = Ideal.under R Q
⊢ (RingEquiv.symm ((MulSemiringAction.toRingAut G S) τ))
      ((MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x -
        x ^ Nat.card (R ⧸ Ideal.under R (Ideal.comap (RingEquiv.symm ((MulSemiringAction.toRingAut G S) τ)) Q))) ∈
    Q

Tactic:
simpa [smul_sub, mul_smul, this] using H (τ⁻¹ • x)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ (MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x - x ^ Nat.card (R ⧸ Ideal.under R (τ • Q)) ∈ τ • Q

Tactic:
have : (Q.map (MulSemiringAction.toRingEquiv G S τ)).under R = Q.under R := by
  rw [← Ideal.comap_symm, ← Ideal.comap_coe, Ideal.under, Ideal.comap_comap]
  congr 1
  exact (MulSemiringAction.toAlgEquiv R S τ).symm.toAlgHom.comp_algebraMap

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this : Ideal.under R (Ideal.map (MulSemiringAction.toRingEquiv G S τ) Q) = Ideal.under R Q
⊢ (MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹)) x - x ^ Nat.card (R ⧸ Ideal.under R (τ • Q)) ∈ τ • Q

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ Ideal.comap ((↑(MulSemiringAction.toRingEquiv G S τ).symm).comp (algebraMap R S)) Q = Ideal.under R Q

Tactic:
congr 1

Result:
case e_f
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ (↑(MulSemiringAction.toRingEquiv G S τ).symm).comp (algebraMap R S) = algebraMap R S

Proof state:
case e_f
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ (↑(MulSemiringAction.toRingEquiv G S τ).symm).comp (algebraMap R S) = algebraMap R S

Tactic:
exact (MulSemiringAction.toAlgEquiv R S τ).symm.toAlgHom.comp_algebraMap

Result:
no goals