α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
this : f a b = a ∨ f a b = b
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b
have := h a b
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
this : f a b = a ∨ f a b = b
⊢ f a b = a ∨ f a b = b
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
this : f a b = a ∨ f a b = b
⊢ liftOrGet f (some a) (some b) = some a ∨ liftOrGet f (some a) (some b) = some b
simp [liftOrGet] at this ⊢
no goals
α : Type u_1
f : α → α → α
h : ∀ (a b : α), f a b = a ∨ f a b = b
a b : α
this : f a b = a ∨ f a b = b
⊢ f a b = a ∨ f a b = b
exact this