internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
refine' ⟨C', hC', hzC', subset_diff.mpr ⟨_, _⟩⟩
Proof state after:
case inr.intro.intro.intro.refine'_1
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ C' ⊆ C ∪ ⋃ i, Cs i

case inr.intro.intro.intro.refine'_2
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ Disjoint C' (range x)
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case inr.intro.intro.intro.refine'_2
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ Disjoint C' (range x)
Tactic:
refine' disjoint_of_subset_left hCzY _
Proof state after:
case inr.intro.intro.intro.refine'_2
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ Disjoint (insert z Y) (range x)
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case inr.intro.intro.intro.refine'_2
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ Disjoint (insert z Y) (range x)
Tactic:
rw [← singleton_union, disjoint_union_left, disjoint_singleton_left]
Proof state after:
case inr.intro.intro.intro.refine'_2
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ z ∉ range x ∧ Disjoint Y (range x)
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case inr.intro.intro.intro.refine'_2
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ z ∉ range x ∧ Disjoint Y (range x)
Tactic:
refine' ⟨not_mem_subset _ hz.2, _⟩
Proof state after:
case inr.intro.intro.intro.refine'_2.refine'_1
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ range x ⊆ ⋃ i, Cs i

case inr.intro.intro.intro.refine'_2.refine'_2
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ Disjoint Y (range x)
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case inr.intro.intro.intro.refine'_2.refine'_2
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ Disjoint Y (range x)
Tactic:
exact disjoint_of_subset_right (subset_insert z _) disjoint_sdiff_left
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
⊢ Y ⊆ M.E
Tactic:
refine' diff_subset.trans (union_subset hC.subset_ground _)
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
⊢ ⋃ x, Cs x ⊆ M.E
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
⊢ ⋃ x, Cs x ⊆ M.E
Tactic:
exact iUnion_subset fun i ↦ (hCs i).subset_ground
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
⊢ range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
Tactic:
rintro e ⟨i, rfl⟩
Proof state after:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
⊢ x i ∈ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
⊢ x i ∈ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
Tactic:
have h' := (hCs i).subset_cl_diff_singleton (x i) (h_mem i).2
Proof state after:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
⊢ x i ∈ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
⊢ x i ∈ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
Tactic:
refine' mem_of_mem_of_subset h' (M.cl_subset_cl _)
Proof state after:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
⊢ Cs i \ {x i} ⊆ ⋃ i, (Cs i \ {x i}) \ insert z (range x)
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
⊢ Cs i \ {x i} ⊆ ⋃ i, (Cs i \ {x i}) \ insert z (range x)
Tactic:
refine' subset_iUnion_of_subset i (subset_diff.mpr ⟨rfl.subset, _⟩)
Proof state after:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
⊢ Disjoint (Cs i \ {x i}) (insert z (range x))
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
⊢ Disjoint (Cs i \ {x i}) (insert z (range x))
Tactic:
rw [disjoint_iff_forall_ne]
Proof state after:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
⊢ ∀ ⦃a : α⦄, a ∈ Cs i \ {x i} → ∀ ⦃b : α⦄, b ∈ insert z (range x) → a ≠ b
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
⊢ ∀ ⦃a : α⦄, a ∈ Cs i \ {x i} → ∀ ⦃b : α⦄, b ∈ insert z (range x) → a ≠ b
Tactic:
rintro y hy z (rfl | ⟨j, rfl⟩) rfl
Proof state after:
case intro.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y✝ : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
y : α
hy : y ∈ Cs i \ {x i}
hz : y ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert y (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert y (range x)
hYE : Y ⊆ M.E
⊢ False

case intro.inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
j : ι
hy : x j ∈ Cs i \ {x i}
⊢ False
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case intro.inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
j : ι
hy : x j ∈ Cs i \ {x i}
⊢ False
Tactic:
refine' hy.2 (mem_singleton_iff.mpr _)
Proof state after:
case intro.inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
j : ι
hy : x j ∈ Cs i \ {x i}
⊢ x j = x i
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case intro.inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
j : ι
hy : x j ∈ Cs i \ {x i}
⊢ x j = x i
Tactic:
rw [h_unique _ _ hy.1]
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case intro.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y✝ : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
i : ι
h' : x i ∈ M.cl (Cs i \ {x i})
y : α
hy : y ∈ Cs i \ {x i}
hz : y ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert y (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert y (range x)
hYE : Y ⊆ M.E
⊢ False
Tactic:
exact hz.2 (mem_iUnion_of_mem i hy.1)
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
⊢ range x ⊆ M.cl Y
Tactic:
refine' h₁.trans (M.cl_subset_cl (iUnion_subset fun x ↦ _))
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝¹ y : α
ι : Type u_2
hC : M.Circuit C
x✝ : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x✝ i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x✝ i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hYE : Y ⊆ M.E
h₁ : range x✝ ⊆ M.cl (⋃ i, (Cs i \ {x✝ i}) \ insert z (range x✝))
x : ι
⊢ (Cs x \ {x✝ x}) \ insert z (range x✝) ⊆ Y
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝¹ y : α
ι : Type u_2
hC : M.Circuit C
x✝ : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x✝ i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x✝ i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hYE : Y ⊆ M.E
h₁ : range x✝ ⊆ M.cl (⋃ i, (Cs i \ {x✝ i}) \ insert z (range x✝))
x : ι
⊢ (Cs x \ {x✝ x}) \ insert z (range x✝) ⊆ Y
Tactic:
refine' diff_subset_diff_left (subset_union_of_subset_right _ _)
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝¹ y : α
ι : Type u_2
hC : M.Circuit C
x✝ : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x✝ i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x✝ i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hYE : Y ⊆ M.E
h₁ : range x✝ ⊆ M.cl (⋃ i, (Cs i \ {x✝ i}) \ insert z (range x✝))
x : ι
⊢ Cs x \ {x✝ x} ⊆ ⋃ x, Cs x
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝¹ y : α
ι : Type u_2
hC : M.Circuit C
x✝ : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x✝ i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x✝ i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hYE : Y ⊆ M.E
h₁ : range x✝ ⊆ M.cl (⋃ i, (Cs i \ {x✝ i}) \ insert z (range x✝))
x : ι
⊢ Cs x \ {x✝ x} ⊆ ⋃ x, Cs x
Tactic:
exact subset_iUnion_of_subset x diff_subset
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
⊢ C \ {z} ⊆ M.cl Y
Tactic:
suffices C \ {z} ⊆ C \ insert z (range x) ∪ range x by
  rw [union_diff_distrib] at hY
  convert this.trans (union_subset_union (subset_union_left.trans_eq hY.symm) h₂) using 1
  rw [union_eq_right.mpr]
  exact M.subset_cl Y
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
⊢ C \ {z} ⊆ C \ insert z (range x) ∪ range x
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
⊢ C \ {z} ⊆ C \ insert z (range x) ∪ range x
Tactic:
rw [← union_singleton, ← diff_diff, diff_subset_iff, singleton_union, ← insert_union,
  insert_diff_singleton, ← singleton_union, union_assoc, diff_union_self]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
⊢ C ⊆ {z} ∪ (C ∪ range x)