mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : Finite (IntermediateField F E)
IF : Type (max 0 u_2) := { K // ∃ x, K = F⟮x⟯ }
this✝ : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional F ↥↑K
⊢ FiniteDimensional F E

Tactic:
have hfin := finiteDimensional_iSup_of_finite (t := fun K : IF ↦ K.1)

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
IF : Type (max 0 u_2) := { K // ∃ x, K = F⟮x⟯ }
this✝ : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional F ↥↑K
hfin : FiniteDimensional F ↥(⨆ i, ↑i)
⊢ FiniteDimensional F E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : I₀.ncard ≤ B'.ncard
⊢ False

Tactic:
hI₀card,

Goal state after:
α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : B.ncard + 1 ≤ B'.ncard
⊢ False
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
α : E
hprim : F⟮α⟯ = ⊤
hfin : FiniteDimensional F ↥F⟮α⟯
⊢ FiniteDimensional F E

Tactic:
rw [hprim] at hfin

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
α : E
hprim : F⟮α⟯ = ⊤
hfin : FiniteDimensional F ↥⊤
⊢ FiniteDimensional 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✝³ : 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:
simp

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B X : Set α
M : Matroid α
⊢ ∀ ⦃I B : Set α⦄,
    (I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) →
      ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I →
        Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B →
          ∃ x ∈ B \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
rintro I X ⟨hIE, B, hB, hIB⟩ hI_not_max hX_max

Goal state after:
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (⋃ b, bif b then I else J) (⋃ b, bif b then X else Y)

Tactic:
refine IsBasis.iUnion_isBasis_iUnion _ _ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)

case refine_2
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)
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:
simp

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 J, M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J

Tactic:
obtain ⟨I, I', hI, hI', hII'⟩ := M.exists_isBasis_subset_isBasis hXY
  refine ⟨I, I' \ I, hI, by rwa [union_sdiff_self, union_eq_self_of_subset_left hII'], ?_⟩
  rw [disjoint_iff_forall_ne]
  rintro e heX _ ⟨heI', heI⟩ rfl
  exact heI <| hI.mem_of_insert_indep heX (hI'.indep.subset (insert_subset heI' hII'))

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
Y✝ : Set α
⊢ (fun x ↦ x = ∅) Y✝ → ∀ a ∈ ∅ \ Y✝, ∃ b ∈ Y✝ \ ∅, (fun x ↦ x = ∅) (insert b (∅ \ {a}))

Tactic:
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 α✝
α : Type u_2
⊢ ∀ (B : Set α), B = ∅ → B ⊆ ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
E X : Set α
hX : X ⊆ E
⊢ (loopyOn E).Indep ∅ ∧ ∅ ⊆ X ∧ ∀ (J : Set α), (loopyOn E).Indep J → ∅ ⊆ J → J ⊆ X → ∅ = J

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

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ¬M = loopyOn M.E ↔ ¬M.IsBase ∅

Tactic:
empty_isBase_iff

Goal state after:
α : Type u_1
M : Matroid α
⊢ ¬M = loopyOn M.E ↔ ¬M = loopyOn M.E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: case refine_1
α : Type u_1
E : Set α
⊢ (freeOn E).E = E ∧ (freeOn E).Indep E

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ (E \ I) = E ∩ I

Tactic:
simp

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

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M M' : Matroid α
⊢ { toMatroid := M } ≤ { toMatroid := M' } ↔ M ≤r M'

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M M' : Matroid α
⊢ { toMatroid := M } < { toMatroid := M' } ↔ M <r M'

Tactic:
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
⊢ (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).matroid.RankFinite

Tactic:
rw [IndepMatroid.ofBddAugment]

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → 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.ofBdd E Indep indep_empty indep_subset ⋯ subset_ground indep_bdd).matroid.RankFinite
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:
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:
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:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
B : Set α
hB : M.IsBase B ∧ I ⊆ B
⊢ I ⊂ M.E

Tactic:
exact hB.2.trans_ssubset hB.1.ssubset_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:
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:
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:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ B ⊆ E

Tactic:
by
  rw [← and_iff_left_of_imp (IsBase.subset_ground (M := N.comapOn E f) (B := B)),
    comapOn_ground_eq, and_congr_left_iff]
  suffices h' : B ⊆ E → InjOn f B from fun hB ↦
    by simp [hB, comapOn_isBase_iff_of_surjOn h.surjOn, h']
  exact fun hBE ↦ h.injOn.mono hBE

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

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.IsRkFinite {e}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
⊢ M.IsRkFinite M.E

Tactic:
by
  rwa [isRkFinite_ground_iff_rankFinite]

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

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

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
I : Set α
e : α
M : Matroid α
heI : e ∉ I
⊢ M.fundCircuit e I \ {e} ⊆ I

Tactic:
by simp [fundCircuit_subset_insert]

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:
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 α
E : Set β
e : ↑M.E ≃ ↑E
I : Set β
x✝ : ↑M.E
⊢ x✝ ∈ Subtype.val ∘ ⇑e ⁻¹' I ↔ x✝ ∈ ⇑e.symm '' E ↓∩ I

Tactic:
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 α
E : Set β
e : ↑M.E ≃ ↑E
⊢ E = (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun x ↦ x ∈ E))).E ∧
    ∀ (I : Set β),
      (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun x ↦ x ∈ E))).Indep I ↔
        M.Indep (Subtype.val '' ⇑e.symm '' E ↓∩ I) ∧ I ⊆ E

