Theorem: Matroid.Circuit.strong_elimination (Matroid/Circuit.lean)

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

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

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⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals