mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case refine_2
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
⊢ Nonempty ((↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ { asIdeal := ⊥.colon {N₁.mkQ x}, isPrime := hx }.asIdeal)

Tactic:
have hxN₂ : x ∈ N₂ := (le_sup_right.trans_eq hx'.symm) (mem_span_singleton_self x)
    refine ⟨.symm (.ofBijective (Submodule.mapQ _ _ (toSpanSingleton A _ ⟨x, hxN₂⟩) ?_) ⟨?_, ?_⟩)⟩
    · simp [SetLike.le_def, ← Quotient.mk_smul, submoduleOf]
    · refine ker_eq_bot.mp (ker_liftQ_eq_bot _ _ _ ?_)
      simp [← Quotient.mk_smul, SetLike.le_def, submoduleOf]
    · rw [mapQ, ← range_eq_top, range_liftQ, range_comp]
      have := congr($(hx').submoduleOf N₂)
      rw [submoduleOf_self, submoduleOf_sup_of_le (by simp_all) (by simp_all),
        submoduleOf_span_singleton_of_mem _ hxN₂] at this
      simpa [← span_singleton_eq_range, LinearMap.range_toSpanSingleton] using this.symm

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

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
hx : (algebraMap R (FractionRing R)) x = (algebraMap R (FractionRing R)) 0
⊢ x = 0

Tactic:
(IsFractionRing.injective R (FractionRing R)).eq_iff

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
hx : x = 0
⊢ x = 0
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
⊢ Function.Surjective ⇑f

Tactic:
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, Subtype.range_val]

Goal state after:
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
⊢ Submodule.span R ↑s = ⊤
Module: Mathlib.RingTheory.Localization.Free

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'

Tactic:
have : Module.Finite Rₛ M' := Module.Finite.of_isLocalizedModule S (Rₚ := Rₛ) f

Goal state after:
R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
I : Type u_1 := Free.ChooseBasisIndex Rₛ M'
b : Basis I Rₛ M' := Free.chooseBasis Rₛ M'
this : Module.Finite Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
a✝ : (derivedSeries G n).Characteristic
⊢ (derivedSeries G (n + 1)).Characteristic

Tactic:
exact Subgroup.commutator_characteristic _ _

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FinitePresentation R M
inst✝ : Flat R M
⊢ IsLocallyConstant (rankAtStalk M)

Tactic:
let e : freeLocus R M ≃ₜ PrimeSpectrum R :=
    (Homeomorph.setCongr freeLocus_eq_univ).trans (Homeomorph.Set.univ (PrimeSpectrum R))

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FinitePresentation R M
inst✝ : Flat R M
e : ↑(freeLocus R M) ≃ₜ PrimeSpectrum R := (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.univ (PrimeSpectrum R))
⊢ IsLocallyConstant (rankAtStalk M)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
⊢ Normal F ↥(⨆ i, t i)

Tactic:
refine { toIsAlgebraic := isAlgebraic_iSup fun i => (h i).1, splits' := fun x => ?_ }
  obtain ⟨s, hx⟩ := exists_finset_of_mem_supr'' (fun i => (h i).1) x.2
  let E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F (i.2 :)).rootSet K)
  have hF : Normal F E := by
    have : IsSplittingField F E (∏ i ∈ s, minpoly F i.snd) := by
      refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_
      · exact Finset.prod_ne_zero_iff.mpr fun i _ => minpoly.ne_zero ((h i.1).isIntegral i.2)
      · simpa [Polynomial.map_map] using! ((h i.1).splits i.2).map (algebraMap (t i.1) K)
    apply Normal.of_isSplittingField (∏ i ∈ s, minpoly F i.2)
  have hE : E ≤ ⨆ i, t i := by
    refine iSup_le fun i => iSup_le fun _ => le_iSup_of_le i.1 ?_
    rw [adjoin_le_iff, ← ((h i.1).splits i.2).image_rootSet (t i.1).val]
    exact fun _ ⟨a, _, h⟩ => h ▸ a.2
  have := hF.splits ⟨x, hx⟩
  rw [minpoly_eq, Subtype.coe_mk, ← minpoly_eq] at this
  have := this.map (inclusion hE).toRingHom -- necessary for performance reasons
  rwa [Polynomial.map_map] at this

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

Goal state before:
pp: F✝ : Type u_1
K✝ : Type u_2
inst✝¹² : Field F✝
inst✝¹¹ : Field K✝
inst✝¹⁰ : Algebra F✝ K✝
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝⁹ : Field K₁
inst✝⁸ : Field K₂
inst✝⁷ : Field K₃
inst✝⁶ : Algebra F✝ K₁
inst✝⁵ : Algebra F✝ K₂
inst✝⁴ : Algebra F✝ K₃
ϕ : K₁ →ₐ[F✝] K₂
χ : K₁ ≃ₐ[F✝] K₂
ψ : K₂ →ₐ[F✝] K₃
ω : K₂ ≃ₐ[F✝] K₃
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x : K
h : (minpoly F x).natDegree < 2
⊢ (minpoly F x).natDegree ≤ 1

Tactic:
by rwa [Nat.le_iff_lt_add_one]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ f ∈ B' ∪ {e}

Tactic:
exact Or.inl hf.1

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : B.ncard < B.ncard
⊢ False

Tactic:
exact hle.ne rfl

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
a : A
m : M
⊢ a * e ((algebraMap R A) 1 ⊗ₜ[R] m) = e (a ⊗ₜ[R] m)

Tactic:
rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right✝ : I ⊆ R
hIA : I ⊆ A
J : Set α
hJ : M.IsBasis' J A
hIJ : I ⊆ J
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J

Tactic:
use J

Goal state after:
case h
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right✝ : I ⊆ R
hIA : I ⊆ A
J : Set α
hJ : M.IsBasis' J A
hIJ : I ⊆ J
⊢ I ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

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

Tactic:
intro hXR

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
⊢ X ⊆ R → (M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X)

Tactic:
intro hXR

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
hXR : X ⊆ R
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: case refine_1
α : Type u_1
M M' : Matroid α
X : Set α
h : M ↾ X = M' ↾ X
I : Set α
hIX : I ⊆ X
⊢ M.Indep I ↔ M'.Indep I

Tactic:
rw [← and_iff_left (a := (M.Indep I)) hIX, ← and_iff_left (a := (M'.Indep I)) hIX,
      ← restrict_indep_iff, h, restrict_indep_iff]

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

Goal state before:
pp: α : Type u_1
I E R : Set α
⊢ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((uniqueBaseOn I E).Indep I_1 ∧ I_1 ⊆ R ↔ (uniqueBaseOn (I ∩ R ∩ E) R).Indep I_1)

Tactic:
uniqueBaseOn_indep_iff',

Goal state after:
α : Type u_1
I E R : Set α
⊢ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → (I_1 ⊆ I ∩ E ∧ I_1 ⊆ R ↔ I_1 ⊆ I ∩ R ∩ E ∩ R)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).Indep (f '' B)

Tactic:
simpa using hBmax.1.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hIJ : I ⊆ f ⁻¹' f '' J₀
hJ : N.Indep (f '' J₀)
hJf : f '' J₀ ⊆ range f
hJX : f '' J₀ ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → f '' J₀ ⊆ t → f '' J₀ = t
hbj : BijOn f J₀ (f '' f ⁻¹' f '' J₀)
K : Set α
hK : N.Indep (f '' K)
hKinj : InjOn f K
hKX : K ⊆ X
hJ₀K : J₀ ⊆ K
⊢ f '' J₀ = f '' K

Tactic:
hJmax hK (image_subset_range _ _)
        (image_mono hKX) (image_mono hJ₀K)

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
X I : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hIX : I ⊆ X
J₀ : Set α
hIJ₀ : I ⊆ J₀
hJ₀X : J₀ ⊆ X
hIJ : I ⊆ f ⁻¹' f '' J₀
hJ : N.Indep (f '' J₀)
hJf : f '' J₀ ⊆ range f
hJX : f '' J₀ ⊆ f '' X
hJmax : ∀ ⦃t : Set β⦄, N.Indep t → t ⊆ range f → t ⊆ f '' X → f '' J₀ ⊆ t → f '' J₀ = t
hbj : BijOn f J₀ (f '' f ⁻¹' f '' J₀)
K : Set α
hK : N.Indep (f '' K)
hKinj : InjOn f K
hKX : K ⊆ X
hJ₀K : J₀ ⊆ K
⊢ f '' K = f '' K
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
refine Indep.isBasis_of_forall_insert ?_ inter_subset_right (fun e he ↦ ?_)
  · rw [dual_indep_iff_exists]
    exact ⟨B, hB, disjoint_of_subset_left inter_subset_left disjoint_sdiff_left⟩
  simp only [sdiff_inter_self_eq_sdiff, mem_sdiff, not_and, not_not, imp_iff_right he.1.1] at he
  simp_rw [dual_dep_iff_forall, insert_subset_iff, and_iff_right he.1.1,
    and_iff_left (inter_subset_left.trans sdiff_subset)]
  refine fun B' hB' ↦ by_contra (fun hem ↦ ?_)
  rw [nonempty_iff_ne_empty, not_ne_iff, ← union_singleton, sdiff_inter_sdiff,
    union_inter_distrib_right, union_empty_iff, singleton_inter_eq_empty, sdiff_eq,
    inter_right_comm, inter_eq_self_of_subset_right hB'.subset_ground, ← sdiff_eq,
    sdiff_eq_empty] at hem
  obtain ⟨f, hfb, hBf⟩ := hB.exchange hB' ⟨he.2, hem.2⟩
  have hi : M.Indep (insert f (B ∩ X)) := by
    refine hBf.indep.subset (insert_subset_insert ?_)
    simp_rw [subset_sdiff, and_iff_right inter_subset_left, disjoint_singleton_right,
      mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]
  exact hfb.2 (hBX.mem_of_insert_indep (Or.elim (hem.1 hfb.1) (False.elim ∘ hfb.2) id) hi).1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ InjOn f B → B ⊆ E → (N.IsBasis (f '' B) N.E ↔ N.IsBase (f '' B))

Tactic:
isBasis_ground_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ InjOn f B → B ⊆ E → True
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})
⊢ e ∈ M.closure I \ I ∧ ∀ e_1 ∈ insert e I, M.Indep (insert e I \ {e_1})

Tactic:
and_iff_right ⟨he, heI⟩

Goal state after:
α : 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})
⊢ ∀ e_1 ∈ insert e I, M.Indep (insert e I \ {e_1})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
obtain rfl | hne := eq_or_ne x e
  · simp [hI.sdiff, mem_fundCircuit]
  suffices (∀ t ⊆ I, e ∈ M.closure t → x ∈ t) ↔ e ∉ M.closure (I \ {x}) by
    simpa [fundCircuit_eq_sInter hecl, hne, ← insert_sdiff_singleton_comm hne.symm,
      (hI.sdiff _).insert_indep_iff, mem_ground_of_mem_closure hecl, heI]
  refine ⟨fun h hecl ↦ (h _ sdiff_subset hecl).2 rfl, fun h J hJ heJ ↦ by_contra fun hxJ ↦ h ?_⟩
  exact M.closure_subset_closure (subset_sdiff_singleton hJ hxJ) heJ

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

Goal state before:
pp: case a
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

Tactic:
gcongr 5 with J hJI; intro heJ
    simp only [restrict_closure_eq']
    refine (inter_subset_inter_left _ ?_).trans subset_union_left
    rwa [inter_eq_self_of_subset_left (hJI.trans hIR)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
⊢ e ∈ M.loops ↔ M.IsLoop e

Tactic:
isLoop_iff

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : e ∈ M.E
⊢ e ∈ M.loops ↔ e ∈ M.loops
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.IsNonloop e ↔ M.IsLoop e

Tactic:
by
  rw [← not_isLoop_iff, not_not]

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

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

Tactic:
by
  rw [← eRk_closure_eq, closure_union_closure_right_eq, eRk_closure_eq]

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 ∈ M.closure {f}
⊢ f ∈ M.closure {e}

Tactic:
by
  rw [← union_empty {_}, singleton_union] at *
  exact (M.closure_exchange (X := ∅)
    ⟨hef, (isNonloop_iff_notMem_loops he.mem_ground).1 he⟩).1

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ∀ C ⊆ I, ¬M.IsCircuit C

Tactic:
rw [indep_iff_forall_subset_not_isCircuit', and_iff_left hI]

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 ∈ M.closure {f}
h : f ∈ M.E → M.IsLoop f
⊢ M.IsLoop e

Tactic:
isLoop_iff

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
⊢ e ∈ M.loops
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
e : α
I E : Set α
⊢ (uniqueBaseOn I E).Indep {e} ↔ e ∈ I ∩ E

Tactic:
uniqueBaseOn_indep_iff',

Goal state after:
α : Type u_1
e : α
I E : Set α
⊢ {e} ⊆ I ∩ E ↔ e ∈ I ∩ E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
hX : X ⊆ M.E
⊢ M.IsBasis I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X

Tactic:
by
  rw [← isBasis'_iff_isBasis, isBasis'_iff_indep_encard_eq_of_finite hIfin]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)

Tactic:
simp_rw [closure_eq_subtypeClosure, iUnion_inter, Subtype.coe_inj]

Goal state after:
ι : 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, ⋯⟩
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
⊢ M.IsFlat F

Tactic:
refine ⟨fun J X hJF hJX e heX ↦ show M.IsBasis _ _ from ?_, hIF.subset_ground⟩

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
J X : Set α
hJF : M.IsBasis J F
hJX : M.IsBasis J X
e : α
heX : e ∈ X
⊢ M.IsBasis I (insert e I)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X Y : Set α
⊢ (M ↾ X).cRk (Y ∩ X) = M.cRk (X ∩ Y)

Tactic:
cRk_restrict_subset _ inter_subset_right,

Goal state after:
α : Type u
M : Matroid α
X Y : Set α
⊢ M.cRk (Y ∩ X) = M.cRk (X ∩ Y)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
⊢ M.closure B = M.E

Tactic:
rw [hB.closure_eq_closure, closure_ground]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
⊢ M.Indep (insert f (B \ {e})) ∧ f ∉ B

Tactic:
by
    simpa [(hB.indep.sdiff _).notMem_closure_iff, hne] using hf

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ M.IsBasis I (insert e I)

Tactic:
hI.insert_isBasis_iff_mem_closure

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
⊢ e ∈ M.closure I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs)

Tactic:
sInter_eq_biInter

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
obtain ⟨B, hB⟩ := hI.subset_isBasis_of_subset hIS
  exact ⟨B, hB.1.isBase_of_spanning hS, hB.2, hB.1.subset⟩

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : E
hx : (aeval x) p = 0
⊢ ∃ x, eval x p = 0

Tactic:
obtain ⟨x, rfl⟩ := h ▸ mem_algebraicClosure_iff'.2 (minpoly.ne_zero_iff.1 <|
    ne_zero_of_dvd_ne_zero hmon.ne_zero (minpoly.dvd _ x hx))

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosed E
h : algebraicClosure F E = ⊥
p : F[X]
hmon : p.Monic
hirr : Irreducible p
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ ∃ x, eval x p = 0
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✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
h✝ : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
alg : ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
a : A
ha : a ∉ s
h : AlgebraicIndepOn R _root_.id (insert a s) ∧ insert a s ⊆ t
⊢ IsAlgebraic (↥(adjoin R s)) (_root_.id a)

Tactic:
exact alg _ <| h.2 <| mem_insert ..

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
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
⊢ lift.{w, u} #ι = lift.{u, w} (trdeg R A)

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.1.algebraMap_injective
  rw [← matroid_cRank_eq, ← (matroid_isBase_iff.mpr hx.to_subtype_range).cardinalMk_eq_cRank,
    lift_mk_eq'.mpr ⟨.ofInjective _ hx.1.injective⟩]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
rw [natSepDegree, ne_eq, Finset.card_eq_zero, ← ne_eq, ← Finset.nonempty_iff_ne_empty]
  use rootOfSplits (SplittingField.splits f) (degree_ne_of_natDegree_ne (by rwa [natDegree_map]))
  classical
  rw [Multiset.mem_toFinset, mem_aroots]
  exact ⟨ne_of_apply_ne _ h, by simp only [← eval_map_algebraMap, eval_rootOfSplits]⟩

Goal state after: