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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsNoetherianRing A
inst✝ : IsFractionRing A A
I : Ideal A
hI : I.IsMaximal
fin : (associatedPrimes A A).Finite
⊢ ↑I ⊆ ⋃ i ∈ associatedPrimes A A, ↑(id i)

Tactic:
simp_rw [id, biUnion_associatedPrimes_eq_compl_nonZeroDivisors]
    exact fun x hx h ↦ hI.ne_top <| I.eq_top_of_isUnit_mem hx
      (IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mp ‹_› h)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
h₄ : a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₁.asIdeal
⊢ a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₁.asIdeal

Tactic:
rwa [show p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) = p₂.asIdeal.comap _ from congr($h.1.1)]

Goal state after:
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
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))

Tactic:
have := (algebraMap R Rₛ).domain_nontrivial

Goal state after:
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
this : Nontrivial R
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))
Module: Mathlib.RingTheory.ClassGroup.Basic

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

Tactic:
have hy' : y ∈ R⁰ := mem_nonZeroDivisors_iff_ne_zero.mpr hy

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

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b = b * a

Tactic:
← mul_inv_eq_one,

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * (b * a)⁻¹ = 1
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✝² : Module.Invertible R M✝
inst✝¹ : Module.Invertible R N
inst✝ : IsLocalRing R
M : Type u
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : 1 = ∑ i ∈ S, i.1 i.2
f : Dual R M
m : M
mem : (f, m) ∈ S
hfm : IsUnit ((f, m).1 (f, m).2)
⊢ Free R M

Tactic:
exact .of_equiv <| .symm <| .ofBijective f (Invertible.bijective_of_surjective <|
    LinearMap.range_eq_top.mp <| Ideal.eq_top_of_isUnit_mem _ ⟨m, rfl⟩ hfm)

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

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

Tactic:
apply eval_gcd_eq_zero

Goal state after:
case hf
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) = 0

case hg
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β (Polynomial.map ιFE g) = 0
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : (B₁ \ insert f (B₂ \ {e})).encard ≤ ((B₂ \ B₁) \ {e}).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
← union_singleton,

Goal state after:
case inr.inr
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : (B₁ \ (B₂ \ {e} ∪ {f})).encard ≤ ((B₂ \ B₁) \ {e}).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : insert f (B \ {e}) ⊆ B'
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
have hcard := hB'.encard_sdiff_comm hB

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hIB' : insert f (B \ {e}) ⊆ B'
hcard : (B' \ B).encard = (B \ B').encard
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
by
  obtain ⟨I, hI⟩ := M.exists_isBasis X (hXY.trans hY)
  obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)
  exact ⟨_, _, hI, hJ, hIJ⟩

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 → 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₀
hch : ∀ (b : ↑(B₀ \ I)), ∃ Ib ⊆ I, Ib.Finite ∧ ¬Indep (insert (↑b) Ib)
⊢ ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)

Tactic:
choose! f hf using hch

Goal state after:
α : 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₀
f : ↑(B₀ \ I) → Set α
hf : ∀ (b : ↑(B₀ \ I)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b) (f b))
⊢ ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case h.refine_2
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ Disjoint (insert e I) B''

Tactic:
← union_singleton,

Goal state after:
case h.refine_2
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ Disjoint (I ∪ {e}) B''
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R X : Set α
⊢ (M ↾ R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R

Tactic:
rw [Dep, restrict_indep_iff, restrict_ground_eq]; tauto

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B X : Set α
M : Matroid α
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X

Tactic:
rintro X - I' ⟨hI'E, B, hB, hI'B⟩ hI'X
    obtain ⟨I, hI⟩ := M.exists_isBasis (M.E \ X)
    obtain ⟨B', hB', hIB', hB'IB⟩ := hI.indep.exists_isBase_subset_union_isBase hB
    obtain rfl : I = B' \ X := hI.eq_of_subset_indep (hB'.indep.sdiff _)
      (subset_sdiff.2 ⟨hIB', (subset_sdiff.1 hI.subset).2⟩)
      (sdiff_subset_sdiff_left hB'.subset_ground)
    simp_rw [maximal_subset_iff']
    refine ⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩
    · rw [subset_inter_iff, and_iff_left hI'E, subset_sdiff, and_iff_right hI'X]
      exact Disjoint.mono_right hB'IB <| disjoint_union_right.2
        ⟨disjoint_sdiff_right.mono_left hI'X, hI'B⟩
    · exact ⟨B', hB', (disjoint_sdiff_left (t := X)).mono_left inter_subset_left⟩
    · exact inter_subset_left.trans sdiff_subset
    simp only [subset_inter_iff, subset_sdiff, and_imp, forall_exists_index]
    refine fun J hJE B'' hB'' hdj hJX hXJ ↦ ⟨⟨hJX, ?_⟩, hJE⟩
    have hI' : (B'' ∩ X) ∪ (B' \ X) ⊆ B' := by
      rw [union_subset_iff, and_iff_left sdiff_subset, ← union_sdiff_cancel hJX,
        inter_union_distrib_left, hdj.symm.inter_eq, empty_union, sdiff_eq, ← inter_assoc,
        ← sdiff_eq, sdiff_subset_comm, sdiff_eq, inter_assoc, ← sdiff_eq, inter_comm]
      exact subset_trans (inter_subset_inter_right _ hB''.subset_ground) hXJ
    obtain ⟨B₁, hB₁, hI'B₁, hB₁I⟩ := (hB'.indep.subset hI').exists_isBase_subset_union_isBase hB''
    rw [union_comm, ← union_assoc, union_eq_self_of_subset_right inter_subset_left] at hB₁I
    obtain rfl : B₁ = B' := by
      refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)
      refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)
      refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)
      refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_
      exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))
    by_contra hdj'
    obtain ⟨e, heJ, heB'⟩ := not_disjoint_iff.mp hdj'
    obtain (heB'' | ⟨-, heX⟩) := hB₁I heB'
    · exact hdj.ne_of_mem heJ heB'' rfl
    exact heX (hJX heJ)

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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
h_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
⊢ (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.RankFinite

Tactic:
obtain ⟨B, hB⟩ := (IndepMatroid.ofBdd E Indep _ _ _ _ _).matroid.exists_isBase
  refine hB.rankFinite_of_finite ?_
  obtain ⟨n, hn⟩ := h_bdd
  exact finite_of_encard_le_coe <| hn B (by simpa using hB.indep)

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : insert e (M.E \ B ∩ (M.E \ X)) ∩ B' = ∅
⊢ False

Tactic:
← union_singleton,

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : (M.E \ B ∩ (M.E \ X) ∪ {e}) ∩ B' = ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
⊢ N ≤r M ↔ ∃ R ⊆ M.E, N = M ↾ R

Tactic:
use IsRestriction.exists_eq_restrict; rintro ⟨R, hR, rfl⟩; exact restrict_isRestriction M R hR

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

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

Tactic:
simp_rw [Coindep, dual_indep_iff_exists', and_comm (a := (_ : Set α) ⊆ _), and_congr_left_iff,
    subset_sdiff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.Finitary
⊢ (N.comapOn E f).Finitary

Tactic:
rw [comapOn]; infer_instance

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 : Matroid β
E B I : Set α
inst✝ : N.RankFinite
⊢ (N.comapOn E f).RankFinite

Tactic:
rw [comapOn]; infer_instance

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : ↑(emptyOn α).E ↪ β
⊢ range ⇑f = (emptyOn β).E ∧
    ∀ (I : Set β), (emptyOn β).Indep I ↔ (emptyOn α).Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
simp only [emptyOn_ground] at f

Goal state after:
case inl
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : ↑∅ ↪ β
⊢ range ⇑f = (emptyOn β).E ∧
    ∀ (I : Set β), (emptyOn β).Indep I ↔ (emptyOn α).Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
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})
f : α
hfI : f ∈ I
⊢ e ∉ I \ {f}

