[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ p fab
[PROOFSTEP]
have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by ext ab; cases ab <;> rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
[PROOFSTEP]
ext ab
[GOAL]
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
ab : α ⊕ β
⊢ fab ab = rec (fun a => fab (inl a)) (fun b => fab (inr b)) ab
[PROOFSTEP]
cases ab
[GOAL]
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
val✝ : α
⊢ fab (inl val✝) = rec (fun a => fab (inl a)) (fun b => fab (inr b)) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
val✝ : β
⊢ fab (inr val✝) = rec (fun a => fab (inl a)) (fun b => fab (inr b)) (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
h1 : fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
⊢ p fab
[PROOFSTEP]
rw [h1]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
h1 : fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
⊢ p fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
[PROOFSTEP]
exact h _ _
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ fab, p fab) ↔ ∃ fa fb, p fun t => rec fa fb t
[PROOFSTEP]
rw [← not_forall_not, forall_sum_pi]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ✝ : Type u_1
δ : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t => rec fa fb t) ↔
    ∃ fa fb, p fun t => rec fa fb t
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ getLeft? x = none ↔ isRight x = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ getLeft? (inl val✝) = none ↔ isRight (inl val✝) = true
[PROOFSTEP]
simp only [getLeft?, isRight, eq_self_iff_true]
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ getLeft? (inr val✝) = none ↔ isRight (inr val✝) = true
[PROOFSTEP]
simp only [getLeft?, isRight, eq_self_iff_true]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ getRight? x = none ↔ isLeft x = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ getRight? (inl val✝) = none ↔ isLeft (inl val✝) = true
[PROOFSTEP]
simp only [getRight?, isLeft, eq_self_iff_true]
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ getRight? (inr val✝) = none ↔ isLeft (inr val✝) = true
[PROOFSTEP]
simp only [getRight?, isLeft, eq_self_iff_true]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
a : α
⊢ getLeft? x = some a ↔ x = inl a
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
a val✝ : α
⊢ getLeft? (inl val✝) = some a ↔ inl val✝ = inl a
[PROOFSTEP]
simp only [getLeft?, Option.some.injEq, inl.injEq]
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
a : α
val✝ : β
⊢ getLeft? (inr val✝) = some a ↔ inr val✝ = inl a
[PROOFSTEP]
simp only [getLeft?, Option.some.injEq, inl.injEq]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
b : β
⊢ getRight? x = some b ↔ x = inr b
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
b : β
val✝ : α
⊢ getRight? (inl val✝) = some b ↔ inl val✝ = inr b
[PROOFSTEP]
simp only [getRight?, Option.some.injEq, inr.injEq]
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
b val✝ : β
⊢ getRight? (inr val✝) = some b ↔ inr val✝ = inr b
[PROOFSTEP]
simp only [getRight?, Option.some.injEq, inr.injEq]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x✝ y x : α ⊕ β
⊢ (!isLeft x) = isRight x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
val✝ : α
⊢ (!isLeft (inl val✝)) = isRight (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
val✝ : β
⊢ (!isLeft (inr val✝)) = isRight (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ isLeft x = false ↔ isRight x = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ isLeft (inl val✝) = false ↔ isRight (inl val✝) = true
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ isLeft (inr val✝) = false ↔ isRight (inr val✝) = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ ¬isLeft x = true ↔ isRight x = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x✝ y x : α ⊕ β
⊢ (!decide (isRight x = isLeft x)) = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
val✝ : α
⊢ (!decide (isRight (inl val✝) = isLeft (inl val✝))) = true
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
val✝ : β
⊢ (!decide (isRight (inr val✝) = isLeft (inr val✝))) = true
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ isRight x = false ↔ isLeft x = true
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ isRight (inl val✝) = false ↔ isLeft (inl val✝) = true
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ isRight (inr val✝) = false ↔ isLeft (inr val✝) = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ ¬isRight x = true ↔ isLeft x = true
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ isLeft x = true ↔ ∃ y, x = inl y
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ isLeft (inl val✝) = true ↔ ∃ y, inl val✝ = inl y
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ isLeft (inr val✝) = true ↔ ∃ y, inr val✝ = inl y
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x y : α ⊕ β
⊢ isRight x = true ↔ ∃ y, x = inr y
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : α
⊢ isRight (inl val✝) = true ↔ ∃ y, inl val✝ = inr y
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
y : α ⊕ β
val✝ : β
⊢ isRight (inr val✝) = true ↔ ∃ y, inr val✝ = inr y
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
α' : Type w
β✝ : Type v
β' : Type x
γ✝ : Type u_1
δ✝ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
ε : Sort u_7
f₁ : α → β
f₂ : β → ε
g₁ : γ → δ
g₂ : δ → ε
x : α ⊕ γ
⊢ Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
[PROOFSTEP]
cases x
[GOAL]
case inl
α✝ : Type u
α' : Type w
β✝ : Type v
β' : Type x
γ✝ : Type u_1
δ✝ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
ε : Sort u_7
f₁ : α → β
f₂ : β → ε
g₁ : γ → δ
g₂ : δ → ε
val✝ : α
⊢ Sum.elim f₂ g₂ (Sum.map f₁ g₁ (inl val✝)) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α✝ : Type u
α' : Type w
β✝ : Type v
β' : Type x
γ✝ : Type u_1
δ✝ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
ε : Sort u_7
f₁ : α → β
f₂ : β → ε
g₁ : γ → δ
g₂ : δ → ε
val✝ : γ
⊢ Sum.elim f₂ g₂ (Sum.map f₁ g₁ (inr val✝)) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ isLeft (Sum.map f g x) = isLeft x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : α
⊢ isLeft (Sum.map f g (inl val✝)) = isLeft (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : γ
⊢ isLeft (Sum.map f g (inr val✝)) = isLeft (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ isRight (Sum.map f g x) = isRight x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : α
⊢ isRight (Sum.map f g (inl val✝)) = isRight (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : γ
⊢ isRight (Sum.map f g (inr val✝)) = isRight (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ getLeft? (Sum.map f g x) = Option.map f (getLeft? x)
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : α
⊢ getLeft? (Sum.map f g (inl val✝)) = Option.map f (getLeft? (inl val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : γ
⊢ getLeft? (Sum.map f g (inr val✝)) = Option.map f (getLeft? (inr val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ getRight? (Sum.map f g x) = Option.map g (getRight? x)
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : α
⊢ getRight? (Sum.map f g (inl val✝)) = Option.map g (getRight? (inl val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → β
g : γ → δ
val✝ : γ
⊢ getRight? (Sum.map f g (inr val✝)) = Option.map g (getRight? (inr val✝))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ x = Sum.elim (update f i x) g (inl i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inl i → Sum.elim f g x_1 = Sum.elim (update f i x) g x_1
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ x = Sum.elim f (update g i x) (inr i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inr i → Sum.elim f g x_1 = Sum.elim f (update g i x) x_1
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : α
x : γ
⊢ update f (inl i) x (inl j) = update (f ∘ inl) i x j
[PROOFSTEP]
rw [← update_inl_comp_inl, Function.comp_apply]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = update (f ∘ inr) i x j
[PROOFSTEP]
rw [← update_inr_comp_inr, Function.comp_apply]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ swap (swap x) = x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ swap (swap (inl val✝)) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ swap (swap (inr val✝)) = inr val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ isLeft (swap x) = isRight x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ isLeft (swap (inl val✝)) = isRight (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ isLeft (swap (inr val✝)) = isRight (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ isRight (swap x) = isLeft x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ isRight (swap (inl val✝)) = isLeft (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ isRight (swap (inr val✝)) = isLeft (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ getLeft? (swap x) = getRight? x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ getLeft? (swap (inl val✝)) = getRight? (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ getLeft? (swap (inr val✝)) = getRight? (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
x : α ⊕ β
⊢ getRight? (swap x) = getLeft? x
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : α
⊢ getRight? (swap (inl val✝)) = getLeft? (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
val✝ : β
⊢ getRight? (swap (inr val✝)) = getLeft? (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s (inl a) (inl c)
⊢ r a c
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
a✝ : r a c
⊢ r a c
[PROOFSTEP]
assumption
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s (inr b) (inr d)
⊢ s b d
[PROOFSTEP]
cases h
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
a✝ : s b d
⊢ s b d
[PROOFSTEP]
assumption
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b
hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b
h : LiftRel r₁ s₁ x y
⊢ LiftRel r₂ s₂ x y
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b
hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b
a✝¹ : α
c✝ : γ
a✝ : r₁ a✝¹ c✝
⊢ LiftRel r₂ s₂ (inl a✝¹) (inl c✝)
[PROOFSTEP]
exact LiftRel.inl (hr _ _ ‹_›)
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b
hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b
b✝ : β
d✝ : δ
a✝ : s₁ b✝ d✝
⊢ LiftRel r₂ s₂ (inr b✝) (inr d✝)
[PROOFSTEP]
exact LiftRel.inr (hs _ _ ‹_›)
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ LiftRel s r (swap x) (swap y)
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ LiftRel s r (swap (inl a✝¹)) (swap (inl c✝))
[PROOFSTEP]
exact LiftRel.inr ‹_›
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ LiftRel s r (swap (inr b✝)) (swap (inr d✝))
[PROOFSTEP]
exact LiftRel.inl ‹_›
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel s r (swap x) (swap y)
⊢ LiftRel r s x y
[PROOFSTEP]
rw [← swap_swap x, ← swap_swap y]
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → γ → Prop
s s₁ s₂ : β → δ → Prop
a : α
b : β
c : γ
d : δ
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel s r (swap x) (swap y)
⊢ LiftRel r s (swap (swap x)) (swap (swap y))
[PROOFSTEP]
exact h.swap
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
h : Lex r s (inl a₁) (inl a₂)
⊢ r a₁ a₂
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
h✝ : r a₁ a₂
⊢ r a₁ a₂
[PROOFSTEP]
assumption
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
h : Lex r s (inr b₁) (inr b₂)
⊢ s b₁ b₂
[PROOFSTEP]
cases h
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
h✝ : s b₁ b₂
⊢ s b₁ b₂
[PROOFSTEP]
assumption
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b✝ b₁ b₂ : β
x y a b : α ⊕ β
h : LiftRel r s a b
⊢ Lex r s a b
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝¹ c✝ : α
a✝ : r a✝¹ c✝
⊢ Lex r s (inl a✝¹) (inl c✝)
[PROOFSTEP]
exact Lex.inl ‹_›
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
b✝ d✝ : β
a✝ : s b✝ d✝
⊢ Lex r s (inr b✝) (inr d✝)
[PROOFSTEP]
exact Lex.inr ‹_›
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
h : Lex r₁ s₁ x y
⊢ Lex r₂ s₂ x y
[PROOFSTEP]
cases h
[GOAL]
case inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
a₁✝ a₂✝ : α
h✝ : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ (inl a₁✝) (inl a₂✝)
[PROOFSTEP]
exact Lex.inl (hr _ _ ‹_›)
[GOAL]
case inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
b₁✝ b₂✝ : β
h✝ : s₁ b₁✝ b₂✝
⊢ Lex r₂ s₂ (inr b₁✝) (inr b₂✝)
[PROOFSTEP]
exact Lex.inr (hs _ _ ‹_›)
[GOAL]
case sep
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b b₁ b₂ : β
hr : ∀ (a b : α), r₁ a b → r₂ a b
hs : ∀ (a b : β), s₁ a b → s₂ a b
a✝ : α
b✝ : β
⊢ Lex r₂ s₂ (inl a✝) (inr b✝)
[PROOFSTEP]
exact Lex.sep _ _
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a : α
aca : Acc r a
⊢ Acc (Lex r s) (inl a)
[PROOFSTEP]
induction' aca with a _ IH
[GOAL]
case intro
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝¹ a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α), r y a → Acc (Lex r s) (inl y)
⊢ Acc (Lex r s) (inl a)
[PROOFSTEP]
constructor
[GOAL]
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝¹ a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α), r y a → Acc (Lex r s) (inl y)
⊢ ∀ (y : α ⊕ β), Lex r s y (inl a) → Acc (Lex r s) y
[PROOFSTEP]
intro y h
[GOAL]
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝¹ a₁ a₂ : α
b b₁ b₂ : β
x y✝ : α ⊕ β
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α), r y a → Acc (Lex r s) (inl y)
y : α ⊕ β
h : Lex r s y (inl a)
⊢ Acc (Lex r s) y
[PROOFSTEP]
cases' h with a' _ h'
[GOAL]
case intro.h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝¹ a₁ a₂ : α
b b₁ b₂ : β
x y : α ⊕ β
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α), r y a → Acc (Lex r s) (inl y)
a' : α
h' : r a' a
⊢ Acc (Lex r s) (inl a')
[PROOFSTEP]
exact IH _ h'
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b : β
acb : Acc s b
⊢ Acc (Lex r s) (inr b)
[PROOFSTEP]
induction' acb with b _ IH
[GOAL]
case intro
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
⊢ Acc (Lex r s) (inr b)
[PROOFSTEP]
constructor
[GOAL]
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
⊢ ∀ (y : α ⊕ β), Lex r s y (inr b) → Acc (Lex r s) y
[PROOFSTEP]
intro y h
[GOAL]
case intro.h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y✝ : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
y : α ⊕ β
h : Lex r s y (inr b)
⊢ Acc (Lex r s) y
[PROOFSTEP]
cases' h with _ _ _ b' _ h' a
[GOAL]
case intro.h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
b' : β
h' : s b' b
⊢ Acc (Lex r s) (inr b')
[PROOFSTEP]
exact IH _ h'
[GOAL]
case intro.h.sep
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
r r₁ r₂ : α → α → Prop
s s₁ s₂ : β → β → Prop
a✝ a₁ a₂ : α
b✝¹ b₁ b₂ : β
x y : α ⊕ β
aca : ∀ (a : α), Acc (Lex r s) (inl a)
b✝ b : β
h✝ : ∀ (y : β), s y b → Acc s y
IH : ∀ (y : β), s y b → Acc (Lex r s) (inr y)
a : α
⊢ Acc (Lex r s) (inl a)
[PROOFSTEP]
exact aca _
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ a, f a = c
[PROOFSTEP]
obtain ⟨a | b, h⟩ := h (inl c)
[GOAL]
case intro.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c
[PROOFSTEP]
exact ⟨a, inl_injective h⟩
[GOAL]
case intro.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c
[PROOFSTEP]
cases h
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
⊢ ∃ a, g a = d
[PROOFSTEP]
obtain ⟨a | b, h⟩ := h (inr d)
[GOAL]
case intro.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d
[PROOFSTEP]
cases h
[GOAL]
case intro.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d
[PROOFSTEP]
exact ⟨b, inr_injective h⟩
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
c : γ
⊢ Sum.elim (const α c) (const β c) = const (α ⊕ β) c
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
c : γ
x : α ⊕ β
⊢ Sum.elim (const α c) (const β c) x = const (α ⊕ β) c x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
c : γ
val✝ : α
⊢ Sum.elim (const α c) (const β c) (inl val✝) = const (α ⊕ β) c (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
c : γ
val✝ : β
⊢ Sum.elim (const α c) (const β c) (inr val✝) = const (α ⊕ β) c (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
⊢ Sum.elim (update f i c) g = update (Sum.elim f g) (inl i) c
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α ⊕ β
⊢ Sum.elim (update f i c) g x = update (Sum.elim f g) (inl i) c x
[PROOFSTEP]
rcases x with x | x
[GOAL]
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
[PROOFSTEP]
by_cases h : x = i
[GOAL]
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : α
⊢ Sum.elim (update f x c) g (inl x) = update (Sum.elim f g) (inl x) c (inl x)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : α
h : ¬x = i
⊢ Sum.elim (update f i c) g (inl x) = update (Sum.elim f g) (inl i) c (inl x)
[PROOFSTEP]
simp [h]
[GOAL]
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : α
c : γ
x : β
⊢ Sum.elim (update f i c) g (inr x) = update (Sum.elim f g) (inl i) c (inr x)
[PROOFSTEP]
simp
[GOAL]
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
⊢ Sum.elim f (update g i c) = update (Sum.elim f g) (inr i) c
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : α ⊕ β
⊢ Sum.elim f (update g i c) x = update (Sum.elim f g) (inr i) c x
[PROOFSTEP]
rcases x with x | x
[GOAL]
case h.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : α
⊢ Sum.elim f (update g i c) (inl x) = update (Sum.elim f g) (inr i) c (inl x)
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)
[PROOFSTEP]
by_cases h : x = i
[GOAL]
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
h : x = i
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
c : γ
x : β
⊢ Sum.elim f (update g x c) (inr x) = update (Sum.elim f g) (inr x) c (inr x)
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → γ
g : β → γ
i : β
c : γ
x : β
h : ¬x = i
⊢ Sum.elim f (update g i c) (inr x) = update (Sum.elim f g) (inr i) c (inr x)
[PROOFSTEP]
simp [h]
