Theorem: Matroid.Indep.fundCct_circuit (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ M.Circuit (M.fundCct e I)
Tactic:
rw [circuit_iff_dep_forall_diff_singleton_indep,
  ← not_indep_iff (fundCct_subset_ground (M.cl_subset_ground I he.1)), fundCct_eq_sInter he.1]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Tactic:
have hu : M.Indep (⋃₀ {J : Set α | J ⊆ I ∧ e ∈ M.cl J}) :=
  hI.subset (sUnion_subset fun J ↦ And.left)
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Tactic:
have hI' : I ∈ {J : Set α | J ⊆ I ∧ e ∈ M.cl J} := ⟨rfl.subset, he.1⟩
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Tactic:
refine' ⟨fun hi ↦ _, fun f hf ↦ _⟩
State after:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ False

case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : f ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})

State before:
case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : f ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Tactic:
obtain rfl | hne := em (e = f)
State after:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e})

case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : f ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hne : ¬e = f
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})

State before:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : f ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hne : ¬e = f
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Tactic:
rw [mem_insert_iff, mem_sInter, eq_comm, iff_false_intro hne, false_or_iff] at hf
State after:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})

State before:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Tactic:
have hi : M.Indep (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.cl J} \ {f}) :=
  hI.subset (diff_subset.trans (sInter_subset_of_mem hI'))
State after:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})

State before:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Tactic:
rw [← insert_diff_singleton_comm hne, hi.insert_indep_iff_of_not_mem, mem_diff,
  and_iff_right ((M.cl_subset_ground _) he.1)]
State after:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ e ∉ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})

case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f}

State before:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f}
Tactic:
exact fun h'e ↦ he.2 (diff_subset.trans (sInter_subset_of_mem hI') h'e)
State after:
no goals

State before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ False
Tactic:
rw [Indep.insert_indep_iff_of_not_mem] at hi
State after:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : e ∈ M.E \ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ False

case refine'_1.hI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})

case refine'_1.heI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}

State before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : e ∈ M.E \ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ False

case refine'_1.hI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})

case refine'_1.heI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
rw [cl_sInter_eq_biInter_cl_of_sUnion_indep _  ⟨_, hI'⟩ hu] at hi
State after:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : e ∈ M.E \ ⋂ I_1 ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, M.cl I_1
⊢ False

case refine'_1.hI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})

case refine'_1.heI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}

State before:
case refine'_1.heI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
exact fun heIs ↦ he.2 (sInter_subset_of_mem hI' heIs)
State after:
no goals

State before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : e ∈ M.E \ ⋂ I_1 ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, M.cl I_1
⊢ False
Tactic:
simp at hi
State after:
no goals

State before:
case refine'_1.hI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
Tactic:
exact hI.subset (sInter_subset_of_mem hI')
State after:
no goals

State before:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e})
Tactic:
refine' hu.subset _
State after:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e} ⊆ ⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J}

State before:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e} ⊆ ⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
simp only [insert_diff_of_mem, mem_singleton]
State after:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {e} ⊆ ⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J}

State before:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {e} ⊆ ⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
exact
  subset_trans diff_subset ((sInter_subset_of_mem hI').trans (subset_sUnion_of_mem hI'))
State after:
no goals

State before:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ e ∉ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
Tactic:
intro hcl
State after:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
hcl : e ∈ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ False

State before:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
hcl : e ∈ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ False
Tactic:
exact (hf _ ⟨diff_subset.trans (sInter_subset_of_mem hI'), hcl⟩).2 rfl
State after:
no goals