awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : Q.IsPrime
h :
  Nat.card.{u_1}
      (HasQuotient.Quotient R (B := Ideal R)
        (Ideal.comap (F := RingHom.{u_1, u_2} R (Localization.AtPrime Q)) (algebraMap R (Localization.AtPrime Q))
          (maximalIdeal (Localization.AtPrime Q)))) =
    Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
x : S
s : ↥Q.primeCompl
⊢ Eq (α := S ⧸ Q)
    ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q)
        (HMul.hMul (α := S) ((φ : (a : S) → S) x : S)
            ((↑s : S) ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) -
          HMul.hMul (β := S) (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))
            ((φ : (a : S) → S) (↑s : S) : S)) :
      S ⧸ Q)
    (0 : S ⧸ Q)

Tactic:
simp [H.mk_apply]

Premises used: AlgHom.IsArithFrobAt.mk_apply
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst_3 : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst_4 : Algebra.IsUnramifiedAt R Q
inst_5 : IsNoetherianRing S
apply :
  ∀ (x : Localization.AtPrime Q),
    Eq (α :=
      HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
        (maximalIdeal (Localization.AtPrime Q)))
      ((Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q)) :
            (a : Localization.AtPrime Q) → Localization.AtPrime Q ⧸ maximalIdeal (Localization.AtPrime Q))
          ((H.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q) x) :
        HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
          (maximalIdeal (Localization.AtPrime Q)))
      ((Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q)) :
            (a : Localization.AtPrime Q) → Localization.AtPrime Q ⧸ maximalIdeal (Localization.AtPrime Q))
          ((H'.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q) x) :
        HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
          (maximalIdeal (Localization.AtPrime Q)))
⊢ Eq (α := Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q) H.localize H'.localize

Tactic:
apply Algebra.FormallyUnramified.ext_of_iInf _
      (Ideal.iInf_pow_eq_bot_of_isLocalRing (maximalIdeal _) Ideal.IsPrime.ne_top')

Premises used: IsLocalRing.maximalIdeal, Algebra.FormallyUnramified.ext_of_iInf, Ideal.iInf_pow_eq_bot_of_isLocalRing, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst_3 : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst_4 : Algebra.IsUnramifiedAt R Q
inst_5 : IsNoetherianRing S
⊢ Eq (α := Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q) H.localize H'.localize

Tactic:
have : H.localize = H'.localize := by
    apply Algebra.FormallyUnramified.ext_of_iInf _
      (Ideal.iInf_pow_eq_bot_of_isLocalRing (maximalIdeal _) Ideal.IsPrime.ne_top')
    intro x
    rw [H.isArithFrobAt_localize.mk_apply, H'.isArithFrobAt_localize.mk_apply]
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst_3 : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst_4 : Algebra.IsUnramifiedAt R Q
inst_5 : IsNoetherianRing S
this : Eq (α := Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q) H.localize H'.localize
H₁ : ∀ (x : S), Eq (α := S) ((φ : (a : S) → S) x : S) ((ψ : (a : S) → S) x : S)
⊢ φ = ψ

Tactic:
ext x
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst_3 : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst_4 : Algebra.IsUnramifiedAt R Q
inst_5 : IsNoetherianRing S
this : Eq (α := Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q) H.localize H'.localize
x : S
H₁ :
  Eq (α := Localization.AtPrime Q)
    ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) ((φ : (a : S) → S) x) :
      Localization.AtPrime Q)
    ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) ((ψ : (a : S) → S) x) :
      Localization.AtPrime Q)
⊢ Eq (α := S) ((φ : (a : S) → S) x : S) ((ψ : (a : S) → S) x : S)

Tactic:
apply IsLocalization.injective (Localization.AtPrime Q) hQ

Premises used: Localization.AtPrime, IsLocalization.injective
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst_3 : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst_4 : Algebra.IsUnramifiedAt R Q
inst_5 : IsNoetherianRing S
this : Eq (α := Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q) H.localize H'.localize
x : S
H₁ :
  Eq (α := Localization.AtPrime Q)
    ((H.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q)
        ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) x) :
      Localization.AtPrime Q)
    ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) ((ψ : (a : S) → S) x) :
      Localization.AtPrime Q)
H₂ :
  Eq (α := Localization.AtPrime Q)
    ((H.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q)
        ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) x) :
      Localization.AtPrime Q)
    ((H'.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q)
        ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) x) :
      Localization.AtPrime Q)
H₃ H₄ :
  Eq (α := Localization.AtPrime Q)
    ((H'.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q)
        ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) x) :
      Localization.AtPrime Q)
    ((H'.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q)
        ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) x) :
      Localization.AtPrime Q)
⊢ Eq (α := Localization.AtPrime Q)
    ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) ((φ : (a : S) → S) x) :
      Localization.AtPrime Q)
    ((algebraMap S (Localization.AtPrime Q) : (a : S) → Localization.AtPrime Q) ((ψ : (a : S) → S) x) :
      Localization.AtPrime Q)

Tactic:
rw [← H.localize_algebraMap, ← H'.localize_algebraMap, this]

Premises used: AlgHom.IsArithFrobAt.localize_algebraMap
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
inst_6 : Q.IsPrime
h : IsArithFrobAt R σ Q
rw : HSMul.hSMul (β := Ideal S) σ (Ideal.comap (F := S →ₐ[R] S) (MulSemiringAction.toAlgHom R S σ) Q)
| σ • Q

Tactic:
rw [← h.comap_eq]

Premises used: AlgHom.IsArithFrobAt.comap_eq
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
inst_6 : Q.IsPrime
h : IsArithFrobAt R σ Q
conv_lhs : HSMul.hSMul (β := Ideal S) σ (Ideal.comap (F := S →ₐ[R] S) (MulSemiringAction.toAlgHom R S σ) Q) = Q
⊢ σ • Q = Q

Tactic:
conv_lhs => rw [← h.comap_eq]

Premises used: AlgHom.IsArithFrobAt.comap_eq
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
inst_6 : Q.IsPrime
h : IsArithFrobAt R σ Q
⊢ Ideal.map (F := S →+* S) (MulSemiringAction.toRingHom G S σ)
      (Ideal.comap (F := S →ₐ[R] S) (MulSemiringAction.toAlgHom R S σ) Q) =
    Q

Tactic:
Q.map_comap_eq_self_of_equiv (MulSemiringAction.toRingEquiv G S σ)

Premises used: MulSemiringAction.toRingHom, Ideal.map, Ideal.map_comap_eq_self_of_equiv, MulSemiringAction.toRingEquiv
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
inst_6 : Q.IsPrime
h : IsArithFrobAt R σ Q
⊢ Ideal.map (F := S →+* S) (MulSemiringAction.toRingHom G S σ)
      (Ideal.comap (F := S →ₐ[R] S) (MulSemiringAction.toAlgHom R S σ) Q) =
    Q

Tactic:
exact Q.map_comap_eq_self_of_equiv (MulSemiringAction.toRingEquiv G S σ)

Premises used: Ideal.map_comap_eq_self_of_equiv, MulSemiringAction.toRingEquiv
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ σ' : G
H : IsArithFrobAt R σ Q
H' : IsArithFrobAt R σ' Q
x : S
⊢ Membership.mem (γ := AddSubgroup S) (Submodule.toAddSubgroup Q) ((σ * σ'⁻¹) • x - x)

Tactic:
simpa [mul_smul] using sub_mem (H (σ'⁻¹ • x)) (H' (σ'⁻¹ • x))

Premises used: sub_mem, Inv.inv, HSMul.hSMul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
rw :
  Eq (α := Ideal R)
    (Ideal.comap (F := R →+* S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G S τ)) : S →+* S) (algebraMap R S))
      Q)
    (Ideal.under R Q)
⊢ Eq (α := Ideal R) (Ideal.under R (B := S) (Ideal.map (F := S ≃+* S) (MulSemiringAction.toRingEquiv G S τ) Q))
    (Ideal.under R Q)

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

Premises used: Ideal.comap_symm, Ideal.comap_coe, Ideal.under, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
e_f :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G S τ)) : S →+* S) (algebraMap R S))
    (algebraMap R S)
⊢ Eq (α := Ideal R)
    (Ideal.comap (F := R →+* S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G S τ)) : S →+* S) (algebraMap R S))
      Q)
    (Ideal.under R Q)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G S τ)) : S →+* S) (algebraMap R S))
    (algebraMap R S)

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

Premises used: AlgHom.comp_algebraMap, AlgEquiv.toAlgHom, MulSemiringAction.toAlgEquiv, AlgEquiv.symm, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, RingEquiv.symm
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G S τ)) : S →+* S) (algebraMap R S))
    (algebraMap R S)

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

