awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
H : Ne (α := Subring D) k ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : Ne (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) b : D) (0 : D)
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
x : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq :
  a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    c
eq1 :
  c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      c⁻¹ * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    1
deq : d = 1 + a⁻¹ * d * a
r : ℕ
hr : Membership.mem (γ := Subring D) k (d ^ p ^ r)
⊢ d ^ p ^ r = (1 + a⁻¹ * d * a) ^ p ^ r

Tactic:
apply_fun (· ^ (p ^ r)) at deq

Premises used: HPow.hPow
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
H : Ne (α := Subring D) k ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : Ne (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) b : D) (0 : D)
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
x : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq :
  a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    c
eq1 :
  c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      c⁻¹ * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    1
r : ℕ
hr : Membership.mem (γ := Subring D) k (d ^ p ^ r)
deq : d ^ p ^ r = (1 + a⁻¹ * d * a) ^ p ^ r
⊢ Eq.{u_1 + 1} (α := D) 1 0

Tactic:
rw [add_pow_expChar_pow_of_commute p r (Commute.one_left _), one_pow,
    GroupWithZero.conj_pow₀ ha₀, ← hr.comm, mul_assoc, inv_mul_cancel₀ ha₀, mul_one,
    right_eq_add] at deq

Premises used: one_pow, add_pow_expChar_pow_of_commute, GroupWithZero.conj_pow₀, mul_assoc, IsMulCentral.comm, mul_one, right_eq_add, inv_mul_cancel₀
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
H : Ne (α := Subring D) k ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : Ne (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) b : D) (0 : D)
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
x : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq :
  a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    c
eq1 :
  c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      c⁻¹ * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    1
r : ℕ
hr : Membership.mem (γ := Subring D) k (d ^ p ^ r)
deq : Eq.{u_1 + 1} (α := D) 1 0
⊢ False

Tactic:
one_ne_zero deq

Premises used: one_ne_zero
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
H : Ne (α := Subring D) k ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : Ne (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) b : D) (0 : D)
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
x : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq :
  a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    c
eq1 :
  c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      c⁻¹ * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    1
r : ℕ
hr : Membership.mem (γ := Subring D) k (d ^ p ^ r)
deq : Eq.{u_1 + 1} (α := D) 1 0
⊢ False

Tactic:
exact one_ne_zero deq

Premises used: one_ne_zero
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
⊢ Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥

Tactic:
have hcenter : Subalgebra.center L D = ⊥ := le_bot_iff.mp IsCentral.out
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
⊢ Ne (α := Subring D) k ⊤

Tactic:
have ntrivial : Subring.center D ≠ ⊤ :=
    congr(Subalgebra.toSubring $hcenter).trans_ne (Subalgebra.toSubring_injective.ne hneq)
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_1 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
⊢ IsScalarTower L (↥k) D

Tactic:
have _ : IsScalarTower L (center D) D := .of_algebraMap_eq fun _ ↦ rfl
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x_1 : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_2 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
x : ↥k
rw :
  Eq (α := D) ((algebraMap (↥k) D : (a : ↥k) → D) x : D)
    ((algebraMap (↥k) D : (a : ↥k) → D) ((algebraMap L ↥k : (a : L) → ↥k) ((algebraMap (↥k) L : (a : ↥k) → L) x) : ↥k) :
      D)
⊢ Eq (α := D) ((algebraMap (↥k) D : (a : ↥k) → D) x : D)
    ((algebraMap L D : (a : L) → D) ((algebraMap (↥k) L : (a : ↥k) → L) x : L) : D)

Tactic:
rw [IsScalarTower.algebraMap_apply L (center D)]

Premises used: Subring.center, Membership.mem, Subtype, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x_1 : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_2 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h_1 : IsScalarTower L (↥k) D
x : ↥k
h : x = (algebraMap L ↥k : (a : L) → ↥k) ((algebraMap (↥k) L : (a : ↥k) → L) x)
⊢ Eq (α := D) ((algebraMap (↥k) D : (a : ↥k) → D) x : D)
    ((algebraMap (↥k) D : (a : ↥k) → D) ((algebraMap L ↥k : (a : L) → ↥k) ((algebraMap (↥k) L : (a : ↥k) → L) x) : ↥k) :
      D)

Tactic:
congr
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x_1 : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_2 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
x : ↥k
⊢ x = (algebraMap L ↥k : (a : L) → ↥k) ((algebraMap (↥k) L : (a : ↥k) → L) x)

Tactic:
(equiv.apply_symm_apply x).symm

Premises used: RingEquiv.apply_symm_apply, Eq.symm
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x_1 : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_2 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
x : ↥k
⊢ x = (algebraMap L ↥k : (a : L) → ↥k) ((algebraMap (↥k) L : (a : ↥k) → L) x)

Tactic:
exact (equiv.apply_symm_apply x).symm

Premises used: RingEquiv.apply_symm_apply, Eq.symm
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_1 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
⊢ IsScalarTower (↥k) L D

Tactic:
have _ : IsScalarTower (center D) L D := .of_algebraMap_eq fun x ↦ by
    rw [IsScalarTower.algebraMap_apply L (center D)]
    congr
    exact (equiv.apply_symm_apply x).symm
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_1 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
h_1 : IsScalarTower (↥k) L D
⊢ Algebra.IsAlgebraic (↥k) D

Tactic:
have _ : Algebra.IsAlgebraic (center D) D := .tower_top (K := L) _
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_1 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
h_1 : IsScalarTower (↥k) L D
h_2 : Algebra.IsAlgebraic (↥k) D
obtain : ∀ (x : D) (hxd : x ∉ k) (hx : IsSeparable (↥k) x), ∃ x ∉ ⊥, IsSeparable L x
⊢ ∃ x ∉ ⊥, IsSeparable L x

Tactic:
obtain ⟨x, hxd, hx⟩ := exists_separable_and_not_isCentral D ntrivial

Premises used: JacobsonNoether.exists_separable_and_not_isCentral
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x_1 : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_2 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
h_1 : IsScalarTower (↥k) L D
h_2 : Algebra.IsAlgebraic (↥k) D
x : D
hxd : x ∉ k
hx : IsSeparable (↥k) x
rwa : ∀ (hxd : x ∉ Subalgebra.toSubring (Subalgebra.center L D)) (hx : IsSeparable (↥k) x), x ∉ ⊥
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hxd : x ∉ Subalgebra.toSubring.{u_2, u_3} (R := L) ⊥) (hx : IsSeparable (↥k) x), x ∉ ⊥
⊢ x ∉ ⊥

Tactic:
rwa [← Subalgebra.center_toSubring L, hcenter] at hxd

Premises used: Subalgebra.center_toSubring
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x_1 : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_2 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
h_1 : IsScalarTower (↥k) L D
h_2 : Algebra.IsAlgebraic (↥k) D
x : D
hxd : x ∉ k
hx : IsSeparable (↥k) x
⊢ ∃ x ∉ ⊥, IsSeparable L x

Tactic:
exact ⟨x, ⟨by rwa [← Subalgebra.center_toSubring L, hcenter] at hxd, IsSeparable.tower_top _ hx⟩⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
⊢ Membership.mem (γ := Set (Subgroup Gal(L/K))) (fixedByFinite K L) ⊤

Tactic:
⟨⊥, IntermediateField.instFiniteSubtypeMemBot K, IntermediateField.fixingSubgroup_bot⟩

Premises used: Set.Mem, setOf, IntermediateField.instFiniteSubtypeMemBot, Bot.bot, And.intro, Exists.intro, Set.image, fixedByFinite, IntermediateField.fixingSubgroup_bot
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 : IntermediateField K L
h_E1 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E1
E2 : IntermediateField K L
h_E2 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E2
⊢ FiniteDimensional.{u_1, u_2} K ↥E1

Tactic:
have : FiniteDimensional K E1 := h_E1
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 : IntermediateField K L
h_E1 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E1
E2 : IntermediateField K L
h_E2 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E2
this : FiniteDimensional.{u_1, u_2} K ↥E1
⊢ FiniteDimensional.{u_1, u_2} K ↥E2

Tactic:
have : FiniteDimensional K E2 := h_E2
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 : IntermediateField K L
h_E1 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E1
E2 : IntermediateField K L
h_E2 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E2
this_1 : FiniteDimensional.{u_1, u_2} K ↥E1
this : FiniteDimensional.{u_1, u_2} K ↥E2
⊢ ∃ (z : Set Gal(L/K)),
    Membership.mem (γ := Set (Set Gal(L/K))) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) '' fixedByFinite K L) z ∧
      z ⊆
        (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E1.fixingSubgroup ∩
          (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E2.fixingSubgroup

Tactic:
⟨(E1 ⊔ E2).fixingSubgroup.carrier, ⟨_, ⟨_, E1.finiteDimensional_sup E2, rfl⟩, rfl⟩, ?_⟩

Premises used: Submonoid.toSubsemigroup, IntermediateField.fixingSubgroup, Max.max, And.intro, Exists.intro, Subsemigroup.carrier, IntermediateField.finiteDimensional_sup, rfl, Subgroup.toSubmonoid
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 : IntermediateField K L
h_E1 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E1
E2 : IntermediateField K L
h_E2 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E2
this_1 : FiniteDimensional.{u_1, u_2} K ↥E1
this : FiniteDimensional.{u_1, u_2} K ↥E2
refine :
  (E1 ⊔ E2).fixingSubgroup.carrier ⊆
    (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E1.fixingSubgroup ∩
      (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E2.fixingSubgroup
⊢ ∃ (z : Set Gal(L/K)),
    Membership.mem (γ := Set (Set Gal(L/K))) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) '' fixedByFinite K L) z ∧
      z ⊆
        (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E1.fixingSubgroup ∩
          (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E2.fixingSubgroup

Tactic:
refine ⟨(E1 ⊔ E2).fixingSubgroup.carrier, ⟨_, ⟨_, E1.finiteDimensional_sup E2, rfl⟩, rfl⟩, ?_⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 : IntermediateField K L
h_E1 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E1
E2 : IntermediateField K L
h_E2 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E2
this_1 : FiniteDimensional.{u_1, u_2} K ↥E1
this : FiniteDimensional.{u_1, u_2} K ↥E2
⊢ (E1 ⊔ E2).fixingSubgroup.carrier ⊆
    (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E1.fixingSubgroup ∩
      (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E2.fixingSubgroup

Tactic:
Set.subset_inter (E1.fixingSubgroup_le le_sup_left) (E2.fixingSubgroup_le le_sup_right)

Premises used: le_sup_left, le_sup_right, IntermediateField.fixingSubgroup_le, Set.subset_inter
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 : IntermediateField K L
h_E1 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E1
E2 : IntermediateField K L
h_E2 : Membership.mem (γ := Set (IntermediateField K L)) (finiteExts K L) E2
this_1 : FiniteDimensional.{u_1, u_2} K ↥E1
this : FiniteDimensional.{u_1, u_2} K ↥E2
⊢ (E1 ⊔ E2).fixingSubgroup.carrier ⊆
    (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E1.fixingSubgroup ∩
      (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) E2.fixingSubgroup

Tactic:
exact Set.subset_inter (E1.fixingSubgroup_le le_sup_left) (E2.fixingSubgroup_le le_sup_right)

Premises used: le_sup_left, le_sup_right, IntermediateField.fixingSubgroup_le, Set.subset_inter
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
U : Set Gal(L/K)
⊢ Membership.mem (γ := FilterBasis Gal(L/K)) (galBasis K L) U ↔
    Membership.mem (γ := Set (Set Gal(L/K))) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) '' fixedByFinite K L) U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
U : Set Gal(L/K)
hU : Membership.mem (γ := Set (Set Gal(L/K))) (FilterBasis.sets (galBasis K L)) U
rcases :
  ∀ (H : Subgroup Gal(L/K)),
    Membership.mem (γ := Set (Subgroup Gal(L/K))) (fixedByFinite K L) H →
      HMul.hMul (α := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H)
          ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H) ⊆
        (fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H
⊢ U * U ⊆ U

Tactic:
rcases hU with ⟨H, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : Subgroup Gal(L/K)
left : Membership.mem (γ := Set (Subgroup Gal(L/K))) (fixedByFinite K L) H
a : Gal(L/K)
haH : Membership.mem (γ := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H) a
b : Gal(L/K)
hbH : Membership.mem (γ := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H) b
⊢ Membership.mem (γ := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H)
    ((fun (x1 x2 : Gal(L/K)) ↦ x1 * x2) a b)

Tactic:
H.mul_mem haH hbH

Premises used: Set.Mem, Subgroup.mul_mem
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : Subgroup Gal(L/K)
left : Membership.mem (γ := Set (Subgroup Gal(L/K))) (fixedByFinite K L) H
a : Gal(L/K)
haH : Membership.mem (γ := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H) a
b : Gal(L/K)
hbH : Membership.mem (γ := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H) b
⊢ Membership.mem (γ := Set Gal(L/K)) ((fun (g : Subgroup Gal(L/K)) ↦ g.carrier) H)
    ((fun (x1 x2 : Gal(L/K)) ↦ x1 * x2) a b)

Tactic:
exact H.mul_mem haH hbH

Premises used: Subgroup.mul_mem