awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
⊢ Eq (α := S) ((φ : (a : S) → S) x : S) ((ψ : (a : S) → S) x : S)
have 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)
Tactic: apply IsLocalization.injective (Localization.AtPrime Q) hQ
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
⊢ 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)
have 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)
Tactic: rw [← H.localize_algebraMap, ← H'.localize_algebraMap, this]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← H.localize_algebraMap, ← H'.localize_algebraMap, this]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← H.localize_algebraMap, ← H'.localize_algebraMap, this]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
| σ • Q
have rw : HSMul.hSMul (β := Ideal S) σ (Ideal.comap (F := S →ₐ[R] S) (MulSemiringAction.toAlgHom R S σ) Q)
Tactic: rw [← h.comap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
⊢ σ • Q = Q
have conv_lhs : HSMul.hSMul (β := Ideal S) σ (Ideal.comap (F := S →ₐ[R] S) (MulSemiringAction.toAlgHom R S σ) Q) = Q
Tactic: conv_lhs => rw [← h.comap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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)
have 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)
Tactic: rw [← Ideal.comap_symm, ← Ideal.comap_coe, Ideal.under, Ideal.comap_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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.comap (F := R →+* S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G S τ)) : S →+* S) (algebraMap R S))
      Q)
    (Ideal.under R Q)
have e_f : Eq (α := R →+* S)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G S τ)) : S →+* S) (algebraMap R S))
  (algebraMap R S)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (hypothesis)
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
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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)
⊢ 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
have 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)
Tactic: rw [Ideal.pointwise_smul_eq_comap, Ideal.mem_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (hypothesis)
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
⊢ ∃ (σ : G), IsArithFrobAt R σ Q
have this : Algebra.IsIntegral R S
Tactic: have := Algebra.IsInvariant.isIntegral R S G
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (hypothesis)
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
⊢ ∃ (σ : G), IsArithFrobAt R σ Q
have this₁ : Q.IsMaximal
Tactic: have : Q.IsMaximal := Ideal.Quotient.maximal_of_isField _ (Finite.isField_of_domain (S ⧸ Q))
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
⊢ ∃ (σ : G), IsArithFrobAt R σ Q
have obtain : ∀ (p : ℕ) (hc : CharP.{u_1} (R ⧸ P) p), ∃ (σ : G), IsArithFrobAt R σ Q
Tactic: obtain ⟨p, hc⟩ := CharP.exists (R ⧸ P)
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (hypothesis)
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
⊢ ∃ (σ : G), IsArithFrobAt R σ Q
have this₁ : Finite.{u_1 + 1} (R ⧸ P)
Tactic: have : Finite (R ⧸ P) := .of_injective _ Ideal.algebraMap_quotient_injective
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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)
⊢ ∃ (σ : G), IsArithFrobAt R σ Q
have intro : ∀ (val : Fintype (R ⧸ P)), ∃ (σ : G), IsArithFrobAt R σ Q
Tactic: cases nonempty_fintype (R ⧸ P)
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (hypothesis)
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 : ℕ)
⊢ ∃ (σ : G), IsArithFrobAt R σ Q
have this₁ : CharP.{u_2} (S ⧸ Q) p
Tactic: have := CharP.of_ringHom_of_ne_zero (algebraMap (R ⧸ P) (S ⧸ Q)) p hp.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (hypothesis)
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
⊢ ∃ (σ : G), IsArithFrobAt R σ Q
have this₁ : ExpChar.{u_2} (S ⧸ Q) p
Tactic: have : ExpChar (S ⧸ Q) p := .prime hp
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
⊢ 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
have 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)
Tactic: rw [← map_pow, ← hk, FiniteField.pow_card]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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)
⊢ 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
have 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)
Tactic: rw [← map_pow, ← hk, FiniteField.pow_card]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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)
⊢ 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
have 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)
Tactic: rw [← map_pow, ← hk, FiniteField.pow_card]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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' := ⋯ }
⊢ ∃ (σ : G), IsArithFrobAt R σ Q
have 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
Tactic: obtain ⟨σ, hσ⟩ := Ideal.Quotient.stabilizerHom_surjective G P Q l
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
have intro : ∀ (x : S),
  HSub.hSub (α := S) ((MulSemiringAction.toAlgHom R S (↑σ : G) : (a : S) → S) x : S)
      (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) ∈
    Q
Tactic: refine ⟨σ, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
x : S
⊢ HSub.hSub (α := S) ((MulSemiringAction.toAlgHom R S (↑σ : G) : (a : S) → S) x : S)
      (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) ∈
    Q
have intro : Eq (α := S ⧸ Q)
  ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) ((MulSemiringAction.toAlgHom R S (↑σ : G) : (a : S) → S) x) : S ⧸ Q)
  ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) (x ^ p ^ (↑k : ℕ)) : S ⧸ Q)
Tactic: rw [← Ideal.Quotient.eq, Nat.card_eq_fintype_card, hk]
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
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
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
hP : ∃ (Q : (↑(P.primesOver S) : Type u_2)), Finite.{u_2 + 1} (S ⧸ (↑Q : Ideal S))
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
have obtain : ∀ (Q : Ideal S) (hQ₁ : Q.IsPrime) (hQ₂ : Q.LiesOver P)
  (hQ₃ :
    Finite.{u_2 + 1}
      (S ⧸
        (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q sorry) :
          Ideal S))),
  ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
Tactic: obtain ⟨⟨Q, hQ₁, hQ₂⟩, hQ₃⟩ := hP
Cleared hypotheses: hP