case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
⊢ insert a s \ t = insert a (s \ t)
ext x
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)

case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : ¬x ∈ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
by_cases h' : x ∈ t
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
this : x ≠ a
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
have : x ≠ a := by
  intro H
  rw [H] at h'
  exact h h'
no goals
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
this : x ≠ a
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
simp [h, h', this]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
H : x = a
⊢ False
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
⊢ x ≠ a
intro H
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : a ∈ t
H : x = a
⊢ False
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
H : x = a
⊢ False
rw [H] at h'
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : a ∈ t
H : x = a
⊢ False
exact h h'
no goals
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : ¬x ∈ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
simp [h, h']