awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
inr : (J ∪ range x) \ {z} ⊆ range x ∪ J \ {z}
⊢ z ∈ M.closure (range x ∪ J \ {z} ∪ ⋃ (i : ι), I i)

Tactic:
refine mem_of_mem_of_subset (hJx.mem_closure_diff_singleton_of_mem (.inl hzJ))
    (M.closure_subset_closure (subset_trans ?_ subset_union_left))

Premises used: Matroid.IsCircuit.mem_closure_diff_singleton_of_mem, subset_trans, Matroid.closure_subset_closure, Set.subset_union_left, Set.mem_of_mem_of_subset, Or.inl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
inr : range x \ {z} ∪ J \ {z} ⊆ range x ∪ J \ {z}
⊢ (J ∪ range x) \ {z} ⊆ range x ∪ J \ {z}

Tactic:
rw [union_diff_distrib, union_comm]

Premises used: Set.union_comm, Set.union_diff_distrib
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ range x \ {z} ∪ J \ {z} ⊆ range x ∪ J \ {z}

Tactic:
union_subset_union_left _ diff_subset

Premises used: Set.diff_subset, Set.union_subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ range x \ {z} ∪ J \ {z} ⊆ range x ∪ J \ {z}

Tactic:
exact union_subset_union_left _ diff_subset

Premises used: Set.diff_subset, Set.union_subset_union_left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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
refine_5 :
  ∀ (hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i, M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : ι), M.IsCircuit (insert (x i) ((fun (i : ι) ↦ C i \ {x i}) i))
refine_2 : M.IsCircuit (C₀ \ range x ∪ range x)
refine_3 : z ∉ range x
refine_4 : ∀ (i : ι), z ∉ (fun (i : ι) ↦ C i \ {x i}) i
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Tactic:
have hwin := IsCircuit.strong_multi_elimination_insert (M := M) x (fun i ↦ (C i \ {x i}))
    (J := C₀ \ range x) (z := z) (by simp) (fun i ↦ ?_) ?_ ⟨hzC₀, ?_⟩ ?_
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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
hwin : ∃ C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i, M.IsCircuit C' ∧ z ∈ C'
refine_5 :
  ∀ (C' : Set α) (hC'ss : C' ⊆ C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i) (hC' : M.IsCircuit C')
    (hzC' : z ∈ C'), ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Tactic:
obtain ⟨C', hC'ss, hC', hzC'⟩ := hwin
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Tactic:
⟨C', hC'ss.trans ?_, hC', hzC'⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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'
refine_5 : C₀ \ range x ∪ ⋃ (i : ι), (fun (i : ι) ↦ C i \ {x i}) i ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x
⊢ ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ range x, M.IsCircuit C' ∧ z ∈ C'

Tactic:
refine ⟨C', hC'ss.trans ?_, hC', hzC'⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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:
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 ..) _), ?_⟩)

Premises used: Iff.mpr, Set.diff_subset, Set.iUnion_subset, HasSubset.Subset.trans, Set.subset_diff, Set.diff_subset_diff_left, Set.union_subset, Set.subset_iUnion, Set.subset_union_left, Set.subset_union_of_subset_right, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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'
refine_5 : ∀ (i : ι), Disjoint (C i \ {x i}) (range x)
⊢ 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 ..) _), ?_⟩)

Premises used: Iff.mpr, Set.diff_subset, Set.iUnion_subset, HasSubset.Subset.trans, Set.subset_diff, Set.diff_subset_diff_left, Set.union_subset, Set.subset_iUnion, Set.subset_union_left, Set.subset_union_of_subset_right, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : ι
refine_5 : ∀ ⦃a : α⦄, a ∈ C i \ {x i} → ∀ ⦃b : α⦄, b ∈ range x → a ≠ b
⊢ Disjoint (C i \ {x i}) (range x)

Tactic:
rw [disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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}
⊢ j = i

Tactic:
h_unique he.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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}
⊢ x j ∈ C j \ {x j}

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

Premises used: And.left, rfl
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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

Tactic:
simp at he
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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
refine_2 : range x ⊆ C₀
⊢ M.IsCircuit (C₀ \ range x ∪ range x)

Tactic:
rwa [diff_union_self, union_eq_self_of_subset_right]

Premises used: Set.union_eq_self_of_subset_right, Set.diff_union_self
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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:
h_mem_C₀ i
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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:
hzC _ (h_mem i)
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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)
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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
refine_4 : ∀ (i : ι), z ∈ C i → z = x i
⊢ ∀ (i : ι), z ∉ (fun (i : ι) ↦ C i \ {x i}) i

Tactic:
simp only [mem_diff, mem_singleton_iff, not_and, not_not]

Premises used: Classical.not_not, Set.mem_singleton_iff, Set.mem_diff, not_and
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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:
fun i hzi ↦ (hzC i hzi).elim

Premises used: False.elim
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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

Premises used: False.elim
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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₀
hX : ∀ x ∈ X, ∃ C ∈ S, C ∩ X = {x}
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
choose! :
  ∀ (C : (x : α) → Set α) (hC : ∀ x ∈ X, C x ∈ S ∧ C x ∩ X = {x}), ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Tactic:
choose! C hC using hX
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : ∀ x ∈ X, C x ∈ S ∧ C x ∩ X = {x}
⊢ (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}

Tactic:
simp only [forall_and] at hC

Premises used: forall_and
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_6 :
  ∀
    (hwin :
      ∃
        C' ⊆
          (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
            range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
        M.IsCircuit C' ∧ z ∈ C'),
    ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
refine_1 : ∀ (i : (↑X : Type u_1)), M.IsCircuit ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i)
refine_2 : ∀ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i ∈ C₀
refine_3 :
  ∀ (i : (↑X : Type u_1)),
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i)
refine_4 :
  ∀ ⦃i i' : (↑X : Type u_1)⦄,
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i')
        ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i) →
      i = i'
refine_5 : ∀ (i : (↑X : Type u_1)), z ∉ (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Tactic:
have hwin := hC₀.strong_multi_elimination (fun x : X ↦ x) (fun x ↦ C x) z ?_ ?_ ?_ ?_ hzC₀ ?_
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
hwin :
  ∃
    C' ⊆
      (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
        range fun (x : (↑X : Type u_1)) ↦ (↑x : α),
    M.IsCircuit C' ∧ z ∈ C'
refine_6 :
  ∀ (C' : Set α)
    (hC'ss :
      C' ⊆
        (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
          range fun (x : (↑X : Type u_1)) ↦ (↑x : α))
    (hC' : M.IsCircuit C') (hz : z ∈ C'), ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Tactic:
obtain ⟨C', hC'ss, hC', hz⟩ := hwin
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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_1 : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
C' : Set α
hC'ss :
  C' ⊆
    (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
      range fun (x : (↑X : Type u_1)) ↦ (↑x : α)
hC' : M.IsCircuit C'
hz : z ∈ C'
⊢ X ⊆ range fun (x : (↑X : Type u_1)) ↦ (↑x : α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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_1 : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
C' : Set α
hC'ss :
  C' ⊆
    (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
      range fun (x : (↑X : Type u_1)) ↦ (↑x : α)
hC' : M.IsCircuit C'
hz : z ∈ C'
refine_6 : ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i ⊆ ⋃₀ S
⊢ ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

Tactic:
refine ⟨C', hC'ss.trans (diff_subset_diff (union_subset_union_right _ ?_) (by simp)), hC', hz⟩
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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_1 : ∀ C ∈ S, z ∉ C
C : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
C' : Set α
hC'ss :
  C' ⊆
    (C₀ ∪ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) \
      range fun (x : (↑X : Type u_1)) ↦ (↑x : α)
hC' : M.IsCircuit C'
hz : z ∈ C'
⊢ ⋃ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i ⊆ ⋃₀ S

Tactic:
simpa using fun e heX ↦ (subset_sUnion_of_mem (hC.1 e heX))

Premises used: And.left, Set.subset_sUnion_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
⊢ ∀ (i : (↑X : Type u_1)), M.IsCircuit ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i)

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

Premises used: And.left
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
⊢ ∀ (i : (↑X : Type u_1)), (fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i ∈ C₀

Tactic:
simpa using fun e heX ↦ hXC₀ heX
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_3 : ∀ (a : α) (b : a ∈ X), {a} ⊆ C a
⊢ ∀ (i : (↑X : Type u_1)),
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i) ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i)

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

Premises used: Set.singleton_subset_iff, Subtype.forall
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
e : α
heX : e ∈ X
⊢ {e} ⊆ C e

Tactic:
simp [← hC.2 e heX]

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
⊢ ∀ (a : α) (b : a ∈ X), {a} ⊆ C a

Tactic:
exact fun e heX ↦ by simp [← hC.2 e heX]
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_4 : ∀ (a : α) (b : a ∈ X) (a_1 : α) (b : a_1 ∈ X), a ∈ C a_1 → a = a_1
⊢ ∀ ⦃i i' : (↑X : Type u_1)⦄,
    Membership.mem (γ := Set α) ((fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i')
        ((fun (x : (↑X : Type u_1)) ↦ (↑x : α)) i) →
      i = i'

Tactic:
simp only [Subtype.forall, Subtype.mk.injEq]

Premises used: Subtype.forall, Subtype.mk.injEq
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
⊢ ∀ (a : α) (b : a ∈ X) (a_1 : α) (b : a_1 ∈ X), a ∈ C a_1 → a = a_1

Tactic:
fun e heX f hfX hef ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
refine_4 : ∀ (e : α) (heX : e ∈ X) (f : α) (hfX : f ∈ X) (hef : e ∈ C f), e = f
⊢ ∀ (a : α) (b : a ∈ X) (a_1 : α) (b : a_1 ∈ X), a ∈ C a_1 → a = a_1

Tactic:
refine fun e heX f hfX hef ↦ ?_
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : 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)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.subset_inter, And.right
-- Module: Mathlib.Combinatorics.Matroid.Circuit
Goal:
α : 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 : (x : α) → Set α
hC : (∀ (x : α) (x_1 : x ∈ X), C x ∈ S) ∧ ∀ (x : α) (x_1 : x ∈ X), C x ∩ X = {x}
⊢ ∀ (i : (↑X : Type u_1)), z ∉ (fun (x : (↑X : Type u_1)) ↦ C (↑x : α)) i

Tactic:
simpa using fun e heX heC ↦ hz _ (hC.1 e heX) heC

Premises used: And.left