awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have this₁ : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
Tactic: have (j : _) : 1 - ζ ^ ((q + k - i) * j) ∈ Q := by
    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]
    exact 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
this_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
Tactic: have h₁ := sum_mem (t := Finset.range k) fun j _ ↦ this j
-- 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
this_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have h₂ : (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) * (ζ ^ (q + k - i) - 1) = (ζ ^ (q + k - i)) ^ k - 1
Tactic: have h₂ := geom_sum_mul (ζ ^ (q + k - i)) k
-- 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
this_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) * (ζ ^ (q + k - i) - 1) = (ζ ^ (q + k - i)) ^ k - 1
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have h₃ : Eq.{u_2 + 1} (α := S) (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) 0 ∨ ζ ^ (q + k - i) = 1
Tactic: rw [pow_right_comm, hζ.1, one_pow, sub_self, mul_eq_zero, sub_eq_zero] 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
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_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : Eq.{u_2 + 1} (α := S) (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) 0 ∨ ζ ^ (q + k - i) = 1
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have inl : ∀ (h₂ : Eq.{u_2 + 1} (α := S) (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) 0), (φ : (a : S) → S) ζ = ζ ^ q
Tactic: rcases h₂ with h₂ | 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
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_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : Eq.{u_2 + 1} (α := S) (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) 0 ∨ ζ ^ (q + k - i) = 1
inl : ∀ (h₂ : Eq.{u_2 + 1} (α := S) (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) 0), (φ : (a : S) → S) ζ = ζ ^ q
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have inr : ∀ (h₂ : ζ ^ (q + k - i) = 1), (φ : (a : S) → S) ζ = ζ ^ q
Tactic: rcases h₂ with h₂ | h₂
Cleared hypotheses: 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
this_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k - i) = 1
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have h₃ : ζ ^ (q + k - i) * ζ ^ i = 1 * ζ ^ i
Tactic: replace h₂ := congr($h₂ * ζ ^ i)
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
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_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k - i + i) = ζ ^ i
⊢ 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_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k - i + i) = ζ ^ i
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 (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
this_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ (q + k - i) * ζ ^ i = 1 * ζ ^ i
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have h₃ : ζ ^ q = ζ ^ i
Tactic: rw [one_mul, ← pow_add, tsub_add_cancel_of_le (by linarith), pow_add, hζ.1, mul_one] 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
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_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ q = ζ ^ i
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have inr : (φ : (a : S) → S) ζ = ζ ^ i
Tactic: rw [h₂, e]
-- 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_1 : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = (φ : (a : S) → S) ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ζ ^ q = ζ ^ i
inr : (φ : (a : S) → S) ζ = ζ ^ i
⊢ (φ : (a : S) → S) ζ = ζ ^ q
have inr₁ : Eq (α := S) ((φ : (a : S) → S) ζ : S) ((φ : (a : S) → S) ζ : S)
Tactic: rw [h₂, e]
-- 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
⊢ 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))
have e_α : Eq (α := Ideal R)
  (Ideal.comap (F := RingHom.{u_1, u_2} R (Localization.AtPrime Q)) (algebraMap R (Localization.AtPrime Q))
    (maximalIdeal (Localization.AtPrime Q)))
  (Ideal.under R Q)
Tactic: congr 2
-- 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
⊢ Eq (α := Ideal R)
    (Ideal.comap (F := RingHom.{u_1, u_2} R (Localization.AtPrime Q)) (algebraMap R (Localization.AtPrime Q))
      (maximalIdeal (Localization.AtPrime Q)))
    (Ideal.under R Q)
have e_α : Eq (α := Ideal R) (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q)))
  (Ideal.under R Q)
Tactic: rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]
-- 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
e_α :
  Eq (α := Ideal R) (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q)))
    (Ideal.under R Q)
⊢ Eq (α := Ideal R)
    (Ideal.comap (F := RingHom.{u_1, u_2} R (Localization.AtPrime Q)) (algebraMap R (Localization.AtPrime Q))
      (maximalIdeal (Localization.AtPrime Q)))
    (Ideal.under R Q)
have e_α₁ : Eq (α := Ideal R) (Ideal.under R (Ideal.under S (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q))))
  (Ideal.under R Q)
Tactic: rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]
-- 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
e_α :
  Eq (α := Ideal R) (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q)))
    (Ideal.under R Q)
e_α₁ :
  Eq (α := Ideal R)
    (Ideal.under R (Ideal.under S (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q))))
    (Ideal.under R Q)
⊢ Eq (α := Ideal R)
    (Ideal.comap (F := RingHom.{u_1, u_2} R (Localization.AtPrime Q)) (algebraMap R (Localization.AtPrime Q))
      (maximalIdeal (Localization.AtPrime Q)))
    (Ideal.under R Q)
have e_α₂ : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q)
Tactic: rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]
-- 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 : Q.IsPrime
⊢ IsArithFrobAt (S := Localization.AtPrime Q) H.localize (maximalIdeal (Localization.AtPrime Q))
have 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))
Tactic: have h : Nat.card (R ⧸ (maximalIdeal _).comap (algebraMap R (Localization.AtPrime Q))) =
      Nat.card (R ⧸ Q.under R) := by
    congr 2
    rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]
-- 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
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 : Localization.AtPrime Q
⊢ Membership.mem (γ := Ideal (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))
    (HSub.hSub (α := Localization.AtPrime Q)
      ((H.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q) x : Localization.AtPrime Q)
      (x ^
        Nat.card.{u_1}
          (HasQuotient.Quotient R (B := Ideal R)
            (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q))))))
have obtain : ∀ (x : S) (s : ↥Q.primeCompl),
  Membership.mem (γ := Ideal (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))
    ((H.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q)
        (IsLocalization.mk' (Localization.AtPrime Q) x s) -
      HPow.hPow (α := Localization.AtPrime Q) (IsLocalization.mk' (Localization.AtPrime Q) x s)
        (Nat.card.{u_1}
          (HasQuotient.Quotient R (B := Ideal R)
            (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q))))))
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq Q.primeCompl 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
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
⊢ Membership.mem (γ := Ideal (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))
    ((H.localize : (a : Localization.AtPrime Q) → Localization.AtPrime Q)
        (IsLocalization.mk' (Localization.AtPrime Q) x s) -
      HPow.hPow (α := Localization.AtPrime Q) (IsLocalization.mk' (Localization.AtPrime Q) x s)
        (Nat.card.{u_1}
          (HasQuotient.Quotient R (B := Ideal R)
            (Ideal.under.{u_1, u_2} R (B := Localization.AtPrime Q) (maximalIdeal (Localization.AtPrime Q))))))
have simp : Membership.mem (γ := Ideal (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))
  (HSub.hSub (α := Localization.AtPrime Q)
    (IsLocalization.mk' (R := S) (M := Q.primeCompl) (Localization.AtPrime Q) ((φ : (a : S) → S) x : S)
      (Subtype.mk (p := fun (x : S) ↦ x ∈ Q.primeCompl) ((φ : (a : S) → S) (↑s : S)) sorry : ↥Q.primeCompl))
    (IsLocalization.mk' (Localization.AtPrime Q)
      (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))
      (s ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))))
Tactic: simp only [localize, coe_mk, Localization.localRingHom_mk', RingHom.coe_coe, h,
    ← IsLocalization.mk'_pow]
-- 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
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
⊢ Membership.mem (γ := Ideal (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))
    (HSub.hSub (α := Localization.AtPrime Q)
      (IsLocalization.mk' (R := S) (M := Q.primeCompl) (Localization.AtPrime Q) ((φ : (a : S) → S) x : S)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ Q.primeCompl) ((φ : (a : S) → S) (↑s : S)) ⋯ : ↥Q.primeCompl))
      (IsLocalization.mk' (Localization.AtPrime Q)
        (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))
        (s ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))))
have rw : HMul.hMul (α := S) ((φ : (a : S) → S) x : S)
      (↑(s ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) : S) -
    HMul.hMul (β := S) (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q)))
      ((↑(Subtype.mk (p := fun (x : S) ↦ x ∈ Q.primeCompl) ((φ : (a : S) → S) (↑s : S)) sorry) : S) : S) ∈
  Q
Tactic: rw [← IsLocalization.mk'_sub,
    IsLocalization.AtPrime.mk'_mem_maximal_iff (Localization.AtPrime Q) 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
φ ψ : 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
have 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)))
Tactic: apply Algebra.FormallyUnramified.ext_of_iInf _
      (Ideal.iInf_pow_eq_bot_of_isLocalRing (maximalIdeal _) Ideal.IsPrime.ne_top')
-- 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
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)))
have rw : HPow.hPow (α :=
    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))
        x :
      HasQuotient.Quotient (Localization.AtPrime Q) (B := Ideal (Localization.AtPrime Q))
        (maximalIdeal (Localization.AtPrime Q)))
    (Nat.card.{u_1}
      (HasQuotient.Quotient R (B := Ideal R)
        (Ideal.under.{u_1, u_2} R (B := 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)
Tactic: rw [H.isArithFrobAt_localize.mk_apply, H'.isArithFrobAt_localize.mk_apply]
-- 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' : ψ.IsArithFrobAt Q
inst_3 : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst_4 : Algebra.IsUnramifiedAt R Q
inst_5 : IsNoetherianRing S
⊢ φ = ψ
have this : 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]
-- 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
⊢ φ = ψ
have H₁ : ∀ (x : S), Eq (α := S) ((φ : (a : S) → S) x : S) ((ψ : (a : S) → S) x : S)
Tactic: ext x