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

Goal state before:
pp: α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ C = M.fundCircuit e I

Tactic:
refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ e ∈ M.closure I

case refine_2
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
heI : e ∈ I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk M.E = M.eRank

Tactic:
eRank_def

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk M.E = M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.E ⊆ X
⊢ M.eRk M.E = M.eRank

Tactic:
eRank_def

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.E ⊆ X
⊢ M.eRk M.E = M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRk M.E = M.eRank

Tactic:
eRank_def

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.eRk M.E = M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.closure_eq_closure, ← hI.indep.isBasis_closure.encard_eq_eRk, hI.encard_eq_eRk]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I ≤ M.eRank

Tactic:
eRank_def

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I ≤ M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRk M.loops = 0

Tactic:
by
  simp [eRk_eq_zero_iff']

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

Goal state before:
pp: case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Tactic:
refine ⟨C', hC'ss.trans ?_, hC', hzC'⟩

Goal state after:
case refine_5
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C₀ \ range x ∪ ⋃ i, C i \ {x i} ⊆ (C₀ ∪ ⋃ i, C i) \ range x
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X : Set α
⊢ (M.comap f).eRk X = M.eRk (f '' X)

Tactic:
by
  obtain ⟨I, hI⟩ := (M.comap f).exists_isBasis' X
  obtain ⟨hI', hinj, -⟩ := comap_isBasis'_iff.1 hI
  rw [← hI.encard_eq_eRk, ← hI'.encard_eq_eRk, hinj.encard_image]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ ∀ (x : α), x ∈ M.closure X ∧ M.IsColoop x ↔ x ∈ X ∧ M.IsColoop x

Tactic:
and_congr_left_iff

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ ∀ (x : α), M.IsColoop x → (x ∈ M.closure X ↔ x ∈ X)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
spanning_iff_exists_isBase_subset

Goal state after:
case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (¬∃ B, M.IsBase B ∧ B ⊆ M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
obtain ⟨I₀, hI₀X, rfl, hfI₀⟩ := show ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀ by
    obtain ⟨I₀, hI₀ss, hbij⟩ := exists_subset_bijOn (f ⁻¹' I ∩ X) f
    refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩
    rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]

Goal state after:
case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ lift.{u, v} #↑(f '' I₀) ≤ lift.{v, u} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
a : α
ha : a ∈ B' \ B
this : ¬N.Indep (insert a B)
⊢ ∃ S, Finite ↑S ∧ S ⊆ B ∧ ¬N.Indep (insert a S)

Tactic:
contrapose! this

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
a : α
ha : a ∈ B' \ B
this : ∀ (S : Set α), Finite ↑S → S ⊆ B → N.Indep (insert a S)
⊢ N.Indep (insert a B)
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s

Tactic:
rw [Transcendental] at h

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : ¬IsAlgebraic (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
⊢ (M ↾ X).eRank = M.eRk X

Tactic:
eRk

Goal state after:
α : Type u
M : Matroid α
X : Set α
⊢ (M ↾ X).eRank = (M ↾ X).eRank
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
classical simp_rw [← algebraicIndependent_equiv (subtypeInsertEquivOption h).symm,
    AlgebraicIndepOn]
  convert! option_iff (x := fun i : s ↦ x i) (a := x i) using 2
  · ext (_ | _) <;> rfl
  · rw [Set.image_eq_range]

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

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

Tactic:
spanning_iff_exists_isBase_subset

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
hS : ∃ B, M.IsBase B ∧ B ⊆ S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
spanning_iff_exists_isBase_subset

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E \ I) ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E \ I
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
⊢ #ι ≤ trdeg R A

Tactic:
← (#ι).lift_id,

Goal state after:
R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
⊢ lift.{v, v} #ι ≤ trdeg R A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ ∀ (s : Set A), AlgebraicIndepOn R _root_.id s → range x ⊆ s → range x = s

Tactic:
intro w

Goal state after:
case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
⊢ AlgebraicIndepOn R _root_.id w → range x ⊆ w → range x = w
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
by
  by_cases h : f * g = 0
  · simp only [h, natSepDegree_zero, zero_le]
  classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _

Goal state after:
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
this : IsTopologicalGroup G
⊢ T2Space G ↔ ⋂₀ F.sets = {1}

Tactic:
rw [IsTopologicalGroup.t2Space_iff_one_closed, ← closure_eq_iff_isClosed,
    R0Space.closure_singleton, ← hG, F.nhds_one_eq, FilterBasis.ker_filter]

Goal state after:
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
⊢ T2Space G ↔ ⋂₀ F.sets ⊆ {1}

Tactic:
rw [F.t2Space_iff hG, subset_antisymm_iff, and_iff_left_iff_imp]
  rintro -
  simpa using! fun _ ↦ F.one

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
this : finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
⊢ fixedField K.fixingSubgroup = K

Tactic:
by
    exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ sepDegree F ↥⊥ = 1

Tactic:
have := lift_sepDegree_eq_of_equiv _ _ _ (botEquiv F E)
  rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this

Goal state after:
Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed ↑H
⊢ ∀ (i : G), IsClosed ↑(comap (↑(MulAut.conj i)) H)

Tactic:
intro g

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : SeparatelyContinuousMul G
H : Subgroup G
h : IsClosed ↑H
g : G
⊢ IsClosed ↑(comap (↑(MulAut.conj g)) H)
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
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional K ↥E
⊢ IsOpen ↑(MulAction.stabilizer Gal(L/K) x)

Tactic:
convert! fixingSubgroup_isOpen E

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
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional K ↥E
⊢ MulAction.stabilizer Gal(L/K) x = E.fixingSubgroup
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := ⋯
L : Type u_2 := ⋯
x✝ : Algebra K L := ⋯
⊢ minpoly K ((algebraMap S L) s) ∣ map (algebraMap R K) (minpoly R s)

Tactic:
isIntegrallyClosed_eq_field_fractions K L hs

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
⊢ map (algebraMap R K) (minpoly R s) ∣ map (algebraMap R K) (minpoly R s)
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ R[x]
⊢ (algebraMap R S) ((minpoly R x).coeff (i + j + 1)) + (minpolyDiv R x).coeff (i + j + 1) * x ∈ R[x]

Tactic:
refine add_mem ?_ (mul_mem H (self_mem_adjoin_singleton R x))

Goal state after:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ R[x]
⊢ (algebraMap R S) ((minpoly R x).coeff (i + j + 1)) ∈ R[x]
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : minpolyDiv R x * (X - C x) = map (algebraMap R S) (minpoly R x)
⊢ False

Tactic:
rw [e, zero_mul] at this

Goal state after:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : 0 = map (algebraMap R S) (minpoly R x)
⊢ False
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := ⋯
L : Type u_2 := ⋯
this : Algebra K L := ⋯
⊢ map (algebraMap R K) (minpoly R (r • s)) = map (algebraMap R K) ((minpoly R s).scaleRoots r)

Tactic:
rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (hs.smul r),
    map_scaleRoots _ _ _ (by simpa [minpoly.ne_zero_iff]),
    ← minpoly.isIntegrallyClosed_eq_field_fractions K L hs]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly K ((algebraMap S L) (r • s)) = (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Subalgebra.toSubmodule R[x] ≤ Submodule.span R (Set.range (minpolyDiv R x).coeff)

Tactic:
rw [← Submodule.span_range_natDegree_eq_adjoin (minpoly.monic hx) (minpoly.aeval _ _),
      Submodule.span_le]
    simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff]
    intro i
    induction i using Nat.strongRecOn with | ind i hi => ?_
    intro hi'
    have : coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) ∈
        Submodule.span R (Set.range (coeff (minpolyDiv R x))) :=
      Submodule.subset_span (Set.mem_range_self _)
    rw [Set.mem_preimage, SetLike.mem_coe, ← Submodule.sub_mem_iff_right _ this]
    refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx ?_)
    · rw [Submodule.span_le, Set.image_subset_iff]
      intro j (hj : j < i)
      exact hi j hj (lt_trans hj hi')
    · rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi'

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
⊢ ∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) = X ^ r

Tactic:
← sub_eq_zero

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
⊢ ∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r = 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
⊢ ((UniqueFactorizationMonoid.factors p).prod * ↑u).Splits

Tactic:
refine (Splits.multisetProd fun f hf ↦ ?_).mul u.isUnit.splits

Goal state after:
case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
f : k[X]
hf : f ∈ UniqueFactorizationMonoid.factors p
⊢ f.Splits
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis (↥s) R S)
⊢ trace R S = 0

Tactic:
ext s

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis (↥s) R S)
s : S
⊢ (trace R S) s = 0 s
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : finSepDegree F ↥F⟮x⟯ = 1 ∧ finSepDegree (↥F⟮x⟯) E = 1
⊢ x ∈ (algebraMap F E).range

Tactic:
(finSepDegree_adjoin_simple_eq_finrank_iff F E x
        (Algebra.IsAlgebraic.isAlgebraic x)).2 hsep,

Goal state after:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : finrank F ↥F⟮x⟯ = 1 ∧ finSepDegree (↥F⟮x⟯) E = 1
⊢ x ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
⊢ finSepDegree F E = Cardinal.toNat (sepDegree F E)

Tactic:
rwa [finSepDegree_eq_finrank_of_isSeparable F (separableClosure F E),
    IsPurelyInseparable.finSepDegree_eq_one (separableClosure F E) E, mul_one] at h

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

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
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
x : K
x✝ : x ∈ ⊤
⊢ x ∈ adjoin E ↑(separableClosure F K)

Tactic:
set S := separableClosure F K

Goal state after:
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
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
x : K
x✝ : x ∈ ⊤
S : IntermediateField F K := separableClosure F K
⊢ x ∈ adjoin E ↑S
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
⊢ ∀ (m : G) (n : A') (a : B), m • n • a = n • m • a

Tactic:
intro g

Goal state after:
G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
g : G
⊢ ∀ (n : A') (a : B), g • n • a = n • g • a
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs = y

Tactic:
← sub_eq_zero

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs - y = 0
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = a.valMinAbs + ↑(if a.val ≤ n / 2 then 0 else n)

Tactic:
rw [valMinAbs_def_pos]
  split_ifs <;> simp [add_zero, sub_add_cancel]

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
⊢ ∀ (g : G), g • Q ≠ Q → a - eval b r ∈ g • Q

Tactic:
intro g

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
⊢ g • Q ≠ Q → a - eval b r ∈ g • Q
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
⊢ traceMatrix A ⇑(b.reindex f) = (reindex f f) (traceMatrix A ⇑b)

Tactic:
ext (x y)

Goal state after:
κ : Type w
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
x y : κ'
⊢ traceMatrix A (⇑(b.reindex f)) x y = (reindex f f) (traceMatrix A ⇑b) x y