-- Mathlib/Data/Matroid/Circuit.lean
/-- A version of `Circuit.strong_multi_elimination` where the collection of circuits is
a `Set (Set α)` and the distinguished elements are a `Set α`, rather than both being indexed. -/
lemma IsCircuit.strong_multi_elimination_set (hC₀ : M.IsCircuit C₀) (X : Set α) (S : Set (Set α))
    (z : α) (hCS : ∀ C ∈ S, M.IsCircuit C) (hXC₀ : X ⊆ C₀) (hX : ∀ x ∈ X, ∃ C ∈ S, C ∩ X = {x})
    (hzC₀ : z ∈ C₀) (hz : ∀ C ∈ S, z ∉ C) : ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Proof state:
case refine_1
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), M.IsCircuit ((fun x => C ↑x) i)

Tactic:
simpa using fun e heX ↦ hCS _ <| hC.1 e heX

Result:
no goals

Proof state:
case refine_3
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), (fun x => ↑x) i ∈ (fun x => C ↑x) i

Tactic:
simp only [Subtype.forall, ← singleton_subset_iff (s := C _)]

Result:
case refine_3
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ a ∈ X, {a} ⊆ C a

Proof state:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz✝ : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
C' : Set α
hC'ss : C' ⊆ (C₀ ∪ ⋃ i, (fun x => C ↑x) i) \ range fun x => ↑x
hC' : M.IsCircuit C'
hz : z ∈ C'
⊢ X ⊆ range fun x => ↑x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : ∀ x ∈ X, C x ∈ S ∧ C x ∩ X = {x}
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Tactic:
simp only [and_imp, forall_and, and_assoc] at hC

Result:
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Proof state:
case refine_4
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ a ∈ X, ∀ a_1 ∈ X, a ∈ C a_1 → a = a_1

Tactic:
refine fun e heX f hfX hef ↦ ?_

Result:
case refine_4
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
e : α
heX : e ∈ X
f : α
hfX : f ∈ X
hef : e ∈ C f
⊢ e = f

Proof state:
case refine_4
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
e : α
heX : e ∈ X
f : α
hfX : f ∈ X
hef : e ∈ C f
⊢ e = f

Tactic:
simpa [hC.2 f hfX] using subset_inter (singleton_subset_iff.2 hef) (singleton_subset_iff.2 heX)

Result:
no goals