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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical ∈ (N.colon {x}).radical.minimalPrimes

Tactic:
Ideal.minimalPrimes_eq_subsingleton_self,

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical ∈ {(N.colon {x}).radical}
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Function.Injective ⇑(LinearMap.lTensor P (Submodule.subtype 𝔪))

Tactic:
apply lTensor_injective_of_exact_of_exact_of_rTensor_injective
    h hg (LinearMap.exact_subtype_mkQ 𝔪) (Submodule.mkQ_surjective _)
    ((LinearMap.lTensor_inj_iff_rTensor_inj _ _).mp hf)
    (Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective)

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
H : ∀ (n : ℕ) (h : n < s.length + 1), motive ↥(s.toFun ⟨n, h⟩)
⊢ motive M

Tactic:
replace H : motive s.last := H s.length s.length.lt_add_one

Goal state after:
A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
H : motive ↥s.last
⊢ motive M
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf : IsLocallyConstant f
g : ↑C₂ → Z
hg : IsLocallyConstant g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg } ⟨x, ⋯⟩
⊢ IsLocallyConstant fun i ↦
    if hi : i ∈ C₁ then { toFun := f, isLocallyConstant := hf } ⟨i, hi⟩
    else { toFun := g, isLocallyConstant := hg } ⟨i, ⋯⟩

Tactic:
rw [IsLocallyConstant.iff_continuous] at hf hg ⊢

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
⊢ Continuous[inst✝¹, dZ] fun i ↦
    if hi : i ∈ C₁ then { toFun := f, isLocallyConstant := hf✝ } ⟨i, hi⟩
    else { toFun := g, isLocallyConstant := hg✝ } ⟨i, ⋯⟩
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
⊢ ∀ ⦃I : Set α⦄, M.Indep I ↔ ∃ B, Maximal M.Indep B ∧ I ⊆ B

Tactic:
by
    refine fun I ↦ ⟨fun h ↦ ?_, fun ⟨B, ⟨h, _⟩, hIB'⟩ ↦ M.indep_subset h hIB'⟩
    obtain ⟨J, hIJ, hmax⟩ := M.indep_maximal M.E rfl.subset I h (M.subset_ground I h)
    rw [maximal_and_iff_right_of_imp M.subset_ground] at hmax
    exact ⟨J, hmax.1, hIJ⟩

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

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B : Set α
hB : Maximal (fun K ↦ M.Indep K ∧ K ⊆ M.E) B
⊢ ∃ B, Maximal M.Indep B

Tactic:
rw [maximal_and_iff_right_of_imp M.subset_ground] at hB

Goal state after:
α : Type u_1
M : IndepMatroid α
B : Set α
hB : Maximal M.Indep B ∧ B ⊆ M.E
⊢ ∃ B, Maximal M.Indep B
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp.refine_1
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
this : R ∙ ↑(e 1) * ↑(e' 1) = 1
⊢ ∃ b, (↑e 1).1 * b = 1

Tactic:
have ⟨r, hr⟩ := span_singleton_eq_one_iff.mp this

Goal state after:
case mp.refine_1
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
this : R ∙ ↑(e 1) * ↑(e' 1) = 1
r : Rˣ
hr : ↑(e 1) * ↑(e' 1) = (algebraMap R A) ↑r
⊢ ∃ b, (↑e 1).1 * b = 1
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp.refine_2
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
this : R ∙ ↑(e' 1) * ↑(e 1) = 1
⊢ ∃ c, c * (↑e 1).1 = 1

Tactic:
have ⟨r, hr⟩ := span_singleton_eq_one_iff.mp this

Goal state after:
case mp.refine_2
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
this : R ∙ ↑(e' 1) * ↑(e 1) = 1
r : Rˣ
hr : ↑(e' 1) * ↑(e 1) = (algebraMap R A) ↑r
⊢ ∃ c, c * (↑e 1).1 = 1
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
⊢ F⟮α⟯ = ⊤ ↔ ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ

Tactic:
refine ⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ,
    fun h ↦ eq_of_le_of_finrank_eq' le_top ?_⟩

Goal state after:
F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
⊢ finrank (↥F⟮α⟯) E = finrank (↥⊤) E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ (∀ (e_1 : α), e_1 = e ∧ e_1 ∉ I ∨ False → ¬M.Indep (insert e_1 I) ∧ e_1 ∈ M.E) ↔
    ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I

Tactic:
or_false,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ (∀ (e_1 : α), e_1 = e ∧ e_1 ∉ I → ¬M.Indep (insert e_1 I) ∧ e_1 ∈ M.E) ↔ ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
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₀
f : ↑(B₀ \ I) → Set α
hf : ∀ (b : ↑(B₀ \ I)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b) (f b))
this : Finite ↑(B₀ \ I)
⊢ ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)

Tactic:
refine ⟨iUnion f ∪ (B₀ ∩ I),
          union_subset (iUnion_subset (fun i ↦ (hf i).1)) inter_subset_right,
          (finite_iUnion fun i ↦ (hf i).2.1).union (hB₀fin.subset inter_subset_left),
          fun x ⟨hxB₀, hxn⟩ hi ↦ ?_⟩

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))
this : Finite ↑(B₀ \ I)
x : α
x✝ : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
⊢ ∀ X ⊆ ∅, ExistsMaximalSubsetProperty (fun x ↦ x = ∅) X

Tactic:
rintro _ _ _ rfl -; exact ⟨∅, by simp [Maximal]⟩

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

Goal state before:
pp: α : Type u_1
I E R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R ∩ E) R

Tactic:
simp_rw [ext_iff_indep, restrict_ground_eq, uniqueBaseOn_ground, true_and,
    restrict_indep_iff, uniqueBaseOn_indep_iff', subset_inter_iff]

Goal state after:
α : Type u_1
I E R : Set α
⊢ ∀ ⦃I_1 : Set α⦄, I_1 ⊆ R → ((I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R)
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:
by
  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:
by
  rw [comapOn]; infer_instance

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}))

