internlm/Lean-Github huggingface dataset:
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 ∪ range x)
Tactic:
exact subset_union_of_subset_right subset_union_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)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
this : C \ {z} ⊆ C \ insert z (range x) ∪ range x
⊢ C \ {z} ⊆ M.cl Y
Tactic:
rw [union_diff_distrib] at hY
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 \ insert z (range x) ∪ (⋃ 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
this : C \ {z} ⊆ C \ insert z (range x) ∪ range x
⊢ C \ {z} ⊆ M.cl 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 \ insert z (range x) ∪ (⋃ 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
this : C \ {z} ⊆ C \ insert z (range x) ∪ range x
⊢ C \ {z} ⊆ M.cl Y
Tactic:
convert this.trans (union_subset_union (subset_union_left.trans_eq hY.symm) h₂) using 1
Proof state after:
case h.e'_4
α : 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 \ insert z (range x) ∪ (⋃ 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
this : C \ {z} ⊆ C \ insert z (range x) ∪ range x
⊢ M.cl Y = Y ∪ M.cl Y
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case h.e'_4
α : 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 \ insert z (range x) ∪ (⋃ 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
this : C \ {z} ⊆ C \ insert z (range x) ∪ range x
⊢ M.cl Y = Y ∪ M.cl Y
Tactic:
rw [union_eq_right.mpr]
Proof state after:
case h.e'_4
α : 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 \ insert z (range x) ∪ (⋃ 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
this : C \ {z} ⊆ C \ insert z (range x) ∪ range x
⊢ Y ⊆ M.cl Y
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case h.e'_4
α : 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 \ insert z (range x) ∪ (⋃ 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
this : C \ {z} ⊆ C \ insert z (range x) ∪ range x
⊢ Y ⊆ M.cl Y
Tactic:
exact M.subset_cl Y
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case 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'
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
hzY : z ∈ Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
exact ((hY.subset hzY).2 (mem_insert z _)).elim
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
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
Tactic:
exact hCzY.trans (insert_subset (Or.inl hz.1) diff_subset)
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
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
Tactic:
rintro x' ⟨i, rfl⟩
Proof state after:
case inr.intro.intro.intro.refine'_2.refine'_1.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
i : ι
⊢ x i ∈ ⋃ i, Cs i
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
case inr.intro.intro.intro.refine'_2.refine'_1.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
i : ι
⊢ x i ∈ ⋃ i, Cs i
Tactic:
exact mem_iUnion_of_mem i (h_mem i).2
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ f ∈ C
Tactic:
obtain ⟨C, hC, hfC, hCss⟩ :=
  @Circuit.strong_multi_elimination _ M C₁ Unit hC₁ (fun _ ↦ e) (fun _ ↦ C₂) (by simpa)
    (by simpa) (by simp) f (by simpa)
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
C : Set α
hC : M.Circuit C
hfC : f ∈ C
hCss : C ⊆ (C₁ ∪ ⋃ i, C₂) \ range fun x => e
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ f ∈ C
Theorem: Matroid.Circuit.strong_elimination
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
C : Set α
hC : M.Circuit C
hfC : f ∈ C
hCss : C ⊆ (C₁ ∪ ⋃ i, C₂) \ range fun x => e
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ f ∈ C
Tactic:
simp only [range_const, iUnion_const] at hCss
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
C : Set α
hC : M.Circuit C
hfC : f ∈ C
hCss : C ⊆ (C₁ ∪ C₂) \ {e}
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ f ∈ C
Theorem: Matroid.Circuit.strong_elimination
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
C : Set α
hC : M.Circuit C
hfC : f ∈ C
hCss : C ⊆ (C₁ ∪ C₂) \ {e}
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ f ∈ C
Tactic:
exact ⟨C, hC, hCss, hfC⟩
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
⊢ ∀ (i : Unit), M.Circuit ((fun x => C₂) i)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
⊢ ∀ (i : Unit), (fun x => e) i ∈ C₁ ∩ (fun x => C₂) i
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
⊢ ∀ (i i' : Unit), (fun x => e) i ∈ (fun x => C₂) i' → i = i'
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
he : e ∈ C₁ ∩ C₂
hf : f ∈ C₁ \ C₂
⊢ f ∈ C₁ \ ⋃ i, (fun x => C₂) i
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Circuit.elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
have hne : (C₁ \ C₂).Nonempty := by
  rw [nonempty_iff_ne_empty, Ne, diff_eq_empty]
  exact fun hss ↦ h (hC₁.eq_of_subset_circuit hC₂ hss)
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Theorem: Matroid.Circuit.elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
obtain (he₁ | he₁) := em (e ∈ C₁)
Proof state after:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}

case inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∉ C₁
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Theorem: Matroid.Circuit.elimination
Proof state before:
case inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∉ C₁
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
exact ⟨C₁, hC₁, subset_diff_singleton subset_union_left he₁⟩
Proof state after:
no goals
Theorem: Matroid.Circuit.elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
⊢ (C₁ \ C₂).Nonempty
Tactic:
rw [nonempty_iff_ne_empty, Ne, diff_eq_empty]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
⊢ ¬C₁ ⊆ C₂
Theorem: Matroid.Circuit.elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
⊢ ¬C₁ ⊆ C₂
Tactic:
exact fun hss ↦ h (hC₁.eq_of_subset_circuit hC₂ hss)
Proof state after:
no goals
Theorem: Matroid.Circuit.elimination
Proof state before:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
obtain (he₂ | he₂) := em (e ∈ C₂)
Proof state after:
case inl.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}

case inl.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∉ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Theorem: Matroid.Circuit.elimination
Proof state before:
case inl.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∉ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
exact ⟨C₂, hC₂, subset_diff_singleton subset_union_right he₂⟩
Proof state after:
no goals
Theorem: Matroid.Circuit.elimination
Proof state before:
case inl.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∈ C₂
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
obtain ⟨C, h⟩ :=  hC₁.strong_elimination hC₂ ⟨he₁,he₂⟩ hne.some_mem
Proof state after:
case inl.inl.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h✝ : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∈ C₂
C : Set α
h : M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ hne.some ∈ C
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Theorem: Matroid.Circuit.elimination
Proof state before:
case inl.inl.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC₁ : M.Circuit C₁
hC₂ : M.Circuit C₂
h✝ : C₁ ≠ C₂
e : α
hne : (C₁ \ C₂).Nonempty
he₁ : e ∈ C₁
he₂ : e ∈ C₂
C : Set α
h : M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e} ∧ hne.some ∈ C
⊢ ∃ C, M.Circuit C ∧ C ⊆ (C₁ ∪ C₂) \ {e}
Tactic:
exact ⟨C, h.1, h.2.1⟩
Proof state after:
no goals
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
⊢ C = M.fundCct e I
Tactic:
have heI : e ∉ I := by
  intro heI; rw [insert_eq_of_mem heI] at hCI; exact (hC.dep.superset hCI).not_indep hI
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
⊢ C = M.fundCct e I
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
⊢ C = M.fundCct e I
Tactic:
have heC : e ∈ C := by
  refine' by_contra fun heC ↦ (hI.subset _).not_dep hC.dep
  rwa [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self heC] at hCI
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ C = M.fundCct e I
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ C = M.fundCct e I
Tactic:
have he : e ∈ M.cl I := by
  rw [mem_cl_iff_exists_circuit_of_not_mem heI]; exact ⟨C, hC, heC, hCI⟩
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
⊢ C = M.fundCct e I
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
⊢ C = M.fundCct e I
Tactic:
by_contra! hne
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
⊢ False
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
⊢ False
Tactic:
obtain ⟨Cf, hCf, hCfss⟩ := hC.elimination (hI.fundCct_circuit ⟨he,heI⟩) hne e
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ False
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ False
Tactic:
refine' hCf.dep.not_indep (hI.subset (hCfss.trans _))
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ (C ∪ M.fundCct e I) \ {e} ⊆ I
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ (C ∪ M.fundCct e I) \ {e} ⊆ I
Tactic:
rw [diff_subset_iff, singleton_union, union_subset_iff, and_iff_right hCI]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ M.fundCct e I ⊆ insert e I
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ M.fundCct e I ⊆ insert e I
Tactic:
exact fundCct_subset_insert _ _
Proof state after:
no goals
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
⊢ e ∉ I
Tactic:
intro heI
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∈ I
⊢ False
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∈ I
⊢ False
Tactic:
rw [insert_eq_of_mem heI] at hCI
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ I
heI : e ∈ I
⊢ False
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ I
heI : e ∈ I
⊢ False
Tactic:
exact (hC.dep.superset hCI).not_indep hI
Proof state after:
no goals
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
⊢ e ∈ C
Tactic:
refine' by_contra fun heC ↦ (hI.subset _).not_dep hC.dep
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∉ C
⊢ C ⊆ I
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∉ C
⊢ C ⊆ I
Tactic:
rwa [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self heC] at hCI
Proof state after:
no goals
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ e ∈ M.cl I
Tactic:
rw [mem_cl_iff_exists_circuit_of_not_mem heI]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e I
Theorem: Matroid.Circuit.eq_fundCct_of_subset_insert_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e I
Tactic:
exact ⟨C, hC, heC, hCI⟩
Proof state after:
no goals