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

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
⊢ (N.comap f).Indep I

pp: case refine_2.refine_2
α : 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
⊢ (N.comap f).Dep (insert e I)

Tactic:
·

Goal state after:
case refine_2.refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
⊢ (N.comap f).Indep I
Module: Mathlib.Combinatorics.Matroid.Dual

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

Tactic:
coindep_iff_exists',

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E \ X
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:
coindep_iff_exists',

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X

Tactic:
obtain ⟨y, hy, h⟩ := hIX.restrict_isBase.exchange hJX.restrict_isBase he

Goal state after:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
⊢ ∃ f ∈ J \ I, M.IsBasis (insert f (I \ {e})) X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : ↑(emptyOn α).E ↪ β
⊢ ∃ M, range ⇑f = M.E ∧ ∀ (I : Set β), M.Indep I ↔ (emptyOn α).Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

pp: case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
⊢ ∃ M_1, range ⇑f = M_1.E ∧ ∀ (I : Set β), M_1.Indep I ↔ M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : ↑(emptyOn α).E ↪ β
⊢ ∃ M, range ⇑f = M.E ∧ ∀ (I : Set β), M.Indep I ↔ (emptyOn α).Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : ↑(emptyOn α).E ↪ β
⊢ ∃ M, range ⇑f = M.E ∧ ∀ (I : Set β), M.Indep I ↔ (emptyOn α).Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
refine ⟨emptyOn β, ?_⟩

Goal state after:
case inl
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N : Matroid β
f : ↑(emptyOn α).E ↪ β
⊢ range ⇑f = (emptyOn β).E ∧
    ∀ (I : Set β), (emptyOn β).Indep I ↔ (emptyOn α).Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

pp: case mpr
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀) → M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀
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₀, M.IsBase B₀ ∧ B = f '' B₀

pp: case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = f '' B₀) → Maximal (M.map f hf).Indep B

Tactic:
·

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₀, M.IsBase B₀ ∧ B = f '' B₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) → ∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀

pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
⊢ (∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀) → (∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D : Set β
⊢ ((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) → ∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
h : (M.map f hf).IsBasis I X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

pp: case refine_2
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).IsBasis I X

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
h : (M.map f hf).IsBasis I X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
C : Set α
this : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, C ⊆ M.E → (M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}))
hCE : ¬C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

pp: α✝ : Type u_1
M✝ : Matroid α✝
C✝ : Set α✝
α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
·

Goal state after:
case inr
α : Type u_1
M : Matroid α
C : Set α
this : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, C ⊆ M.E → (M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e}))
hCE : ¬C ⊆ M.E
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
f : α
heI : f ∉ I
he : f ∈ M.closure I
h : ∀ f_1 ∈ I, f ∉ M.closure (I \ {f_1})
⊢ M.Indep (insert f I \ {f})

pp: case inr
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ M.Indep (insert e I \ {f})

Tactic:
·

Goal state after:
case inl
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
f : α
heI : f ∉ I
he : f ∈ M.closure I
h : ∀ f_1 ∈ I, f ∉ M.closure (I \ {f_1})
⊢ M.Indep (insert f I \ {f})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ ∃ e ∈ C, I = C \ {e}

pp: case refine_2
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) → M.IsBasis I C

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ ∃ e ∈ C, I = C \ {e}
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I

pp: case refine_2
α : Type u_1
M : Matroid α
C I : Set α
hC✝ : M.IsCircuit C
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : 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 ⊆ I ∧ e ∈ M.closure J}

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})

pp: case refine_3
α : 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
⊢ ∀ f ∈ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}, e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
·

Goal state after:
case refine_1
α : 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 ⊆ I ∧ e ∈ 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 ∈ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

pp: case refine_3
α : 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
⊢ ∀ f ∈ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}, e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
·

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 ∈ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) → M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

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

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) → M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
I : Set α
x : α
hI : M.Indep I
hecl : x ∈ M.closure I
heI : x ∉ I
⊢ x ∈ M.fundCircuit x I ↔ M.Indep (insert x I \ {x})

pp: case inr
α : Type u_1
M : Matroid α
I : Set α
e x : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
hne : x ≠ e
⊢ x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

Tactic:
·

Goal state after:
case inl
α : Type u_1
M : Matroid α
I : Set α
x : α
hI : M.Indep I
hecl : x ∈ M.closure I
heI : x ∉ I
⊢ x ∈ M.fundCircuit x I ↔ M.Indep (insert x I \ {x})
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
hCI : C ⊆ I
⊢ C = M.fundCircuit e I

pp: case inr
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
⊢ C = M.fundCircuit e I

Tactic:
·

Goal state after:
case inl
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
hCI : C ⊆ I
⊢ C = M.fundCircuit e I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ e ∈ M.closure I

pp: case refine_2
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
heI : e ∈ I
⊢ False

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ e ∈ M.closure I
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}
tfae_4_iff_5 : M.Dep {e} ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE

Tactic:
tfae_finish

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)

pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X

Tactic:
·

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

Goal state before:
pp: case a
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

pp: case a
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) ⊆
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J})

Tactic:
·

Goal state after:
case a
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
union_empty

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure X = M.closure X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M.loops ∩ R ∪ ∅ = M.loops ∩ R

Tactic:
union_empty

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ M.loops ∩ R = M.loops ∩ R
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.eRk (M.E \ X)

Tactic:
by
  rw [← eRk_inter_ground, union_inter_distrib_right, inter_eq_self_of_subset_left sdiff_subset,
    union_eq_self_of_subset_right
      (subset_sdiff.2 ⟨inter_subset_right, hXY.symm.mono_left inter_subset_left⟩)]

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

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

pp: case neg
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
by
  rw [isNonloop_iff, ← singleton_dep, dep_iff, not_and, not_imp_not, singleton_subset_iff]
  exact ⟨fun h ↦ ⟨fun _ ↦ h, singleton_subset_iff.mp h.subset_ground⟩, fun h ↦ h.1 h.2⟩

Goal state after:
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.loops = M.closure {f}

pp: case inr
α : 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.loops = M.closure {f}

Tactic:
·

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.loops = M.closure {f}
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
⊢ M₂.IsCircuit C

pp: case refine_2
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₂.IsCircuit C
⊢ M₁.IsCircuit C

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
⊢ M₂.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inl
α : 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 ι
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

pp: case inr
α : 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 ι
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
·

Goal state after:
case inl
α : 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 ι
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ 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 {f, e} = M.closure {e, f}

Tactic:
pair_comm

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ M.closure {e, f} = M.closure {e, f}
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ M.IsCircuit {e, f}

pp: case refine_2
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.IsCircuit {e, f}
⊢ M.closure {e} = M.closure {f}

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ M.IsCircuit {e, f}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

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

Tactic:
·

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
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
e : α
he hf : M.IsNonloop e
⊢ M.closure {e} = M.closure {e} ↔ e = e ∨ ¬M.Indep {e, e}

pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}

Tactic:
·

Goal state after:
case inl
α : Type u_1
M : Matroid α
e : α
he hf : M.IsNonloop e
⊢ M.closure {e} = M.closure {e} ↔ e = e ∨ ¬M.Indep {e, e}
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr.inl
α : Type u_1
M : Matroid α
f : α
hf : M.IsNonloop f
x : α
he : M.IsNonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.Indep ({x, f} \ {x})

pp: case inr.inr
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
x : α
hf : M.IsNonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
M : Matroid α
f : α
hf : M.IsNonloop f
x : α
he : M.IsNonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.Indep ({x, f} \ {x})
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤r M
⊢ M.IsNonloop e

Tactic:
obtain ⟨R, -, rfl⟩ := hNM; exact h.of_restrict

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
h : M✶.IsColoop e
⊢ M.IsLoop e

Tactic:
by rw [← dual_dual M]; exact h.dual_isLoop

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

Goal state before:
pp: case refine_5
α : 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
hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

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}))

pp: case refine_2
α : 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
⊢ M.IsCircuit (C₀ \ range x ∪ range x)

pp: case refine_3
α : 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
⊢ z ∉ range x

pp: case refine_4
α : 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 : ι), z ∉ C i \ {x i}

Tactic:
·

Goal state after:
case refine_5
α : 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
hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C'