-- Mathlib/Data/Matroid/Circuit.lean
/-- A generalization of the strong circuit elimination axiom `Matroid.IsCircuit.strong_elimination`
to an infinite collection of isCircuits.

It states that, given a circuit `C₀`, a arbitrary collection `C : ι → Set α` of circuits,
an element `x i` of `C₀ ∩ C i` for each `i`, and an element `z ∈ C₀` outside all the `C i`,
the union of `C₀` and the `C i` contains a circuit containing `z` but none of the `x i`.

This is one of the axioms when defining infinite matroids via circuits.

TODO : A similar statement will hold even when all mentions of `z` are removed. -/
lemma IsCircuit.strong_multi_elimination (hC₀ : M.IsCircuit C₀) (x : ι → α) (C : ι → Set α) (z : α)
    (hC : ∀ i, M.IsCircuit (C i)) (h_mem_C₀ : ∀ i, x i ∈ C₀) (h_mem : ∀ i, x i ∈ C i)
    (h_unique : ∀ ⦃i i'⦄, x i ∈ C i' → i = i') (hzC₀ : z ∈ C₀) (hzC : ∀ i, z ∉ C i) :
    ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Proof state:
case refine_3
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ z ∉ range x

Tactic:
rintro ⟨i, hi, rfl⟩

Result:
case refine_3.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
i : ι
hzC₀ : x i ∈ C₀
hzC : ∀ (i_1 : ι), x i ∉ C i_1
⊢ False

Proof state:
case refine_5.intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, (fun i => C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i j : ι
he : x j ∈ C i \ {x i}
⊢ False

Tactic:
obtain rfl : j = i := h_unique he.1

Result:
case refine_5.intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, (fun i => C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
j : ι
he : x j ∈ C j \ {x j}
⊢ False

Proof state:
case refine_5.intro.intro.intro
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, (fun i => C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C₀ \ range x ∪ ⋃ i, (fun i => C i \ {x i}) i ⊆ (C₀ ∪ ⋃ i, C i) \ range x

Tactic:
refine union_subset (diff_subset_diff_left subset_union_left)
  (iUnion_subset fun i ↦ subset_diff.2
    ⟨diff_subset.trans (subset_union_of_subset_right (subset_iUnion ..) _), ?_⟩)

Result:
case refine_5.intro.intro.intro
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, (fun i => C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i : ι
⊢ Disjoint (C i \ {x i}) (range x)

Proof state:
case refine_2.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
i : ι
⊢ x i ∈ C₀

Tactic:
exact h_mem_C₀ i

Result:
no goals

Proof state:
case refine_4
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ ∀ (i : ι), z ∈ C i → z = x i

Tactic:
exact fun i hzi ↦ (hzC i hzi).elim

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
⊢ ∀ (i : ι), x i ∉ (fun i => C i \ {x i}) i

Tactic:
simp

Result:
no goals

Proof state:
case refine_5.intro.intro.intro
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, (fun i => C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i : ι
⊢ ∀ ⦃a : α⦄, a ∈ C i \ {x i} → ∀ ⦃b : α⦄, b ∈ range x → a ≠ b

Tactic:
rintro _ he _ ⟨j, hj, rfl⟩ rfl

Result:
case refine_5.intro.intro.intro.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
C' : Set α
hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ i, (fun i => C i \ {x i}) i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
i j : ι
he : x j ∈ C i \ {x i}
⊢ False

Proof state:
case refine_3.intro.refl
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
i : ι
hzC₀ : x i ∈ C₀
hzC : ∀ (i_1 : ι), x i ∉ C i_1
⊢ False

Tactic:
exact hzC _ (h_mem i)

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
z : α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
hzC₀ : z ∈ C₀
hzC : ∀ (i : ι), z ∉ C i
i : ι
⊢ M.IsCircuit (insert (x i) ((fun i => C i \ {x i}) i))

Tactic:
simpa [insert_eq_of_mem (h_mem i)] using hC i

Result:
no goals