mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ {x | M.IsBasis I (insert x I)} \ I
hu : M.Indep (insert e I)
⊢ e ∈ I

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ {x | M.IsBasis I (insert x I)} \ I
hu : M.Indep (insert e I)
⊢ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E B I✝ X R J I : Set α
h : ∀ J ⊆ I, J.Finite → J ⊆ E
e : α
heI : e ∈ I
⊢ e ∈ E

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
E B I✝ X R J I : Set α
h : ∀ J ⊆ I, J.Finite → J ⊆ E
e : α
heI : e ∈ I
⊢ e ∈ E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E : Set α
⊢ uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E

Tactic:
simp only [uniqueBaseOn, restrict_eq_restrict_iff, freeOn_indep_iff, subset_inter_iff]

Goal state after:
α : Type u_1
I E : Set α
⊢ ∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I : Set α
⊢ uniqueBaseOn ∅ I = loopyOn I

Tactic:
← dual_inj,

Goal state after:
α : Type u_1
I : Set α
⊢ (uniqueBaseOn ∅ I)✶ = (loopyOn I)✶
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
hIE : I ⊆ E
hI : I.Nonempty
⊢ ¬(uniqueBaseOn I E).IsBase ∅

Tactic:
simpa using

Goal state after:
α : Type u_1
E I : Set α
hIE : I ⊆ E
hI : I.Nonempty
⊢ ¬∅ = I
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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
B : Set α
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ ↑n
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground ⋯).matroid.IsBase B
⊢ Indep B

Tactic:
simpa using

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 B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
B : Set α
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ ↑n
hB : (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground ⋯).matroid.IsBase B
⊢ Indep B
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
⊢ M₁ = M₂✶ ↔ M₂ = M₁✶

Tactic:
← dual_inj,

Goal state after:
α : Type u_1
M₁ M₂ : Matroid α
⊢ M₁✶ = M₂✶✶ ↔ M₂ = M₁✶
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 : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).Indep (f '' B)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ N.Indep (f '' B)
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M M' : Matroid α
h : M ≤r M'
h' : M' ≤r M
⊢ M = M'

Tactic:
simpa using

Goal state after:
α : Type u_1
M M' : Matroid α
h : M ≤r M'
h' : M' ≤r M
⊢ M = M'
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N = M ∨ N <r M

Tactic:
simpa using

Goal state after:
α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N = M ∨ N <r M
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 : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
x : α
hxI : x ∈ I
⊢ x ∈ E

Tactic:
simpa using

Goal state after:
α : 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 : Set α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
x : α
hxI : x ∈ I
⊢ x ∈ E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
h : M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M.IsBasis (B ∩ X) X

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hX : X ⊆ M.E
h : M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M.IsBasis (B ∩ X) X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E

Tactic:
simpa using

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ I ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
hMN : N ≤r M
B : Set α
h : M.IsBasis B N.E
⊢ N.IsBase B

Tactic:
simpa using

Goal state after:
α : Type u_1
M N : Matroid α
hMN : N ≤r M
B : Set α
h : M.IsBasis B N.E
⊢ N.IsBase B
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite (X ∩ M.E)
⊢ M.IsRkFinite (M.closure X)

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite (X ∩ M.E)
⊢ M.IsRkFinite (M.closure X)
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
⊢ insert (f e) (f '' I) ⊆ (M.map f hf).E

Tactic:
simpa using

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
⊢ insert e I ⊆ f ⁻¹' f '' M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.IsCircuit ∅
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
h : M.IsCircuit ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ {e} ⊆ M.E

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∈ M.closure I
⊢ e ∈ M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
a : α
haX : a ∈ X
h : ∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t
⊢ a = e

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
a : α
haX : a ∈ X
h : ∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t
⊢ a = e
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
X : Set α
hX : ⇑f '' X ⊆ range ⇑f
I : Set α
x✝ : M.IsBasis (⇑f ⁻¹' ⇑f '' I) (⇑f ⁻¹' ⇑f '' X) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' ⇑f '' I) (⇑f ⁻¹' ⇑f '' X)
hIX : ⇑f '' I ⊆ ⇑f '' X
⊢ M.IsBasis I X ∧ ⇑f '' I = ⇑f '' I ∧ ⇑f '' X = ⇑f '' X

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
X : Set α
hX : ⇑f '' X ⊆ range ⇑f
I : Set α
x✝ : M.IsBasis (⇑f ⁻¹' ⇑f '' I) (⇑f ⁻¹' ⇑f '' X) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' ⇑f '' I) (⇑f ⁻¹' ⇑f '' X)
hIX : ⇑f '' I ⊆ ⇑f '' X
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x
hi : M.Indep {e}
B : Set α
hB : M.IsBase B
heB : {e} ⊆ B
⊢ e ∈ B

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
h : (∀ (x : Set α), M.IsBase x → e ∈ M.E) ∧ ∀ (x : Set α), M.IsBase x → e ∉ x
hi : M.Indep {e}
B : Set α
hB : M.IsBase B
heB : {e} ⊆ B
⊢ e ∈ B
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
this : M.IsBasis I M.loops
⊢ I = ∅

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
h : M.IsBasis I X
this : M.IsBasis I M.loops
⊢ I = ∅
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.RankPos
B : Set ↑M.E
hB : (M.restrictSubtype M.E).IsBase B
⊢ M.IsBase (Subtype.val '' B)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M✝ : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst✝ : M.RankPos
B : Set ↑M.E
hB : (M.restrictSubtype M.E).IsBase B
⊢ M.IsBase (Subtype.val '' B)
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.RankPos
B : Set ↑M.E
hB : (M.restrictSubtype M.E).IsBase B
hB' : M.IsBase (Subtype.val '' B)
⊢ B.Nonempty

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M✝ : Matroid α
N : Matroid β
E X I : Set α
M : Matroid α
inst✝ : M.RankPos
B : Set ↑M.E
hB : (M.restrictSubtype M.E).IsBase B
hB' : M.IsBase (Subtype.val '' B)
⊢ B.Nonempty
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ (M.comap f).IsLoop e ↔ M.IsLoop (f e)

Tactic:
by
  simp [isLoop_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ ∃ B, M.IsBase B ∧ e ∈ B

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ ∃ B, M.IsBase B ∧ e ∈ B
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 ι
⊢ M.IsCircuit J

Tactic:
simpa using

Goal state after:
α : 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 ι
⊢ M.IsCircuit J
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
⊢ n ≤ M.eRk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, hIX, hI, hIc⟩ ↦ ?_⟩

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

case refine_2
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.eRk X
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ι : Nonempty ι
i : ι
⊢ M.closure (I i) = M.closure (insert (x i) (I i))

Tactic:
simpa using

Goal state after:
α : 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ι : Nonempty ι
i : ι
⊢ M.closure (I i) = M.closure (insert (x i) (I i))
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B
B : Set α
hB : M.IsBase B
⊢ ?m.80

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
h : ∀ (B : Set α), M✶.IsBase B → e ∈ M✶.E \ B
B : Set α
hB : M.IsBase B
⊢ ?m.80
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case h₂
α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk {e} ≤ 1

Tactic:
simpa using

Goal state after:
case h₂
α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk {e} ≤ 1
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
h : Y ∩ M.E ⊆ M.closure X
⊢ M.eRk Y ≤ M.eRk X

Tactic:
simpa using

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
x✝ : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
heE : e ∈ M.closure B
heB : e ∉ B
⊢ False

Tactic:
obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heB).1 heE

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
x✝ : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
B : Set α
hB : M.IsBase B
h : ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
heE : e ∈ M.closure B
heB : e ∉ B
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : 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 : ι
⊢ M.IsCircuit (insert (x i) (C i \ {x i}))

Tactic:
simpa using

Goal state after:
case refine_1
α : 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 : ι
⊢ M.IsCircuit (C i)
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
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
hlt : M.eRk X < M.eRk Y
z : α
hz : z ∈ Y \ X
hr : M.eRk (Insert.insert z X) = M.eRk X + 1
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (Insert.insert e X) ≤ M.eRk X
hlt : M.eRk X < M.eRk Y
z : α
hz : z ∈ Y \ X
hr : M.eRk (Insert.insert z X) = M.eRk X + 1
⊢ False
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
⊢ M.Indep I ↔ M.eRk I = I.encard

Tactic:
refine ⟨fun h ↦ by rw [h.eRk_eq_encard], fun h ↦ ?_⟩

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
⊢ M.Indep I

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis' I

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
h : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
X : Set α
heX : e ∈ M.closure X
heX' : e ∉ X
⊢ False

pp: case refine_2
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
h : ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
· obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heX').1 heX
      exact h.1 hC heC

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
h : ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
h : ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
h : ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ I.Finite

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ I.Finite
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hIfin : I.Finite
h : M.eRank ≤ M.eRk I
⊢ M.IsBase I

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hIfin : I.Finite
h : M.eRank ≤ M.eRk I
⊢ M.IsBase I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_6
α : 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'
⊢ ⋃ i, C ↑i ⊆ ⋃₀ S

Tactic:
simpa using

Goal state after:
case refine_6
α : 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'
⊢ ∀ i ∈ X, C i ⊆ ⋃₀ S
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
F : Set α
⊢ M.IsFlat F ↔ ∃ (h : F ⊆ M.E), M.subtypeClosure.IsClosed ⟨F, h⟩

Tactic:
simpa using

Goal state after:
α : Type u_2
M : Matroid α
F : Set α
⊢ M.IsFlat F → F ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : 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}
⊢ ∀ (i : ↑X), M.IsCircuit (C ↑i)

Tactic:
simpa using

Goal state after:
case refine_1
α : 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}
⊢ ∀ a ∈ X, M.IsCircuit (C a)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_2
α : 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}
⊢ ∀ (i : ↑X), ↑i ∈ C₀

Tactic:
simpa using

Goal state after:
case refine_2
α : 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}
⊢ ∀ a ∈ X, a ∈ C₀
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr.refine_1
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ M.fundCircuit x B \ {x} ⊆ B

Tactic:
simpa using

Goal state after:
case inr.refine_1
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ M.fundCircuit x B ⊆ insert x B
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_4
α : 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}
e : α
heX : e ∈ X
f : α
hfX : f ∈ X
hef : e ∈ C f
⊢ e = f

Tactic:
simpa using

Goal state after:
case refine_4
α : 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}
e : α
heX : e ∈ X
f : α
hfX : f ∈ X
hef : e ∈ C f
⊢ e = f
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.eRank = 0
⊢ M = loopyOn M.E

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
h : M.eRank = 0
⊢ M = loopyOn M.E