awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : 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))
⊢ m ≠ 0

Tactic:
have hm : m ≠ 0 := by rintro rfl; exact hk' (by 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
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
obtain : ∀ (k : ℕ) (hk : k > 0) (hζ : IsPrimitiveRoot ζ k), (φ : (a : S) → S) ζ = ζ ^ q
⊢ (φ : (a : S) → S) ζ = ζ ^ q

Tactic:
obtain ⟨k, hk, hζ⟩ := IsPrimitiveRoot.exists_pos hζ hm

Premises used: IsPrimitiveRoot.exists_pos
-- 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ζ_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
⊢ (↑k : S) ∉ Q

Tactic:
have hk' : ↑k ∉ Q := fun h ↦ hk' (Q.mem_of_dvd (Nat.cast_dvd_cast (hζ.2 m ‹_›)) 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
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
⊢ NeZero k

Tactic:
have : NeZero k := ⟨hk.ne'⟩
-- 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ζ_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)
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) 1 1
⊢ HPow.hPow (α := S) ((φ : (a : S) → S) ζ : S) k = 1

Tactic:
rw [← map_pow, hζ.1, map_one]

Premises used: map_pow, map_one, IsPrimitiveRoot.pow_eq_one
-- 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ζ_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
obtain : ∀ (i : ℕ) (hi : i < k) (e : ζ ^ i = (φ : (a : S) → S) ζ), (φ : (a : S) → S) ζ = ζ ^ q
⊢ (φ : (a : S) → S) ζ = ζ ^ q

Tactic:
obtain ⟨i, hi, e⟩ := hζ.eq_pow_of_pow_eq_one (ξ := φ ζ) (by rw [← map_pow, hζ.1, map_one])

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one
-- 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ζ_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
linarith₁ : q + k < i → GT.gt (α := ℤ) 2 0
⊢ i ≤ q + k

Tactic:
linarith
-- 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ζ_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 : ℕ
rw : HSub.hSub (α := S) ((φ : (a : S) → S) (ζ ^ j) : S) ((ζ ^ j) ^ q) ∈ Q
⊢ 1 - ζ ^ ((q + k - i) * j) ∈ 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]

Premises used: one_pow, add_mul, HMul.hMul, pow_add, tsub_add_cancel_of_le, IsPrimitiveRoot.isUnit, map_pow, IsUnit.pow, pow_mul, sub_mul, Ideal.mul_unit_mem_iff_mem, NeZero.out, mul_comm, mul_one, IsPrimitiveRoot.pow_eq_one, one_mul
-- 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ζ_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 : ℕ
⊢ HSub.hSub (α := S) ((φ : (a : S) → S) (ζ ^ j) : S) ((ζ ^ j) ^ q) ∈ Q

Tactic:
H _

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
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 : ℕ
⊢ HSub.hSub (α := S) ((φ : (a : S) → S) (ζ ^ j) : S) ((ζ ^ j) ^ q) ∈ Q

Tactic:
exact 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
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

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 _
-- 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ζ_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
⊢ ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q

Tactic:
have h₁ := sum_mem (t := Finset.range k) fun j _ ↦ this j
-- 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ζ_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
⊢ (∑ 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
-- 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ζ_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
⊢ 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₂

Premises used: one_pow, sub_self, pow_right_comm, sub_eq_zero, mul_eq_zero, IsPrimitiveRoot.pow_eq_one
-- 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ζ_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
inr : ∀ (h₂ : ζ ^ (q + k - i) = 1), (φ : (a : S) → S) ζ = ζ ^ q
⊢ (φ : (a : S) → S) ζ = ζ ^ q

Tactic:
rcases h₂ with h₂ | 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
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
⊢ (φ : (a : S) → S) ζ = ζ ^ q

Tactic:
simp [h₂, pow_mul, hk'] at h₁

Premises used: pow_mul
-- 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ζ_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
⊢ ζ ^ (q + k - i) * ζ ^ i = 1 * ζ ^ i

Tactic:
replace h₂ := congr($h₂ * ζ ^ i)
-- 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ζ_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
linarith₁ : q + k < i → GT.gt (α := ℤ) 2 0
⊢ i ≤ q + k

Tactic:
linarith
-- 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ζ_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
⊢ ζ ^ q = ζ ^ i

Tactic:
rw [one_mul, ← pow_add, tsub_add_cancel_of_le (by linarith), pow_add, hζ.1, mul_one] at h₂

Premises used: pow_add, tsub_add_cancel_of_le, mul_one, IsPrimitiveRoot.pow_eq_one, one_mul
-- 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ζ_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
inr₁ inr₂ : Eq (α := S) ((φ : (a : S) → S) ζ : S) ((φ : (a : S) → S) ζ : S)
⊢ (φ : (a : S) → S) ζ = ζ ^ q

Tactic:
rw [h₂, e]
-- 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 : R
⊢ Eq (α := Localization.AtPrime Q)
    (OneHom.toFun (M := Localization.AtPrime Q)
      (↑(↑(Localization.localRingHom Q Q (↑φ : S →+* S) ⋯) : Localization.AtPrime Q →* Localization.AtPrime Q) :
        OneHom (Localization.AtPrime Q) (Localization.AtPrime Q))
      ((algebraMap R (Localization.AtPrime Q) : (a : R) → Localization.AtPrime Q) x))
    ((algebraMap R (Localization.AtPrime Q) : (a : R) → Localization.AtPrime Q) x)

Tactic:
simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime Q),
      Localization.localRingHom_to_map]

Premises used: Localization.localRingHom_to_map, Localization.AtPrime, IsScalarTower.algebraMap_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
x : S
⊢ 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:
Localization.localRingHom_to_map _ _ _ H.comap_eq.symm _

Premises used: Localization.localRingHom_to_map, AlgHom.IsArithFrobAt.comap_eq, Eq.symm
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : Q.IsPrime
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)
⊢ 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:
congr 2
-- 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
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)
e_α₂ e_α₃ : Eq (α := Ideal R) (Ideal.under R 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)

Tactic:
rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]

Premises used: Ideal.under_under, Localization.AtPrime.under_maximalIdeal, Ideal.under_def
-- 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
⊢ 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]
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : Q.IsPrime
h :
  Nat.card.{u_1}
      (HasQuotient.Quotient R (B := Ideal R)
        (Ideal.comap (F := RingHom.{u_1, u_2} R (Localization.AtPrime Q)) (algebraMap R (Localization.AtPrime Q))
          (maximalIdeal (Localization.AtPrime Q)))) =
    Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
x : Localization.AtPrime Q
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))))))
⊢ 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))))))

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq Q.primeCompl x

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_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
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
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)) ⋯ : ↥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)))))
⊢ 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:
simp only [localize, coe_mk, Localization.localRingHom_mk', RingHom.coe_coe, h,
    ← IsLocalization.mk'_pow]

Premises used: IsLocalization.mk'_pow, AlgHom.coe_mk, Localization.localRingHom_mk', RingHom.coe_coe, AlgHom.IsArithFrobAt.localize
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst_3 : Q.IsPrime
h :
  Nat.card.{u_1}
      (HasQuotient.Quotient R (B := Ideal R)
        (Ideal.comap (F := RingHom.{u_1, u_2} R (Localization.AtPrime Q)) (algebraMap R (Localization.AtPrime Q))
          (maximalIdeal (Localization.AtPrime Q)))) =
    Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))
x : S
s : ↥Q.primeCompl
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)) ⋯) : S) : S) ∈
    Q
⊢ 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)))))

Tactic:
rw [← IsLocalization.mk'_sub,
    IsLocalization.AtPrime.mk'_mem_maximal_iff (Localization.AtPrime Q) Q]

Premises used: IsLocalization.AtPrime.mk'_mem_maximal_iff, Localization.AtPrime, IsLocalization.mk'_sub, IsLocalization.AtPrime.isLocalRing