mathlib-initiative/mathlib-tactics huggingface dataset:
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
C' : Set α
hC'C : C' ⊆ C
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
C' : Set α
hC'C : C' ⊆ C
hC' : M₂.IsCircuit C'
⊢ M₂.IsCircuit C'
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
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
C' : Set α
hC'C : C' ⊆ C
hC' : M₁.IsCircuit C'
⊢ M₁.IsCircuit C'

Tactic:
]

Goal state after:
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
C' : Set α
hC'C : C' ⊆ C
hC' : M₁.IsCircuit C'
⊢ M₁.IsCircuit C'
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
R X I : Set α
hI : M.IsBasis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
⊢ I.encard = M.eRk (X ∩ R)

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
R X I : Set α
hI : M.IsBasis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
⊢ I.encard = M.eRk (X ∩ R)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
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.closure ∅ = M.closure ∅

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R X I : Set α
hI : M.IsBasis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
⊢ M.eRk (X ∩ R ∩ M.E) = M.eRk (X ∩ R ∩ M.E)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
X : Set α
M : Matroid α
R : Set α
h : X ⊆ R
⊢ M.eRk X = M.eRk X

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
Y : Set α
⊢ M.eRk (X ∪ Y) = M.eRk (X ∪ Y)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : ∃ C ⊆ insert z ((⋃ i, I i) ∪ J \ {z}), M.IsCircuit C ∧ z ∈ C
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
]

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 ι
hcl : ∃ C ⊆ insert z ((⋃ i, I i) ∪ J \ {z}), M.IsCircuit C ∧ z ∈ C
⊢ ∃ 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 {e, f} = M.closure {e, f}

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
e : α
⊢ M.eRk (insert e X) = M.eRk (insert e X)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
⊢ M.eRk (insert e X) = M.eRk (insert e X)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ X.encard

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ X.encard
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 Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ I.encard ≤ J.encard

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ I.encard ≤ J.encard
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.Rank.ENat

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

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
J : Set α
h : n ≤ J.encard
hJ : M.IsBasis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
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}
hf : M.IsNonloop f
⊢ ¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

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}
hf : M.IsNonloop f
⊢ ¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
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
⊢ M.eRk I ≤ M.eRk X

Tactic:
]

Goal state after:
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
⊢ M.eRk I ≤ M.eRk X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ n

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n
I : Set α
hI : M.IsBasis' I X
⊢ I.encard ≤ n
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 ι
C' : Set α
hC'ss : C' ⊆ J ∪ ⋃ i, I i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ i, I i

Tactic:
]

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 ι
C' : Set α
hC'ss : C' ⊆ J ∪ ⋃ i, I i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ i, I i
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}
hf : M.IsNonloop f
⊢ e ∉ M.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}
hf : M.IsNonloop f
⊢ e ∉ M.E \ M.closure {f}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I ≤ M.eRk M.E

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.eRk I ≤ M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ I = ∅ ↔ X ∩ M.E ⊆ M.loops

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ I = ∅ ↔ X ∩ M.E ⊆ M.loops
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.eRk (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.eRk (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
]

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

Goal state before:
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 ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ i, I i)

Tactic:
]

Goal state after:
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 ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ i, I i)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ X ∩ (M.E \ Y)) + M.eRk (M.E \ X ∪ M.E \ Y) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)
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.IsNonloop f

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.IsNonloop f
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
]

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

Goal state before:
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.IsNonloop e

Tactic:
]

Goal state after:
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.IsNonloop e
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
Y X : Set α
hY : M.eRk Y ≤ 0
⊢ M.eRk X = M.eRk X

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ M.IsNonloop e ∧ e ∈ R ↔ M.IsNonloop e ∧ e ∈ R

Tactic:
]

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

Goal state before:
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 ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ range x \ {z} ∪ J \ {z} ⊆ range x ∪ J \ {z}

Tactic:
]

Goal state after:
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 ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ range x \ {z} ∪ J \ {z} ⊆ range x ∪ J \ {z}
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
e : α
E : Set α
⊢ e ∈ E ↔ e ∈ E

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ X.encard + M.eRk Y ≤ X.encard + M.eRk Y

Tactic:
]

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

Goal state before:
pp: α : Type u_1
e : α
I E : Set α
⊢ e ∈ I ∩ E ↔ e ∈ I ∩ E

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk X + M.eRk Y ≤ M.eRk X + M.eRk Y

Tactic:
]

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

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

Tactic:
]

Goal state after:
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:
]

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.Finite ↔ M.RankFinite
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.loops = M.loops

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ M.IsLoop e

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ M.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRank = ⊤ ↔ M.eRank = ⊤

Tactic:
]

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: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ ¬I.Finite ↔ ¬I.Finite

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis I X

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis J X

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis J X
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
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y
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
I : Set α
hI : M.IsBasis' I X
J : Set α
hr : J.encard ≤ I.encard
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure J = M.closure J

Tactic:
]

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
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i : ι
⊢ ∀ ⦃a : α⦄, a ∈ C i \ {x i} → ∀ ⦃b : α⦄, b ∈ range x → a ≠ b

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
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, C i \ {x i}
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i : ι
⊢ ∀ ⦃a : α⦄, a ∈ C i \ {x i} → ∀ ⦃b : α⦄, b ∈ range x → a ≠ b
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ M.eRk (insert e X) = M.eRk X + 1

Tactic:
]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ M.eRk (insert e X) = M.eRk X + 1
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:
]

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
⊢ False
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ I.encard + 1 = I.encard + 1

Tactic:
]

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

Goal state before:
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₀

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
⊢ range x ⊆ C₀

Tactic:
]

Goal state after:
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₀

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
⊢ range x ⊆ C₀
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : M.IsRkFinite X
⊢ M.eRk Y = M.eRk Y

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.eRk (insert e X) ≤ M.eRk X
hX : ¬M.IsRkFinite X
⊢ ⊤ = ⊤

Tactic:
]

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

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

Tactic:
]

Goal state after: