awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
zero : ∀ [CharZero K], ExpChar K 1 → elemExponent K a ≤ n
prime : ∀ (hp : Nat.Prime p) [CharP K p], elemExponent K a ≤ n
⊢ elemExponent K a ≤ n

Tactic:
rcases ‹ExpChar K p› with _ | ⟨hp⟩

Premises used: ExpChar
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
inst_4 : CharZero K
h_1 : ExpChar K 1
⊢ elemExponent K a ≤ n

Tactic:
elemExponent_eq_zero_of_charZero K a ▸ Nat.zero_le _

Premises used: Nat.zero_le, Eq.rec, IsPurelyInseparable.elemExponent_eq_zero_of_charZero, Eq.symm
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
inst_4 : CharZero K
h_1 : ExpChar K 1
⊢ elemExponent K a ≤ n

Tactic:
exact elemExponent_eq_zero_of_charZero K a ▸ Nat.zero_le _
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
prime : ∀ (y : K) (hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n), elemExponent K a ≤ n
⊢ elemExponent K a ≤ n

Tactic:
obtain ⟨y, hy⟩ := RingHom.mem_range.mp <| h

Premises used: RingHom.mem_range, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
rwa :
  HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
      ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) y : K[X]) : L) =
    0
rwa₁ :
  HSub.hSub (α := L) (β := L) ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) : L)
      ((algebraMap K L : (a : K) → L) y : L) =
    0
rwa₂ : HSub.hSub (β := L) (a ^ ringExpChar K ^ n) ((algebraMap K L : (a : K) → L) y : L) = 0
rwa₃ : a ^ ringExpChar K ^ n = (algebraMap K L : (a : K) → L) y
rwa₄ rwa₅ rwa₆ rwa₇ : (algebraMap K L : (a : K) → L) y = a ^ ringExpChar K ^ n
⊢ Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)

Tactic:
rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]

Premises used: map_sub, sub_eq_zero, Polynomial.aeval_X_pow, eq_comm, Polynomial.aeval_C
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
⊢ Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)

Tactic:
have hf₁ : f.aeval a = 0 := by rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
hf₁ : Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
⊢ f.Monic

Tactic:
have hf₂ : f.Monic := monic_X_pow_sub_C y <| Nat.pos_iff_ne_zero.mp <| expChar_pow_pos K _ _
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
hf₁ : Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hf₂ : f.Monic
rw : (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)).natDegree = ringExpChar K ^ n
rw₁ : ringExpChar K ^ n * natDegree.{u_2} (R := K) X = ringExpChar K ^ n
rw₂ : ringExpChar K ^ n * 1 = ringExpChar K ^ n
rw₃ rw₄ : ringExpChar K ^ n = ringExpChar K ^ n
⊢ f.natDegree = ringExpChar K ^ n

Tactic:
rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]

Premises used: Polynomial.natDegree_X, Polynomial.natDegree_pow, Polynomial.natDegree_sub_C, mul_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
hf₁ : Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hf₂ : f.Monic
⊢ f.natDegree = ringExpChar K ^ n

Tactic:
have hf₃ : f.natDegree = ringExpChar K ^ n := by
      rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
hf₁ : Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hf₂ : f.Monic
hf₃ : f.natDegree = ringExpChar K ^ n
⊢ elemExponent K a ≤ n

Tactic:
(Nat.pow_le_pow_iff_right <| Nat.Prime.one_lt hp).mp <|
      ringExpChar.eq K p ▸ hf₃ ▸ minpoly_natDegree_eq K a ▸
      natDegree_le_natDegree (minpoly.min K a hf₂ hf₁)

Premises used: ringExpChar.eq, Polynomial.natDegree_le_natDegree, Nat.Prime.one_lt, Eq.rec, IsPurelyInseparable.minpoly_natDegree_eq, minpoly.min, Iff.mp, Nat.pow_le_pow_iff_right
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
p : ℕ
h_1 : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a ^ ringExpChar K ^ n
f : K[X] := HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ n)) ((C : (a : K) → K[X]) y : K[X])
hf₁ : Eq.{u_3 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hf₂ : f.Monic
hf₃ : f.natDegree = ringExpChar K ^ n
⊢ elemExponent K a ≤ n

Tactic:
exact (Nat.pow_le_pow_iff_right <| Nat.Prime.one_lt hp).mp <|
      ringExpChar.eq K p ▸ hf₃ ▸ minpoly_natDegree_eq K a ▸
      natDegree_le_natDegree (minpoly.min K a hf₂ hf₁)

Premises used: Nat.Prime.one_lt, Iff.mp, Nat.pow_le_pow_iff_right
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
p : ℕ
inst_4 : ExpChar K p
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ p ^ n)
⊢ elemExponent K a ≤ n

Tactic:
elemExponent_le_of_pow_mem (ringExpChar.eq K p ▸ h)

Premises used: ringExpChar.eq, IsPurelyInseparable.elemExponent_le_of_pow_mem, Eq.rec, Eq.symm
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : n < elemExponent K a
⊢ a ^ ringExpChar K ^ n ∉ RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)

Tactic:
fun hn ↦ (Nat.not_lt_of_ge <| elemExponent_le_of_pow_mem hn) h

Premises used: IsPurelyInseparable.elemExponent_le_of_pow_mem, Nat.not_lt_of_ge, Not
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
p : ℕ
inst_4 : ExpChar K p
a : L
n : ℕ
h : n < elemExponent K a
⊢ a ^ p ^ n ∉ RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)

Tactic:
ringExpChar.eq K p ▸ elemExponent_min h

Premises used: ringExpChar.eq, IsPurelyInseparable.elemExponent_min, Eq.rec
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : HasExponent K L
a : L
⊢ elemExponent K a ≤ exponent K L

Tactic:
elemExponent_le_of_pow_mem <| exponent_def K a

Premises used: IsPurelyInseparable.elemExponent_le_of_pow_mem, IsPurelyInseparable.exponent_def
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
let : ∀ (p : ℕ), ExpChar K p → HasExponent K L
⊢ HasExponent K L

Tactic:
let ⟨p, _⟩ := ExpChar.exists K
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
zero : ∀ [CharZero K], ExpChar K 1 → HasExponent K L
prime : ∀ (hp : Nat.Prime p) [CharP K p], HasExponent K L
⊢ HasExponent K L

Tactic:
rcases ‹ExpChar K p› with _ | ⟨hp⟩

Premises used: ExpChar
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
inst_5 : CharZero K
h : ExpChar K 1
⊢ HasExponent K L

Tactic:
⟨0, fun a ↦ surjective_algebraMap_of_isSeparable K L _⟩

Premises used: ringExpChar, IsPurelyInseparable.surjective_algebraMap_of_isSeparable, IsPurelyInseparable.HasExponent.mk, HPow.hPow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
inst_5 : CharZero K
h : ExpChar K 1
⊢ HasExponent K L

Tactic:
exact ⟨0, fun a ↦ surjective_algebraMap_of_isSeparable K L _⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
⊢ HasExponent K L

Tactic:
⟨e, fun a ↦ ⟨elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a), ?_⟩⟩

Premises used: ringExpChar, HSub.hSub, IsPurelyInseparable.HasExponent.mk, IsPurelyInseparable.elemReduct, IsPurelyInseparable.elemExponent, HPow.hPow, Exists.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
prime :
  ∀ (a : L),
    ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
      a ^ ringExpChar K ^ e
⊢ HasExponent K L

Tactic:
refine ⟨e, fun a ↦ ⟨elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a), ?_⟩⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
⊢ ∀ (a : L), elemExponent K a ≤ e

Tactic:
have h_elemexp_bound (a : L) : elemExponent K a ≤ e :=
      Nat.le_log_of_pow_le (Nat.Prime.one_lt <| ringExpChar.eq K p ▸ hp)
        (minpoly_natDegree_eq K a ▸ minpoly.natDegree_le a)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
inst_4 : FiniteDimensional K L
p : ℕ
h : ExpChar K p
hp : Nat.Prime p
hchar : CharP K p
e : ℕ := Nat.log (ringExpChar K) (Module.finrank K L)
a : L
h_elemexp_bound : ∀ (a : L), elemExponent K a ≤ e
prime :
  HPow.hPow (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a) : L)
      (ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e
prime₁ : (a ^ ringExpChar K ^ elemExponent K a) ^ ringExpChar K ^ (e - elemExponent K a) = a ^ ringExpChar K ^ e
prime₂ : a ^ (ringExpChar K ^ elemExponent K a * ringExpChar K ^ (e - elemExponent K a)) = a ^ ringExpChar K ^ e
prime₃ : a ^ ringExpChar K ^ (elemExponent K a + (e - elemExponent K a)) = a ^ ringExpChar K ^ e
prime₄ prime₅ : a ^ ringExpChar K ^ e = a ^ ringExpChar K ^ e
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (elemReduct K a ^ ringExpChar K ^ (e - elemExponent K a)) =
    a ^ ringExpChar K ^ e

Tactic:
rw [map_pow, algebraMap_elemReduct_eq, ← pow_mul, ← pow_add,
      Nat.add_sub_cancel' (h_elemexp_bound a)]

Premises used: pow_add, map_pow, pow_mul, IsPurelyInseparable.algebraMap_elemReduct_eq, Nat.add_sub_cancel'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : L
rw : (algebraMap K L : (a : K) → L) (elemReduct K a ^ p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₁ : HPow.hPow (α := L) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) (p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₂ : (a ^ p ^ elemExponent K a) ^ p ^ (n - elemExponent K a) = a ^ p ^ n
rw₃ : a ^ (p ^ elemExponent K a * p ^ (n - elemExponent K a)) = a ^ p ^ n
rw₄ : a ^ p ^ (elemExponent K a + (n - elemExponent K a)) = a ^ p ^ n
rw₅ rw₆ : a ^ p ^ n = a ^ p ^ n
⊢ (algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) = a ^ p ^ n

Tactic:
rw [iterateFrobeniusAux, map_pow, algebraMap_elemReduct_eq' K p, ← pow_mul, ← pow_add,
    Nat.add_sub_cancel' <| (elemExponent_le_exponent K a).trans hn]

Premises used: pow_add, map_pow, pow_mul, IsPurelyInseparable.algebraMap_elemReduct_eq', IsPurelyInseparable.elemExponent_le_exponent, LE.le.trans, Nat.add_sub_cancel', _private.0.IsPurelyInseparable.iterateFrobeniusAux
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a :
  Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 1 : L)
⊢ iterateFrobeniusAux K L p n 1 = 1

Tactic:
apply (algebraMap K L).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L) (1 : L)
a₁ : HPow.hPow (α := L) 1 (p ^ n) = 1
a₂ a₃ : Eq.{u_3 + 1} (α := L) 1 1
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 1) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 1 : L)

Tactic:
rw [(algebraMap K L).map_one,
      algebraMap_iterateFrobeniusAux K p hn 1,
      one_pow]

Premises used: one_pow, Algebra.algebraMap, RingHom.map_one, _private.0.IsPurelyInseparable.algebraMap_iterateFrobeniusAux, OfNat.ofNat
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
a₁ :
  Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a * iterateFrobeniusAux K L p n b) : L)
⊢ iterateFrobeniusAux K L p n (a * b) = iterateFrobeniusAux K L p n a * iterateFrobeniusAux K L p n b

Tactic:
apply (algebraMap K L).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
a₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n a) : L)
      ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
a₂ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) =
    HMul.hMul (β := L) (a ^ p ^ n) ((algebraMap K L : (a : K) → L) (iterateFrobeniusAux K L p n b) : L)
a₃ : ((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) = a ^ p ^ n * b ^ p ^ n
a₄ : (a * b) ^ p ^ n = a ^ p ^ n * b ^ p ^ n
a₅ a₆ : a ^ p ^ n * b ^ p ^ n = a ^ p ^ n * b ^ p ^ n
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a * b)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a * iterateFrobeniusAux K L p n b) : L)

Tactic:
rw [(algebraMap K L).map_mul,
      algebraMap_iterateFrobeniusAux K p hn a,
      algebraMap_iterateFrobeniusAux K p hn b,
      algebraMap_iterateFrobeniusAux K p hn (a * b),
      mul_pow]

Premises used: HMul.hMul, Algebra.algebraMap, _private.0.IsPurelyInseparable.algebraMap_iterateFrobeniusAux, RingHom.map_mul, mul_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a :
  Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 0) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 0 : L)
⊢ iterateFrobeniusAux K L p n 0 = 0

Tactic:
apply (algebraMap K L).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a : p ^ n ≠ 0
⊢ Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n 0) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 0 : L)

Tactic:
rw [(algebraMap K L).map_zero,
      algebraMap_iterateFrobeniusAux K p hn 0,
      zero_pow]

Premises used: Algebra.algebraMap, RingHom.map_zero, _private.0.IsPurelyInseparable.algebraMap_iterateFrobeniusAux, OfNat.ofNat, zero_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
⊢ p ^ n ≠ 0

Tactic:
Nat.pos_iff_ne_zero.mp <| expChar_pow_pos K p n

Premises used: Nat.pos_iff_ne_zero, expChar_pow_pos, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
⊢ p ^ n ≠ 0

Tactic:
exact Nat.pos_iff_ne_zero.mp <| expChar_pow_pos K p n

Premises used: Nat.pos_iff_ne_zero, expChar_pow_pos, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)

Tactic:
have inj := (algebraMap K L).injective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
⊢ ExpChar L p

Tactic:
have : ExpChar L p := expChar_of_injective_ringHom inj p
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
a b : L
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := K) (β := L) (⇑(algebraMap K L : K →+* L) : (a : K) → L)
this : ExpChar L p
a₁ :
  Eq.{u_3 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n (a + b)) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) (iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b) : L)
⊢ iterateFrobeniusAux K L p n (a + b) = iterateFrobeniusAux K L p n a + iterateFrobeniusAux K L p n b

Tactic:
apply inj