Tactic:
refine (hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}

case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

case refine_3
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ f ∈ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}, e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr
α : 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
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}) ⊆ C

Tactic:
refine insert_subset heC <| (sInter_subset_of_mem (t := C \ {e}) ?_).trans sdiff_subset

Goal state after:
case inr
α : 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
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ C \ {e} ∈ {J | J ⊆ I ∧ e ∈ M.closure J}
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
by
  simp [union_comm]

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ i, I i)

Tactic:
refine mem_of_mem_of_subset (hJx.mem_closure_sdiff_singleton_of_mem (.inl hzJ))
    (M.closure_subset_closure (subset_trans ?_ subset_union_left))

Goal state after:
case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ (J ∪ range x) \ {z} ⊆ range x ∪ J \ {z}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X < ⊤ ↔ M.IsRkFinite X

Tactic:
by
  rw [lt_top_iff_ne_top, eRk_ne_top_iff]

Goal state after:
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
J X : Set α
hJF : M.IsBasis J F
hJX : M.IsBasis J X
e : α
heX : e ∈ X
⊢ M.IsBasis I (insert e I)

Tactic:
exact (hIF.isBasis_of_isBasis_of_subset_of_subset (hJX.isBasis_union hJF) hJF.subset
      (hIF.subset.trans subset_union_right)).isBasis_subset (subset_insert _ _)
      (insert_subset (Or.inl heX) (hIF.subset.trans subset_union_right))

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Dep (insert e I) ↔ M.Dep (insert e I) ∧ e ∉ I ∨ False

Tactic:
or_false,

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Dep (insert e I) ↔ M.Dep (insert e I) ∧ e ∉ I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
C : Set α
hC : M.IsCircuit C
hCs : C.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x

Tactic:
obtain (rfl | ⟨e, rfl⟩) := hCs.eq_empty_or_singleton

Goal state after:
case inl
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
hC : M.IsCircuit ∅
hCs : ∅.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x

case inr
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
e : α
hC : M.IsCircuit {e}
hCs : {e}.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case neg
α : 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)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
⊢ B ⊆ B ∩ B' ∪ U

Tactic:
have hUB : (B ∩ B') ∪ U ⊆ B :=
    union_subset inter_subset_left (iUnion_subset fun e ↦ (hSB e.1 e.2))

Goal state after:
case neg
α : 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)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
hUB : B ∩ B' ∪ U ⊆ B
⊢ B ⊆ B ∩ B' ∪ U
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case pos
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∈ M.E
⊢ M.fundCocircuit e X = {e}

pp: case neg
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∉ M.E
⊢ M.fundCocircuit e X = {e}

Tactic:
· rw [fundCocircuit, fundCircuit_eq_of_mem]
    exact ⟨he, heX⟩

Goal state after:
case neg
α : Type u_1
X : Set α
e : α
M : Matroid α
heX : e ∉ X
he : e ∉ M.E
⊢ M.fundCocircuit e X = {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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : (eval₂Hom ((algebraMap S B).comp ↑f) fun i ↦ ↑g (x i)) p = 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0

Tactic:
← eval₂Hom_map_hom,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : (eval₂Hom (algebraMap S B) fun i ↦ ↑g (x i)) ((MvPolynomial.map ↑f) p) = 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0
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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ (eval₂Hom ((algebraMap S B).comp ↑f) fun i ↦ ↑g (x i)) q = 0

Tactic:
← eval₂Hom_map_hom,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ (eval₂Hom (algebraMap S B) fun i ↦ ↑g (x i)) ((MvPolynomial.map ↑f) q) = 0
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case mp
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) →
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

Tactic:
rintro ⟨⟨x, hxE, rfl⟩, h2⟩

Goal state after:
case mp
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
⊢ ∃ x_1, (x_1 ∈ M.E ∧ (M.Indep (insert x_1 I) → x_1 ∈ I)) ∧ f x_1 = f x
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
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (algebraicClosure F K) ↔ x ∈ algebraicClosure F E

Tactic:
exact map_mem_algebraicClosure_iff i

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 α
inst✝ : FaithfulSMul G α
g h : G
disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)
comm : Commute g h
⊢ g = 1

Tactic:
rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ,
    compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint

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:
by
  simp_rw [← matroid_spanning_iff, ← matroid_isBase_iff, and_comm (a := _ ⊆ s)]
  exact Matroid.spanning_iff_exists_isBase_subset (subset_univ _)

Goal state after: