mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∉ X
x✝ : ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C
C : Set α
hCX : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ X

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ M.Indep {f}

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ e ∉ {f}

Tactic:
by simpa

Goal state after:
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
h : M.IsCocircuit {e}
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ C ∩ {e} = {e}

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.eRk {e} = 1 ↔ M.IsNonloop e

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.eRk_eq⟩
  rwa [← indep_singleton, indep_iff_eRk_eq_encard_of_finite (by simp), encard_singleton]

Goal state after:
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
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ {e} ⊆ M.E

Tactic:
by simpa

Goal state after:
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
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ {e} ⊆ M✶.E

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
F : Set α
hF : M.IsFlat F
⊢ F ∈ {F_1 | M.IsFlat F_1 ∧ F ∩ M.E ⊆ F_1}

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsColoop e ↔ e ∉ M.closure (M.E \ {e})

Tactic:
by
  rw [isColoop_iff_sdiff_closure, not_iff_not]
  refine ⟨fun h ↦ by rwa [h], fun h ↦ (M.closure_subset_ground _).antisymm fun x hx ↦ ?_⟩
  obtain (rfl | hne) := eq_or_ne x e
  · assumption
  exact M.subset_closure (M.E \ {e}) sdiff_subset (show x ∈ M.E \ {e} from ⟨hx, hne⟩)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.subtypeClosure ⟨⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E, ⋯⟩ = M.subtypeClosure ⟨⋃ i, Xs i ∩ M.E, ⋯⟩

Tactic:
convert! M.subtypeClosure.closure_iSup_closure (fun i ↦ ⟨Xs i ∩ M.E, inter_subset_right⟩)

Goal state after:
case e'_2.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ ⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E = ↑(⨆ i, M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩)

case e'_3.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ ⋃ i, Xs i ∩ M.E = ↑(⨆ i, ⟨Xs i ∩ M.E, ⋯⟩)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ (i : Unit), M.IsCircuit C₂

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ (i : Unit), e ∈ C₁

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ (i : Unit), e ∈ C₂

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ f ∈ C₁

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ (i : Unit), f ∉ C₂

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ ∀ (x : α), x ∉ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)

Tactic:
refine fun e ⟨hecl, he⟩ ↦ he (.inl ?_)

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
x✝ : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
⊢ e ∈ M.closure X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
x✝ : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X)
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ M.closure X

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ {e} ⊆ M.coloops

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ {x} ⊆ I

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ {e} ⊆ X

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
C : Set α
hCs : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ X

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e | M.IsNonloop e}
⊢ M ↾ {e | M.IsNonloop e} ↾ X = M ↾ X

Tactic:
restrict_restrict_eq

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e | M.IsNonloop e}
⊢ M ↾ X = M ↾ X

case hR
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ {e | M.IsNonloop e}
⊢ X ⊆ {e | M.IsNonloop e}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ Indep ?m.39 (⋃ i, I ↑i)

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
Js : ι → Set α
hI : M.Indep I
hJs : ∀ (i : ι), Js i ⊆ I
⊢ ⋃ i, Js i ⊆ I

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∉ M✶.E

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)

Tactic:
refine (hI.inter_left _).isBasis_of_subset_of_subset_closure inter_subset_left ?_
  simp_rw [← biInter_inter hA,
  closure_biInter_eq_biInter_closure_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I)
      (hI.subset (by simp)), subset_iInter_iff]
  exact fun i hiA ↦ (biInter_subset_of_mem hiA).trans (h i hiA).subset_closure

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ {e} ⊆ M.E

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ I
⊢ I \ {e} ⊂ I

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
h : e ∈ M.closure (X \ {e})
⊢ {e} ⊆ M.closure (X \ {e})

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ X
heE : e ∈ M.E
⊢ {e} ⊆ X

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
⊢ M₁.E = M₂.E

Tactic:
simpa using h univ

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

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
⊢ M.Spanning S ↔ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E

Tactic:
refine ⟨fun h ↦ ⟨?_, h.subset_ground⟩, fun ⟨⟨B, hB, hBS⟩, hSE⟩ ↦ hB.spanning.superset hBS⟩
  obtain ⟨B, hB⟩ := M.exists_isBasis S
  have hB' := hB.isBasis_closure_right
  rw [h.closure_eq, isBasis_ground_iff] at hB'
  exact ⟨B, hB', hB.subset⟩

Goal state after:
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⟩

Goal state after:
case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
n : ℕ
g : F[X]
hgs : g.Separable
hge : (expand F (q ^ n)) g = f
⊢ HasSeparableContraction q f
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(aeval fun o ↦ o.elim a x)

Tactic:
refine MvPolynomial.ringHom_ext ?_ ?_ <;>
    simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingEquiv.coe_toRingHom,
      AlgHom.coe_toRingHom, AlgHom.coe_toRingHom]
  · intro r
    rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_C, aeval_C, Polynomial.aeval_C,
      IsScalarTower.algebraMap_apply R (adjoin R (range x)) A]
  · rintro (⟨⟩ | ⟨i⟩)
    · rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]
    · rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Polynomial.aeval_C,
        hx.algebraMap_aevalEquiv, aeval_X, aeval_X, Option.elim]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
⊢ AlgebraicIndependent S x

Tactic:
by
  nontriviality S
  have := Module.nontrivial R S
  exact hx.extendScalars S

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
have := f.map (algebraMap F f.SplittingField) |>.card_roots'

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
this : (map (algebraMap F f.SplittingField) f).roots.card ≤ (map (algebraMap F f.SplittingField) f).natDegree
⊢ f.natSepDegree ≤ f.natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
inst✝ : DecidableEq E
h : (map (algebraMap F E) f).Splits
⊢ f.natSepDegree = (f.aroots E).toFinset.card

Tactic:
rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
    (SplittingField.splits f).roots_map,
    Multiset.toFinset_map, Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ ((f * g).aroots (AlgebraicClosure F)).toFinset.card ≤
    (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
aroots_mul h,

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f.aroots (AlgebraicClosure F) + g.aroots (AlgebraicClosure F)).toFinset.card ≤
    (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∈ s
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})

Tactic:
rw [← image_singleton, ← inj.image_sdiff_subset (singleton_subset_iff.mpr hj)]
    rwa [insert_eq_of_mem hi] at H₂

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ ((f * g).aroots (AlgebraicClosure F)).toFinset.card =
      (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
aroots_mul h,

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f.aroots (AlgebraicClosure F) + g.aroots (AlgebraicClosure F)).toFinset.card =
      (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
q : ℕ
hF : ExpChar F q
n : ℕ
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
by
  obtain - | hprime := hF
  · simp only [one_pow, expand_one]
  have := Fact.mk hprime
  classical
  simpa only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_def, map_expand,
    Fintype.card_coe] using Fintype.card_eq.2
      ⟨(f.map (algebraMap F (AlgebraicClosure F))).rootsExpandPowEquivRoots q n⟩

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

Goal state before:
pp: 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
this : ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B, ∃ ia, (ia.1 ∈ B ∧ ia.2 ∈ B) ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib

Tactic:
by simpa

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

Goal state before:
pp: R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝¹ : TopologicalSpace R := B'.topology
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
this : ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B', ∃ ia, (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib

Tactic:
by simpa

Goal state after:
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)

Tactic:
have halg : IsIntegral F x := by_contra fun h' ↦ by
      simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h

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
halg : IsIntegral F x
⊢ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)
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:
· rw [basis'.tendsto_iff basis]
    suffices ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
    intro U U_in
    rcases B.mul U_in with ⟨V, V_in, hV⟩
    refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
    intro a b a_in b_in
    exact hV <| mul_mem_mul a_in b_in

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)

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.Galois.Basic

Goal state before:
pp: case h_splits
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) := ⋯
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.map (algebraMap K E) (minpoly K x) ∣ Polynomial.map (algebraMap F E) p

Tactic:
← f.comp_algebraMap,

Goal state after:
case h_splits
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Polynomial.map (algebraMap K E) (minpoly K x) ∣ Polynomial.map ((↑f).comp (algebraMap F K)) p
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
x✝ : Algebra.IsSeparable F ↥F⟮x⟯
⊢ IsSeparable F x

Tactic:
exact isSeparable_of_mem_isSeparable F E <| mem_adjoin_simple_self F x

Goal state after:
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
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : w1 * w2⁻¹ ∈ H
⊢ False

Tactic:
rw [h] at h_in_H

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : f⁻¹ * g ∈ H
⊢ False
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case right
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] := ⋯
⊢ adjoin (↥L) (T'.rootSet E) = ⊤

Tactic:
· have h' : T'.rootSet E = T.rootSet E := by simp [Set.ext_iff, Polynomial.mem_rootSet', T']
    rw [← lift_inj, lift_adjoin, ← coe_val, hT₂.1.image_rootSet] at hT₂
    rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]

Goal state after: