Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep (Matroid/Modular.lean)

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
⊢ M.Indep (⋃ i, Is i)
Tactic:
choose Js hJs using fun i ↦ (hIs i).subset_basis_of_subset (hIX i)
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
⊢ M.Indep (⋃ i, Is i)

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
⊢ M.Indep (⋃ i, Is i)
Tactic:
refine Indep.subset ?_ <| iUnion_mono (fun i ↦ (hJs i).2)
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
⊢ M.Indep (⋃ i, Js i)

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
⊢ M.Indep (⋃ i, Js i)
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis _ (iUnion_subset (fun i ↦ (hJs i).1.indep.subset_ground))
State after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
⊢ M.Indep (⋃ i, Js i)

State before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
⊢ M.Indep (⋃ i, Js i)
Tactic:
by_contra hcon
State after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
⊢ False

State before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
⊢ False
Tactic:
have ex_i : ∃ i e, e ∈ (Js i) \ J := by
  by_contra! h'
  rw [← hJ.subset.antisymm (iUnion_subset fun i e he ↦ by_contra fun heJ ↦ h' i e ⟨he, heJ⟩)]
    at hcon
  exact hcon hJ.indep
State after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
ex_i : ∃ i e, e ∈ Js i \ J
⊢ False

State before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
ex_i : ∃ i e, e ∈ Js i \ J
⊢ False
Tactic:
obtain ⟨i₀, e, hei₀, heJ⟩ := ex_i
State after:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
⊢ False

State before:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
⊢ False
Tactic:
obtain ⟨Ks, hdj, hKs, huKs⟩ := skewFamily_iff_exist_bases.1 h
State after:
case intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ False
Tactic:
have hssE : Js i₀ ∪ (⋃ i ∈ ({i₀}ᶜ : Set ι), Ks i) ⊆ M.E := by
  refine union_subset (hJs i₀).1.indep.subset_ground ?_
  simp only [mem_compl_iff, mem_singleton_iff, iUnion_subset_iff]
  exact fun i _ ↦ (huKs i).indep.subset_ground
State after:
case intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
⊢ False
Tactic:
obtain ⟨K', hK', hss⟩ := (hJs i₀).1.indep.subset_basis_of_subset subset_union_left hssE
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
he' : e ∈ M.cl (K' \ {e})
⊢ False
Tactic:
exact hK'.indep.not_mem_cl_diff_of_mem (hss hei₀) he'
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
⊢ ∃ i e, e ∈ Js i \ J
Tactic:
by_contra! h'
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
h' : ∀ (i : ι) (e : α), e ∉ Js i \ J
⊢ False

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
h' : ∀ (i : ι) (e : α), e ∉ Js i \ J
⊢ False
Tactic:
rw [← hJ.subset.antisymm (iUnion_subset fun i e he ↦ by_contra fun heJ ↦ h' i e ⟨he, heJ⟩)]
  at hcon
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep J
h' : ∀ (i : ι) (e : α), e ∉ Js i \ J
⊢ False

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep J
h' : ∀ (i : ι) (e : α), e ∉ Js i \ J
⊢ False
Tactic:
exact hcon hJ.indep
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
Tactic:
refine union_subset (hJs i₀).1.indep.subset_ground ?_
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, iUnion_subset_iff]
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ ∀ (i : ι), ¬i = i₀ → Ks i ⊆ M.E

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ ∀ (i : ι), ¬i = i₀ → Ks i ⊆ M.E
Tactic:
exact fun i _ ↦ (huKs i).indep.subset_ground
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
⊢ ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
Tactic:
intro i hne f hf
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
⊢ f ∈ K'

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
⊢ f ∈ K'
Tactic:
by_contra hfK'
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ False

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ False
Tactic:
apply hKs.indep.not_mem_cl_diff_of_mem (mem_iUnion.2 ⟨i,hf⟩)
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ f ∈ M.cl ((⋃ i, Ks i) \ {f})

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ f ∈ M.cl ((⋃ i, Ks i) \ {f})
Tactic:
have hcl : f ∈ M.cl K' := by
  exact hK'.subset_cl (Or.inr <| mem_biUnion hne hf)
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ f ∈ M.cl ((⋃ i, Ks i) \ {f})

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ f ∈ M.cl ((⋃ i, Ks i) \ {f})
Tactic:
refine mem_of_mem_of_subset
  (M.cl_subset_cl (subset_diff_singleton hK'.subset hfK') hcl) (M.cl_subset_cl_of_subset_cl ?_)
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i) \ {f} ⊆ M.cl ((⋃ i, Ks i) \ {f})

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i) \ {f} ⊆ M.cl ((⋃ i, Ks i) \ {f})
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, mem_union, mem_iUnion, exists_prop, not_exists,
  diff_singleton_subset_iff, union_subset_iff, iUnion_subset_iff]
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ Js i₀ ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f})) ∧ ∀ (i : ι), ¬i = i₀ → Ks i ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ Js i₀ ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f})) ∧ ∀ (i : ι), ¬i = i₀ → Ks i ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))
Tactic:
refine ⟨(hJs i₀).1.subset.trans ?_, fun i _ ↦ ?_⟩
State after:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ Xs i₀ ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))

case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝¹ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i✝ : ι
hne : i✝ ≠ i₀
f : α
hf : f ∈ Ks i✝
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))

State before:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝¹ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i✝ : ι
hne : i✝ ≠ i₀
f : α
hf : f ∈ Ks i✝
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))
Tactic:
refine subset_trans ?_ <|
  insert_subset_insert (M.subset_cl _ (diff_subset.trans hKs.indep.subset_ground))
State after:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝¹ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i✝ : ι
hne : i✝ ≠ i₀
f : α
hf : f ∈ Ks i✝
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f ((⋃ i, Ks i) \ {f})

State before:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝¹ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i✝ : ι
hne : i✝ ≠ i₀
f : α
hf : f ∈ Ks i✝
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f ((⋃ i, Ks i) \ {f})
Tactic:
rw [insert_diff_singleton]
State after:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝¹ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i✝ : ι
hne : i✝ ≠ i₀
f : α
hf : f ∈ Ks i✝
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f (⋃ i, Ks i)

State before:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝¹ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i✝ : ι
hne : i✝ ≠ i₀
f : α
hf : f ∈ Ks i✝
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f (⋃ i, Ks i)
Tactic:
exact (subset_iUnion Ks i).trans (subset_insert _ _)
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ f ∈ M.cl K'
Tactic:
exact hK'.subset_cl (Or.inr <| mem_biUnion hne hf)
State after:
no goals

State before:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ Xs i₀ ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))
Tactic:
refine (huKs i₀).subset_cl.trans (subset_trans (M.cl_subset_cl ?_) (subset_insert _ _))
State after:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ Ks i₀ ⊆ (⋃ i, Ks i) \ {f}

State before:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ Ks i₀ ⊆ (⋃ i, Ks i) \ {f}
Tactic:
refine subset_diff_singleton (subset_iUnion Ks i₀) (fun hf' ↦ ?_)
State after:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
hf' : f ∈ Ks i₀
⊢ False

State before:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
hf' : f ∈ Ks i₀
⊢ False
Tactic:
exact (hdj hne).ne_of_mem hf hf' rfl
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
⊢ e ∈ M.cl (K' \ {e})
Tactic:
refine mem_of_mem_of_subset (hJ.subset_cl (mem_iUnion_of_mem _ hei₀)) ?_
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
⊢ M.cl J ⊆ M.cl (K' \ {e})

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
⊢ M.cl J ⊆ M.cl (K' \ {e})
Tactic:
rw [cl_subset_cl_iff_subset_cl]
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
⊢ J ⊆ M.cl (K' \ {e})

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
⊢ J ⊆ M.cl (K' \ {e})
Tactic:
rintro f hf
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
⊢ f ∈ M.cl (K' \ {e})

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
⊢ f ∈ M.cl (K' \ {e})
Tactic:
obtain ⟨i, hfi⟩ := mem_iUnion.1 (hJ.subset hf)
State after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
⊢ f ∈ M.cl (K' \ {e})

State before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
⊢ f ∈ M.cl (K' \ {e})
Tactic:
obtain (rfl | hi) := eq_or_ne i₀ i
State after:
case intro.inl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
hfi : f ∈ Js i₀
⊢ f ∈ M.cl (K' \ {e})

case intro.inr
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
⊢ f ∈ M.cl (K' \ {e})

State before:
case intro.inr
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
⊢ f ∈ M.cl (K' \ {e})
Tactic:
refine mem_of_mem_of_subset ((hJs i).1.subset.trans (huKs i).subset_cl hfi) (M.cl_subset_cl ?_)
State after:
case intro.inr
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
⊢ Ks i ⊆ K' \ {e}

State before:
case intro.inr
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
⊢ Ks i ⊆ K' \ {e}
Tactic:
refine subset_diff_singleton (hK'' i hi.symm) (fun heK ↦ ?_)
State after:
case intro.inr
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
heK : e ∈ Ks i
⊢ False

State before:
case intro.inr
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
heK : e ∈ Ks i
⊢ False
Tactic:
apply Loop.not_nonloop <| h.loop_of_mem_inter hi ⟨(hJs i₀).1.subset hei₀, (huKs i).subset heK⟩
State after:
case intro.inr
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
heK : e ∈ Ks i
⊢ M.Nonloop e

State before:
case intro.inr
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i✝ j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
heK : e ∈ Ks i
⊢ M.Nonloop e
Tactic:
exact (hK'.indep.subset hss).nonloop_of_mem hei₀
State after:
no goals

State before:
case intro.inl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
hfi : f ∈ Js i₀
⊢ f ∈ M.cl (K' \ {e})
Tactic:
apply M.subset_cl (K' \ {e}) (diff_subset.trans hK'.indep.subset_ground)
State after:
case intro.inl.a
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
hfi : f ∈ Js i₀
⊢ f ∈ K' \ {e}

State before:
case intro.inl.a
ι : Type u_1
α : Type u_2
M : Matroid α
B I J✝ X X' Y Y' F : Set α
Xs Ys Js✝ Is : ι → Set α
i j : ι
e✝ f✝ : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
hfi : f ∈ Js i₀
⊢ f ∈ K' \ {e}
Tactic:
exact ⟨hss hfi, fun (h : f = e) ↦ heJ <| h ▸ hf⟩
State after:
no goals