Tactic:
have hrw : ∀ I : Set β, Subtype.val ∘ ⇑e ⁻¹' I = ⇑e.symm '' E ↓∩ I := fun I ↦ by ext; simp

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
E : Set β
e : ↑M.E ≃ ↑E
hrw : ∀ (I : Set β), Subtype.val ∘ ⇑e ⁻¹' I = ⇑e.symm '' E ↓∩ I
⊢ E = (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun x ↦ x ∈ E))).E ∧
    ∀ (I : Set β),
      (M.mapSetEmbedding (e.toEmbedding.trans (Embedding.subtype fun x ↦ x ∈ E))).Indep I ↔
        M.Indep (Subtype.val '' ⇑e.symm '' E ↓∩ I) ∧ I ⊆ E
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
rw [hI.closure_sInter_eq_biInter_closure_of_forall_subset ⟨I, by simpa⟩ (by simp +contextual)]

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

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

Tactic:
simp

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

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

Goal state before:
pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X ∩ M.E)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (M.restrictSubtype M.E).map Subtype.val ⋯ = M

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

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
⊢ (M ↾ R).loops = M.loops ∩ R ∪ R \ M.E

Tactic:
rw [← closure_empty, ← closure_empty, restrict_closure_eq', empty_inter]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
hX : X ⊆ M.E
h : M.eRk X = n
I : Set α
hI : M.IsBasis I X
⊢ I.encard = n

Tactic:
rw [hI.encard_eq_eRk, ← h]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ (loopyOn E).closure ∅ = E ∧ (loopyOn E).E = E

Tactic:
simp

Goal state after:
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 ∩ M.E ∪ Y ∩ M.E) = M.eRk (M.E \ X)

Tactic:
inter_eq_self_of_subset_left sdiff_subset,

Goal state after:
α : 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)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
hf : f ∈ M.E
⊢ M.closure (insert f M.loops) = M.closure {f}

Tactic:
closure_insert_congr_right M.closure_loops,

Goal state after:
case inl
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
hf : f ∈ M.E
⊢ M.closure (insert f ∅) = M.closure {f}
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:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRank ≤ M.eRk (X ∪ M.E \ X)

Tactic:
by rw [← eRk_inter_ground, eRank_def, union_sdiff_self,
    union_inter_cancel_right]

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

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.IsCocircuit {e} ↔ M.IsColoop e

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
h : M.eRk I = I.encard
hinf : I.Infinite
⊢ M.Indep I

Tactic:
hinf.encard_eq

Goal state after:
case inr
α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
h : M.eRk I = ⊤
hinf : I.Infinite
⊢ M.Indep I
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:
simp

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

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
M✝ : Matroid α
F X Y : Set α
e f : α
M : Matroid α
hs : ∀ a ∈ ∅, M.IsFlat ↑a
⊢ M.IsFlat ↑(sInf ∅)

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

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}, X ∩ M.E ⊆ t'

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
⊢ (M.comap f).eRk X = M.eRk (f '' X)

Tactic:
obtain ⟨hI', hinj, -⟩ := comap_isBasis'_iff.1 hI

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hinj : InjOn f I
⊢ (M.comap f).eRk X = M.eRk (f '' X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
h : M = loopyOn X
⊢ (loopyOn X).eRank = 0 ∧ (loopyOn X).E = X

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

Goal state after: