Theorem: Matroid.sInter_insert_each (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
X : Set (Set α)
a : α
⊢ insert a (⋂₀ X) = ⋂₀ {x | ∃ x_1 ∈ X, insert a x_1 = x}
Tactic:
ext x
State after:
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ x ∈ insert a (⋂₀ X) ↔ x ∈ ⋂₀ {x | ∃ x_1 ∈ X, insert a x_1 = x}

State before:
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ x ∈ insert a (⋂₀ X) ↔ x ∈ ⋂₀ {x | ∃ x_1 ∈ X, insert a x_1 = x}
Tactic:
simp
State after:
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ (x = a ∨ ∀ t ∈ X, x ∈ t) ↔ ∀ a_1 ∈ X, x = a ∨ x ∈ a_1

State before:
case h
α : Type u_1
X : Set (Set α)
a x : α
⊢ (x = a ∨ ∀ t ∈ X, x ∈ t) ↔ ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
Tactic:
refine' ⟨fun h y y_mem ↦ _, fun h ↦ _⟩
State after:
case h.refine'_1
α : Type u_1
X : Set (Set α)
a x : α
h : x = a ∨ ∀ t ∈ X, x ∈ t
y : Set α
y_mem : y ∈ X
⊢ x = a ∨ x ∈ y

case h.refine'_2
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
⊢ x = a ∨ ∀ t ∈ X, x ∈ t

State before:
case h.refine'_2
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
⊢ x = a ∨ ∀ t ∈ X, x ∈ t
Tactic:
obtain (rfl | ne) := eq_or_ne x a
State after:
case h.refine'_2.inl
α : Type u_1
X : Set (Set α)
x : α
h : ∀ a ∈ X, x = x ∨ x ∈ a
⊢ x = x ∨ ∀ t ∈ X, x ∈ t

case h.refine'_2.inr
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
ne : x ≠ a
⊢ x = a ∨ ∀ t ∈ X, x ∈ t

State before:
case h.refine'_2.inr
α : Type u_1
X : Set (Set α)
a x : α
h : ∀ a_1 ∈ X, x = a ∨ x ∈ a_1
ne : x ≠ a
⊢ x = a ∨ ∀ t ∈ X, x ∈ t
Tactic:
exact Or.inr (fun t t_mem ↦ (or_iff_right ne).1 (h t t_mem))
State after:
no goals

State before:
case h.refine'_1
α : Type u_1
X : Set (Set α)
a x : α
h : x = a ∨ ∀ t ∈ X, x ∈ t
y : Set α
y_mem : y ∈ X
⊢ x = a ∨ x ∈ y
Tactic:
obtain (rfl | h) := h
State after:
case h.refine'_1.inl
α : Type u_1
X : Set (Set α)
x : α
y : Set α
y_mem : y ∈ X
⊢ x = x ∨ x ∈ y

case h.refine'_1.inr
α : Type u_1
X : Set (Set α)
a x : α
y : Set α
y_mem : y ∈ X
h : ∀ t ∈ X, x ∈ t
⊢ x = a ∨ x ∈ y

State before:
case h.refine'_1.inr
α : Type u_1
X : Set (Set α)
a x : α
y : Set α
y_mem : y ∈ X
h : ∀ t ∈ X, x ∈ t
⊢ x = a ∨ x ∈ y
Tactic:
exact Or.inr (h y y_mem)
State after:
no goals

State before:
case h.refine'_1.inl
α : Type u_1
X : Set (Set α)
x : α
y : Set α
y_mem : y ∈ X
⊢ x = x ∨ x ∈ y
Tactic:
exact Or.inl rfl
State after:
no goals

State before:
case h.refine'_2.inl
α : Type u_1
X : Set (Set α)
x : α
h : ∀ a ∈ X, x = x ∨ x ∈ a
⊢ x = x ∨ ∀ t ∈ X, x ∈ t
Tactic:
exact Or.inl rfl
State after:
no goals