Premises used: AlgHom.comp_algebraMap, AlgEquiv.toAlgHom, MulSemiringAction.toAlgEquiv, AlgEquiv.symm
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
⊢ Eq (α := Ideal R) (Ideal.under R (B := S) (Ideal.map (F := S ≃+* S) (MulSemiringAction.toRingEquiv G S τ) Q))
    (Ideal.under R 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
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this :
  Eq (α := Ideal R) (Ideal.under R (B := S) (Ideal.map (F := S ≃+* S) (MulSemiringAction.toRingEquiv G S τ) Q))
    (Ideal.under R Q)
rw :
  Membership.mem (α := S) Q
    ((RingEquiv.symm
            (((MulSemiringAction.toRingAut G S : MonoidHom.{u_3, u_2} G (RingAut S)) : (a : G) → RingAut S) τ) :
          (a : S) → S)
        (HSub.hSub (α := S) ((MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹) : (a : S) → S) x : S)
          (x ^
            Nat.card.{u_1}
              (HasQuotient.Quotient R (B := Ideal R)
                (Ideal.under R
                  (Ideal.comap (F := S ≃+* S)
                    (RingEquiv.symm
                      (((MulSemiringAction.toRingAut G S : MonoidHom.{u_3, u_2} G (RingAut S)) : (a : G) → RingAut S)
                        τ))
                    Q))))) :
      S)
⊢ HSub.hSub (α := S) ((MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹) : (a : S) → S) x : S)
      (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R (τ • Q)))) ∈
    τ • Q

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

Premises used: Ideal.pointwise_smul_eq_comap, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
σ : G
H : IsArithFrobAt R σ Q
τ : G
x : S
this :
  Eq (α := Ideal R) (Ideal.under R (B := S) (Ideal.map (F := S ≃+* S) (MulSemiringAction.toRingEquiv G S τ) Q))
    (Ideal.under R Q)
⊢ Membership.mem (α := S) Q
    ((RingEquiv.symm
            (((MulSemiringAction.toRingAut G S : MonoidHom.{u_3, u_2} G (RingAut S)) : (a : G) → RingAut S) τ) :
          (a : S) → S)
        (HSub.hSub (α := S) ((MulSemiringAction.toAlgHom R S (τ * σ * τ⁻¹) : (a : S) → S) x : S)
          (x ^
            Nat.card.{u_1}
              (HasQuotient.Quotient R (B := Ideal R)
                (Ideal.under R
                  (Ideal.comap (F := S ≃+* S)
                    (RingEquiv.symm
                      (((MulSemiringAction.toRingAut G S : MonoidHom.{u_3, u_2} G (RingAut S)) : (a : G) → RingAut S)
                        τ))
                    Q))))) :
      S)

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

Premises used: smul_sub, Inv.inv, HSMul.hSMul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
⊢ Algebra.IsIntegral R S

Tactic:
have := Algebra.IsInvariant.isIntegral R S G
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this : Algebra.IsIntegral R S
⊢ Q.IsMaximal

Tactic:
have : Q.IsMaximal := Ideal.Quotient.maximal_of_isField _ (Finite.isField_of_domain (S ⧸ Q))
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this : Q.IsMaximal
obtain : ∀ (p : ℕ) (hc : CharP.{u_1} (R ⧸ P) p), ∃ (σ : G), IsArithFrobAt R σ Q
⊢ ∃ (σ : G), IsArithFrobAt R σ Q

Tactic:
obtain ⟨p, hc⟩ := CharP.exists (R ⧸ P)

Premises used: CharP.exists, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
⊢ Finite.{u_1 + 1} (R ⧸ P)

Tactic:
have : Finite (R ⧸ P) := .of_injective _ Ideal.algebraMap_quotient_injective
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this : Finite.{u_1 + 1} (R ⧸ P)
intro : ∀ (val : Fintype (R ⧸ P)), ∃ (σ : G), IsArithFrobAt R σ Q
⊢ ∃ (σ : G), IsArithFrobAt R σ Q

Tactic:
cases nonempty_fintype (R ⧸ P)

Premises used: HasQuotient.Quotient, nonempty_fintype
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
⊢ CharP.{u_2} (S ⧸ Q) p

Tactic:
have := CharP.of_ringHom_of_ne_zero (algebraMap (R ⧸ P) (S ⧸ Q)) p hp.ne_zero
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this_3 : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
this : CharP.{u_2} (S ⧸ Q) p
⊢ ExpChar.{u_2} (S ⧸ Q) p

Tactic:
have : ExpChar (S ⧸ Q) p := .prime hp
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this_3 : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
this_4 : CharP.{u_2} (S ⧸ Q) p
this : ExpChar.{u_2} (S ⧸ Q) p
r : R ⧸ P
rw :
  Eq.{u_2 + 1} (α := S ⧸ Q) ((algebraMap (R ⧸ P) (S ⧸ Q) : (a : R ⧸ P) → S ⧸ Q) (r ^ p ^ (↑k : ℕ)) : S ⧸ Q)
    ((algebraMap (R ⧸ P) (S ⧸ Q) : (a : R ⧸ P) → S ⧸ Q) r : S ⧸ Q)
rw₁ :
  Eq.{u_2 + 1} (α := S ⧸ Q)
    ((algebraMap (R ⧸ P) (S ⧸ Q) : (a : R ⧸ P) → S ⧸ Q) (r ^ Fintype.card.{u_1} (R ⧸ P)) : S ⧸ Q)
    ((algebraMap (R ⧸ P) (S ⧸ Q) : (a : R ⧸ P) → S ⧸ Q) r : S ⧸ Q)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := S ⧸ Q) ((algebraMap (R ⧸ P) (S ⧸ Q) : (a : R ⧸ P) → S ⧸ Q) r : S ⧸ Q)
    ((algebraMap (R ⧸ P) (S ⧸ Q) : (a : R ⧸ P) → S ⧸ Q) r : S ⧸ Q)
⊢ HPow.hPow (α := S ⧸ Q) ((algebraMap (R ⧸ P) (S ⧸ Q) : (a : R ⧸ P) → S ⧸ Q) r : S ⧸ Q) (p ^ (↑k : ℕ)) =
    (algebraMap (R ⧸ P) (S ⧸ Q) : (a : R ⧸ P) → S ⧸ Q) r

Tactic:
rw [← map_pow, ← hk, FiniteField.pow_card]

Premises used: map_pow, FiniteField.pow_card
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this_3 : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
this_4 : CharP.{u_2} (S ⧸ Q) p
this : ExpChar.{u_2} (S ⧸ Q) p
l : Gal((S ⧸ Q)/R ⧸ P) :=
  let __spread.0 : S ⧸ Q ≃+* S ⧸ Q := iterateFrobeniusEquiv (S ⧸ Q) p (↑k : ℕ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
intro :
  ∀ (σ : ↥(MulAction.stabilizer G Q))
    (hσ :
      ((Ideal.Quotient.stabilizerHom Q P G : MonoidHom.{u_3, u_2} ↥(MulAction.stabilizer G Q) Gal((S ⧸ Q)/R ⧸ P)) :
            (a : ↥(MulAction.stabilizer G Q)) → Gal((S ⧸ Q)/R ⧸ P))
          σ =
        l),
    ∃ (σ : G), IsArithFrobAt R σ Q
⊢ ∃ (σ : G), IsArithFrobAt R σ Q

Tactic:
obtain ⟨σ, hσ⟩ := Ideal.Quotient.stabilizerHom_surjective G P Q l

Premises used: Ideal.Quotient.stabilizerHom_surjective
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this_3 : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
this_4 : CharP.{u_2} (S ⧸ Q) p
this : ExpChar.{u_2} (S ⧸ Q) p
l : Gal((S ⧸ Q)/R ⧸ P) :=
  let __spread.0 : S ⧸ Q ≃+* S ⧸ Q := iterateFrobeniusEquiv (S ⧸ Q) p (↑k : ℕ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ :
  ((Ideal.Quotient.stabilizerHom Q P G : MonoidHom.{u_3, u_2} ↥(MulAction.stabilizer G Q) Gal((S ⧸ Q)/R ⧸ P)) :
        (a : ↥(MulAction.stabilizer G Q)) → Gal((S ⧸ Q)/R ⧸ P))
      σ =
    l
⊢ ∃ (σ : G), IsArithFrobAt R σ Q

Tactic:
⟨σ, fun x ↦ ?_⟩

Premises used: Exists.intro, Subtype.val