Tactic:
simp [heI]

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

Goal state before:
pp: α : Type u_1
I : Set α
e : α
M : Matroid α
heI : e ∉ I
⊢ e ∉ M.fundCircuit e I ∩ I

Tactic:
simp [heI]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ M.fundCircuit e X = {e}

Tactic:
suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
    simpa [subset_antisymm_iff, fundCircuit]
  exact fun b hbX h ↦ h _ (singleton_subset_iff.2 heX) Subset.rfl

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 : Matroid β
M : Matroid α
E : Set β
e : ↑M.E ≃ ↑E
I : Set β
⊢ Subtype.val ∘ ⇑e ⁻¹' I = ⇑e.symm '' E ↓∩ I

Tactic:
by ext; simp

Goal state after:
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
heI : e ∈ I
⊢ insert e I ⊆ I

Tactic:
simp [heI]

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

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

Tactic:
← union_singleton,

Goal state after:
α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk (M.closure X ∪ {e}) = M.eRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
← union_singleton,

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

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

Tactic:
← union_singleton,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
⊢ M.eRk (I ∪ {e}) = M.eRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
by
  rw [insert_inter_distrib, insert_union_distrib]
  apply M.eRk_submod

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis I X

Tactic:
rw [← hJX.encard_eq_eRk] at hI

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
refine ⟨fun h ↦ ⟨h.eRk_eq.symm.le, h.subset_ground⟩, fun ⟨h, hX⟩ ↦ ?_⟩
  obtain ⟨I, hI⟩ := M.exists_isBasis X
  exact (hI.indep.isBase_of_eRk_ge
    hI.indep.finite (h.trans hI.eRk_eq_eRk.symm.le)).spanning_of_superset hI.subset

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ M.closure (insert e X) = insert e (M.closure X)

Tactic:
← union_singleton,

Goal state after:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ M.closure (X ∪ {e}) = insert e (M.closure X)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
hK : K ⊆ M.coloops
⊢ M.closure K = K ∪ M.loops

Tactic:
← empty_union K,

Goal state after:
α : Type u_1
M : Matroid α
K : Set α
hK : K ⊆ M.coloops
⊢ M.closure (∅ ∪ K) = ∅ ∪ K ∪ M.loops
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
obtain ⟨C, hC, hC', -⟩ := hC₁.strong_elimination hC₂ he₁ he₂ hf₁ hf₂

Goal state after:
case pos
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
hnss : ¬C₁ ⊆ C₂
f : α
hf₁ : f ∈ C₁
hf₂ : f ∉ C₂
he₁ : e ∈ C₁
he₂ : e ∈ C₂
C : Set α
hC : C ⊆ (C₁ ∪ C₂) \ {e}
hC' : M.IsCircuit C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
e : α
X : Set α
⊢ M.cRk (insert e (M.closure X)) = M.cRk (insert e X)

Tactic:
← union_singleton,

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
e : α
X : Set α
⊢ M.cRk (M.closure X ∪ {e}) = M.cRk (insert e X)
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
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
key : aeval x = (Polynomial.aeval (x default)).comp ↑i
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Tactic:
simp [key]

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

Goal state before:
pp: α : 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})
⊢ I = insert e (I \ {e})

Tactic:
simp [heI]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ I = insert e (I \ {e})

Tactic:
simp [heI]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
⊢ M.closure (I \ X) ⊂ M.closure I

Tactic:
by
  refine hI.closure_ssubset_closure <| sdiff_subset.ssubset_of_ne fun h ↦ ?_
  rw [sdiff_eq_left, disjoint_iff_inter_eq_empty] at h
  simp [h] at hX

Goal state after: