mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
⊢ (piecewise h₁ h₂ h f g hfg) x = g ⟨x, hx⟩

Tactic:
simp only [piecewise,
    coe_mk]
  split_ifs with h
  · exact hfg x ⟨h, hx⟩
  · rfl

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩

Tactic:
let : ∀ j : C₀, Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) Iff.rfl

Goal state after:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩

Tactic:
let : ∀ j : C₀, Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) Iff.rfl

Goal state after:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case mp
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₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
q₁ : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (preimageEquivFiber R S p) ((preimageEquivFiber R S p).symm q₁) ≤ (preimageEquivFiber R S p) q₂ →
    (preimageEquivFiber R S p).symm q₁ ≤ q₂

Tactic:
obtain ⟨q₂, rfl⟩ := (preimageEquivFiber R S p).symm.surjective q₂

Goal state after:
case mp
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₁ q₂ : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (preimageEquivFiber R S p) ((preimageEquivFiber R S p).symm q₁) ≤
      (preimageEquivFiber R S p) ((preimageEquivFiber R S p).symm q₂) →
    (preimageEquivFiber R S p).symm q₁ ≤ (preimageEquivFiber R S p).symm q₂
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
⊢ IsSolvable G

Tactic:
obtain ⟨n, hn⟩ := id hG''

Goal state after:
G : Type u_1
inst✝² : Group G
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ IsSolvable G
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_1
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
f : L →ₐ[F] L
⊢ map f K ≤ ⨆ f, map (↑f) K

Tactic:
exact le_iSup_of_le (f.restrictNormal' L)
      (fun b ⟨a, h⟩ ↦ ⟨a, h.1, h.2 ▸ f.restrictNormal_commutes L a⟩)

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx✝ : AlgebraicIndependent R x
s : Set ι
hx : AlgebraicIndepOn R x s
⊢ (range fun i ↦ x ↑i) = x '' s

Tactic:
by aesop

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
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 => ?_ }

Goal state after:
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)
x : ↥(⨆ i, t i)
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits
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)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
hF : Normal F ↥E
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits

Tactic:
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

Goal state after:
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)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
hF : Normal F ↥E
hE : E ≤ ⨆ i, t i
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
⊢ Finite (IntermediateField F E)

Tactic:
let g : IntermediateField F E → G := fun K ↦
    ⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| .of_finite K α).map _, by
      convert! Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)
      rw [Polynomial.map_map]; rfl⟩

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G := fun K ↦ ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
⊢ Finite (IntermediateField F E)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : X ⊆ M.E
⊢ M.IsBasis I X

Tactic:
by
  rw [isBasis_iff (by aesop_mat : X ⊆ M.E), and_iff_right hI, and_iff_right hIX]
  exact fun J hJ hIJ hJX ↦ hIJ.antisymm (hmax hJ hIJ hJX)

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

Goal state before:
pp: case refine_2
α : 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
⊢ ∃ B, M.IsBase B ∧ Disjoint (X \ B' ∩ M.E) B

pp: case refine_3
α : 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
⊢ X \ B' ∩ M.E ⊆ X

pp: case refine_4
α : 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
⊢ ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E

Tactic:
· exact ⟨B', hB', (disjoint_sdiff_left (t := X)).mono_left inter_subset_left⟩

Goal state after:
case refine_3
α : 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
⊢ X \ B' ∩ M.E ⊆ X

case refine_4
α : 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
⊢ ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint t B) ∧ t ⊆ X → X \ B' ∩ M.E ⊆ t → t ⊆ X \ B' ∩ M.E
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

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

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).matroid.RankFinite

Tactic:
rw [IndepMatroid.ofBddAugment]
  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✝ 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
⊢ J₀ = K

Tactic:
← hKinj.image_eq_image_iff hJ₀K Subset.rfl,

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 '' J₀ = f '' K
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
obtain ⟨B, hB⟩ := (N.comap f).exists_isBase
  refine hB.rankFinite_of_finite ?_
  simp only [comap_isBase_iff] at hB
  exact (hB.1.indep.finite.of_finite_image hB.2.1)

Goal state after:
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})
⊢ M.fundCircuit e I ⊆ C

Tactic:
have heI : e ∈ M.closure I := M.closure_subset_closure hCeI heCcl

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
⊢ M.fundCircuit e I ⊆ C
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
E : Set α
M : Matroid α
hM : M.E = E
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E

Tactic:
rw [← hM, restrictSubtype_dual]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ Monotone M.eRk

Tactic:
rintro X Y (hXY : X ⊆ Y)

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
⊢ M.eRk X ≤ M.eRk Y
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ M.Indep {f e} ∧ InjOn f {e} ↔ M.IsNonloop (f e)

Tactic:
indep_singleton,

Goal state after:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ M.IsNonloop (f e) ∧ InjOn f {e} ↔ M.IsNonloop (f e)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
eRk_ne_top_iff

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite X ↔ M.IsRkFinite X
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:
rw [← isBasis'_iff_isBasis, isBasis'_iff_indep_encard_eq_of_finite hIfin]

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
x✝ : ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
e : α
heX : e ∈ X
he : M.IsNonloop e
hXe : X ⊆ M.closure {e}
⊢ M.eRk X = 1

Tactic:
← he.eRk_eq

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
x✝ : ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
e : α
heX : e ∈ X
he : M.IsNonloop e
hXe : X ⊆ M.closure {e}
⊢ M.eRk X = M.eRk {e}
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
⊢ (∀ i ∈ Js, M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)

Tactic:
have hiI := hI.subset hiX

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)
⊢ (∀ i ∈ Js, M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M✶.closure (M.E \ B)

Tactic:
hB.compl_isBase_dual.closure_eq,

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M✶.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ M.IsCocircuit (M.fundCocircuit e B)

Tactic:
by
  apply hB.compl_isBase_dual.indep.fundCircuit_isCircuit _ (by simp [he])
  rw [hB.compl_isBase_dual.closure_eq, dual_ground]
  exact hB.subset_ground he

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
⊢ AlgebraicIndependent R ![x i]

Tactic:
← FinVec.map_eq

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
this : AlgebraicIndependent R (FinVec.map x ![i])
⊢ AlgebraicIndependent R ![x i]
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: 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})

Tactic:
rw [Indep.insert_sdiff_indep_iff (hI.subset (sdiff_subset ..)) heI]

Goal state after:
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
⊢ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: 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
h : f ∈ M.closure (I \ {e})
⊢ e ∈ M.closure (I \ {e})

Tactic:
exact closure_insert_eq_of_mem_closure h ▸ M.closure_subset_closure (by intro; simp_all) he

Goal state after:
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
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0
p : MvPolynomial ι R
hp : (aeval f) p = 0
⊢ (aeval fun i ↦ (aeval x) (f i)) p = 0

Tactic:
rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ X
heE : e ∈ M.E
⊢ e ∈ M.closure (X \ {e}) ↔ M.closure (X \ {e}) = M.closure X

Tactic:
by
  simpa using subset_closure_sdiff_iff_closure_eq (Y := {e}) (X := X) (by simpa)

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

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
spanning_iff_exists_isBase_subset',

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E ↔ ∃ B, M.IsBase B ∧ B ⊆ S
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
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
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : y = x
⊢ x ∈ I

Tactic:
← hfy

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
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : y = x
⊢ y ∈ I
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_2.none
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X none)) = (aeval fun o ↦ o.elim a x) (X none)

Tactic:
rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]

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

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
⊢ g • a ∈ s ↔ a ∈ s

Tactic:
constructor <;> (intro; apply s_subset)

Goal state after:
case mp
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : g • a ∈ s
⊢ a ∈ (fixedBy α g)ᶜ

case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ g • a ∈ (fixedBy α g)ᶜ
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
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o ↦ o.elim a x
y : ι
⊢ x y ∈ range fun o ↦ o.elim a x

Tactic:
exact ⟨some y, rfl⟩

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✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (matroid R A).closure s = s ↔ ∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s

Tactic:
matroid_closure_eq

Goal state after:
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 : Set A
⊢ ↑(algebraicClosure (↥(adjoin R s)) A) = s ↔ ∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
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 : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
fin : (matroid R A).cRank < ℵ₀
⊢ IsTranscendenceBasis R x

Tactic:
← Matroid.rankFinite_iff_cRank_lt_aleph0

Goal state after:
ι : 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 : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
fin : (matroid R A).RankFinite
⊢ IsTranscendenceBasis R x
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ ⋂₀ F.sets ⊆ {1} → {1} ⊆ ⋂₀ F.sets

Tactic:
rintro -

Goal state after:
G : Type u
inst✝ : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ {1} ⊆ ⋂₀ F.sets
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm✝ : f.Monic
x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m
m n : ℕ
y : F
hm : m ≠ 0
h : f = (X ^ q ^ n - C y) ^ m
⊢ f.natSepDegree = 1

Tactic:
simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]

Goal state after: