[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
b : β
f : α → β
a : Option α
⊢ Option.elim' b f a = Option.elim a b f
[PROOFSTEP]
cases a
[GOAL]
case none
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
b : β
f : α → β
⊢ Option.elim' b f none = Option.elim none b f
[PROOFSTEP]
rfl
[GOAL]
case some
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
b : β
f : α → β
val✝ : α
⊢ Option.elim' b f (some val✝) = Option.elim (some val✝) b f
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
a b : α
⊢ a ∈ some b ↔ b = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (a : α), a ∈ none → p a
[PROOFSTEP]
simp [false_imp_iff]
[GOAL]
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
x✝ : ∃ a, a ∈ none ∧ p a
a : α
h : a ∈ none
right✝ : p a
⊢ False
[PROOFSTEP]
cases h
[GOAL]
α : Type u_1
β : Type u_2
a : α
o : Option α
⊢ a ∈ toList o ↔ a ∈ o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
a : α
⊢ a ∈ toList none ↔ a ∈ none
[PROOFSTEP]
simp [toList, eq_comm]
[GOAL]
case some
α : Type u_1
β : Type u_2
a val✝ : α
⊢ a ∈ toList (some val✝) ↔ a ∈ some val✝
[PROOFSTEP]
simp [toList, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsCommutative α f
a b : Option α
⊢ liftOrGet f a b = liftOrGet f b a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsCommutative α f
b : Option α
⊢ liftOrGet f none b = liftOrGet f b none
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsCommutative α f
b : Option α
val✝ : α
⊢ liftOrGet f (some val✝) b = liftOrGet f b (some val✝)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsCommutative α f
⊢ liftOrGet f none none = liftOrGet f none none
[PROOFSTEP]
simp [liftOrGet, IsCommutative.comm]
[GOAL]
case none.some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsCommutative α f
val✝ : α
⊢ liftOrGet f none (some val✝) = liftOrGet f (some val✝) none
[PROOFSTEP]
simp [liftOrGet, IsCommutative.comm]
[GOAL]
case some.none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsCommutative α f
val✝ : α
⊢ liftOrGet f (some val✝) none = liftOrGet f none (some val✝)
[PROOFSTEP]
simp [liftOrGet, IsCommutative.comm]
[GOAL]
case some.some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsCommutative α f
val✝¹ val✝ : α
⊢ liftOrGet f (some val✝¹) (some val✝) = liftOrGet f (some val✝) (some val✝¹)
[PROOFSTEP]
simp [liftOrGet, IsCommutative.comm]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
a b c : Option α
⊢ liftOrGet f (liftOrGet f a b) c = liftOrGet f a (liftOrGet f b c)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
b c : Option α
⊢ liftOrGet f (liftOrGet f none b) c = liftOrGet f none (liftOrGet f b c)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
b c : Option α
val✝ : α
⊢ liftOrGet f (liftOrGet f (some val✝) b) c = liftOrGet f (some val✝) (liftOrGet f b c)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
c : Option α
⊢ liftOrGet f (liftOrGet f none none) c = liftOrGet f none (liftOrGet f none c)
[PROOFSTEP]
cases c
[GOAL]
case none.some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
c : Option α
val✝ : α
⊢ liftOrGet f (liftOrGet f none (some val✝)) c = liftOrGet f none (liftOrGet f (some val✝) c)
[PROOFSTEP]
cases c
[GOAL]
case some.none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
c : Option α
val✝ : α
⊢ liftOrGet f (liftOrGet f (some val✝) none) c = liftOrGet f (some val✝) (liftOrGet f none c)
[PROOFSTEP]
cases c
[GOAL]
case some.some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
c : Option α
val✝¹ val✝ : α
⊢ liftOrGet f (liftOrGet f (some val✝¹) (some val✝)) c = liftOrGet f (some val✝¹) (liftOrGet f (some val✝) c)
[PROOFSTEP]
cases c
[GOAL]
case none.none.none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
⊢ liftOrGet f (liftOrGet f none none) none = liftOrGet f none (liftOrGet f none none)
[PROOFSTEP]
simp [liftOrGet, IsAssociative.assoc]
[GOAL]
case none.none.some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
val✝ : α
⊢ liftOrGet f (liftOrGet f none none) (some val✝) = liftOrGet f none (liftOrGet f none (some val✝))
[PROOFSTEP]
simp [liftOrGet, IsAssociative.assoc]
[GOAL]
case none.some.none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
val✝ : α
⊢ liftOrGet f (liftOrGet f none (some val✝)) none = liftOrGet f none (liftOrGet f (some val✝) none)
[PROOFSTEP]
simp [liftOrGet, IsAssociative.assoc]
[GOAL]
case none.some.some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
val✝¹ val✝ : α
⊢ liftOrGet f (liftOrGet f none (some val✝¹)) (some val✝) = liftOrGet f none (liftOrGet f (some val✝¹) (some val✝))
[PROOFSTEP]
simp [liftOrGet, IsAssociative.assoc]
[GOAL]
case some.none.none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
val✝ : α
⊢ liftOrGet f (liftOrGet f (some val✝) none) none = liftOrGet f (some val✝) (liftOrGet f none none)
[PROOFSTEP]
simp [liftOrGet, IsAssociative.assoc]
[GOAL]
case some.none.some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
val✝¹ val✝ : α
⊢ liftOrGet f (liftOrGet f (some val✝¹) none) (some val✝) = liftOrGet f (some val✝¹) (liftOrGet f none (some val✝))
[PROOFSTEP]
simp [liftOrGet, IsAssociative.assoc]
[GOAL]
case some.some.none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
val✝¹ val✝ : α
⊢ liftOrGet f (liftOrGet f (some val✝¹) (some val✝)) none = liftOrGet f (some val✝¹) (liftOrGet f (some val✝) none)
[PROOFSTEP]
simp [liftOrGet, IsAssociative.assoc]
[GOAL]
case some.some.some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsAssociative α f
val✝² val✝¹ val✝ : α
⊢ liftOrGet f (liftOrGet f (some val✝²) (some val✝¹)) (some val✝) =
    liftOrGet f (some val✝²) (liftOrGet f (some val✝¹) (some val✝))
[PROOFSTEP]
simp [liftOrGet, IsAssociative.assoc]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsIdempotent α f
a : Option α
⊢ liftOrGet f a a = a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsIdempotent α f
⊢ liftOrGet f none none = none
[PROOFSTEP]
simp [liftOrGet, IsIdempotent.idempotent]
[GOAL]
case some
α : Type u_1
β : Type u_2
f : α → α → α
inst✝ : IsIdempotent α f
val✝ : α
⊢ liftOrGet f (some val✝) (some val✝) = some val✝
[PROOFSTEP]
simp [liftOrGet, IsIdempotent.idempotent]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α → α
a : Option α
⊢ liftOrGet f none a = a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
f : α → α → α
⊢ liftOrGet f none none = none
[PROOFSTEP]
simp [liftOrGet]
[GOAL]
case some
α : Type u_1
β : Type u_2
f : α → α → α
val✝ : α
⊢ liftOrGet f none (some val✝) = some val✝
[PROOFSTEP]
simp [liftOrGet]
[GOAL]
α : Type u_1
β : Type u_2
f : α → α → α
a : Option α
⊢ liftOrGet f a none = a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
f : α → α → α
⊢ liftOrGet f none none = none
[PROOFSTEP]
simp [liftOrGet]
[GOAL]
case some
α : Type u_1
β : Type u_2
f : α → α → α
val✝ : α
⊢ liftOrGet f (some val✝) none = some val✝
[PROOFSTEP]
simp [liftOrGet]