Theorem: Set.insertIf_true_eq_insert (GMLInit/Data/Set/Insert.lean)

State before:
α : Sort u_1
a : α
s : Set α
⊢ s.insertIf a True = s.insert a
Tactic:
apply Set.ext
State after:
case a
α : Sort u_1
a : α
s : Set α
⊢ ∀ (x : α), x ∈ s.insertIf a True ↔ x ∈ s.insert a

State before:
case a
α : Sort u_1
a : α
s : Set α
⊢ ∀ (x : α), x ∈ s.insertIf a True ↔ x ∈ s.insert a
Tactic:
intro x
State after:
case a
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True ↔ x ∈ s.insert a

State before:
case a
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True ↔ x ∈ s.insert a
Tactic:
constructor
State after:
case a.mp
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True → x ∈ s.insert a

case a.mpr
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insert a → x ∈ s.insertIf a True

State before:
case a.mp
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True → x ∈ s.insert a
Tactic:
intro
| Or.inl ⟨_,_⟩ => left; assumption
| Or.inr _ => right; assumption
State after:
no goals

State before:
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
left✝ : x = a
right✝ : True
⊢ x ∈ s.insert a
Tactic:
left
State after:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
left✝ : x = a
right✝ : True
⊢ x ∈ Set.pure a

State before:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
left✝ : x = a
right✝ : True
⊢ x ∈ Set.pure a
Tactic:
assumption
State after:
no goals

State before:
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
h✝ : x ∈ s
⊢ x ∈ s.insert a
Tactic:
right
State after:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
h✝ : x ∈ s
⊢ x ∈ s

State before:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insertIf a True
h✝ : x ∈ s
⊢ x ∈ s
Tactic:
assumption
State after:
no goals

State before:
case a.mpr
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insert a → x ∈ s.insertIf a True
Tactic:
intro
| Or.inl _ => left; constructor; assumption; trivial
| Or.inr _ => right; assumption
State after:
no goals

State before:
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x ∈ s.insertIf a True
Tactic:
left
State after:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x ∈ Set.pureIf a True

State before:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x ∈ Set.pureIf a True
Tactic:
constructor
State after:
case h.left
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x = a

case h.right
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ True

State before:
case h.left
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ x = a

case h.right
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ True
Tactic:
assumption
State after:
case h.right
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ True

State before:
case h.right
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ Set.pure a
⊢ True
Tactic:
trivial
State after:
no goals

State before:
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ s
⊢ x ∈ s.insertIf a True
Tactic:
right
State after:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ s
⊢ x ∈ s

State before:
case h
α : Sort u_1
a : α
s : Set α
x : α
x✝ : x ∈ s.insert a
h✝ : x ∈ s
⊢ x ∈ s
Tactic:
assumption
State after:
no goals