awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
inst : Subsingleton α
this :
  Eq (α := (a : FreeRing α) → FreeCommRing α) (⇑(coeRingHom α) : (a : FreeRing α) → FreeCommRing α)
    (⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α)) :
      (a : FreeAbelianGroup (List α)) → FreeAbelianGroup (Multiset α))
⊢ Bijective (α := FreeRing α) (β := FreeCommRing α)
    (⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α)) :
      (a : FreeAbelianGroup (List α)) → FreeAbelianGroup (Multiset α))

Tactic:
apply Equiv.bijective

Premises used: Equiv.bijective
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
inst : Subsingleton α
x y : FreeRing α
rw :
  x * y =
    ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
      ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) (y * x))
rw₁ :
  x * y =
    ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
      (HMul.hMul (α := FreeCommRing α) (β := FreeCommRing α)
        ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) y : FreeCommRing α)
        ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α))
rw₂ :
  x * y =
    ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
      (HMul.hMul (α := FreeCommRing α) (β := FreeCommRing α)
        ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
        ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) y : FreeCommRing α))
rw₃ :
  x * y =
    ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
      ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) (x * y))
rw₄ rw₅ : x * y = x * y
⊢ x * y = y * x

Tactic:
rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),
        (subsingletonEquivFreeCommRing α).map_mul, mul_comm,
        ← (subsingletonEquivFreeCommRing α).map_mul,
        (subsingletonEquivFreeCommRing α).symm_apply_apply]

Premises used: HMul.hMul, FreeRing.subsingletonEquivFreeCommRing, RingEquiv.map_mul, RingEquiv.symm_apply_apply, mul_comm
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
hC :
  ∀ (x : ℤ) (m : α →₀ ℕ),
    Eq (α := ℤ)
      (MvPolynomial.coeff m
        ((RingHom.comp (β := MvPolynomial α ℤ)
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                ((FreeCommRing.lift : (a : α → MvPolynomial α ℤ) → FreeCommRing α →+* MvPolynomial α ℤ) fun (a : α) ↦
                  MvPolynomial.X a)
                (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of))
              MvPolynomial.C :
            (a : ℤ) → MvPolynomial α ℤ)
          x))
      (MvPolynomial.coeff m
        ((RingHom.comp (RingHom.id (MvPolynomial α ℤ)) MvPolynomial.C : (a : ℤ) → MvPolynomial α ℤ) x))
hX :
  ∀ (i : α) (m : α →₀ ℕ),
    Eq (α := ℤ)
      (MvPolynomial.coeff m
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              ((FreeCommRing.lift : (a : α → MvPolynomial α ℤ) → FreeCommRing α →+* MvPolynomial α ℤ) fun (a : α) ↦
                MvPolynomial.X a)
              (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of) :
            (a : MvPolynomial α ℤ) → MvPolynomial α ℤ)
          (MvPolynomial.X i)))
      (MvPolynomial.coeff m
        ((RingHom.id (MvPolynomial α ℤ) : (a : MvPolynomial α ℤ) → MvPolynomial α ℤ) (MvPolynomial.X i)))
⊢ Eq.{u + 1} (α := MvPolynomial α ℤ →+* MvPolynomial α ℤ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      ((FreeCommRing.lift : (a : α → MvPolynomial α ℤ) → FreeCommRing α →+* MvPolynomial α ℤ) fun (a : α) ↦
        MvPolynomial.X a)
      (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of))
    (RingHom.id (MvPolynomial α ℤ))

Tactic:
ext
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : ℤ
m : α →₀ ℕ
⊢ Eq (α := ℤ)
    (MvPolynomial.coeff m
      ((RingHom.comp (β := MvPolynomial α ℤ)
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              ((FreeCommRing.lift : (a : α → MvPolynomial α ℤ) → FreeCommRing α →+* MvPolynomial α ℤ) fun (a : α) ↦
                MvPolynomial.X a)
              (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of))
            MvPolynomial.C :
          (a : ℤ) → MvPolynomial α ℤ)
        x))
    (MvPolynomial.coeff m
      ((RingHom.comp (RingHom.id (MvPolynomial α ℤ)) MvPolynomial.C : (a : ℤ) → MvPolynomial α ℤ) x))

Tactic:
simp
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
i : α
m : α →₀ ℕ
⊢ Eq (α := ℤ)
    (MvPolynomial.coeff m
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            ((FreeCommRing.lift : (a : α → MvPolynomial α ℤ) → FreeCommRing α →+* MvPolynomial α ℤ) fun (a : α) ↦
              MvPolynomial.X a)
            (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of) :
          (a : MvPolynomial α ℤ) → MvPolynomial α ℤ)
        (MvPolynomial.X i)))
    (MvPolynomial.coeff m
      ((RingHom.id (MvPolynomial α ℤ) : (a : MvPolynomial α ℤ) → MvPolynomial α ℤ) (MvPolynomial.X i)))

Tactic:
simp
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
h :
  ∀ (x : α),
    Eq (α := FreeCommRing α)
      ((RingHom.comp (β := MvPolynomial α ℤ) (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of)
              ((FreeCommRing.lift : (a : α → MvPolynomial α ℤ) → FreeCommRing α →+* MvPolynomial α ℤ) fun (a : α) ↦
                MvPolynomial.X a) :
            (a : FreeCommRing α) → FreeCommRing α)
          (FreeCommRing.of x) :
        FreeCommRing α)
      ((RingHom.id (FreeCommRing α) : (a : FreeCommRing α) → FreeCommRing α) (FreeCommRing.of x) : FreeCommRing α)
⊢ Eq.{u + 1} (α := FreeCommRing α →+* FreeCommRing α)
    (RingHom.comp (β := MvPolynomial α ℤ) (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of)
      ((FreeCommRing.lift : (a : α → MvPolynomial α ℤ) → FreeCommRing α →+* MvPolynomial α ℤ) fun (a : α) ↦
        MvPolynomial.X a))
    (RingHom.id (FreeCommRing α))

Tactic:
ext
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : α
⊢ Eq (α := FreeCommRing α)
    ((RingHom.comp (β := MvPolynomial α ℤ) (MvPolynomial.eval₂Hom (Int.castRingHom (FreeCommRing α)) FreeCommRing.of)
            ((FreeCommRing.lift : (a : α → MvPolynomial α ℤ) → FreeCommRing α →+* MvPolynomial α ℤ) fun (a : α) ↦
              MvPolynomial.X a) :
          (a : FreeCommRing α) → FreeCommRing α)
        (FreeCommRing.of x) :
      FreeCommRing α)
    ((RingHom.id (FreeCommRing α) : (a : FreeCommRing α) → FreeCommRing α) (FreeCommRing.of x) : FreeCommRing α)

Tactic:
simp
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := α) of

Tactic:
FreeAbelianGroup.of_injective.comp FreeMonoid.of_injective

Premises used: FreeRing.of, FreeMonoid.of_injective, Function.Injective.comp, FreeAbelianGroup.of, FreeAbelianGroup.of_injective, FreeRing
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
x : α
⊢ of x ≠ 0

Tactic:
FreeAbelianGroup.of_ne_zero _

Premises used: FreeAbelianGroup.of_ne_zero, FreeRing.of, FreeRing
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
x : α
⊢ 0 ≠ of x

Tactic:
FreeAbelianGroup.zero_ne_of _

Premises used: FreeRing.of, FreeAbelianGroup.zero_ne_of, FreeRing
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
x : α
⊢ of x ≠ 1

Tactic:
FreeAbelianGroup.of_injective.ne <| FreeMonoid.of_ne_one _

Premises used: FreeMonoid.of_ne_one, FreeRing.of, Function.Injective.ne, FreeAbelianGroup.of, FreeAbelianGroup.of_injective, FreeRing
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
x : α
⊢ 1 ≠ of x

Tactic:
FreeAbelianGroup.of_injective.ne <| FreeMonoid.one_ne_of _

Premises used: FreeRing.of, Function.Injective.ne, FreeMonoid.one_ne_of, FreeAbelianGroup.of, FreeAbelianGroup.of_injective, FreeRing
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
⊢ C z

Tactic:
have hn : ∀ x, C x → C (-x) := fun x ih => neg_one_mul x ▸ hm _ _ hn1 ih
  have h1 : C 1 := neg_neg (1 : FreeRing α) ▸ hn _ hn1
  FreeAbelianGroup.induction_on z (neg_add_cancel (1 : FreeRing α) ▸ ha _ _ hn1 h1)
    (fun m => List.recOn m h1 fun a _ ih => hm _ _ (hb a) ih)
    (fun _ ih => hn _ ih) ha

Premises used: FreeAbelianGroup.induction_on, neg_one_mul, Eq.rec, neg_neg, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
R : Type v
inst : Ring R
f : α → R
x : α
⊢ (((lift : (a : α → R) → FreeRing α →+* R) f : RingHom.{u, v} (FreeRing α) R) : (a : FreeRing α) → R) (of x) = f x

Tactic:
congr_fun (lift.left_inv f) x

Premises used: Quotient.liftOn', FreeRing.lift, FreeGroup.Lift.aux, Con.liftOn, congr_fun, List.foldr, Equiv.left_inv, List.prod
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
R : Type v
inst : Ring R
f : RingHom.{u, v} (FreeRing α) R
⊢ (lift : (a : α → R) → FreeRing α →+* R) ((⇑f : (a : FreeRing α) → R) ∘ of) = f

Tactic:
lift.right_inv f

Premises used: Equiv.right_inv, FreeRing.of, FreeRing.lift, FreeAbelianGroup.of
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
R : Type v
inst : Ring R
f g : RingHom.{u, v} (FreeRing α) R
h : ∀ (x : α), Eq.{v + 1} (α := R) ((f : (a : FreeRing α) → R) (of x) : R) ((g : (a : FreeRing α) → R) (of x) : R)
⊢ f = g

Tactic:
lift.symm.injective (funext h)

Premises used: FreeRing.lift, funext, Equiv.injective, Equiv.symm
-- Module: Mathlib.RingTheory.FreeRing
Goal:
α : Type u
β : Type v
f : α → β
x : α
⊢ (map f : (a : FreeRing α) → FreeRing β) (of x) = of (f x)

Tactic:
lift_of _ _

Premises used: FreeRing.of, FreeRing.lift_of, FreeAbelianGroup.of
-- 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
x : S
rw :
  HSub.hSub (α := S) ((φ : (a : S) → S) x : S)
      (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) ∈
    Q
⊢ (Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) ((φ : (a : S) → S) x) =
    HPow.hPow (α := S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x : S ⧸ Q)
      (Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))

Tactic:
rw [← map_pow, Ideal.Quotient.eq]

Premises used: map_pow, Ideal.Quotient.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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ HSub.hSub (α := S) ((φ : (a : S) → S) x : S)
      (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) ∈
    Q

Tactic:
H x

Premises used: Set.Mem
-- 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
x : S
⊢ HSub.hSub (α := S) ((φ : (a : S) → S) x : S)
      (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) ∈
    Q

Tactic:
exact H 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
by_contra! : ∀ (h : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))), False
⊢ _root_.Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))

Tactic:
by_contra! h
-- 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 : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
⊢ Q = ⊤

Tactic:
simpa [Nat.card_eq_zero_of_infinite, ← Ideal.eq_top_iff_one] using H 0

Premises used: Nat.card_eq_zero_of_infinite, Ideal.eq_top_iff_one, OfNat.ofNat
-- 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 : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
⊢ φ.IsArithFrobAt ⊤

Tactic:
obtain rfl : Q = ⊤ := by simpa [Nat.card_eq_zero_of_infinite, ← Ideal.eq_top_iff_one] using H 0

Premises used: rfl
-- 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 : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
H₁ : φ.IsArithFrobAt ⊤
⊢ Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under.{u_1, u_2} R (B := S) ⊤))

Tactic:
obtain rfl : Q = ⊤ := by simpa [Nat.card_eq_zero_of_infinite, ← Ideal.eq_top_iff_one] using H 0

Premises used: rfl
-- 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
H : φ.IsArithFrobAt ⊤
h : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under.{u_1, u_2} R (B := S) ⊤))
⊢ Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)

Tactic:
simp only [Ideal.comap_top] at h

Premises used: Ideal.comap_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
H : φ.IsArithFrobAt ⊤
h : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)
⊢ False

Tactic:
not_finite (R ⧸ (⊤ : Ideal R))

Premises used: HasQuotient.Quotient, Top.top, not_finite
-- 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
H : φ.IsArithFrobAt ⊤
h : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)
⊢ False

Tactic:
exact not_finite (R ⧸ (⊤ : Ideal R))

Premises used: HasQuotient.Quotient, Top.top, not_finite
-- 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
⊢ 0 < Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))

Tactic:
have := H.finite_quotient
  Nat.card_pos

Premises used: Nat.card_pos, AlgHom.IsArithFrobAt.finite_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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
hx : x ∈ Q
⊢ Membership.mem (γ := Submodule S S) (Ideal.comap φ Q) x

Tactic:
simp_all only [Ideal.mem_comap, ← Ideal.Quotient.eq_zero_iff_mem (I := Q), H.mk_apply,
    zero_pow_eq, ite_eq_right_iff, H.card_pos.ne', false_implies]

Premises used: AlgHom.IsArithFrobAt.mk_apply, false_implies, Ideal.Quotient.eq_zero_iff_mem, LT.lt.ne', zero_pow_eq, ite_eq_right_iff, AlgHom.IsArithFrobAt.card_pos, 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
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)
obtain :
  ∀ (x : R),
    OneHom.toFun (↑(↑(Ideal.quotientMap Q (↑φ : S →+* S) ⋯) : S ⧸ Q →* S ⧸ Q) : OneHom (S ⧸ Q) (S ⧸ Q))
        ((algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)) (S ⧸ Q) :
            (a : R ⧸ Ideal.under R Q) → S ⧸ Q)
          ((Ideal.Quotient.mk (Ideal.under R Q) : (a : R) → R ⧸ Ideal.under R Q) x)) =
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)) (S ⧸ Q) : (a : R ⧸ Ideal.under R Q) → S ⧸ Q)
        ((Ideal.Quotient.mk (Ideal.under R Q) : (a : R) → R ⧸ Ideal.under R Q) x)
⊢ OneHom.toFun (↑(↑(Ideal.quotientMap Q (↑φ : S →+* S) ⋯) : S ⧸ Q →* S ⧸ Q) : OneHom (S ⧸ Q) (S ⧸ Q))
      ((algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)) (S ⧸ Q) :
          (a : R ⧸ Ideal.under R Q) → S ⧸ Q)
        x) =
    (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)) (S ⧸ Q) : (a : R ⧸ Ideal.under R Q) → S ⧸ Q) x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- 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
x : R
⊢ OneHom.toFun (↑(↑(Ideal.quotientMap Q (↑φ : S →+* S) ⋯) : S ⧸ Q →* S ⧸ Q) : OneHom (S ⧸ Q) (S ⧸ Q))
      ((algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)) (S ⧸ Q) :
          (a : R ⧸ Ideal.under R Q) → S ⧸ Q)
        ((Ideal.Quotient.mk (Ideal.under R Q) : (a : R) → R ⧸ Ideal.under R Q) x)) =
    (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)) (S ⧸ Q) : (a : R ⧸ Ideal.under R Q) → S ⧸ Q)
      ((Ideal.Quotient.mk (Ideal.under R Q) : (a : R) → R ⧸ Ideal.under R Q) x)

Tactic:
DFunLike.congr_arg (Ideal.Quotient.mk Q) (φ.commutes x)

Premises used: Quotient.liftOn', Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, AlgHom.commutes, DFunLike.congr_arg
-- 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
x : R
⊢ OneHom.toFun (↑(↑(Ideal.quotientMap Q (↑φ : S →+* S) ⋯) : S ⧸ Q →* S ⧸ Q) : OneHom (S ⧸ Q) (S ⧸ Q))
      ((algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)) (S ⧸ Q) :
          (a : R ⧸ Ideal.under R Q) → S ⧸ Q)
        ((Ideal.Quotient.mk (Ideal.under R Q) : (a : R) → R ⧸ Ideal.under R Q) x)) =
    (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)) (S ⧸ Q) : (a : R ⧸ Ideal.under R Q) → S ⧸ Q)
      ((Ideal.Quotient.mk (Ideal.under R Q) : (a : R) → R ⧸ Ideal.under R Q) x)

Tactic:
exact DFunLike.congr_arg (Ideal.Quotient.mk Q) (φ.commutes x)

Premises used: Ideal.Quotient.mk, AlgHom.commutes, DFunLike.congr_arg
-- 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
x : S ⧸ Q
obtain :
  ∀ (x : S),
    (H.restrict : (a : S ⧸ Q) → S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x) =
      HPow.hPow (α := S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x : S ⧸ Q)
        (Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))
⊢ (H.restrict : (a : S ⧸ Q) → S ⧸ Q) x = x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- 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
x : S
⊢ (H.restrict : (a : S ⧸ Q) → S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x) =
    HPow.hPow (α := S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x : S ⧸ Q)
      (Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))

Tactic:
H.mk_apply x

Premises used: AlgHom.IsArithFrobAt.mk_apply, Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk
-- 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
x : S
⊢ (H.restrict : (a : S ⧸ Q) → S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x) =
    HPow.hPow (α := S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x : S ⧸ Q)
      (Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))

Tactic:
exact H.mk_apply x

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
x : S
⊢ Eq (α := S ⧸ Q) ((H.restrict : (a : S ⧸ Q) → S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x) : S ⧸ Q)
    ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) ((φ : (a : S) → S) x) : S ⧸ Q)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- 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
rw : ∀ (a : S ⧸ Q), Eq (α := S ⧸ Q) ((H.restrict : (a : S ⧸ Q) → S ⧸ Q) a : S ⧸ Q) (0 : S ⧸ Q) → a = 0
⊢ Function.Injective (α := S ⧸ Q) (β := S ⧸ Q) (⇑H.restrict : (a : S ⧸ Q) → S ⧸ Q)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : Q.IsPrime
x : S ⧸ Q
hx : Eq (α := S ⧸ Q) ((H.restrict : (a : S ⧸ Q) → S ⧸ Q) x : S ⧸ Q) (0 : S ⧸ Q)
⊢ x = 0

Tactic:
simpa [restrict_apply, H.card_pos.ne'] using hx

Premises used: LT.lt.ne', AlgHom.IsArithFrobAt.card_pos, AlgHom.IsArithFrobAt.restrict_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
inst_3 : Q.IsPrime
⊢ Ideal.comap φ Q = Q

Tactic:
le_antisymm (fun x hx ↦ ?_) H.le_comap

Premises used: AlgHom.IsArithFrobAt.le_comap, le_antisymm
-- 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
refine : ∀ (x : S) (hx : Membership.mem (γ := Submodule S S) (Ideal.comap φ Q) x), x ∈ Q
⊢ Ideal.comap φ Q = Q

Tactic:
refine le_antisymm (fun x hx ↦ ?_) H.le_comap

Premises used: AlgHom.IsArithFrobAt.le_comap, le_antisymm
-- 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
x : S
hx : Membership.mem (γ := Submodule S S) (Ideal.comap φ Q) x
rwa : Eq (α := S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x : S ⧸ Q) (0 : S ⧸ Q)
rwa₁ :
  Eq (α := S ⧸ Q) ((H.restrict : (a : S ⧸ Q) → S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x) : S ⧸ Q)
    ((H.restrict : (a : S ⧸ Q) → S ⧸ Q) 0 : S ⧸ Q)
rwa₂ :
  Eq (α := S ⧸ Q) ((H.restrict : (a : S ⧸ Q) → S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x) : S ⧸ Q) (0 : S ⧸ Q)
rwa₃ : Eq (α := S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) ((φ : (a : S) → S) x) : S ⧸ Q) (0 : S ⧸ Q)
rwa₄ : Membership.mem (α := S) Q ((φ : (a : S) → S) x : S)
rwa₅ rwa₆ rwa₇ rwa₈ : Membership.mem (γ := Ideal S) (Ideal.comap φ Q) x
⊢ x ∈ Q

Tactic:
rwa [← Ideal.Quotient.eq_zero_iff_mem, ← H.restrict_injective.eq_iff, map_zero, restrict_mk,
    Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap]

Premises used: Function.Injective.eq_iff, map_zero, AlgHom.IsArithFrobAt.restrict_injective, Ideal.Quotient.eq_zero_iff_mem, AlgHom.IsArithFrobAt.restrict_mk, 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ : ζ ^ m = 1
hk' : (↑m : S) ∉ Q
set :
  let q := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q));
  (φ : (a : S) → S) ζ = ζ ^ q
⊢ (φ : (a : S) → S) ζ = ζ ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))

Tactic:
set q := Nat.card (R ⧸ Q.under R)

Premises used: Nat.card, HasQuotient.Quotient, Ideal.under
-- 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 : IsDomain S
ζ : S
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hζ : HPow.hPow (β := ℕ) ζ 0 = 1
hk' : (↑0 : S) ∉ Q
⊢ (↑0 : S) ∈ Q

Tactic:
simp
-- 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 : IsDomain S
ζ : S
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hζ : HPow.hPow (β := ℕ) ζ 0 = 1
hk' : (↑0 : S) ∉ Q
⊢ False

Tactic:
exact hk' (by simp)