mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ α, F⟮α⟯ = ⊤

Tactic:
obtain ⟨α, hα⟩ := @IsCyclic.exists_generator Eˣ _ _
  use α
  rw [eq_top_iff]
  rintro x -
  by_cases hx : x = 0
  · rw [hx]
    exact F⟮α.val⟯.zero_mem
  · obtain ⟨n, hn⟩ := Set.mem_range.mp (hα (Units.mk0 x hx))
    rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0]]
    exact zpow_mem (mem_adjoin_simple_self F (E := E) ↑α) n

Goal state after:
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : Algebra.adjoin F (rootSet 0 E) = ⊤
⊢ Normal F E

Tactic:
rootSet_zero,

Goal state after:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : F[] = ⊤
⊢ Normal F E
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
M : (Skeleton (SemimoduleCat R))ˣ
this : {M N : Skeleton (SemimoduleCat R)} → M = N → ↑(Quotient.out M) ≃ₗ[R] ↑(Quotient.out N)
⊢ ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm (id ((equivShrink (Skeleton (SemimoduleCat R))ˣ) M))) = ↑M

Tactic:
by simp

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

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

Tactic:
obtain ⟨f, hf, hB'⟩ := exch B₂ B₁ hB₂ hB₁ e he

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

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

Tactic:
sdiff_sdiff_right,

Goal state after:
case inr.inr
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : ((B₁ \ B₂ ∪ B₁ ∩ {e}) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
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
I : Set α
e : α
hIe : ¬Indep (insert e I)
h : ∀ I₀ ⊆ I, I₀.Finite → Indep (insert e I₀)
J : Set α
hJss : J ⊆ insert e I
hJfin : J.Finite
⊢ J ⊆ insert e (J \ {e})

Tactic:
by simp

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 = finrank F E ↔ Function.Injective fun ψ ↦ ψ α

Tactic:
← AlgHom.card_of_splits F E A hA,

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
⊢ (range fun ψ ↦ ψ α).toFinset.card = Fintype.card (E →ₐ[F] A) ↔ Function.Injective fun ψ ↦ ψ α
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✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
x : A ⊗[R] ↥(submoduleAlgebra e)
⊢ (LinearMap.mul'' R A ∘ₗ (AlgebraTensorModule.lTensor A A) (submoduleAlgebra e).subtype) 0 =
    (AlgebraTensorModule.congr (LinearEquiv.refl A A) (submoduleAlgebraEquiv e) ≪≫ₗ e) 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
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 | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀} ⊆ {b | b ⊆ E₀}

Tactic:
by simp

Goal state after:
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 ∧ Disjoint I' B'

Tactic:
and_iff_right hI'X

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
⊢ Disjoint I' B'
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:
by rintro _ _ _ rfl -; exact ⟨∅, by simp [Maximal]⟩

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J : Set α
⊢ (loopyOn E).IsBase ∅ ∧ ∅.Finite

Tactic:
by simp

Goal state after:
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
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
⊢ B₁ = B'

Tactic:
by
      refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)
      refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)
      refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)
      refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_
      exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I X R J K : Set α
hK : ∀ J ⊆ K, J.Finite → J ⊆ I ∩ E
e : α
heK : e ∈ K
⊢ {e}.Finite

Tactic:
by simp

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 : α → β
⊢ N.Indep (f '' ∅) ∧ InjOn f ∅

Tactic:
by simp

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
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hcard : I.encard < B.encard
⊢ ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
by
        obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
        exact ⟨e, ⟨heB, heI⟩, hi⟩

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
⊢ f '' X ⊆ (N ↾ range f).E

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I J : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset.card < hJfin.toFinset.card
⊢ ↑hIfin.toFinset ⊆ I

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I J : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1
hJfin : J.Finite
hIJ : hIfin.toFinset.card < hJfin.toFinset.card
⊢ ↑hJfin.toFinset ⊆ J

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ f '' insert e I ⊆ N.E

Tactic:
exact (image_mono (insert_subset heX h.2.2)).trans h.1.subset_ground

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 β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
x : α
hx : x ∈ I
y : α
hy : y ∈ I
⊢ {x, y}.Finite

Tactic:
by simp

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 β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
x : α
hx : x ∈ I
y : α
hy : y ∈ I
⊢ x ∈ {x, y}

