mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)

pp: case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)

pp: case refine_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)

pp: case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
·

Goal state after:
case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)

pp: case refine_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)

pp: case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
·

Goal state after:
case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)

pp: case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
·

Goal state after:
case refine_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
·

Goal state after:
case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ ⋂₀ F.sets = {1} ↔ ⋂₀ F.sets ⊆ {1}

Tactic:
subset_antisymm_iff,

Goal state after:
G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ ⋂₀ F.sets ⊆ {1} ∧ {1} ⊆ ⋂₀ F.sets ↔ ⋂₀ F.sets ⊆ {1}
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

pp: case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)

pp: case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
·

Goal state after:
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m

pp: case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ f.natSepDegree = 1

Tactic:
·

Goal state after:
case refine_1
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
⊢ ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E → IsGalois F E

pp: case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois F E → IsGalois (↥⊥) E

Tactic:
·

Goal state after:
case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E → IsGalois F E
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois F E → IsGalois (↥⊥) E

Tactic:
·

Goal state after:
case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois F E → IsGalois (↥⊥) E
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

pp: case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
x✝ : ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : minpoly F x = (expand F (q ^ n)) (X - C y)
⊢ (minpoly F x).natSepDegree = 1

Tactic:
·

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)

pp: case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
·

Goal state after:
case hmul_left
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x₀ * x) (𝓝 0) (𝓝 0)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case e'_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (∃ n, x ^ q ^ n ∈ (algebraMap F E).range) ↔ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0

pp: case convert_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0

Tactic:
·

Goal state after:
case e'_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (∃ n, x ^ q ^ n ∈ (algebraMap F E).range) ↔ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
·

Goal state after:
case hmul_right
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ (x₀ : R), Tendsto (fun x ↦ x * x₀) (𝓝 0) (𝓝 0)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case convert_2.refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0

pp: case convert_2.refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
n : ℕ
y : F
h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
⊢ (minpoly F x).natSepDegree = 1

Tactic:
·

Goal state after:
case convert_2.refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
K L : IntermediateField F E
le : K ≤ L
x : E
hx : x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) K
⊢ x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) L

pp: case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
K : IntermediateField F E
x : E
hx :
  x ∈
    IntermediateField.restrictScalars F
      (separableClosure (↥(IntermediateField.restrictScalars F (separableClosure (↥K) E))) E)
⊢ x ∈ IntermediateField.restrictScalars F (separableClosure (↥K) E)

Tactic:
·

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
K L : IntermediateField F E
le : K ≤ L
x : E
hx : x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) K
⊢ x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) L
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
K : IntermediateField F E
x : E
hx :
  x ∈
    IntermediateField.restrictScalars F
      (separableClosure (↥(IntermediateField.restrictScalars F (separableClosure (↥K) E))) E)
⊢ x ∈ IntermediateField.restrictScalars F (separableClosure (↥K) E)

Tactic:
·

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
K : IntermediateField F E
x : E
hx :
  x ∈
    IntermediateField.restrictScalars F
      (separableClosure (↥(IntermediateField.restrictScalars F (separableClosure (↥K) E))) E)
⊢ x ∈ IntermediateField.restrictScalars F (separableClosure (↥K) E)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmul
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ Tendsto (fun p ↦ p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

pp: case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)

pp: case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)

Tactic:
·

Goal state after:
case hmul
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ Tendsto (fun p ↦ p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

pp: case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
·

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case inst
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := ⋯
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := ⋯
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
⊢ Algebra.EssFiniteType (↥(adjoin F ↑s)) E

pp: case inst
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := ⋯
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := ⋯
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
⊢ Algebra.IsAlgebraic (↥(adjoin F ↑s)) E

Tactic:
·

Goal state after:
case inst
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := ⋯
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := ⋯
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
⊢ Algebra.EssFiniteType (↥(adjoin F ↑s)) E
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)

pp: case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)

Tactic:
·

Goal state after:
case hmulleft
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: case inst
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := ⋯
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := ⋯
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
⊢ Algebra.IsAlgebraic (↥(adjoin F ↑s)) E

Tactic:
·

Goal state after:
case inst
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := ⋯
Hexists : {s | IsTranscendenceBasis F Subtype.val}.Nonempty
s : Finset E := ⋯
hs : Function.argminOn d {s | IsTranscendenceBasis F Subtype.val} Hexists ∈ {s | IsTranscendenceBasis F Subtype.val}
t : Finset E
ht : IsTranscendenceBasis F Subtype.val
H :
  (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s <
    (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑t
⊢ Algebra.IsAlgebraic (↥(adjoin F ↑s)) E
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)

Tactic:
·

Goal state after:
case hmulright
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : IsTopologicalRing R
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : (𝓝 0).HasBasis p b
hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)