simp only [range_const, iUnion_const] at hCss
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
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