Tactic:
by simp

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 β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
x : α
hx : x ∈ I
y : α
hy : y ∈ I
⊢ y ∈ {x, y}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f)✶.E = (N✶.comapOn E f).E

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ f '' M.E = (M.mapSetEmbedding { toFun := M.E.domRestrict f, inj' := ⋯ }).E

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ (M.map f hf).Dep (insert (f e) (f '' I))

Tactic:
← not_indep_iff (by simpa [← image_insert_eq] using image_mono hss)

Goal state after:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ¬(M.map f hf).Indep (insert (f e) (f '' I))
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Minimal (fun x ↦ ¬M.Indep x) C

Tactic:
simp_rw [minimal_iff_forall_ssubset, and_iff_right hC.not_indep, not_not]
  exact fun ⦃t⦄ a ↦ ssubset_indep hC a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf)✶.E = (M✶.map f hf).E

Tactic:
by simp

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 β
f : α → β
⊢ InjOn f (emptyOn α).E

Tactic:
by simp

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 : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
e : β
he : e ∈ I
⊢ {e}.Finite

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (M.mapEmbedding f).Indep I ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
rw [mapEmbedding, map_indep_iff]

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set β
⊢ (M.mapEmbedding f).IsBase B ↔ M.IsBase (⇑f ⁻¹' B) ∧ B ⊆ range ⇑f

Tactic:
by
  rw [mapEmbedding, map_isBase_iff]
  refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' B, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
  rintro ⟨B, hB, rfl⟩
  rw [preimage_image_eq _ f.injective]
  exact ⟨hB, image_subset_range _ _⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
h : M.Indep (⇑f.symm '' I)
⊢ I = ⇑f '' ⇑f.symm '' I

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
h : M.Dep (⇑f.symm '' D)
⊢ D = ⇑f '' ⇑f.symm '' D

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
h : M.IsBase (⇑f.symm '' B)
⊢ B = ⇑f '' ⇑f.symm '' B

Tactic:
by simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)
⊢ I = ⇑f '' ⇑f.symm '' I

Tactic:
by simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
h : M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)
⊢ X = ⇑f '' ⇑f.symm '' X

Tactic:
by simp

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 X I : Set α
M : Matroid α
inst✝ : M.Nonempty
this : Nonempty ↑M.E
⊢ (M.restrictSubtype M.E).E.Nonempty

Tactic:
by simp

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

Goal state before:
pp: α : 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ι : IsEmpty ι
⊢ J ⊆ J ∪ ⋃ i, I i

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ ∀ (i : ι), x i ∉ C i \ {x i}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz✝ : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
C' : Set α
hC'ss : C' ⊆ (C₀ ∪ ⋃ i, C ↑i) \ range fun x ↦ ↑x
hC' : M.IsCircuit C'
hz : z ∈ C'
⊢ X ⊆ range fun x ↦ ↑x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
h : M.eRk {e} = 1
⊢ {e}.Finite

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∀ ⦃i i' : Unit⦄, e ∈ C₂ → i = i'

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
C : Set α
hCs : C ⊆ (C₁ ∪ ⋃ i, C₂) \ range fun i ↦ e
hC : M.IsCircuit C
hfC : f ∈ C
⊢ C₁ ∪ ⋃ i, C₂ ⊆ C₁ ∪ C₂

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
C : Set α
hCs : C ⊆ (C₁ ∪ ⋃ i, C₂) \ range fun i ↦ e
hC : M.IsCircuit C
hfC : f ∈ C
⊢ {e} ⊆ range fun i ↦ e

Tactic:
by simp

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

Goal state before:
pp: α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ e ∉ R \ {e}

Tactic:
by simp

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
⊢ ∅ ⊆ Y ∧ ∅.Finite ∧ ∅ ⊆ M.closure ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
x✝ : ∃ x ∈ M.E, M.IsLoop x
e : α
left✝ : e ∈ M.E
he : M.IsLoop e
⊢ {e}.Subsingleton

Tactic:
by simp

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

Goal state before:
pp: α : 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 ⋯
this : B \ B' ⊆ U
⊢ ℵ₀ ≤ #↑(B' \ B)

Tactic:
by simp

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

Goal state before:
pp: α : 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 ⋯
this : B \ B' ⊆ U
e : ↑(B' \ B)
⊢ ℵ₀ ≤ #↑(B' \ B)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

Tactic:
have := hA.coe_sort
  convert! closure_iInter_eq_iInter_closure_of_iUnion_indep (Is := fun i : A ↦ I i) (by simpa) <;>
  simp

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.closure (bif i then I else J) = bif i then M.closure I else M.closure J

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋃ i ∈ A, X i ∩ I ⊆ I

Tactic:
by simp

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

Goal state before:
pp: case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert f (M.E \ (insert f (M.E \ B) \ {e}))

Tactic:
sdiff_sdiff_right,

Goal state after:
case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert f (M.E \ insert f (M.E \ B) ∪ M.E ∩ {e})
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra.Transcendental R A
x : A
hx : Transcendental R x
⊢ 1 ≤ Cardinal.mk ↑↑⟨{x}, ⋯⟩

Tactic:
by simp

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

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

Tactic:
by simp

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
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
⊢ t ∩ s ∪ ∅ ⊆ s

Tactic:
by simp

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Subsingleton R
this : Subsingleton A
⊢ 1 ≤ Cardinal.mk ↑↑⟨{0}, ⋯⟩

Tactic:
by simp

Goal state after: