awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Ring K
inst_4 : Algebra F K
e : K ≃ₐ[F] E
inst_5 : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u_1, u_2} (R := F) (algebraMap F E)) x
have h₁ : Separable (minpoly.{u_1, u_3} F (B := K) ((e.symm : (a : E) → K) x : K))
Tactic: rw [IsSeparable, ← minpoly.algEquiv_eq e.symm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : Ring E
inst_2 : Algebra F E
L : Subalgebra F E
inst_3 : IsPurelyInseparable.{u_1, u_2} F ↥L
inst_4 : Algebra.IsSeparable.{u_1, u_2} F ↥L
x : E
hx : x ∈ L
⊢ Membership.mem (γ := Subalgebra F E) ⊥ x
have obtain : ∀ (y : F) (hy : (algebraMap F ↥L : (a : F) → ↥L) y = Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx),
  Membership.mem (γ := Subalgebra F E) ⊥ x
Tactic: obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
inst_3 : IsPurelyInseparable.{u, v} F ↥L
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
x : E
hx : x ∈ L
⊢ Membership.mem (γ := IntermediateField F E) ⊥ x
have obtain : ∀ (y : F) (hy : (algebraMap F ↥L : (a : F) → ↥L) y = Subtype.mk (p := fun (x : E) ↦ x ∈ L) x hx),
  Membership.mem (γ := IntermediateField F E) ⊥ x
Tactic: obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
⊢ IsPurelyInseparable F E ↔
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have rw : (∀ (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)) ↔
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
Tactic: rw [isPurelyInseparable_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
⊢ (∀ (x : E),
      IsIntegral F x ∧
        (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)) ↔
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have refine_1 : ∀
  (h :
    ∀ (x : E),
      IsIntegral F x ∧
        (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x))
  (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
Tactic: refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
refine_1 :
  ∀
    (h :
      ∀ (x : E),
        IsIntegral F x ∧
          (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x))
    (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
⊢ (∀ (x : E),
      IsIntegral F x ∧
        (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)) ↔
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have refine_2 : ∀
  (h :
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n))
  (x : E),
  IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
Tactic: refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h :
  ∀ (x : E),
    IsIntegral F x ∧
      (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
x : E
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
have refine_1 : ∀ (g : F[X]) (h1 : g.Separable) (n : ℕ)
  (h2 : Eq (α := F[X]) ((expand F (q ^ n) : (a : F[X]) → F[X]) g : F[X]) (minpoly F x : F[X])),
  ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
Tactic: obtain ⟨g, h1, n, h2⟩ := (minpoly.irreducible (h x).1).hasSeparableContraction q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
⊢ IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
have hdeg : natSepDegree (minpoly F x) = 1
Tactic: have hdeg := (minpoly.natSepDegree_eq_one_iff_pow_mem q).2 (h x)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
⊢ IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
have halg : IsIntegral F x
Tactic: have halg : IsIntegral F x := by_contra fun h' ↦ by
    simp only [minpoly.eq_zero h', natSepDegree_zero, zero_ne_one] at hdeg
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
halg : IsIntegral F x
⊢ IsIntegral F x ∧
    (IsSeparable F x → Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x)
have refine_2 : ∀ (hsep : IsSeparable F x), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
Tactic: refine ⟨halg, fun hsep ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
halg : IsIntegral F x
hsep : IsSeparable F x
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
have refine_2 : ∀ (hdeg : natDegree (minpoly F x) = 1) (halg : IsIntegral F x) (hsep : IsSeparable F x),
  Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
Tactic: rwa [hsep.natSepDegree_eq_natDegree, minpoly.natDegree_eq_one_iff] at hdeg
Cleared hypotheses: hdeg, halg, hsep
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
halg : IsIntegral F x
hsep : IsSeparable F x
refine_2 :
  ∀ (hdeg : natDegree (minpoly F x) = 1) (halg : IsIntegral F x) (hsep : IsSeparable F x),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
have refine_2₁ : ∀ (hdeg : Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x) (halg : IsIntegral F x)
  (hsep : IsSeparable F x), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
Tactic: rwa [hsep.natSepDegree_eq_natDegree, minpoly.natDegree_eq_one_iff] at hdeg
Cleared hypotheses: hdeg, halg, hsep
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
⊢ IsPurelyInseparable F E
have refine : ∀ (x : E) (h : IsSeparable F x), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
Tactic: refine ⟨⟨fun x ↦ (isIntegral' F (algebraMap E K x)).tower_bot_of_field⟩, fun x h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
have h₁ : Separable (minpoly.{u, w} F (B := K) ((algebraMap E K : (a : E) → K) x : K))
Tactic: rw [IsSeparable, ← minpoly.algebraMap_eq (algebraMap E K).injective] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
x : E
h : Separable (minpoly.{u, w} F (B := K) ((algebraMap E K : (a : E) → K) x : K))
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
have obtain : ∀ (y : F)
  (h : Eq.{w + 1} (α := K) (((algebraMap F K : F →+* K) : (a : F) → K) y : K) ((algebraMap E K : (a : E) → K) x : K)),
  Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
Tactic: obtain ⟨y, h⟩ := inseparable F _ h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : IsPurelyInseparable F K
⊢ IsPurelyInseparable E K
have obtain : ∀ (q : ℕ), ExpChar F q → IsPurelyInseparable E K
Tactic: obtain ⟨q, _⟩ := ExpChar.exists F
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : IsPurelyInseparable F K
q : ℕ
h_1 : ExpChar F q
⊢ IsPurelyInseparable E K
have this : ExpChar E q
Tactic: haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : IsPurelyInseparable F K
q : ℕ
h_1 : ExpChar F q
this : ExpChar E q
⊢ IsPurelyInseparable E K
have rw : ∀
  (h :
    ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)),
  ExpChar F q →
    ∀ (this : ExpChar E q) (x : K),
      ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
Tactic: rw [isPurelyInseparable_iff_pow_mem _ q] at h ⊢
Cleared hypotheses: h, h_1, this
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h : ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
h_1 : ExpChar F q
this : ExpChar E q
x : K
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
have obtain : ∀ (n : ℕ) (y : F) (h : ((algebraMap F K : F →+* K) : (a : F) → K) y = x ^ q ^ n),
  ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
Tactic: obtain ⟨n, y, h⟩ := h x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
⊢ IsPurelyInseparable F K
have obtain : ∀ (q : ℕ), ExpChar F q → IsPurelyInseparable F K
Tactic: obtain ⟨q, _⟩ := ExpChar.exists F
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
q : ℕ
h : ExpChar F q
⊢ IsPurelyInseparable F K
have this : ExpChar E q
Tactic: haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
q : ℕ
h : ExpChar F q
this : ExpChar E q
⊢ IsPurelyInseparable F K
have rw : ∀
  (h2 :
    ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n))
  (h1 :
    ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)),
  ExpChar F q →
    ∀ (this : ExpChar E q) (x : K),
      ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
Tactic: rw [isPurelyInseparable_iff_pow_mem _ q] at h1 h2 ⊢
Cleared hypotheses: h1, h2, h, this
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2 : ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1 : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
have obtain : ∀ (n : ℕ) (y : E) (h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n),
  ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
Tactic: obtain ⟨n, y, h2⟩ := h2 x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1 : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
have obtain : ∀ (m : ℕ) (z : F) (h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m),
  ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
Tactic: obtain ⟨m, z, h1⟩ := h1 y
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
have refine : ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)
Tactic: refine ⟨n + m, z, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
⊢ ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)
have rw : (algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) z : E) = x ^ q ^ (n + m)
Tactic: rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
rw : (algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) z : E) = x ^ q ^ (n + m)
⊢ ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)
have rw₁ : (algebraMap E K : (a : E) → K) (y ^ q ^ m) = x ^ q ^ (n + m)
Tactic: rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
rw : (algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) z : E) = x ^ q ^ (n + m)
rw₁ : (algebraMap E K : (a : E) → K) (y ^ q ^ m) = x ^ q ^ (n + m)
⊢ ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)
have rw₂ : HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ m) = x ^ q ^ (n + m)
Tactic: rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
rw : (algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) z : E) = x ^ q ^ (n + m)
rw₁ : (algebraMap E K : (a : E) → K) (y ^ q ^ m) = x ^ q ^ (n + m)
rw₂ : HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ m) = x ^ q ^ (n + m)
⊢ ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)
have rw₃ : (x ^ q ^ n) ^ q ^ m = x ^ q ^ (n + m)
Tactic: rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
rw : (algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) z : E) = x ^ q ^ (n + m)
rw₁ : (algebraMap E K : (a : E) → K) (y ^ q ^ m) = x ^ q ^ (n + m)
rw₂ : HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ m) = x ^ q ^ (n + m)
rw₃ : (x ^ q ^ n) ^ q ^ m = x ^ q ^ (n + m)
⊢ ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)
have rw₄ : x ^ (q ^ n * q ^ m) = x ^ q ^ (n + m)
Tactic: rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
rw : (algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) z : E) = x ^ q ^ (n + m)
rw₁ : (algebraMap E K : (a : E) → K) (y ^ q ^ m) = x ^ q ^ (n + m)
rw₂ : HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ m) = x ^ q ^ (n + m)
rw₃ : (x ^ q ^ n) ^ q ^ m = x ^ q ^ (n + m)
rw₄ : x ^ (q ^ n * q ^ m) = x ^ q ^ (n + m)
⊢ ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)
have rw₅ : x ^ q ^ (n + m) = x ^ q ^ (n + m)
Tactic: rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]