mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ x ∈
      ((fun q ↦
            {
              asIdeal :=
                RingHom.ker
                  (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
              isPrime := ⋯ })
          ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal ↔
    x ∈ q.asIdeal

Tactic:
have := @PrimeSpectrum.isPrime

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type ?u.120} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ x ∈
      ((fun q ↦
            {
              asIdeal :=
                RingHom.ker
                  (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
              isPrime := ⋯ })
          ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal ↔
    x ∈ q.asIdeal
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: ⊢ Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]

Tactic:
decide

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: ⊢ Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]

Tactic:
decide

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
⊢ Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]

Tactic:
decide

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
⊢ Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]

Tactic:
decide

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
⊢ Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]

Tactic:
decide

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
⊢ Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]

Tactic:
decide

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
⊢ { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ } =
    { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ } *
        ⁅{ toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ },
          { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ } *
              { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ } *
            { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }⁻¹⁆ *
      { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }⁻¹

Tactic:
decide

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ x ≠ 1

Tactic:
decide

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ ∃ α, F⟮α⟯ = ⊤

Tactic:
use α

Goal state after:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ F⟮↑α⟯ = ⊤
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
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K)) = ⊤

Tactic:
eq_top_iff,

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ ⊤ ≤ Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K))
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
p_linear : Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
⊢ β ∈ F⟮γ⟯

Tactic:
by
    have finale : β = algebraMap F⟮γ⟯ E (-p.coeff 0 / p.coeff 1) := by
      simp [map_div₀, map_neg, ← coeff_map, ← coeff_map, p_linear,
        mul_sub, coeff_C, mul_div_cancel_left₀ β (mt leadingCoeff_eq_zero.mp h_ne_zero)]
    rw [finale]
    exact Subtype.mem (-p.coeff 0 / p.coeff 1)

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
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
i : ι
⊢ (Polynomial.map (algebraMap F ↥(t i)) (minpoly F x)).Splits

Tactic:
← minpoly.algHom_eq (inclusion (iInf_le t i)) (inclusion (iInf_le t i)).injective

Goal state after:
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
i : ι
⊢ (Polynomial.map (algebraMap F ↥(t i)) (minpoly F ((inclusion ⋯) x))).Splits
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ M.RankPos

Tactic:
rw [rankPos_iff]

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
h : B.Nonempty
⊢ ¬M.IsBase ∅
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I (M.E \ B)
⊢ I ⊆ B

pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B

Tactic:
← subset_compl_iff_disjoint_right,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : I ⊆ (M.E \ B)ᶜ
⊢ I ⊆ B

case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
hIb : M.IsBase I
⊢ False

Tactic:
obtain ⟨I', hII', hI', hne⟩ := hInotmax

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hIb : M.IsBase I
I' : Set α
hII' : M.Indep I'
hI' : I ⊆ I'
hne : ¬I = I'
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : X ⊆ M.E
J : Set α
hJ : I ⊆ J
hJmax : Maximal (fun K ↦ M.Indep K ∧ K ⊆ X) J
⊢ ∃ J, M.IsBasis J X ∧ I ⊆ J

Tactic:
exact ⟨J, ⟨hJmax, hX⟩, hJ⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ M.IsBasis (I ∪ I') Y

Tactic:
union_eq_self_of_subset_left hII'

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ M.IsBasis I' Y
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
⊢ ∃ J, I' ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (M.E \ X)

Goal state after:
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
I : Set α
hI : M.IsBasis I (M.E \ X)
⊢ ∃ J, I' ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_1
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ I' ⊆ X \ B' ∧ I' ⊆ M.E

Tactic:
and_iff_left hI'E,

Goal state after:
case refine_1
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
⊢ I' ⊆ X \ B'
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
⊢ (emptyOn α)✶ = emptyOn α

Tactic:
rw [← ground_eq_empty_iff]; rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E

Tactic:
rw [dual_isBase_iff, and_iff_left h]

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

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

Tactic:
← isBasis_ground_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ (N.comap f).IsBasis B (N.comap f).E ↔ N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
f : α
hf : f ∈ I
hne : f ≠ e
⊢ False

Tactic:
exact h f hf (mem_closure_of_mem' _ (by simp [heI, hne.symm]))

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 β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
⊢ ∃ I₀_1, M.Indep I₀_1 ∧ f '' I₀ = f '' I₀_1

Tactic:
refine ⟨I₀, indep_of_forall_finite_subset_indep _ fun J₀ hJ₀I₀ hJ₀ ↦ ?_, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I₀ : Set α
hI₀E : I₀ ⊆ M.E
hI : ∀ J ⊆ f '' I₀, J.Finite → (M.map f hf).Indep J
h' : f '' I₀ ⊆ f '' M.E
J₀ : Set α
hJ₀I₀ : J₀ ⊆ I₀
hJ₀ : J₀.Finite
⊢ M.Indep J₀
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
J : Set α
hJ : M.IsBasis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

Tactic:
← hJ.encard_eq_eRk

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
J : Set α
h : n ≤ J.encard
hJ : M.IsBasis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
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:
rw [closure, inter_eq_self_of_subset_left hX]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
he : M.IsColoop e
⊢ e ∈ M.closure X ↔ e ∈ X

Tactic:
rw [he.mem_closure_iff_mem]

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.IsBasis I (insert e I) ↔ e ∈ M.closure I

Tactic:
by
  rw [hI.closure_eq_setOfPred_isBasis_insert, mem_ofPred]

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
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
suffices aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T by
    obtain ⟨T, hT, hTfin, hXT⟩ := aux
    obtain ⟨I, hI⟩ := M.exists_isBasis' T
    exact ⟨_, hI.subset.trans hT, hTfin.subset hI.subset, hI.indep, by rwa [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 ⊆ Y, T.Finite ∧ X ⊆ M.closure T
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Indep B ∧ M.closure B = M.E

Tactic:
← isBasis_ground_iff,

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBasis B M.E ↔ M.Indep B ∧ M.closure B = M.E
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
Transcendental,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ ¬IsAlgebraic R ((Polynomial.aeval (X i)) f)
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
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ False

Tactic:
obtain rfl := hI.eq_of_isBasis (hfb.isBasis_subset (insert_subset hfIJ.1
    (by (rw [sdiff_subset_iff, singleton_union]; exact hJI.subset))) (subset_insert _ _))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M✶.RankPos ↔ ∃ C, M.IsCircuit C

Tactic:
by
  rw [rankPos_iff, dual_isBase_iff, sdiff_empty, not_iff_comm, not_exists,
    ← ground_indep_iff_isBase, indep_iff_forall_subset_not_isCircuit]
  exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.RankPos ↔ ∃ K, M.IsCocircuit K

Tactic:
by
  rw [← dual_dual M, dual_rankPos_iff_exists_isCircuit, dual_dual M]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ Transcendental R ((Polynomial.aeval (X i)) f) → Transcendental R f

Tactic:
Transcendental,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ ¬IsAlgebraic R ((Polynomial.aeval (X i)) f) → ¬IsAlgebraic R f
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e = f ∨ e ∈ I
⊢ M.Indep (insert f I \ {e})

Tactic:
obtain rfl | heI := heI

Goal state after:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
hfI : e ∈ M.closure I
he : e ∈ M.closure (insert e I \ {e})
⊢ M.Indep (insert e I \ {e})

case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e})
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.E ⊆ M.closure T

Tactic:
← hS.closure_eq

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
⊢ M.IsBase I

Tactic:
obtain ⟨B, hB, hBI⟩ := hIs.exists_isBase_subset; rwa [← hB.eq_of_subset_indep hI hBI]

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

Goal state before:
pp: α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M = M'

Tactic:
by
  have hsp' : M.Spanning = M'.Spanning := by
    ext S
    refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE])
      (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
      (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
  rw [← dual_inj, ext_iff_indep, dual_ground, dual_ground, and_iff_right h]
  intro I hIE
  rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]

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

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∈ I
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x

Tactic:
simp [hxI, show ∃ y ∈ I, f y = f x from ⟨x, hxI, rfl⟩]

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
x : α
⊢ (g * h⁻¹) • x = h⁻¹ • x ↔ x ∈ fixedBy α g

Tactic:
comm.inv_right,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ (h⁻¹ * g) • x = h⁻¹ • x ↔ x ∈ fixedBy α g
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
S : Type v
inst✝¹ : CommRing S
inst✝ : IsDomain S
this : lift.{u, max u v} (trdeg S (MvPolynomial ι S)) = lift.{max u v, u} #ι
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι

Tactic:
lift_id',

Goal state after:
ι : Type u
S : Type v
inst✝¹ : CommRing S
inst✝ : IsDomain S
this : trdeg S (MvPolynomial ι S) = lift.{max u v, u} #ι
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
x : AlgebraicClosure F
hf : f ≠ 0 ∧ (aeval x) f = 0
hg : g ≠ 0 ∧ (aeval x) g = 0
u v : F[X]
hfg : u * f + v * g = 1
⊢ False

Tactic:
simpa only [map_add, map_mul, map_one, hf.2, hg.2, mul_zero, add_zero,
    zero_ne_one] using congr(aeval x $hfg)

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
x₀ : R
U : Set M
h : U = {0}
⊢ ∃
    V ∈
      (have this := default;
        this).sets,
    V ⊆ (fun x ↦ x₀ • x) ⁻¹' U

Tactic:
use {0}, rfl

Goal state after:
case right
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
x₀ : R
U : Set M
h : U = {0}
⊢ {0} ⊆ (fun x ↦ x₀ • x) ⁻¹' U
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ Cardinal.toNat (insepDegree F F) = 1

Tactic:
insepDegree_self,

Goal state after:
F : Type u
inst✝ : Field F
⊢ Cardinal.toNat 1 = 1
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:
eq_top_iff,

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⟮α⟯ = ⊤
⊢ ⊤ ≤ Algebra.adjoin F ((minpoly F α).rootSet E)
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
⊢ insepDegree F ↥⊥ = 1

Tactic:
insepDegree_self,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} 1
⊢ insepDegree F ↥⊥ = 1