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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard < J.ncard
f : α
hfJ : f ∈ J
hfI₀ : f ∉ I₀
hfi : Indep (insert f I₀)
⊢ f ∈ I₀ ∪ B₀ → f ∈ B₀

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I X ∧ I ⊆ R ↔ M.IsBasis' I X

Tactic:
and_iff_left_iff_imp

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I X → I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ J ⊆ I ∧ J ⊆ E ↔ J ⊆ I

Tactic:
and_iff_left_iff_imp

Goal state after:
α : Type u_1
E I J : Set α
hIE : I ⊆ E
⊢ J ⊆ I → J ⊆ E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ {B | M✶.IsBase B} = (fun X ↦ M.E \ X) '' {B | M.IsBase B}

Tactic:
ext B
  simp only [mem_ofPred_eq, mem_image, dual_isBase_iff']
  refine ⟨fun h ↦ ⟨_, h.1, sdiff_sdiff_cancel_left h.2⟩,
    fun ⟨B', hB', h⟩ ↦ ⟨?_,h.symm.trans_subset sdiff_subset⟩⟩
  rwa [← h, sdiff_sdiff_cancel_left hB'.subset_ground]

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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hcard : I.encard < B.encard
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
        exact ⟨e, ⟨heB, heI⟩, hi⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) ∧ InjOn f I ↔ N.Indep (f '' I)

Tactic:
and_iff_left_iff_imp

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ N.Indep (f '' I) → InjOn f I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E \ X

Tactic:
and_iff_left hX

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E \ X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
I : Set ↑M.E
⊢ M.Indep ↑I ∧ InjOn (fun x ↦ ↑(invFunOn (⇑f) univ x)) (⇑f '' I) ↔ M.Indep (Subtype.val '' I)

Tactic:
and_iff_left_iff_imp

Goal state after:
case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
I : Set ↑M.E
⊢ M.Indep ↑I → InjOn (fun x ↦ ↑(invFunOn (⇑f) univ x)) (⇑f '' I)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
⊢ M.IsCircuit (insert e I)

Tactic:
rw [isCircuit_iff_dep_forall_sdiff_singleton_indep, hI.insert_dep_iff, and_iff_right ⟨he, heI⟩]
  rintro f (rfl | hfI)
  · simpa [heI]
  rw [← insert_sdiff_singleton_comm (by rintro rfl; contradiction),
    (hI.sdiff _).insert_indep_iff_of_notMem (by simp [heI])]
  exact ⟨mem_ground_of_mem_closure he, h f hfI⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.IsBase (M.E \ B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ M.IsBase (M.E \ B)

Tactic:
and_iff_left_iff_imp

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set ↑M.E
⊢ M.IsBasis (Subtype.val '' B) M.E ↔ M.IsBase (Subtype.val '' B)

Tactic:
isBasis_ground_iff

Goal state after:
α : Type u_1
M : Matroid α
B : Set ↑M.E
⊢ M.IsBase (Subtype.val '' B) ↔ M.IsBase (Subtype.val '' B)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsLoop e ↔ e ∈ (M ↾ R).E ∧ M.IsLoop e

Tactic:
simp only [restrict_isLoop_iff, restrict_ground_eq, and_congr_right_iff, or_iff_left_iff_imp]

Goal state after:
α : Type u_1
M : Matroid α
e : α
R : Set α
hR : R ⊆ M.E
⊢ e ∈ R → e ∉ M.E → M.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
⊢ M.eRk I = M.eRk X

Tactic:
rw [← hIX.encard_eq_eRk, hIX.indep.eRk_eq_encard]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
⊢ M.eRk I = M.eRk X

Tactic:
rw [← hIX.encard_eq_eRk, hIX.indep.eRk_eq_encard]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ ¬((∃ C ⊆ I, M.IsCircuit C) ∧ I ⊆ M.E) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
heX : e ∉ X
I : Set α
hI : M.IsBasis' I X
⊢ e ∈ M.closure I

Tactic:
hI.closure_eq_closure

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
heX : e ∉ X
I : Set α
hI : M.IsBasis' I X
⊢ e ∈ M.closure X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
Y : Set α
⊢ M.eRk (I ∪ Y) = M.eRk (X ∪ Y)

Tactic:
← eRk_union_closure_left_eq,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
Y : Set α
⊢ M.eRk (M.closure I ∪ Y) = M.eRk (X ∪ Y)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e X ∩ insert e Y) + M.eRk (insert e X ∪ insert e Y) ≤ M.eRk (insert e X) + M.eRk (insert e Y)

Tactic:
apply M.eRk_submod

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ X ∩ (M.E \ Y)) + M.eRk (M.E \ X ∪ M.E \ Y) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)

Tactic:
apply M.eRk_submod

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ (¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})) ↔ ¬M.Indep {e, f}

Tactic:
and_iff_left_iff_imp

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ ¬M.Indep {e, f} → ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: ι : Type u_1
α : Type u_2
M✝ : Matroid α
F X Y : Set α
e f : α
M : Matroid α
s : Set ↑(Iic M.E)
hs : ∀ a ∈ s, M.IsFlat ↑a
hne : s.Nonempty
x✝¹ : Nonempty ↑s
x✝ : α
⊢ x✝ ∈ ↑(sInf s) ↔ x✝ ∈ ⋂ i, ↑↑i

Tactic:
aesop

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.closure X = ⋂₀ {F | M.IsFlat F ∧ X ⊆ F}

Tactic:
closure,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F} = ⋂₀ {F | M.IsFlat F ∧ X ⊆ F}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (M.closure X)

Tactic:
closure,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F})
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : X ⊆ M.E
⊢ M.eRank ≤ M.eRk X ∧ X ⊆ M.E ↔ M.eRank ≤ M.eRk X

Tactic:
and_iff_left hX

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : X ⊆ M.E
⊢ M.eRank ≤ M.eRk X ↔ M.eRank ≤ M.eRk X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure X

Tactic:
rw [← closure_inter_ground]
  exact M.mem_closure_of_mem ⟨heX, h⟩

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

Goal state before:
pp: α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C ∧ C ⊆ R → e ∉ C) ↔ (¬∃ C ⊆ insert e R, M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R

Tactic:
aesop

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
this : I ⊆ M.E
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
I : Set α
hI : M.IsBasis' I T
⊢ X ⊆ M.closure I

Tactic:
hI.closure_eq_closure

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
I : Set α
hI : M.IsBasis' I T
⊢ X ⊆ M.closure T
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inr
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∉ I
⊢ e ∈ M.E \ M.closure I ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
or_iff_left h

Goal state after:
case inr
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∉ I
⊢ e ∈ M.E \ M.closure I ↔ e ∈ M.E \ M.closure I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ∧ I ⊆ {e | M.IsNonloop e} ↔ M.Indep I

Tactic:
and_iff_left_iff_imp

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I → I ⊆ {e | M.IsNonloop e}
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr.inr.inr
α : 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}))
⊢ insert e B ⊆ insert e (insert f (M.E \ (M.E \ B ∪ {f})))

Tactic:
← sdiff_sdiff,

Goal state after:
case inr.inr.inr
α : 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}))
⊢ insert e B ⊆ insert e (insert f ((M.E \ (M.E \ B)) \ {f}))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e} ∩ M.E)
hf : f ∉ M.E
heB : e ∈ B
a✝ : α
⊢ a✝ ∈ insert f B \ {e} ∩ M.E → a✝ ∈ B \ {e}

Tactic:
aesop

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

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

Tactic:
insert_eq_of_mem hin,

Goal state after:
case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (M.closure (I \ {e}))
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
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom
⊢ Injective ⇑(aeval x).toRingHom

Tactic:
rw [← this, RingHom.coe_comp]

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom
⊢ Injective (⇑(aeval x).toRingHom ∘ ⇑(MvPolynomial.map (algebraMap R K)))
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
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ i ∉ s

Tactic:
← Set.disjoint_singleton_right

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Disjoint s {i}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBasis B M.E
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
isBasis_ground_iff

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B ⊆ S
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.Spanning (M.E \ (M.E \ S))

Tactic:
sdiff_sdiff_cancel_left hS

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.Spanning S
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

Tactic:
by_cases he : M.Indep (insert e I)

Goal state after:
case pos
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
he : M.Indep (insert e I)
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E

case neg
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
he : ¬M.Indep (insert e I)
⊢ e ∈ R ∧ (M.Indep (insert e I) ∧ insert e I ⊆ R → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S

Tactic:
rw [spanning_iff, restrict_ground_eq, and_iff_left hSR, restrict_closure_eq _ hSR, inter_eq_right]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ s ∈ fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s

Tactic:
simp_rw [mem_fixedBy, ← eq_inv_smul_iff, Set.ext_iff, Set.mem_inv_smul_set_iff, Iff.comm]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
⊢ fixedBy α g ∈ fixedBy (Set α) h

Tactic:
ext x
  rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]

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

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ range x = Subtype.val '' range (Set.inclusion hxs)

Tactic:
rw [← range_comp, val_comp_inclusion, Subtype.range_val]

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

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsDomain A
inst✝ : FaithfulSMul R A
s : Set A
⊢ Algebra.IsAlgebraic (↥(adjoin R s)) A ↔ ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val

Tactic:
simp_rw [← matroid_spanning_iff, ← matroid_isBase_iff, and_comm (a := _ ⊆ s)]
  exact Matroid.spanning_iff_exists_isBase_subset (subset_univ _)

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
rw [mul_eq_zero] at h
    wlog hf : f = 0 generalizing f g
    · simpa only [mul_comm, add_comm, and_comm,
        isCoprime_comm] using this g f h.symm (h.resolve_left hf)
    rw [hf, zero_mul, natSepDegree_zero, zero_add, isCoprime_zero_left, isUnit_iff, eq_comm,
      natSepDegree_eq_zero_iff, natDegree_eq_zero]
    refine ⟨fun ⟨x, h⟩ ↦ ?_, ?_⟩
    · by_cases hx : x = 0
      · exact .inl ⟨rfl, by rw [← h, hx, map_zero]⟩
      exact .inr ⟨x, Ne.isUnit hx, h⟩
    rintro (⟨-, h⟩ | ⟨x, -, h⟩)
    · exact ⟨0, by rw [h, map_zero]⟩
    exact ⟨x, h⟩

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
⊢ ⋂₀ F.sets ⊆ {1} ∧ {1} ⊆ ⋂₀ F.sets ↔ ⋂₀ F.sets ⊆ {1}

Tactic:
and_iff_left_iff_imp

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
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:
· let _ := (inclusion le).toAlgebra
    have : IsScalarTower K L E := .of_algebraMap_eq' rfl
    exact hx.tower_top _

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.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).natDegree

Tactic:
exact minpoly.natDegree_pos <| IsAlgebraic.isIntegral ⟨_, hnezero, h⟩

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

Goal state before:
pp: case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ Algebra.adjoin F ((minpoly F α).rootSet E) = ⊤

Tactic:
rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← h1]

Goal state after:
case adjoin_rootSet'
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
h1 : F⟮α⟯ = ⊤
⊢ F⟮α⟯.toSubalgebra ≤ Algebra.adjoin F ((minpoly F α).rootSet E)
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
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
⊢ Polynomial.eval₂ (algebraMap K E) x (Polynomial.map (algebraMap F K) p) = 0

Tactic:
Polynomial.eval₂_map,

Goal state after:
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
⊢ Polynomial.eval₂ ((algebraMap K E).comp (algebraMap F K)) x p = 0
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : IsTopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x✝¹ : TopologicalSpace M := B'.topology
x✝ : Set M
⊢ x✝ ∈ B' → ∃ V ∈ 𝓝 0, ∃ j ∈ B', V • id j ⊆ id x✝

Tactic:
simpa using! B.smul

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
⊢ f ≠ 0

Tactic:
aesop

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

Goal state before:
pp: case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
⊢ 1 ∈ ↑(adjoin k {y}).fixingSubgroup ∧ (fun x ↦ σ • x) 1 = σ

Tactic:
simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]

Goal state after: