mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case pos
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : adjoin F (⨆ x, (minpoly F x).rootSet L) = ⊤
x : L
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L
y : K
hx : x ∈ (minpoly F y).rootSet L
iy : IsIntegral F y
⊢ (Polynomial.map (algebraMap F L') (minpoly F x)).Splits

pp: case neg
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : adjoin F (⨆ x, (minpoly F x).rootSet L) = ⊤
x : L
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L
y : K
hx : x ∈ (minpoly F y).rootSet L
iy : ¬IsIntegral F y
⊢ (Polynomial.map (algebraMap F L') (minpoly F x)).Splits

Tactic:
· exact (splits y).of_dvd (map_ne_zero (minpoly.ne_zero iy))
      ((map_dvd_map' _).mpr (minpoly.dvd F x (mem_rootSet.mp hx).2))

Goal state after:
case neg
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : adjoin F (⨆ x, (minpoly F x).rootSet L) = ⊤
x : L
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L
y : K
hx : x ∈ (minpoly F y).rootSet L
iy : ¬IsIntegral F y
⊢ (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
⊢ IsNormalClosure F K ↥(normalClosure F K L)

Tactic:
have ⟨φ⟩ := ne
  apply (h.toIsAlgebraic.of_injective φ φ.injective).isNormalClosure_normalClosure
  simp_rw [← minpoly.algHom_eq _ φ.injective]
  exact fun _ ↦ h.splits _

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M = N ↔ Pic.mk R M.AsModule = N

Tactic:
mk_eq_self

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M = N ↔ M = N
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M : Pic R
⊢ M⁻¹ = (Pic.mk R M.AsModule)⁻¹

Tactic:
mk_eq_self

Goal state after:
R : Type u
inst✝ : CommSemiring R
M : Pic R
⊢ M⁻¹ = M⁻¹
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M * N = M * Pic.mk R N.AsModule

Tactic:
mk_eq_self

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M * N = M * N
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
A : Type u_5
B : Type u_6
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : Algebra R A
x✝¹ x✝ : Pic R
⊢ Pic.mk R x✝¹.AsModule * Pic.mk R x✝.AsModule = x✝¹ * x✝

Tactic:
mk_eq_self

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

Goal state before:
pp: R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ (AlgebraicIndependent R Subtype.val ∧
      ∀ (s_1 : Set A), AlgebraicIndepOn R _root_.id s_1 → range Subtype.val ⊆ s_1 → range Subtype.val = s_1) ↔
    AlgebraicIndepOn R _root_.id s ∧ ∀ ⦃y : Set A⦄, AlgebraicIndepOn R _root_.id y → s ⊆ y → s = y

Tactic:
Subtype.range_val

Goal state after:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ (AlgebraicIndependent R Subtype.val ∧ ∀ (s_1 : Set A), AlgebraicIndepOn R _root_.id s_1 → s ⊆ s_1 → s = s_1) ↔
    AlgebraicIndepOn R _root_.id s ∧ ∀ ⦃y : Set A⦄, AlgebraicIndepOn R _root_.id y → s ⊆ y → s = y
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
⊢ ∃ σ, σ x = y

Tactic:
set f : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := algEquiv hx (eq_of_root hy h_ev)

Goal state after:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
⊢ ∃ σ, σ x = y
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}))
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset

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'
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset

Goal state after:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
⊢ I ≠ B'

Tactic:
(rintro rfl; exact hI' hB')

Goal state after:
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
⊢ (range fun ψ ↦ ψ α).toFinset.card = Finset.univ.card ↔ Function.Injective fun ψ ↦ ψ α

Tactic:
toFinset_range,

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
⊢ (Finset.image (fun ψ ↦ ψ α) Finset.univ).card = Finset.univ.card ↔ Function.Injective fun ψ ↦ ψ α
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ B ∩ X ⊆ I

Tactic:
by rw [hI.eq_of_subset_indep (hB.indep.inter_right X) (subset_inter hIB hI.subset)
    inter_subset_right]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

Tactic:
by
  rw [IsBasis, maximal_iff_forall_insert (fun I J hI hIJ ↦ ⟨hI.1.subset hIJ, hIJ.trans hI.2⟩)]
  simp only [hI, hIX, and_self, insert_subset_iff, and_true, not_and, true_and, mem_sdiff, and_imp,
    Dep, hI.subset_ground]
  exact ⟨fun h e heX heI ↦ ⟨fun hi ↦ h.1 e heI hi heX, h.2 heX⟩,
    fun h ↦ ⟨fun e heI hi heX ↦ (h e heX heI).1 hi,
      fun e heX ↦ (em (e ∈ I)).elim (fun h ↦ hI.subset_ground h) fun heI ↦ (h _ heX heI).2 ⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ J = J ∪ I

Tactic:
union_eq_self_of_subset_right hIJ

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ J = J
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep (J ∪ I)

Tactic:
union_eq_self_of_subset_right hIJ

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis I X
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep J
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (uniqueBaseOn I E).Finitary

Tactic:
by
  refine ⟨fun K hK ↦ ?_⟩
  simp only [uniqueBaseOn_indep_iff'] at hK ⊢
  exact fun e heK ↦ singleton_subset_iff.1 <| hK _ (by simpa) (by simp)

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 : (M.E \ (B ∪ X) ∪ {e}) ∩ B' = ∅
⊢ False

Tactic:
union_inter_distrib_right,

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 ∪ X) ∩ B' ∪ {e} ∩ B' = ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Dual

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

Tactic:
by
  simp_rw [coindep_iff_exists', subset_sdiff]
  exact ⟨fun ⟨⟨B, hB, _, hBX⟩, hX⟩ ↦ ⟨B, hB, hX, hBX.symm⟩,
    fun ⟨B, hB, hXE, hXB⟩ ↦ ⟨⟨B, hB, hB.subset_ground, hXB.symm⟩, hXE⟩⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B₀ = J

Tactic:
← hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ f '' B₀ = f '' J
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (X ∩ M.E) = M.eRk X

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk (X ∩ M.E) = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X Y : Set α
M : Matroid α
hXY : Disjoint X Y
⊢ M.eRk ((M.E \ X ∪ Y) ∩ M.E) = M.eRk (M.E \ X)

Tactic:
union_inter_distrib_right,

Goal state after:
α : Type u_1
X Y : Set α
M : Matroid α
hXY : Disjoint X Y
⊢ M.eRk (M.E \ X ∩ M.E ∪ Y ∩ M.E) = M.eRk (M.E \ X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk (M.closure X) = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
indep_iff_forall_subset_not_isCircuit',

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E ↔ ∀ C ⊆ I, ¬M.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ M.closure {e} = M.closure {f}

Tactic:
rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X ≤ X.encard

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X ≤ X.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
⊢ M.eRk X ≤ M.eRk Y

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X ≤ M.eRk Y
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
⊢ M.eRk X ≤ n

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X ≤ n
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
lt_top_iff_ne_top,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X ≠ ⊤ ↔ M.IsRkFinite X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
⊢ M.closure X = M.closure Y

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
I : Set α
hI : M.IsBasis' I X
⊢ M.closure X = M.closure Y
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.E \ M.closure X
⊢ M.eRk (insert e X) = M.eRk X + 1

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∈ M.E \ M.closure X
I : Set α
hI : M.IsBasis' I X
⊢ M.eRk (insert e X) = M.eRk X + 1
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ X ∩ M.E ⊆ M.closure X

Tactic:
simp_rw [closure_def, subset_sInter_iff]

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}, X ∩ M.E ⊆ t'
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hIX : M.IsBasis' I X
e : α
heX : e ∈ X
heI : M.IsColoop e
⊢ e ∈ M.closure X

Tactic:
heI.mem_closure_iff_mem

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hIX : M.IsBasis' I X
e : α
heX : e ∈ X
heI : M.IsColoop e
⊢ e ∈ X
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X I : Set α
hI : M.IsBasis' I X
⊢ M.cRk (M.closure X) = M.cRk X
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case pos
α : 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 : (B' \ B).Finite
⊢ #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
rw [← cast_ncard h, ← cast_ncard, hB.ncard_sdiff_comm hB']

Goal state after:
case pos
α : 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 : (B' \ B).Finite
⊢ (B \ B').Finite
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ M.closure (⋂ i, Is i) = ⋂ i, M.closure (Is i)

Tactic:
by
  convert!
    h.closure_sInter_eq_biInter_closure_of_forall_subset (range_nonempty Is)
      (by simp [subset_iUnion])
  simp

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

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
⊢ toENat (M ↾ X).cRank = M.eRk X

Tactic:
toENat_cRank_eq,

Goal state after:
α : Type u
M : Matroid α
X : Set α
⊢ (M ↾ X).eRank = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
e : α
he : e ∈ I
heJ : e ∉ J
⊢ e ∈ M.closure (I \ {e})

Tactic:
exact mem_of_mem_of_subset
    (hJ.subset_closure he) (M.closure_subset_closure (subset_sdiff_singleton hJ.subset heJ))

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

Goal state before:
pp: σ : Type u_3
R : Type u_4
inst✝ : CommRing R
⊢ AlgebraicIndependent R X

Tactic:
by
  rw [AlgebraicIndependent, aeval_X_left]
  exact injective_id

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)

Tactic:
simp_rw [union_comm I J, hJ.union_indep_iff_forall_notMem_closure_right hI, union_comm]

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

Goal state before:
pp: case refine_2
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ ⋃₀ c ⊆ t

Tactic:
exact fun x ⟨w, hyc, hwy⟩ ↦ (hc hyc).2 hwy

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
⊢ fixedBy α g ∈ fixedBy (Set α) h

Tactic:
by
  ext x
  rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
    smul_left_cancel_iff, mem_fixedBy]

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

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ range x = range Subtype.val

Tactic:
Subtype.range_val

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
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ range x = range x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R (range Subtype.val))) A
⊢ Algebra.IsAlgebraic (↥(adjoin R (range fun i ↦ ↑i))) A

Tactic:
Subtype.range_val

Goal state after:
case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
⊢ Algebra.IsAlgebraic (↥(adjoin R I)) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
⊢ (matroid R A).IsBasis s t ↔ AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a

Tactic:
Matroid.IsBasis,

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 t : Set A
⊢ Maximal (fun A_1 ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔
    AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
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✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ (matroid R A).IsBasis s t ↔ s = t

Tactic:
Matroid.IsBasis,

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✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ Maximal (fun A_1 ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

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

Tactic:
← lift_lift.{u},

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

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
intro U

Goal state after:
case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
U : Set G
⊢ U ∈ B → ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ ib ∈ B, ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id ib

Tactic:
intro U

Goal state after:
case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
U : Set G
⊢ U ∈ B → ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
x₀ : G
⊢ B.N x₀ = map (fun x ↦ x₀ * x) (𝓝 1)

Tactic:
nhds_one_eq

Goal state after:
case refine_3
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
x₀ : G
⊢ B.N x₀ = map (fun x ↦ x₀ * x) B.filter