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

Goal state before:
pp: α : Type u_1
M : Matroid α
hM : ∃ M_1, M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
hM : ∃ M_1, M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : Matroid α
hM : ∃ M_1, M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ (I : Set α), M.Indep I → I ⊆ M.E

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
hM : ∃ M_1, M.E = M_1.E ∧ ∀ (I : Set α), M_1.Indep I ↔ M.Indep I
⊢ ∀ (I : Set α), M.Indep I → I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
h : IsBase B ∧ B.Finite
⊢ ∃ B, IsBase B

Tactic:
;

Goal state after:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
h : IsBase B ∧ B.Finite
⊢ ∃ B, IsBase B
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ (M ↾ Y).IsBase I

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I X Y J : Set α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
hXY : X ⊆ Y
hJY : M.IsBasis J Y
⊢ (M ↾ Y).IsBase I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
B : Set α
⊢ N.IsBasis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔
    N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ I.encard = J.encard

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I X J : Set α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ I.encard = J.encard
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.Finitary
⊢ (N.comap f ↾ E).Finitary

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.Finitary
⊢ (N.comap f ↾ E).Finitary
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.RankFinite
⊢ (N.comap f ↾ E).RankFinite

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M : Matroid α
N : Matroid β
E B I : Set α
inst✝ : N.RankFinite
⊢ (N.comap f ↾ E).RankFinite
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : I = J
⊢ M.Indep I

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : I = J
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
hI : M.Indep D₀
⊢ False

Tactic:
;

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
hI : M.Indep D₀
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : B = J
⊢ M.IsBase B

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : B = J
⊢ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : 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})
hfI : e ∈ I
⊢ False

Tactic:
;

Goal state after:
α : 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})
hfI : e ∈ I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hC : M.IsCircuit I
h : M.IsBasis I I
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hC : M.IsCircuit I
h : M.IsBasis I I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
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:
rintro ⟨e, he, rfl⟩

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C
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:
;

Goal state after:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶
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:
;

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

Goal state before:
pp: α : 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
⊢ I ⊆ I ∧ e ∈ M.closure I ∧ e ∉ I

Tactic:
simp [hecl, heI]

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

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

Tactic:
rw [mapEmbedding, map_isBasis_iff']

Goal state after:
α : 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.Map

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f.symm '' ⇑f '' I)
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (⇑f.symm '' ⇑f '' I)
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.IsBase I
⊢ M.IsBase (⇑f.symm '' ⇑f '' I)
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
by
  simp [restrictSubtype]

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

Goal state before:
pp: α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val

Tactic:
;

Goal state after:
α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ I ⊆ range Subtype.val
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis ∅ X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
⊢ M.closure {e} ⊆ M.closure J → M.closure {e} ∩ R ⊆ (M ↾ R).closure J

Tactic:
;

Goal state after:
case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
⊢ M.closure {e} ⊆ M.closure J → M.closure {e} ∩ R ⊆ (M ↾ R).closure J
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.Finitary
X : Set α
⊢ ((M ↾ X).comap Subtype.val).Finitary

Tactic:
;

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.Finitary
X : Set α
⊢ ((M ↾ X).comap Subtype.val).Finitary
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.RankFinite
X : Set α
⊢ ((M ↾ X).comap Subtype.val).RankFinite

Tactic:
;

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.RankFinite
X : Set α
⊢ ((M ↾ X).comap Subtype.val).RankFinite
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
⊢ M.closure {e} ∩ R ⊆ (M ↾ R).closure J → M.closure {e} ⊆ M.closure J

Tactic:
;

Goal state after:
case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
⊢ M.closure {e} ∩ R ⊆ (M ↾ R).closure J → M.closure {e} ⊆ M.closure J
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:
;

Goal state after:
α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ (loopyOn E).closure ∅ = E ∧ (loopyOn E).E = E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ (M ↾ R).closure J
⊢ M.closure {e} ⊆ M.closure J

Tactic:
refine closure_subset_closure_of_subset_closure ?_

Goal state after:
case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ (M ↾ R).closure J
⊢ {e} ⊆ M.closure J
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ∨ ¬M.IsLoop e

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ∨ ¬M.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ ¬M.IsLoop e

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ ¬M.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hX : M.Dep I
hI : M.IsBasis I I
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hX : M.Dep I
hI : M.IsBasis I I
⊢ False
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} ∪ ∅)
⊢ f ∈ M.closure ({e} ∪ ∅)

Tactic:
singleton_union

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure (insert f ∅)
⊢ f ∈ M.closure (insert e ∅)
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}
h : f ∈ M.E → M.IsLoop f
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → M.IsLoop f
⊢ False
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}
h : f ∈ M.E → f ∈ M.loops
⊢ e ∈ M.loops

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
⊢ e ∈ M.loops
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.IsNonloop f

Tactic:
rw [isNonloop_iff, and_comm]
  by_contra! h; apply he.not_isLoop
  rw [isLoop_iff] at *; convert! hef using 1
  obtain (hf | hf) := em (f ∈ M.E)
  · rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops,
      insert_empty_eq]
  rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]

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

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (X ∩ M.E) ≤ M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
R : Set α
h : (M ↾ R).IsNonloop e
⊢ M.IsNonloop e

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
e : α
R : Set α
h : (M ↾ R).IsNonloop e
⊢ M.IsNonloop e
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
;

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

Goal state before:
pp: α : Type u_1
X Y : Set α
M : Matroid α
h : Y ⊆ X
⊢ M.eRk (Y ∪ X \ Y) ≤ M.eRk Y + M.eRk (X \ Y)

Tactic:
;

Goal state after:
α : Type u_1
X Y : Set α
M : Matroid α
h : Y ⊆ X
⊢ M.eRk (Y ∪ X \ Y) ≤ M.eRk Y + M.eRk (X \ Y)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.Finite ↔ M.RankFinite

Tactic:
exact ⟨fun h ↦ hB.rankFinite_of_finite h, fun h ↦ hB.finite⟩

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

Goal state after:
α : Type u_1
M : Matroid α
e : α
h : M✶.IsColoop e
⊢ M✶✶.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
e : α
h : M✶.IsLoop e
⊢ M✶✶.IsColoop e
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:
;

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 α
I X : Set α
hI : M.Indep I
hIfin : I.Finite
hIX : I ⊆ X
h : M.eRk X ≤ M.eRk I
⊢ I.encard = M.eRk X

Tactic:
rw [h.antisymm (M.eRk_mono hIX), hI.eRk_eq_encard]

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

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

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

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
e : α
h : M.IsLoop e
⊢ ¬M✶.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (⋂ i, ↑i)

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (⋂ i, ↑i)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ (M ↾ X).eRk X = M.eRank

Tactic:
restrict_eRk_eq _ rfl.subset,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ M.eRk X = M.eRank
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure (Y ∩ M.E)

Tactic:
;

Goal state after:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure (Y ∩ M.E)
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:
;

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
h : M = loopyOn X
⊢ (loopyOn X).eRank = 0 ∧ (loopyOn X).E = X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
x✝ : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ {e} ∪ M.closure X
hC : M.IsCircuit C
heC : e ∈ C
⊢ e ∈ M.closure X

Tactic:
singleton_union

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
x✝ : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X)
hC : M.IsCircuit C
heC : e ∈ C
⊢ e ∈ M.closure X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
⊢ M.Indep (insert e I)

Tactic:
refine (em (e ∈ I)).elim (fun h ↦ by rwa [insert_eq_of_mem h]) fun h ↦ ?_

Goal state after:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x | M.IsBasis I (insert x I)}

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x | M.IsBasis I (insert x I)}
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.IsBasis I (M.closure I)

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.IsBasis I (M.closure I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep (insert e I)

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
K x✝ : Set α
⊢ M✶.Dep x✝ ↔ (∀ (B : Set α), M.IsBase B → (x✝ ∩ B).Nonempty) ∧ x✝ ⊆ M.E

Tactic:
;

Goal state after:
α : Type u_1
M : Matroid α
K x✝ : Set α
⊢ M✶.Dep x✝ ↔ (∀ (B : Set α), M.IsBase B → (x✝ ∩ B).Nonempty) ∧ x✝ ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
hI.insert_indep_iff,

Goal state after:
case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∈ M.E \ M.closure I ∨ e ∈ I ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ M.Indep (insert f (I \ {e})) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
hI.insert_indep_iff,

Goal state after:
case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I \ {e} ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBasis I M.E

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBasis I M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
⊢ M.closure B = M.E

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
⊢ M.closure B = M.E
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
I X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis' I X
⊢ #↑I = M.cRk X

Tactic:
rw [cRk, (isBase_restrict_iff'.2 hIX).cardinalMk_eq_cRank]

Goal state after: