awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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 α))
⊢ x * y = y * x
have rw₂ : x * y =
  ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
    (HMul.hMul (α := FreeCommRing α) (β := FreeCommRing α)
      ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
      ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) y : FreeCommRing α))
Tactic: rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),
        (subsingletonEquivFreeCommRing α).map_mul, mul_comm,
        ← (subsingletonEquivFreeCommRing α).map_mul,
        (subsingletonEquivFreeCommRing α).symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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 α))
⊢ x * y = y * x
have rw₃ : x * y =
  ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
    ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) (x * y))
Tactic: rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),
        (subsingletonEquivFreeCommRing α).map_mul, mul_comm,
        ← (subsingletonEquivFreeCommRing α).map_mul,
        (subsingletonEquivFreeCommRing α).symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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))
⊢ x * y = y * x
have rw₄ : x * y = x * y
Tactic: rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),
        (subsingletonEquivFreeCommRing α).map_mul, mul_comm,
        ← (subsingletonEquivFreeCommRing α).map_mul,
        (subsingletonEquivFreeCommRing α).symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
⊢ 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 α ℤ))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
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))
⊢ 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 α ℤ))
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
⊢ 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 α))
have 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 α)
Tactic: ext
-- 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
x : S
⊢ (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)))
have 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
Tactic: rw [← map_pow, Ideal.Quotient.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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
⊢ _root_.Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
have by_contra! : ∀ (h : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))), False
Tactic: by_contra! h
-- 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
h : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
⊢ False
have H₁ : φ.IsArithFrobAt ⊤
Tactic: obtain rfl : Q = ⊤ := by simpa [Nat.card_eq_zero_of_infinite, ← Ideal.eq_top_iff_one] using H 0
Cleared hypotheses: Q, H, h
-- 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
φ : 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 ⊤
⊢ False
have h₁ : 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
Cleared hypotheses: Q, H, h
-- 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
φ : 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) ⊤))
⊢ False
have h₁ : Infinite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊤)
Tactic: simp only [Ideal.comap_top] at h
Cleared hypotheses: h
-- 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
x : HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)
⊢ 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
have obtain : ∀ (x : R),
  OneHom.toFun (↑(↑(Ideal.quotientMap Q (↑φ : S →+* S) sorry) : 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: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S ⧸ Q
⊢ (H.restrict : (a : S ⧸ Q) → S ⧸ Q) x = x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
have 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)))
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : Q.IsPrime
⊢ Function.Injective (α := S ⧸ Q) (β := S ⧸ Q) (⇑H.restrict : (a : S ⧸ Q) → S ⧸ Q)
have rw : ∀ (a : S ⧸ Q), Eq (α := S ⧸ Q) ((H.restrict : (a : S ⧸ Q) → S ⧸ Q) a : S ⧸ Q) (0 : S ⧸ Q) → a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- 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
inst_3 : Q.IsPrime
⊢ Ideal.comap φ Q = Q
have refine : ∀ (x : S) (hx : Membership.mem (γ := Submodule S S) (Ideal.comap φ Q) x), x ∈ Q
Tactic: refine le_antisymm (fun x hx ↦ ?_) H.le_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
φ : 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
⊢ x ∈ Q
have rwa : Eq (α := S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) x : S ⧸ Q) (0 : S ⧸ 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]
-- 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
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)
⊢ x ∈ Q
have 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)
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]
-- 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
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)
⊢ x ∈ Q
have 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)
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]
-- 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
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)
⊢ x ∈ Q
have rwa₃ : Eq (α := S ⧸ Q) ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) ((φ : (a : S) → S) x) : S ⧸ Q) (0 : S ⧸ 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]
-- 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
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)
⊢ x ∈ Q
have rwa₄ : Membership.mem (α := S) Q ((φ : (a : S) → S) x : S)
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]
-- 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ : ζ ^ m = 1
hk' : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have hm : m ≠ 0
Tactic: have hm : m ≠ 0 := by rintro rfl; exact hk' (by simp)
-- 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
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ : ζ ^ m = 1
hk' : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have obtain : ∀ (k : ℕ) (hk : k > 0) (hζ : IsPrimitiveRoot ζ k), (φ : (a : S) → S) ζ = ζ ^ q
Tactic: obtain ⟨k, hk, hζ⟩ := IsPrimitiveRoot.exists_pos hζ hm
-- 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk' : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have hk'₁ : (↑k : S) ∉ Q
Tactic: have hk' : ↑k ∉ Q := fun h ↦ hk' (Q.mem_of_dvd (Nat.cast_dvd_cast (hζ.2 m ‹_›)) h)
-- 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk'_1 : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : (↑k : S) ∉ Q
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have this : NeZero k
Tactic: have : NeZero k := ⟨hk.ne'⟩
-- 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
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk'_1 : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : (↑k : S) ∉ Q
this : NeZero k
⊢ HPow.hPow (α := S) ((φ : (a : S) → S) ζ : S) k = 1
have rw : Eq (α := S) ((φ : (a : S) → S) (ζ ^ k) : S) (1 : S)
Tactic: rw [← map_pow, hζ.1, map_one]
-- 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
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk'_1 : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : (↑k : S) ∉ Q
this : NeZero k
rw : Eq (α := S) ((φ : (a : S) → S) (ζ ^ k) : S) (1 : S)
⊢ HPow.hPow (α := S) ((φ : (a : S) → S) ζ : S) k = 1
have rw₁ : Eq (α := S) ((φ : (a : S) → S) 1 : S) (1 : S)
Tactic: rw [← map_pow, hζ.1, map_one]
-- 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
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk'_1 : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : (↑k : S) ∉ Q
this : NeZero k
rw : Eq (α := S) ((φ : (a : S) → S) (ζ ^ k) : S) (1 : S)
rw₁ : Eq (α := S) ((φ : (a : S) → S) 1 : S) (1 : S)
⊢ HPow.hPow (α := S) ((φ : (a : S) → S) ζ : S) k = 1
have rw₂ : Eq.{u_2 + 1} (α := S) 1 1
Tactic: rw [← map_pow, hζ.1, map_one]
-- 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
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk'_1 : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : (↑k : S) ∉ Q
this : NeZero k
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have obtain : ∀ (i : ℕ) (hi : i < k) (e : ζ ^ i = (φ : (a : S) → S) ζ), (φ : (a : S) → S) ζ = ζ ^ q
Tactic: obtain ⟨i, hi, e⟩ := hζ.eq_pow_of_pow_eq_one (ξ := φ ζ) (by rw [← map_pow, hζ.1, map_one])
-- 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
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk'_1 : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : (↑k : S) ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
j : ℕ
⊢ i ≤ q + k
have linarith : q + k < i →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑q : ℤ) + (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 - (↑k : ℤ)) +
      (HAdd.hAdd (α := ℤ) (↑q : ℤ) (↑k : ℤ) + 1 - (↑i : ℤ)) =
    0
Tactic: linarith
-- 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
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk'_1 : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : (↑k : S) ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
j : ℕ
linarith :
  q + k < i →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑q : ℤ) + (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 - (↑k : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑q : ℤ) (↑k : ℤ) + 1 - (↑i : ℤ)) =
      0
⊢ i ≤ q + k
have linarith₁ : q + k < i → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- 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
inst_3 : IsDomain S
ζ : S
m : ℕ
hζ_1 : ζ ^ m = 1
hk'_1 : (↑m : S) ∉ Q
q : ℕ := Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : (↑k : S) ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
j : ℕ
⊢ 1 - ζ ^ ((q + k - i) * j) ∈ Q
have rw : HSub.hSub (α := S) ((φ : (a : S) → S) (ζ ^ j) : S) ((ζ ^ j) ^ q) ∈ Q
Tactic: rw [← Ideal.mul_unit_mem_iff_mem _ ((hζ.isUnit NeZero.out).pow (i * j)),
      sub_mul, one_mul, ← pow_add, ← add_mul, tsub_add_cancel_of_le (by linarith), add_mul,
        pow_add, pow_mul _ k, hζ.1, one_pow, mul_one, pow_mul, e, ← map_pow, mul_comm, pow_mul]