[GOAL]
α✝ : Type ?u.229
β✝ : Type ?u.232
γ✝ : Type ?u.235
f✝ : α✝ → β✝ → γ✝
a✝ : Option α✝
b✝ : Option β✝
c : Option γ✝
α β γ : Type u_1
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = Seq.seq (f <$> a) fun x => b
[PROOFSTEP]
cases a
[GOAL]
case none
α✝ : Type ?u.229
β✝ : Type ?u.232
γ✝ : Type ?u.235
f✝ : α✝ → β✝ → γ✝
a : Option α✝
b✝ : Option β✝
c : Option γ✝
α β γ : Type u_1
f : α → β → γ
b : Option β
⊢ map₂ f none b = Seq.seq (f <$> none) fun x => b
[PROOFSTEP]
rfl
[GOAL]
case some
α✝ : Type ?u.229
β✝ : Type ?u.232
γ✝ : Type ?u.235
f✝ : α✝ → β✝ → γ✝
a : Option α✝
b✝ : Option β✝
c : Option γ✝
α β γ : Type u_1
f : α → β → γ
b : Option β
val✝ : α
⊢ map₂ f (some val✝) b = Seq.seq (f <$> some val✝) fun x => b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
a✝ : Option α
b : Option β
c : Option γ
f : α → β → γ
a : Option α
⊢ map₂ f a none = none
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
⊢ map₂ f none none = none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
val✝ : α
⊢ map₂ f (some val✝) none = none
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
a✝ : Option α
b✝ : Option β
c : Option γ
f : α → β → γ
a : Option α
b : β
⊢ map₂ f a (some b) = Option.map (fun a => f a b) a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
a : Option α
b✝ : Option β
c : Option γ
f : α → β → γ
b : β
⊢ map₂ f none (some b) = Option.map (fun a => f a b) none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
a : Option α
b✝ : Option β
c : Option γ
f : α → β → γ
b : β
val✝ : α
⊢ map₂ f (some val✝) (some b) = Option.map (fun a => f a b) (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
a : Option α
b : Option β
c✝ : Option γ
c : γ
⊢ c ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c
[PROOFSTEP]
simp [map₂]
[GOAL]
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
a : Option α
b : Option β
c : Option γ
⊢ map₂ f a b = none ↔ a = none ∨ b = none
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
b : Option β
c : Option γ
⊢ map₂ f none b = none ↔ none = none ∨ b = none
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
b : Option β
c : Option γ
val✝ : α
⊢ map₂ f (some val✝) b = none ↔ some val✝ = none ∨ b = none
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
c : Option γ
⊢ map₂ f none none = none ↔ none = none ∨ none = none
[PROOFSTEP]
simp
[GOAL]
case none.some
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
c : Option γ
val✝ : β
⊢ map₂ f none (some val✝) = none ↔ none = none ∨ some val✝ = none
[PROOFSTEP]
simp
[GOAL]
case some.none
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
c : Option γ
val✝ : α
⊢ map₂ f (some val✝) none = none ↔ some val✝ = none ∨ none = none
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
c : Option γ
val✝¹ : α
val✝ : β
⊢ map₂ f (some val✝¹) (some val✝) = none ↔ some val✝¹ = none ∨ some val✝ = none
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β → γ
a✝ : Option α
b✝ : Option β
c : Option γ
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = map₂ (fun a b => f b a) b a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β → γ
a : Option α
b✝ : Option β
c : Option γ
f : α → β → γ
b : Option β
⊢ map₂ f none b = map₂ (fun a b => f b a) b none
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β → γ
a : Option α
b✝ : Option β
c : Option γ
f : α → β → γ
b : Option β
val✝ : α
⊢ map₂ f (some val✝) b = map₂ (fun a b => f b a) b (some val✝)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
⊢ map₂ f none none = map₂ (fun a b => f b a) none none
[PROOFSTEP]
rfl
[GOAL]
case none.some
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
val✝ : β
⊢ map₂ f none (some val✝) = map₂ (fun a b => f b a) (some val✝) none
[PROOFSTEP]
rfl
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
val✝ : α
⊢ map₂ f (some val✝) none = map₂ (fun a b => f b a) none (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
val✝¹ : α
val✝ : β
⊢ map₂ f (some val✝¹) (some val✝) = map₂ (fun a b => f b a) (some val✝) (some val✝¹)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_3
β : Type u_4
γ : Type u_2
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
f : α → β → γ
g : γ → δ
⊢ Option.map g (map₂ f a b) = map₂ (fun a b => g (f a b)) a b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_3
β : Type u_4
γ : Type u_2
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
f : α → β → γ
g : γ → δ
⊢ Option.map g (map₂ f none b) = map₂ (fun a b => g (f a b)) none b
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_3
β : Type u_4
γ : Type u_2
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
f : α → β → γ
g : γ → δ
val✝ : α
⊢ Option.map g (map₂ f (some val✝) b) = map₂ (fun a b => g (f a b)) (some val✝) b
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_3
β : Type u_4
γ : Type u_2
f✝ : α → β → γ
c : Option γ
δ : Type u_1
f : α → β → γ
g : γ → δ
⊢ Option.map g (map₂ f none none) = map₂ (fun a b => g (f a b)) none none
[PROOFSTEP]
rfl
[GOAL]
case none.some
α : Type u_3
β : Type u_4
γ : Type u_2
f✝ : α → β → γ
c : Option γ
δ : Type u_1
f : α → β → γ
g : γ → δ
val✝ : β
⊢ Option.map g (map₂ f none (some val✝)) = map₂ (fun a b => g (f a b)) none (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case some.none
α : Type u_3
β : Type u_4
γ : Type u_2
f✝ : α → β → γ
c : Option γ
δ : Type u_1
f : α → β → γ
g : γ → δ
val✝ : α
⊢ Option.map g (map₂ f (some val✝) none) = map₂ (fun a b => g (f a b)) (some val✝) none
[PROOFSTEP]
rfl
[GOAL]
case some.some
α : Type u_3
β : Type u_4
γ : Type u_2
f✝ : α → β → γ
c : Option γ
δ : Type u_1
f : α → β → γ
g : γ → δ
val✝¹ : α
val✝ : β
⊢ Option.map g (map₂ f (some val✝¹) (some val✝)) = map₂ (fun a b => g (f a b)) (some val✝¹) (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_4
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
f : γ → β → δ
g : α → γ
⊢ map₂ f (Option.map g a) b = map₂ (fun a b => f (g a) b) a b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_4
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
f : γ → β → δ
g : α → γ
⊢ map₂ f (Option.map g none) b = map₂ (fun a b => f (g a) b) none b
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_4
β : Type u_3
γ : Type u_2
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
f : γ → β → δ
g : α → γ
val✝ : α
⊢ map₂ f (Option.map g (some val✝)) b = map₂ (fun a b => f (g a) b) (some val✝) b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_2
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
f : α → γ → δ
g : β → γ
⊢ map₂ f a (Option.map g b) = map₂ (fun a b => f a (g b)) a b
[PROOFSTEP]
cases b
[GOAL]
case none
α : Type u_2
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
a : Option α
c : Option γ
δ : Type u_1
f : α → γ → δ
g : β → γ
⊢ map₂ f a (Option.map g none) = map₂ (fun a b => f a (g b)) a none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_2
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
a : Option α
c : Option γ
δ : Type u_1
f : α → γ → δ
g : β → γ
val✝ : β
⊢ map₂ f a (Option.map g (some val✝)) = map₂ (fun a b => f a (g b)) a (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_2
β : Type u_1
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
x : Option (α × β)
⊢ Option.map (uncurry f) x = map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_2
β : Type u_1
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
⊢ Option.map (uncurry f) none = map₂ f (Option.map Prod.fst none) (Option.map Prod.snd none)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_2
β : Type u_1
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
f : α → β → γ
val✝ : α × β
⊢ Option.map (uncurry f) (some val✝) = map₂ f (Option.map Prod.fst (some val✝)) (Option.map Prod.snd (some val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ map₂ f (map₂ g none b) c = map₂ f' none (map₂ g' b c)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝ : α
⊢ map₂ f (map₂ g (some val✝) b) c = map₂ f' (some val✝) (map₂ g' b c)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ map₂ f (map₂ g none none) c = map₂ f' none (map₂ g' none c)
[PROOFSTEP]
cases c
[GOAL]
case none.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝ : β
⊢ map₂ f (map₂ g none (some val✝)) c = map₂ f' none (map₂ g' (some val✝) c)
[PROOFSTEP]
cases c
[GOAL]
case some.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝ : α
⊢ map₂ f (map₂ g (some val✝) none) c = map₂ f' (some val✝) (map₂ g' none c)
[PROOFSTEP]
cases c
[GOAL]
case some.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝¹ : α
val✝ : β
⊢ map₂ f (map₂ g (some val✝¹) (some val✝)) c = map₂ f' (some val✝¹) (map₂ g' (some val✝) c)
[PROOFSTEP]
cases c
[GOAL]
case none.none.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ map₂ f (map₂ g none none) none = map₂ f' none (map₂ g' none none)
[PROOFSTEP]
simp [h_assoc]
[GOAL]
case none.none.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝ : γ
⊢ map₂ f (map₂ g none none) (some val✝) = map₂ f' none (map₂ g' none (some val✝))
[PROOFSTEP]
simp [h_assoc]
[GOAL]
case none.some.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝ : β
⊢ map₂ f (map₂ g none (some val✝)) none = map₂ f' none (map₂ g' (some val✝) none)
[PROOFSTEP]
simp [h_assoc]
[GOAL]
case none.some.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝¹ : β
val✝ : γ
⊢ map₂ f (map₂ g none (some val✝¹)) (some val✝) = map₂ f' none (map₂ g' (some val✝¹) (some val✝))
[PROOFSTEP]
simp [h_assoc]
[GOAL]
case some.none.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝ : α
⊢ map₂ f (map₂ g (some val✝) none) none = map₂ f' (some val✝) (map₂ g' none none)
[PROOFSTEP]
simp [h_assoc]
[GOAL]
case some.none.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝¹ : α
val✝ : γ
⊢ map₂ f (map₂ g (some val✝¹) none) (some val✝) = map₂ f' (some val✝¹) (map₂ g' none (some val✝))
[PROOFSTEP]
simp [h_assoc]
[GOAL]
case some.some.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝¹ : α
val✝ : β
⊢ map₂ f (map₂ g (some val✝¹) (some val✝)) none = map₂ f' (some val✝¹) (map₂ g' (some val✝) none)
[PROOFSTEP]
simp [h_assoc]
[GOAL]
case some.some.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
ε' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
val✝² : α
val✝¹ : β
val✝ : γ
⊢ map₂ f (map₂ g (some val✝²) (some val✝¹)) (some val✝) = map₂ f' (some val✝²) (map₂ g' (some val✝¹) (some val✝))
[PROOFSTEP]
simp [h_assoc]
[GOAL]
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
a : Option α
b : Option β
c : Option γ
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ map₂ f a b = map₂ g b a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
b : Option β
c : Option γ
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ map₂ f none b = map₂ g b none
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
b : Option β
c : Option γ
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
val✝ : α
⊢ map₂ f (some val✝) b = map₂ g b (some val✝)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
c : Option γ
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ map₂ f none none = map₂ g none none
[PROOFSTEP]
simp [h_comm]
[GOAL]
case none.some
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
c : Option γ
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
val✝ : β
⊢ map₂ f none (some val✝) = map₂ g (some val✝) none
[PROOFSTEP]
simp [h_comm]
[GOAL]
case some.none
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
c : Option γ
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
val✝ : α
⊢ map₂ f (some val✝) none = map₂ g none (some val✝)
[PROOFSTEP]
simp [h_comm]
[GOAL]
case some.some
α : Type u_2
β : Type u_3
γ : Type u_1
f : α → β → γ
c : Option γ
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
val✝¹ : α
val✝ : β
⊢ map₂ f (some val✝¹) (some val✝) = map₂ g (some val✝) (some val✝¹)
[PROOFSTEP]
simp [h_comm]
[GOAL]
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f none (map₂ g b c) = map₂ g' b (map₂ f' none c)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝ : α
⊢ map₂ f (some val✝) (map₂ g b c) = map₂ g' b (map₂ f' (some val✝) c)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f none (map₂ g none c) = map₂ g' none (map₂ f' none c)
[PROOFSTEP]
cases c
[GOAL]
case none.some
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝ : β
⊢ map₂ f none (map₂ g (some val✝) c) = map₂ g' (some val✝) (map₂ f' none c)
[PROOFSTEP]
cases c
[GOAL]
case some.none
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝ : α
⊢ map₂ f (some val✝) (map₂ g none c) = map₂ g' none (map₂ f' (some val✝) c)
[PROOFSTEP]
cases c
[GOAL]
case some.some
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝¹ : α
val✝ : β
⊢ map₂ f (some val✝¹) (map₂ g (some val✝) c) = map₂ g' (some val✝) (map₂ f' (some val✝¹) c)
[PROOFSTEP]
cases c
[GOAL]
case none.none.none
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f none (map₂ g none none) = map₂ g' none (map₂ f' none none)
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case none.none.some
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝ : γ
⊢ map₂ f none (map₂ g none (some val✝)) = map₂ g' none (map₂ f' none (some val✝))
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case none.some.none
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝ : β
⊢ map₂ f none (map₂ g (some val✝) none) = map₂ g' (some val✝) (map₂ f' none none)
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case none.some.some
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝¹ : β
val✝ : γ
⊢ map₂ f none (map₂ g (some val✝¹) (some val✝)) = map₂ g' (some val✝¹) (map₂ f' none (some val✝))
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case some.none.none
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝ : α
⊢ map₂ f (some val✝) (map₂ g none none) = map₂ g' none (map₂ f' (some val✝) none)
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case some.none.some
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝¹ : α
val✝ : γ
⊢ map₂ f (some val✝¹) (map₂ g none (some val✝)) = map₂ g' none (map₂ f' (some val✝¹) (some val✝))
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case some.some.none
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝¹ : α
val✝ : β
⊢ map₂ f (some val✝¹) (map₂ g (some val✝) none) = map₂ g' (some val✝) (map₂ f' (some val✝¹) none)
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case some.some.some
α : Type u_4
β : Type u_5
γ : Type u_6
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
val✝² : α
val✝¹ : β
val✝ : γ
⊢ map₂ f (some val✝²) (map₂ g (some val✝¹) (some val✝)) = map₂ g' (some val✝¹) (map₂ f' (some val✝²) (some val✝))
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ map₂ f (map₂ g none b) c = map₂ g' (map₂ f' none c) b
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝ : α
⊢ map₂ f (map₂ g (some val✝) b) c = map₂ g' (map₂ f' (some val✝) c) b
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ map₂ f (map₂ g none none) c = map₂ g' (map₂ f' none c) none
[PROOFSTEP]
cases c
[GOAL]
case none.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝ : β
⊢ map₂ f (map₂ g none (some val✝)) c = map₂ g' (map₂ f' none c) (some val✝)
[PROOFSTEP]
cases c
[GOAL]
case some.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝ : α
⊢ map₂ f (map₂ g (some val✝) none) c = map₂ g' (map₂ f' (some val✝) c) none
[PROOFSTEP]
cases c
[GOAL]
case some.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
c : Option γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝¹ : α
val✝ : β
⊢ map₂ f (map₂ g (some val✝¹) (some val✝)) c = map₂ g' (map₂ f' (some val✝¹) c) (some val✝)
[PROOFSTEP]
cases c
[GOAL]
case none.none.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ map₂ f (map₂ g none none) none = map₂ g' (map₂ f' none none) none
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case none.none.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝ : γ
⊢ map₂ f (map₂ g none none) (some val✝) = map₂ g' (map₂ f' none (some val✝)) none
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case none.some.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝ : β
⊢ map₂ f (map₂ g none (some val✝)) none = map₂ g' (map₂ f' none none) (some val✝)
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case none.some.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝¹ : β
val✝ : γ
⊢ map₂ f (map₂ g none (some val✝¹)) (some val✝) = map₂ g' (map₂ f' none (some val✝)) (some val✝¹)
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case some.none.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝ : α
⊢ map₂ f (map₂ g (some val✝) none) none = map₂ g' (map₂ f' (some val✝) none) none
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case some.none.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝¹ : α
val✝ : γ
⊢ map₂ f (map₂ g (some val✝¹) none) (some val✝) = map₂ g' (map₂ f' (some val✝¹) (some val✝)) none
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case some.some.none
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝¹ : α
val✝ : β
⊢ map₂ f (map₂ g (some val✝¹) (some val✝)) none = map₂ g' (map₂ f' (some val✝¹) none) (some val✝)
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case some.some.some
α : Type u_5
β : Type u_6
γ : Type u_4
f✝ : α → β → γ
δ : Type u_1
ε : Type u_2
δ' : Type u_3
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
val✝² : α
val✝¹ : β
val✝ : γ
⊢ map₂ f (map₂ g (some val✝²) (some val✝¹)) (some val✝) = map₂ g' (map₂ f' (some val✝²) (some val✝)) (some val✝¹)
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
β' : Type u_3
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ a) (Option.map g₂ b)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
β' : Type u_3
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ Option.map g (map₂ f none b) = map₂ f' (Option.map g₁ none) (Option.map g₂ b)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
β' : Type u_3
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
val✝ : α
⊢ Option.map g (map₂ f (some val✝) b) = map₂ f' (Option.map g₁ (some val✝)) (Option.map g₂ b)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
β' : Type u_3
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ Option.map g (map₂ f none none) = map₂ f' (Option.map g₁ none) (Option.map g₂ none)
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case none.some
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
β' : Type u_3
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
val✝ : β
⊢ Option.map g (map₂ f none (some val✝)) = map₂ f' (Option.map g₁ none) (Option.map g₂ (some val✝))
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case some.none
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
β' : Type u_3
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
val✝ : α
⊢ Option.map g (map₂ f (some val✝) none) = map₂ f' (Option.map g₁ (some val✝)) (Option.map g₂ none)
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case some.some
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
β' : Type u_3
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
val✝¹ : α
val✝ : β
⊢ Option.map g (map₂ f (some val✝¹) (some val✝)) = map₂ f' (Option.map g₁ (some val✝¹)) (Option.map g₂ (some val✝))
[PROOFSTEP]
simp [h_distrib]
[GOAL]
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' a) b
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ Option.map g (map₂ f none b) = map₂ f' (Option.map g' none) b
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
val✝ : α
⊢ Option.map g (map₂ f (some val✝) b) = map₂ f' (Option.map g' (some val✝)) b
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ Option.map g (map₂ f none none) = map₂ f' (Option.map g' none) none
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case none.some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
val✝ : β
⊢ Option.map g (map₂ f none (some val✝)) = map₂ f' (Option.map g' none) (some val✝)
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case some.none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
val✝ : α
⊢ Option.map g (map₂ f (some val✝) none) = map₂ f' (Option.map g' (some val✝)) none
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case some.some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
val✝¹ : α
val✝ : β
⊢ Option.map g (map₂ f (some val✝¹) (some val✝)) = map₂ f' (Option.map g' (some val✝¹)) (some val✝)
[PROOFSTEP]
simp [h_distrib]
[GOAL]
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ Option.map g (map₂ f a b) = map₂ f' a (Option.map g' b)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ Option.map g (map₂ f none b) = map₂ f' none (Option.map g' b)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
val✝ : α
⊢ Option.map g (map₂ f (some val✝) b) = map₂ f' (some val✝) (Option.map g' b)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ Option.map g (map₂ f none none) = map₂ f' none (Option.map g' none)
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case none.some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
val✝ : β
⊢ Option.map g (map₂ f none (some val✝)) = map₂ f' none (Option.map g' (some val✝))
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case some.none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
val✝ : α
⊢ Option.map g (map₂ f (some val✝) none) = map₂ f' (some val✝) (Option.map g' none)
[PROOFSTEP]
simp [h_distrib]
[GOAL]
case some.some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
val✝¹ : α
val✝ : β
⊢ Option.map g (map₂ f (some val✝¹) (some val✝)) = map₂ f' (some val✝¹) (Option.map g' (some val✝))
[PROOFSTEP]
simp [h_distrib]
[GOAL]
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' a b)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
b : Option β
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
⊢ map₂ f (Option.map g none) b = Option.map g' (map₂ f' none b)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
b : Option β
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
val✝ : α
⊢ map₂ f (Option.map g (some val✝)) b = Option.map g' (map₂ f' (some val✝) b)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
⊢ map₂ f (Option.map g none) none = Option.map g' (map₂ f' none none)
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case none.some
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
val✝ : β
⊢ map₂ f (Option.map g none) (some val✝) = Option.map g' (map₂ f' none (some val✝))
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case some.none
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
val✝ : α
⊢ map₂ f (Option.map g (some val✝)) none = Option.map g' (map₂ f' (some val✝) none)
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
case some.some
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
val✝¹ : α
val✝ : β
⊢ map₂ f (Option.map g (some val✝¹)) (some val✝) = Option.map g' (map₂ f' (some val✝¹) (some val✝))
[PROOFSTEP]
simp [h_left_comm]
[GOAL]
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' a b)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
b : Option β
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ map₂ f none (Option.map g b) = Option.map g' (map₂ f' none b)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
b : Option β
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
val✝ : α
⊢ map₂ f (some val✝) (Option.map g b) = Option.map g' (map₂ f' (some val✝) b)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ map₂ f none (Option.map g none) = Option.map g' (map₂ f' none none)
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case none.some
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
val✝ : β
⊢ map₂ f none (Option.map g (some val✝)) = Option.map g' (map₂ f' none (some val✝))
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case some.none
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
val✝ : α
⊢ map₂ f (some val✝) (Option.map g none) = Option.map g' (map₂ f' (some val✝) none)
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
case some.some
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
val✝¹ : α
val✝ : β
⊢ map₂ f (some val✝¹) (Option.map g (some val✝)) = Option.map g' (map₂ f' (some val✝¹) (some val✝))
[PROOFSTEP]
simp [h_right_comm]
[GOAL]
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
α' : Type u_3
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ b) (Option.map g₂ a)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
α' : Type u_3
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ Option.map g (map₂ f none b) = map₂ f' (Option.map g₁ b) (Option.map g₂ none)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
α' : Type u_3
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
val✝ : α
⊢ Option.map g (map₂ f (some val✝) b) = map₂ f' (Option.map g₁ b) (Option.map g₂ (some val✝))
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
α' : Type u_3
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ Option.map g (map₂ f none none) = map₂ f' (Option.map g₁ none) (Option.map g₂ none)
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case none.some
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
α' : Type u_3
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
val✝ : β
⊢ Option.map g (map₂ f none (some val✝)) = map₂ f' (Option.map g₁ (some val✝)) (Option.map g₂ none)
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case some.none
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
α' : Type u_3
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
val✝ : α
⊢ Option.map g (map₂ f (some val✝) none) = map₂ f' (Option.map g₁ none) (Option.map g₂ (some val✝))
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case some.some
α : Type u_5
β : Type u_6
γ : Type u_4
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
α' : Type u_3
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
val✝¹ : α
val✝ : β
⊢ Option.map g (map₂ f (some val✝¹) (some val✝)) = map₂ f' (Option.map g₁ (some val✝)) (Option.map g₂ (some val✝¹))
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' b) a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ Option.map g (map₂ f none b) = map₂ f' (Option.map g' b) none
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
val✝ : α
⊢ Option.map g (map₂ f (some val✝) b) = map₂ f' (Option.map g' b) (some val✝)
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ Option.map g (map₂ f none none) = map₂ f' (Option.map g' none) none
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case none.some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
val✝ : β
⊢ Option.map g (map₂ f none (some val✝)) = map₂ f' (Option.map g' (some val✝)) none
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case some.none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
val✝ : α
⊢ Option.map g (map₂ f (some val✝) none) = map₂ f' (Option.map g' none) (some val✝)
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case some.some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
β' : Type u_2
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
val✝¹ : α
val✝ : β
⊢ Option.map g (map₂ f (some val✝¹) (some val✝)) = map₂ f' (Option.map g' (some val✝)) (some val✝¹)
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ Option.map g (map₂ f a b) = map₂ f' b (Option.map g' a)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ Option.map g (map₂ f none b) = map₂ f' b (Option.map g' none)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
b : Option β
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
val✝ : α
⊢ Option.map g (map₂ f (some val✝) b) = map₂ f' b (Option.map g' (some val✝))
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ Option.map g (map₂ f none none) = map₂ f' none (Option.map g' none)
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case none.some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
val✝ : β
⊢ Option.map g (map₂ f none (some val✝)) = map₂ f' (some val✝) (Option.map g' none)
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case some.none
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
val✝ : α
⊢ Option.map g (map₂ f (some val✝) none) = map₂ f' none (Option.map g' (some val✝))
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
case some.some
α : Type u_4
β : Type u_5
γ : Type u_3
f : α → β → γ
c : Option γ
δ : Type u_1
α' : Type u_2
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
val✝¹ : α
val✝ : β
⊢ Option.map g (map₂ f (some val✝¹) (some val✝)) = map₂ f' (some val✝) (Option.map g' (some val✝¹))
[PROOFSTEP]
simp [h_antidistrib]
[GOAL]
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' b a)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
b : Option β
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ map₂ f (Option.map g none) b = Option.map g' (map₂ f' b none)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
b : Option β
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
val✝ : α
⊢ map₂ f (Option.map g (some val✝)) b = Option.map g' (map₂ f' b (some val✝))
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ map₂ f (Option.map g none) none = Option.map g' (map₂ f' none none)
[PROOFSTEP]
simp [h_left_anticomm]
[GOAL]
case none.some
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
val✝ : β
⊢ map₂ f (Option.map g none) (some val✝) = Option.map g' (map₂ f' (some val✝) none)
[PROOFSTEP]
simp [h_left_anticomm]
[GOAL]
case some.none
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
val✝ : α
⊢ map₂ f (Option.map g (some val✝)) none = Option.map g' (map₂ f' none (some val✝))
[PROOFSTEP]
simp [h_left_anticomm]
[GOAL]
case some.some
α : Type u_5
β : Type u_4
γ : Type u_3
f✝ : α → β → γ
c : Option γ
α' : Type u_1
δ : Type u_2
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
val✝¹ : α
val✝ : β
⊢ map₂ f (Option.map g (some val✝¹)) (some val✝) = Option.map g' (map₂ f' (some val✝) (some val✝¹))
[PROOFSTEP]
simp [h_left_anticomm]
[GOAL]
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
a : Option α
b : Option β
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' b a)
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
b : Option β
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ map₂ f none (Option.map g b) = Option.map g' (map₂ f' b none)
[PROOFSTEP]
cases b
[GOAL]
case some
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
b : Option β
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
val✝ : α
⊢ map₂ f (some val✝) (Option.map g b) = Option.map g' (map₂ f' b (some val✝))
[PROOFSTEP]
cases b
[GOAL]
case none.none
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ map₂ f none (Option.map g none) = Option.map g' (map₂ f' none none)
[PROOFSTEP]
simp [h_right_anticomm]
[GOAL]
case none.some
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
val✝ : β
⊢ map₂ f none (Option.map g (some val✝)) = Option.map g' (map₂ f' (some val✝) none)
[PROOFSTEP]
simp [h_right_anticomm]
[GOAL]
case some.none
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
val✝ : α
⊢ map₂ f (some val✝) (Option.map g none) = Option.map g' (map₂ f' none (some val✝))
[PROOFSTEP]
simp [h_right_anticomm]
[GOAL]
case some.some
α : Type u_4
β : Type u_5
γ : Type u_3
f✝ : α → β → γ
c : Option γ
β' : Type u_1
δ : Type u_2
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
val✝¹ : α
val✝ : β
⊢ map₂ f (some val✝¹) (Option.map g (some val✝)) = Option.map g' (map₂ f' (some val✝) (some val✝¹))
[PROOFSTEP]
simp [h_right_anticomm]
[GOAL]
α : Type u_2
β : Type u_1
γ : Type ?u.32843
f✝ : α → β → γ
a✝ : Option α
b : Option β
c : Option γ
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
o : Option β
⊢ map₂ f (some a) o = o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_2
β : Type u_1
γ : Type ?u.32843
f✝ : α → β → γ
a✝ : Option α
b : Option β
c : Option γ
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
⊢ map₂ f (some a) none = none
case some
α : Type u_2
β : Type u_1
γ : Type ?u.32843
f✝ : α → β → γ
a✝ : Option α
b : Option β
c : Option γ
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
val✝ : β
⊢ map₂ f (some a) (some val✝) = some val✝
[PROOFSTEP]
exacts [rfl, congr_arg some (h _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type ?u.33033
f✝ : α → β → γ
a : Option α
b✝ : Option β
c : Option γ
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
o : Option α
⊢ map₂ f o (some b) = o
[PROOFSTEP]
simp [h, map₂]


[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
⊢ ∀ {α : TypeVec m} (x : Comp F G α),
    (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get)
        ((fun {α} => comp.mk ∘ repr ∘ (MvFunctor.map fun i => repr) ∘ Comp.get) x) =
      x
[PROOFSTEP]
intros
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
α✝ : TypeVec m
x✝ : Comp F G α✝
⊢ (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get)
      ((fun {α} => comp.mk ∘ repr ∘ (MvFunctor.map fun i => repr) ∘ Comp.get) x✝) =
    x✝
[PROOFSTEP]
simp only [(· ∘ ·), comp.get_mk, abs_repr, map_map, TypeVec.comp, MvFunctor.id_map', Comp.mk_get]
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
⊢ ∀ {α β : TypeVec m} (f : α ⟹ β) (p : Obj (comp (P F) fun i => P (G i)) α),
    (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get) (f <$$> p) =
      f <$$> (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get) p
[PROOFSTEP]
intros
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
α✝ β✝ : TypeVec m
f✝ : α✝ ⟹ β✝
p✝ : Obj (comp (P F) fun i => P (G i)) α✝
⊢ (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get) (f✝ <$$> p✝) =
    f✝ <$$> (fun {α} => Comp.mk ∘ (MvFunctor.map fun i => abs) ∘ abs ∘ comp.get) p✝
[PROOFSTEP]
simp only [(· ∘ ·)]
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
α✝ β✝ : TypeVec m
f✝ : α✝ ⟹ β✝
p✝ : Obj (comp (P F) fun i => P (G i)) α✝
⊢ Comp.mk ((fun i => abs) <$$> abs (comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun i => abs) <$$> abs (comp.get p✝))
[PROOFSTEP]
rw [← abs_map]
[GOAL]
n m : ℕ
F : TypeVec n → Type u_1
fF : MvFunctor F
q : MvQPF F
G : Fin2 n → TypeVec m → Type u
fG : (i : Fin2 n) → MvFunctor (G i)
q' : (i : Fin2 n) → MvQPF (G i)
α β : TypeVec m
f : α ⟹ β
α✝ β✝ : TypeVec m
f✝ : α✝ ⟹ β✝
p✝ : Obj (comp (P F) fun i => P (G i)) α✝
⊢ Comp.mk (abs ((fun i => abs) <$$> comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun i => abs) <$$> abs (comp.get p✝))
[PROOFSTEP]
simp only [comp.get_map, map_map, TypeVec.comp, abs_map, map_mk]


[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd
[PROOFSTEP]
rintro (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
[GOAL]
case mp.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
⊢ r { fst := i✝, snd := a }.fst { fst := j✝, snd := b }.fst ∨
    ∃ h, s { fst := j✝, snd := b }.fst (h ▸ { fst := i✝, snd := a }.snd) { fst := j✝, snd := b }.snd
[PROOFSTEP]
exact Or.inl hij
[GOAL]
case mp.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ r { fst := i✝, snd := a }.fst { fst := i✝, snd := b }.fst ∨
    ∃ h, s { fst := i✝, snd := b }.fst (h ▸ { fst := i✝, snd := a }.snd) { fst := i✝, snd := b }.snd
[PROOFSTEP]
exact Or.inr ⟨rfl, hab⟩
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b
[PROOFSTEP]
obtain ⟨i, a⟩ := a
[GOAL]
case mpr.mk
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
i : ι
a : α i
⊢ (r { fst := i, snd := a }.fst b.fst ∨ ∃ h, s b.fst (h ▸ { fst := i, snd := a }.snd) b.snd) →
    Lex r s { fst := i, snd := a } b
[PROOFSTEP]
obtain ⟨j, b⟩ := b
[GOAL]
case mpr.mk.mk
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r { fst := i, snd := a }.fst { fst := j, snd := b }.fst ∨
      ∃ h, s { fst := j, snd := b }.fst (h ▸ { fst := i, snd := a }.snd) { fst := j, snd := b }.snd) →
    Lex r s { fst := i, snd := a } { fst := j, snd := b }
[PROOFSTEP]
dsimp only
[GOAL]
case mpr.mk.mk
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r i j ∨ ∃ h, s j (h ▸ a) b) → Lex r s { fst := i, snd := a } { fst := j, snd := b }
[PROOFSTEP]
rintro (h | ⟨rfl, h⟩)
[GOAL]
case mpr.mk.mk.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
h : r i j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b }
[PROOFSTEP]
exact Lex.left _ _ h
[GOAL]
case mpr.mk.mk.inr.intro
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : s i ((_ : i = i) ▸ a) b
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b }
[PROOFSTEP]
exact Lex.right _ _ h
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) × α i
h : Lex r₁ s₁ a b
⊢ Lex r₂ s₂ a b
[PROOFSTEP]
obtain ⟨a, b, hij⟩ | ⟨a, b, hab⟩ := h
[GOAL]
case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r₁ i✝ j✝
⊢ Lex r₂ s₂ { fst := i✝, snd := a } { fst := j✝, snd := b }
[PROOFSTEP]
exact Lex.left _ _ (hr _ _ hij)
[GOAL]
case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ : ι
a b : α i✝
hab : s₁ i✝ a b
⊢ Lex r₂ s₂ { fst := i✝, snd := a } { fst := i✝, snd := b }
[PROOFSTEP]
exact Lex.right _ _ (hs _ _ _ hab)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b ↔ Lex r (fun i => Function.swap (s i)) b a
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b → Lex r (fun i => Function.swap (s i)) b a
[PROOFSTEP]
rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
[GOAL]
case mp.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : Function.swap r i✝ j✝
⊢ Lex r (fun i => Function.swap (s i)) { fst := j✝, snd := b } { fst := i✝, snd := a }
case mp.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : s i✝ a b
⊢ Lex r (fun i => Function.swap (s i)) { fst := i✝, snd := b } { fst := i✝, snd := a }
[PROOFSTEP]
exacts [Lex.left _ _ h, Lex.right _ _ h]
[GOAL]
case mpr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r (fun i => Function.swap (s i)) b a → Lex (Function.swap r) s a b
[PROOFSTEP]
rintro (⟨a, b, h⟩ | ⟨a, b, h⟩)
[GOAL]
case mpr.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : r i✝ j✝
⊢ Lex (Function.swap r) s { fst := j✝, snd := b } { fst := i✝, snd := a }
case mpr.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : Function.swap (s i✝) a b
⊢ Lex (Function.swap r) s { fst := i✝, snd := b } { fst := i✝, snd := a }
[PROOFSTEP]
exacts [Lex.left _ _ h, Lex.right _ _ h]
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsIrrefl ι r
inst✝ : ∀ (i : ι), IsIrrefl (α i) (s i)
⊢ ∀ (a : (i : ι) × α i), ¬Lex r s a a
[PROOFSTEP]
rintro _ (⟨a, b, hi⟩ | ⟨a, b, ha⟩)
[GOAL]
case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : IsIrrefl ι r
inst✝ : ∀ (i : ι), IsIrrefl (α i) (s i)
i✝ : ι
a : α i✝
hi : r i✝ i✝
⊢ False
[PROOFSTEP]
exact irrefl _ hi
[GOAL]
case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : IsIrrefl ι r
inst✝ : ∀ (i : ι), IsIrrefl (α i) (s i)
i✝ : ι
a : α i✝
ha : s i✝ a a
⊢ False
[PROOFSTEP]
exact irrefl _ ha
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
⊢ ∀ (a b c : (i : ι) × α i), Lex r s a b → Lex r s b c → Lex r s a c
[PROOFSTEP]
rintro _ _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, c, hk⟩ | ⟨_, c, hc⟩)
[GOAL]
case left.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ j✝¹ : ι
a : α i✝
b : α j✝¹
hij : r i✝ j✝¹
j✝ : ι
c : α j✝
hk : r j✝¹ j✝
⊢ Lex r s { fst := i✝, snd := a } { fst := j✝, snd := c }
[PROOFSTEP]
exact Lex.left _ _ (_root_.trans hij hk)
[GOAL]
case left.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
c : α j✝
hc : s j✝ b c
⊢ Lex r s { fst := i✝, snd := a } { fst := j✝, snd := c }
[PROOFSTEP]
exact Lex.left _ _ hij
[GOAL]
case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
j✝ : ι
c : α j✝
hk : r i✝ j✝
⊢ Lex r s { fst := i✝, snd := a } { fst := j✝, snd := c }
[PROOFSTEP]
exact Lex.left _ _ hk
[GOAL]
case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
c : α i✝
hc : s i✝ b c
⊢ Lex r s { fst := i✝, snd := a } { fst := i✝, snd := c }
[PROOFSTEP]
exact Lex.right _ _ (_root_.trans hab hc)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsSymm ι r
inst✝ : ∀ (i : ι), IsSymm (α i) (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a
[PROOFSTEP]
rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
[GOAL]
case left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsSymm ι r
inst✝ : ∀ (i : ι), IsSymm (α i) (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
⊢ Lex r s { fst := j✝, snd := b } { fst := i✝, snd := a }
[PROOFSTEP]
exact Lex.left _ _ (symm hij)
[GOAL]
case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsSymm ι r
inst✝ : ∀ (i : ι), IsSymm (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ Lex r s { fst := i✝, snd := b } { fst := i✝, snd := a }
[PROOFSTEP]
exact Lex.right _ _ (symm hab)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a → a = b
[PROOFSTEP]
rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, _, hji⟩ | ⟨_, _, hba⟩)
[GOAL]
case left.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
hji : r j✝ i✝
⊢ { fst := i✝, snd := a } = { fst := j✝, snd := b }
[PROOFSTEP]
exact (asymm hij hji).elim
[GOAL]
case left.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
i✝ : ι
a b : α i✝
hij : r i✝ i✝
hba : s i✝ b a
⊢ { fst := i✝, snd := a } = { fst := i✝, snd := b }
[PROOFSTEP]
exact (irrefl _ hij).elim
[GOAL]
case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hji : r i✝ i✝
⊢ { fst := i✝, snd := a } = { fst := i✝, snd := b }
[PROOFSTEP]
exact (irrefl _ hji).elim
[GOAL]
case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsAsymm ι r
inst✝ : ∀ (i : ι), IsAntisymm (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ { fst := i✝, snd := a } = { fst := i✝, snd := b }
[PROOFSTEP]
exact ext rfl (heq_of_eq $ antisymm hab hba)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b ∨ Lex r s b a
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩
[GOAL]
case mk.mk
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a : α i
j : ι
b : α j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
obtain hij | rfl | hji := trichotomous_of r i j
[GOAL]
case mk.mk.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.left _ _ hij)
[GOAL]
case mk.mk.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a b : α i
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
obtain hab | hba := total_of (s i) a b
[GOAL]
case mk.mk.inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.right _ _ hab)
[GOAL]
case mk.mk.inr.inl.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Lex.right _ _ hba)
[GOAL]
case mk.mk.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTotal (α i) (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Lex.left _ _ hji)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b ∨ a = b ∨ Lex r s b a
[PROOFSTEP]
rintro ⟨i, a⟩ ⟨j, b⟩
[GOAL]
case mk.mk
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a : α i
j : ι
b : α j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨
    { fst := i, snd := a } = { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
obtain hij | rfl | hji := trichotomous_of r i j
[GOAL]
case mk.mk.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a : α i
j : ι
b : α j
hij : r i j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨
    { fst := i, snd := a } = { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.left _ _ hij)
[GOAL]
case mk.mk.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a b : α i
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨
    { fst := i, snd := a } = { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
obtain hab | rfl | hba := trichotomous_of (s i) a b
[GOAL]
case mk.mk.inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨
    { fst := i, snd := a } = { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inl (Lex.right _ _ hab)
[GOAL]
case mk.mk.inr.inl.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a : α i
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := a } ∨
    { fst := i, snd := a } = { fst := i, snd := a } ∨ Lex r s { fst := i, snd := a } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Or.inl rfl)
[GOAL]
case mk.mk.inr.inl.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b } ∨
    { fst := i, snd := a } = { fst := i, snd := b } ∨ Lex r s { fst := i, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Or.inr $ Lex.right _ _ hba)
[GOAL]
case mk.mk.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrichotomous ι r
inst✝ : ∀ (i : ι), IsTrichotomous (α i) (s i)
i : ι
a : α i
j : ι
b : α j
hji : r j i
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b } ∨
    { fst := i, snd := a } = { fst := j, snd := b } ∨ Lex r s { fst := j, snd := b } { fst := i, snd := a }
[PROOFSTEP]
exact Or.inr (Or.inr $ Lex.left _ _ hji)
[GOAL]
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd
[PROOFSTEP]
rintro (⟨a, b, hij⟩ | ⟨i, hab⟩)
[GOAL]
case mp.left
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r a₁✝ a₂✝
⊢ r { fst := a₁✝, snd := a }.fst { fst := a₂✝, snd := b }.fst ∨
    ∃ h, s { fst := a₂✝, snd := b }.fst (h ▸ { fst := a₁✝, snd := a }.snd) { fst := a₂✝, snd := b }.snd
[PROOFSTEP]
exact Or.inl hij
[GOAL]
case mp.right
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r { fst := i, snd := b₁✝ }.fst { fst := i, snd := b₂✝ }.fst ∨
    ∃ h, s { fst := i, snd := b₂✝ }.fst (h ▸ { fst := i, snd := b₁✝ }.snd) { fst := i, snd := b₂✝ }.snd
[PROOFSTEP]
exact Or.inr ⟨rfl, hab⟩
[GOAL]
case mpr
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) ×' α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b
[PROOFSTEP]
obtain ⟨i, a⟩ := a
[GOAL]
case mpr.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
⊢ (r { fst := i, snd := a }.fst b.fst ∨ ∃ h, s b.fst (h ▸ { fst := i, snd := a }.snd) b.snd) →
    Lex r s { fst := i, snd := a } b
[PROOFSTEP]
obtain ⟨j, b⟩ := b
[GOAL]
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r { fst := i, snd := a }.fst { fst := j, snd := b }.fst ∨
      ∃ h, s { fst := j, snd := b }.fst (h ▸ { fst := i, snd := a }.snd) { fst := j, snd := b }.snd) →
    Lex r s { fst := i, snd := a } { fst := j, snd := b }
[PROOFSTEP]
dsimp only
[GOAL]
case mpr.mk.mk
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
⊢ (r i j ∨ ∃ h, s j (h ▸ a) b) → Lex r s { fst := i, snd := a } { fst := j, snd := b }
[PROOFSTEP]
rintro (h | ⟨rfl, h⟩)
[GOAL]
case mpr.mk.mk.inl
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a : α i
j : ι
b : α j
h : r i j
⊢ Lex r s { fst := i, snd := a } { fst := j, snd := b }
[PROOFSTEP]
exact Lex.left _ _ h
[GOAL]
case mpr.mk.mk.inr.intro
ι : Sort u_1
α : ι → Sort u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
i : ι
a b : α i
h : s i ((_ : i = i) ▸ a) b
⊢ Lex r s { fst := i, snd := a } { fst := i, snd := b }
[PROOFSTEP]
exact Lex.right _ h
[GOAL]
ι : Sort u_1
α : ι → Sort u_2
r r₁✝ r₂✝ : ι → ι → Prop
s s₁✝ s₂✝ : (i : ι) → α i → α i → Prop
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) ×' α i
h : Lex r₁ s₁ a b
⊢ Lex r₂ s₂ a b
[PROOFSTEP]
obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h
[GOAL]
case left
ι : Sort u_1
α : ι → Sort u_2
r r₁✝ r₂✝ : ι → ι → Prop
s s₁✝ s₂✝ : (i : ι) → α i → α i → Prop
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ { fst := a₁✝, snd := a } { fst := a₂✝, snd := b }
[PROOFSTEP]
exact Lex.left _ _ (hr _ _ hij)
[GOAL]
case right
ι : Sort u_1
α : ι → Sort u_2
r r₁✝ r₂✝ : ι → ι → Prop
s s₁✝ s₂✝ : (i : ι) → α i → α i → Prop
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁✝ b₂✝ : α i
hab : s₁ i b₁✝ b₂✝
⊢ Lex r₂ s₂ { fst := i, snd := b₁✝ } { fst := i, snd := b₂✝ }
[PROOFSTEP]
exact Lex.right _ (hs _ _ _ hab)


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
y : β
o : Option α
⊢ y ∈ Option.map f o ↔ ∃ x, x ∈ o ∧ f x = y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
H : Function.Injective f
a : α
o : Option α
⊢ f a ∈ Option.map f o ↔ a ∈ o
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
o : Option α
p : β → Prop
⊢ (∀ (y : β), y ∈ Option.map f o → p y) ↔ ∀ (x : α), x ∈ o → p (f x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
o : Option α
p : β → Prop
⊢ (∃ y, y ∈ Option.map f o ∧ p y) ↔ ∃ x, x ∈ o ∧ p (f x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
Hf : Function.Injective f
a₁ a₂ : α
H : Option.map f (some a₁) = Option.map f (some a₂)
⊢ some a₁ = some a₂
[PROOFSTEP]
rw [Hf (Option.some.inj H)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x : Option α
f : α → Option β
b : β
⊢ Option.bind x f = some b ↔ ∃ a, x = some a ∧ f a = some b
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → Option β
b : β
⊢ Option.bind none f = some b ↔ ∃ a, none = some a ∧ f a = some b
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → Option β
b : β
val✝ : α
⊢ Option.bind (some val✝) f = some b ↔ ∃ a, some val✝ = some a ∧ f a = some b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o : Option α
f : α → Option β
⊢ Option.bind o f = none ↔ ∀ (b : β) (a : α), a ∈ o → ¬b ∈ f a
[PROOFSTEP]
simp only [eq_none_iff_forall_not_mem, mem_def, bind_eq_some, not_exists, not_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f g : α → β
h : Option.map f = Option.map g
x : α
⊢ some (f x) = some (g x)
[PROOFSTEP]
simp only [← map_some', h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))
[PROOFSTEP]
rw [map_map, h, ← map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : α → Option β
x : Option α
⊢ (pbind x fun a x => f a) = Option.bind x f
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : α → Option β
⊢ (pbind none fun a x => f a) = Option.bind none f
[PROOFSTEP]
simp only [pbind, none_bind', some_bind']
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : α → Option β
val✝ : α
⊢ (pbind (some val✝) fun a x => f a) = Option.bind (some val✝) f
[PROOFSTEP]
simp only [pbind, none_bind', some_bind']
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p : α✝ → Prop
f✝ : (a : α✝) → p a → β✝
x✝ : Option α✝
α β γ : Type u_5
f : β → γ
x : Option α
g : α → Option β
⊢ Option.map f (x >>= g) = do
    let a ← x
    Option.map f (g a)
[PROOFSTEP]
simp only [← map_eq_map, ← bind_pure_comp, LawfulMonad.bind_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : β → γ
x : Option α
g : α → Option β
⊢ Option.map f (Option.bind x g) = Option.bind x fun a => Option.map f (g a)
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : β → γ
g : α → Option β
⊢ Option.map f (Option.bind none g) = Option.bind none fun a => Option.map f (g a)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : β → γ
g : α → Option β
val✝ : α
⊢ Option.map f (Option.bind (some val✝) g) = Option.bind (some val✝) fun a => Option.map f (g a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : β → γ
x : Option α
g : (a : α) → a ∈ x → Option β
⊢ Option.map f (pbind x g) = pbind x fun a H => Option.map f (g a H)
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : β → γ
g : (a : α) → a ∈ none → Option β
⊢ Option.map f (pbind none g) = pbind none fun a H => Option.map f (g a H)
[PROOFSTEP]
simp only [pbind, map_none']
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : β → γ
val✝ : α
g : (a : α) → a ∈ some val✝ → Option β
⊢ Option.map f (pbind (some val✝) g) = pbind (some val✝) fun a H => Option.map f (g a H)
[PROOFSTEP]
simp only [pbind, map_none']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : α → β
x : Option α
g : (b : β) → b ∈ Option.map f x → Option γ
⊢ pbind (Option.map f x) g = pbind x fun a h => g (f a) (_ : f a ∈ Option.map f x)
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : α → β
g : (b : β) → b ∈ Option.map f none → Option γ
⊢ pbind (Option.map f none) g = pbind none fun a h => g (f a) (_ : f a ∈ Option.map f none)
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : α → β
val✝ : α
g : (b : β) → b ∈ Option.map f (some val✝) → Option γ
⊢ pbind (Option.map f (some val✝)) g = pbind (some val✝) fun a h => g (f a) (_ : f a ∈ Option.map f (some val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ f a (_ : p a) ∈ pmap f x h
[PROOFSTEP]
rw [mem_def] at ha ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a (_ : p a))
[PROOFSTEP]
subst ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
ha : a ∈ some a
⊢ pmap f (some a) h = some (f a (_ : p a))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x✝ : Option α
g : γ → α
x : Option γ
H : ∀ (a : α), a ∈ Option.map g x → p a
⊢ pmap f (Option.map g x) H = pmap (fun a h => f (g a) h) x (_ : ∀ (a : γ), a ∈ x → p (g a))
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : γ → α
H : ∀ (a : α), a ∈ Option.map g none → p a
⊢ pmap f (Option.map g none) H = pmap (fun a h => f (g a) h) none (_ : ∀ (a : γ), a ∈ none → p (g a))
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : γ → α
val✝ : γ
H : ∀ (a : α), a ∈ Option.map g (some val✝) → p a
⊢ pmap f (Option.map g (some val✝)) H = pmap (fun a h => f (g a) h) (some val✝) (_ : ∀ (a : γ), a ∈ some val✝ → p (g a))
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
g : β → γ
f : (a : α) → p a → β
x : Option α
H : ∀ (a : α), a ∈ x → p a
⊢ Option.map g (pmap f x H) = pmap (fun a h => g (f a h)) x H
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
g : β → γ
f : (a : α) → p a → β
H : ∀ (a : α), a ∈ none → p a
⊢ Option.map g (pmap f none H) = pmap (fun a h => g (f a h)) none H
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
g : β → γ
f : (a : α) → p a → β
val✝ : α
H : ∀ (a : α), a ∈ some val✝ → p a
⊢ Option.map g (pmap f (some val✝) H) = pmap (fun a h => g (f a h)) (some val✝) H
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p✝ : α → Prop
f✝ : (a : α) → p✝ a → β
x✝ : Option α
p : α → Prop
f : α → β
x : Option α
H : ∀ (a : α), a ∈ x → p a
⊢ pmap (fun a x => f a) x H = Option.map f x
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p✝ : α → Prop
f✝ : (a : α) → p✝ a → β
x : Option α
p : α → Prop
f : α → β
H : ∀ (a : α), a ∈ none → p a
⊢ pmap (fun a x => f a) none H = Option.map f none
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p✝ : α → Prop
f✝ : (a : α) → p✝ a → β
x : Option α
p : α → Prop
f : α → β
val✝ : α
H : ∀ (a : α), a ∈ some val✝ → p a
⊢ pmap (fun a x => f a) (some val✝) H = Option.map f (some val✝)
[PROOFSTEP]
simp only [map_none', map_some', pmap]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x✝ : Option α✝
α β γ : Type u_5
x : Option α
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
H : ∀ (a : β), a ∈ x >>= g → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ x >>= g
⊢ pmap f (x >>= g) H = do
    let a ← x
    pmap f (g a) (_ : ∀ (b : β), b ∈ g a → p b)
[PROOFSTEP]
cases x
[GOAL]
case none
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x : Option α✝
α β γ : Type u_5
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
H : ∀ (a : β), a ∈ none >>= g → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ none >>= g
⊢ pmap f (none >>= g) H = do
    let a ← none
    pmap f (g a) (_ : ∀ (b : β), b ∈ g a → p b)
[PROOFSTEP]
simp only [pmap, bind_eq_bind, none_bind, some_bind]
[GOAL]
case some
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x : Option α✝
α β γ : Type u_5
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
val✝ : α
H : ∀ (a : β), a ∈ some val✝ >>= g → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ some val✝ >>= g
⊢ pmap f (some val✝ >>= g) H = do
    let a ← some val✝
    pmap f (g a) (_ : ∀ (b : β), b ∈ g a → p b)
[PROOFSTEP]
simp only [pmap, bind_eq_bind, none_bind, some_bind]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x✝ : Option α✝
α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : β → Option γ
H : ∀ (a : α), a ∈ x → p a
⊢ pmap f x H >>= g = pbind x fun a h => g (f a (_ : p a))
[PROOFSTEP]
cases x
[GOAL]
case none
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x : Option α✝
α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
g : β → Option γ
H : ∀ (a : α), a ∈ none → p a
⊢ pmap f none H >>= g = pbind none fun a h => g (f a (_ : p a))
[PROOFSTEP]
simp only [pmap, bind_eq_bind, none_bind, some_bind, pbind]
[GOAL]
case some
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x : Option α✝
α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
g : β → Option γ
val✝ : α
H : ∀ (a : α), a ∈ some val✝ → p a
⊢ pmap f (some val✝) H >>= g = pbind (some val✝) fun a h => g (f a (_ : p a))
[PROOFSTEP]
simp only [pmap, bind_eq_bind, none_bind, some_bind, pbind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → a ∈ x → Option β
h' : ∀ (a : α) (H : a ∈ x), f a H = none → x = none
⊢ pbind x f = none ↔ x = none
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
f : (a : α) → a ∈ none → Option β
h' : ∀ (a : α) (H : a ∈ none), f a H = none → none = none
⊢ pbind none f = none ↔ none = none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ pbind (some val✝) f = none ↔ some val✝ = none
[PROOFSTEP]
simp only [pbind, iff_false]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
⊢ ¬f val✝ (_ : some val✝ = some val✝) = none
[PROOFSTEP]
intro h
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
val✝ : α
f : (a : α) → a ∈ some val✝ → Option β
h' : ∀ (a : α) (H : a ∈ some val✝), f a H = none → some val✝ = none
h : f val✝ (_ : some val✝ = some val✝) = none
⊢ False
[PROOFSTEP]
cases h' _ rfl h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → a ∈ x → Option β
y : β
⊢ pbind x f = some y ↔ ∃ z H, f z H = some y
[PROOFSTEP]
rcases x with (_ | x)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
⊢ pbind none f = some y ↔ ∃ z H, f z H = some y
[PROOFSTEP]
simp only [pbind, false_iff, not_exists]
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
⊢ ∀ (x : α) (x_1 : x ∈ none), ¬f x x_1 = some y
[PROOFSTEP]
intro z h
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
f : (a : α) → a ∈ none → Option β
z : α
h : z ∈ none
⊢ ¬f z h = some y
[PROOFSTEP]
simp at h
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ pbind (some x) f = some y ↔ ∃ z H, f z H = some y
[PROOFSTEP]
simp only [pbind]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ f x (_ : some x = some x) = some y ↔ ∃ z H, f z H = some y
[PROOFSTEP]
refine ⟨λ h => ⟨x, rfl, h⟩, ?_⟩
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
⊢ (∃ z H, f z H = some y) → f x (_ : some x = some x) = some y
[PROOFSTEP]
rintro ⟨z, H, hz⟩
[GOAL]
case some.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H : z ∈ some x
hz : f z H = some y
⊢ f x (_ : some x = some x) = some y
[PROOFSTEP]
simp only [mem_def, Option.some_inj] at H
[GOAL]
case some.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
y : β
x : α
f : (a : α) → a ∈ some x → Option β
z : α
H✝ : z ∈ some x
hz : f z H✝ = some y
H : x = z
⊢ f x (_ : some x = some x) = some y
[PROOFSTEP]
simpa [H] using hz
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
h : ∀ (a : α), a ∈ x → p a
⊢ pmap f x h = none ↔ x = none
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ none → p a
⊢ pmap f none h = none ↔ none = none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
val✝ : α
h : ∀ (a : α), a ∈ some val✝ → p a
⊢ pmap f (some val✝) h = none ↔ some val✝ = none
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : Option α
hf : ∀ (a : α), a ∈ x → p a
y : β
⊢ pmap f x hf = some y ↔ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
rcases x with (_ | x)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
hf : ∀ (a : α), a ∈ none → p a
⊢ pmap f none hf = some y ↔ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
simp only [not_mem_none, exists_false, pmap, not_false_iff, exists_prop_of_false]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
⊢ pmap f (some x) hf = some y ↔ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
constructor
[GOAL]
case some.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
⊢ pmap f (some x) hf = some y → ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
intro h
[GOAL]
case some.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
h : pmap f (some x) hf = some y
⊢ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
simp only [pmap, Option.some_inj] at h
[GOAL]
case some.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
h : f x (_ : p x) = y
⊢ ∃ a H, f a (_ : p a) = y
[PROOFSTEP]
refine ⟨x, rfl, h⟩
[GOAL]
case some.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
y : β
x : α
hf : ∀ (a : α), a ∈ some x → p a
⊢ (∃ a H, f a (_ : p a) = y) → pmap f (some x) hf = some y
[PROOFSTEP]
rintro ⟨a, H, rfl⟩
[GOAL]
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : α
hf : ∀ (a : α), a ∈ some x → p a
a : α
H : some x = some a
⊢ pmap f (some x) hf = some (f a (_ : p a))
[PROOFSTEP]
simp only [mem_def, Option.some_inj] at H
[GOAL]
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f : (a : α) → p a → β
x : α
hf : ∀ (a : α), a ∈ some x → p a
a : α
H✝ : some x = some a
H : x = a
⊢ pmap f (some x) hf = some (f a (_ : p a))
[PROOFSTEP]
simp only [H, pmap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : (a : α) → p a → β
x : Option (Option α)
H : ∀ (a : Option α), a ∈ x → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) x H) = pmap f (join x) (_ : ∀ (a : α), a ∈ join x → p a)
[PROOFSTEP]
rcases x with (_ | _ | x)
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → p a → β
H : ∀ (a : Option α), a ∈ none → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) none H) = pmap f (join none) (_ : ∀ (a : α), a ∈ join none → p a)
[PROOFSTEP]
simp
[GOAL]
case some.none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x : Option α
f : (a : α) → p a → β
H : ∀ (a : Option α), a ∈ some none → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) (some none) H) = pmap f (join (some none)) (_ : ∀ (a : α), a ∈ join (some none) → p a)
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : (a : α) → p a → β
x : α
H : ∀ (a : Option α), a ∈ some (some x) → ∀ (a_2 : α), a_2 ∈ a → p a_2
⊢ join (pmap (pmap f) (some (some x)) H) = pmap f (join (some (some x))) (_ : ∀ (a : α), a ∈ join (some (some x)) → p a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x : Option α
⊢ (Option.orElse none fun x_1 => x) = x
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
⊢ (Option.orElse none fun x => none) = none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
val✝ : α
⊢ (Option.orElse none fun x => some val✝) = some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x : Option α
⊢ (Option.orElse x fun x => none) = x
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
⊢ (Option.orElse none fun x => none) = none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
val✝ : α
⊢ (Option.orElse (some val✝) fun x => none) = some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Inhabited α
o : Option α
⊢ getD o default = iget o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Inhabited α
⊢ getD none default = iget none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : Inhabited α
val✝ : α
⊢ getD (some val✝) default = iget (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : Prop
inst✝ : Decidable p
u : Unit
⊢ _root_.guard p = some u ↔ p
[PROOFSTEP]
cases u
[GOAL]
case unit
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : Prop
inst✝ : Decidable p
⊢ _root_.guard p = some PUnit.unit ↔ p
[PROOFSTEP]
by_cases h : p
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : Prop
inst✝ : Decidable p
h : p
⊢ _root_.guard p = some PUnit.unit ↔ p
[PROOFSTEP]
simp [_root_.guard, h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ _root_.guard p = some PUnit.unit ↔ p
[PROOFSTEP]
simp [_root_.guard, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
simpa [liftOrGet] using h a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
o : Option α
⊢ casesOn' o (f none) (f ∘ fun a => some a) = f o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
⊢ casesOn' none (f none) (f ∘ fun a => some a) = f none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
val✝ : α
⊢ casesOn' (some val✝) (f none) (f ∘ fun a => some a) = f (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o o' : Option α
x : α
⊢ (HOrElse.hOrElse o fun x => o') = some x ↔ o = some x ∨ o = none ∧ o' = some x
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o' : Option α
x : α
⊢ (HOrElse.hOrElse none fun x => o') = some x ↔ none = some x ∨ none = none ∧ o' = some x
[PROOFSTEP]
simp only [true_and, false_or, eq_self_iff_true, none_orElse]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o' : Option α
x val✝ : α
⊢ (HOrElse.hOrElse (some val✝) fun x => o') = some x ↔ some val✝ = some x ∨ some val✝ = none ∧ o' = some x
[PROOFSTEP]
simp only [some_orElse, or_false, false_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o o' : Option α
⊢ (HOrElse.hOrElse o fun x => o') = none ↔ o = none ∧ o' = none
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o' : Option α
⊢ (HOrElse.hOrElse none fun x => o') = none ↔ none = none ∧ o' = none
[PROOFSTEP]
simp only [true_and, none_orElse, eq_self_iff_true]
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
o' : Option α
val✝ : α
⊢ (HOrElse.hOrElse (some val✝) fun x => o') = none ↔ some val✝ = none ∧ o' = none
[PROOFSTEP]
simp only [some_orElse, false_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
o : Option α
⊢ Option.elim o (f none) (f ∘ some) = f o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
⊢ Option.elim none (f none) (f ∘ some) = f none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Option α → β
val✝ : α
⊢ Option.elim (some val✝) (f none) (f ∘ some) = f (some val✝)
[PROOFSTEP]
rfl