mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ {α, β} ⊆ ↑F⟮γ⟯

Tactic:
have α_in_Fγ : α ∈ F⟮γ⟯ := by
        rw [← add_sub_cancel_right α (c • β)]
        exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fγ : α ∈ F⟮γ⟯
⊢ {α, β} ⊆ ↑F⟮γ⟯
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
f_root : eval₂ ιEE' (eval₂ ιEE' x (C γ - C (ιFE c) * X)) (Polynomial.map ιFE f) = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots

Tactic:
eval₂_sub,

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
f_root : eval₂ ιEE' (eval₂ ιEE' x (C γ) - eval₂ ιEE' x (C (ιFE c) * X)) (Polynomial.map ιFE f) = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
⊢ P (IntermediateField.restrictScalars F (↥K)⟮β⟯)

Tactic:
rw [← hK, adjoin_simple_adjoin_simple]

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K ↦ ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
⊢ P F⟮α, β⟯
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M.IsBase (M.E \ (M.E \ B)) ↔ M.IsBase B

Tactic:
sdiff_sdiff_cancel_left h

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M.IsBase B ↔ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X

Tactic:
by
  rw [← isRkFinite_inter_ground_iff (X := X)]
  exact ⟨fun h ↦ h.subset <| M.inter_ground_subset_closure X, fun h ↦ by simpa using h.closure⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B₀ = J

Tactic:
rw [← hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground, hbij.image_eq]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B = f '' J
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Nonempty
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).E.Nonempty

Tactic:
by simp [M.ground_nonempty]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X

Tactic:
exact fun h ↦ (image_subset_image_iff Subtype.val_injective).1 h.subset

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ∅.encard = 0

Tactic:
encard_empty

Goal state after:
α : Type u_1
M : Matroid α
⊢ 0 = 0
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
obtain hι | hι := isEmpty_or_nonempty ι

Goal state after:
case inl
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : IsEmpty ι
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∩ M.E) = M.closure X

Tactic:
closure_inter_ground

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure X = M.closure X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B

Tactic:
refine fun ⟨h, heE⟩ B hB ↦ by_contra fun heB ↦ ?_

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
x✝ : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
heE : e ∈ M.E
heB : e ∉ B
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : ∀ x ∈ X, C x ∈ S ∧ C x ∩ X = {x}
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Tactic:
simp only [forall_and] at hC

Goal state after:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : M.Dep X
⊢ ¬M.eRk X = X.encard

Tactic:
← indep_iff_eRk_eq_encard

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : M.Dep X
⊢ ¬M.Indep X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
⊢ M.IsFlat (⋂ i, Fs i)

Tactic:
refine ⟨fun I X hI hIX ↦ subset_iInter fun i ↦ ?_,
    (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩

Goal state after:
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
⊢ X ⊆ Fs i
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ M.eRk ∅ = 0

Tactic:
eRk_empty

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ 0 = 0
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
⊢ ∅.encard = 0

Tactic:
encard_empty

Goal state after:
α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
⊢ 0 = 0
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'

Tactic:
rintro F' ⟨hF', hIF'⟩ e (he : M.IsBasis I (insert e I))

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
F : Set α := {x | M.IsBasis I (insert x I)}
hIF : M.IsBasis I F
hF : M.IsFlat F
F' : Set α
hF' : M.IsFlat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.IsBasis I (insert e I)
⊢ e ∈ F'
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.E
⊢ e ∉ M.closure I ↔ M.Indep (insert e I)

Tactic:
hI.notMem_closure_iff,

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.E
⊢ M.Indep (insert e I) ∧ e ∉ I ↔ M.Indep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure (X ∩ M.E))
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
closure_inter_ground

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure X)
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e})

Tactic:
Indep.insert_sdiff_indep_iff (hI.subset (sdiff_subset ..)) heI

Goal state after:
case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
⊢ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (I ∩ M.E) = M.closure I

Tactic:
closure_inter_ground

Goal state after:
case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure I = M.closure I
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
⊢ t ⊆ x ⁻¹' ↑(supported R t)

Tactic:
intro _ h

Goal state after:
ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ a✝ ∈ x ⁻¹' ↑(supported R t)
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ HasSeparableContraction q f

Tactic:
· rcases exists_separable_of_irreducible q irred ‹q.Prime›.ne_zero with ⟨n, g, hgs, hge⟩
    exact ⟨g, hgs, n, hge⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: 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
i : E ≃ₐ[F] K
⊢ AlgebraicClosure K ≃ₐ[F] AlgebraicClosure E

Tactic:
by
  let _ : Algebra E K := i.toAlgHom.toRingHom.toAlgebra
  have : Algebra.IsAlgebraic E K := by
    constructor
    intro x
    have h := isAlgebraic_algebraMap (R := E) (A := K) (i.symm.toAlgHom x)
    rw [show ∀ y : E, (algebraMap E K) y = i.toAlgHom y from fun y ↦ rfl] at h
    simpa only [AlgEquiv.coe_toAlgHom, AlgEquiv.apply_symm_apply] using h
  apply AlgEquiv.restrictScalars (R := F) (S := E)
  exact IsAlgClosure.equivOfAlgebraic E K (AlgebraicClosure K) (AlgebraicClosure E)

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ (𝓝 1).HasBasis (fun V ↦ V ∈ B) id

Tactic:
by
  rw [B.nhds_one_eq]
  exact B.toFilterBasis.hasBasis

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∃ V ∈ 𝓝 0,
        ∃
          W ∈
            (have this := default;
              this).sets,
          V • W ⊆ U

Tactic:
rintro U (rfl : U ∈ {{(0 : M)}})
        use univ, univ_mem, {0}, rfl
        rintro a ⟨x, -, m, rfl, rfl⟩
        simp only [smul_zero, mem_singleton_iff]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
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
hnezero : X ^ q ^ n - C y ≠ 0
⊢ 1 ≤ (minpoly F x).natSepDegree

Tactic:
Nat.one_le_iff_ne_zero,

Goal state after:
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
hnezero : X ^ q ^ n - C y ≠ 0
⊢ (minpoly F x).natSepDegree ≠ 0
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Algebra.IsAlgebraic (↥⊤) E

Tactic:
Algebra.isAlgebraic_iff_isIntegral

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Algebra.IsIntegral (↥⊤) E
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
l : ℕ
hl : b✝ ∈ V ^ (l + 1)
⊢ a✝ * b✝ ∈ V ^ (k + 1 + l + 1)

Tactic:
add_assoc,

Goal state after:
case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
l : ℕ
hl : b✝ ∈ V ^ (l + 1)
⊢ a✝ * b✝ ∈ V ^ (k + 1 + (l + 1))
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set Gal(L/K)
⊢ s ∈ 𝓝 1 ↔ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
rw [GroupFilterBasis.nhds_one_eq]
  constructor
  · rintro ⟨-, ⟨-, ⟨E, fin, rfl⟩, rfl⟩, hE⟩
    exact ⟨E, fin, hE⟩
  · rintro ⟨E, fin, hE⟩
    exact ⟨E.fixingSubgroup, ⟨E.fixingSubgroup, ⟨E, fin, rfl⟩, rfl⟩, hE⟩

Goal state after:
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case left
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (T.rootSet ↥K) = ⊤
T' : (↥L)[X] := ⋯
⊢ (Polynomial.map (algebraMap (↥L) E) T').Splits

Tactic:
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
    exact Polynomial.Splits.of_algHom hT₂.1 (IsScalarTower.toAlgHom _ _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := Basis.finiteDimensional_of_finite b
⊢ B.dualSubmodule (Submodule.span R (Set.range ⇑(B.flip.dualBasis ⋯ b))) = Submodule.span R (Set.range ⇑b)

Tactic:
dualSubmodule_span_of_basis B hB,

Goal state after:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := Basis.finiteDimensional_of_finite b
⊢ Submodule.span R (Set.range ⇑(B.dualBasis hB (B.flip.dualBasis ⋯ b))) = Submodule.span R (Set.range ⇑b)
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := Basis.finiteDimensional_of_finite b
⊢ B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
dualSubmodule_span_of_basis B hB,

Goal state after:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := Basis.finiteDimensional_of_finite b
⊢ B.flip.dualSubmodule (Submodule.span R (Set.range ⇑(B.dualBasis hB b))) = Submodule.span R (Set.range ⇑b)
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := Basis.finiteDimensional_of_finite b
⊢ B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
dualSubmodule_span_of_basis B hB,

Goal state after:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := Basis.finiteDimensional_of_finite b
⊢ B.dualSubmodule (Submodule.span R (Set.range ⇑(B.dualBasis hB b))) = Submodule.span R (Set.range ⇑b)
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := Basis.finiteDimensional_of_finite b
⊢ B.dualSubmodule (Submodule.span R (Set.range ⇑(B.dualBasis hB b))) = Submodule.span R (Set.range ⇑b)

Tactic:
dualSubmodule_span_of_basis B hB,

Goal state after:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
this : FiniteDimensional S M := Basis.finiteDimensional_of_finite b
⊢ Submodule.span R (Set.range ⇑(B.dualBasis hB (B.dualBasis hB b))) = Submodule.span R (Set.range ⇑b)