Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Yury G. Kudryashov

! This file was ported from Lean 3 source module data.sum.basic
! leanprover-community/mathlib commit bd9851ca476957ea4549eb19b40e7b5ade9428cc
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Logic.Function.Basic

/-!
# Disjoint union of types

This file proves basic results about the sum type `α ⊕ β`.

`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.

## Main declarations

* `Sum.getLeft`: Retrieves the left content of `x : α ⊕ β` or returns `none` if it's coming from
  the right.
* `Sum.getRight`: Retrieves the right content of `x : α ⊕ β` or returns `none` if it's coming from
  the left.
* `Sum.isLeft`: Returns whether `x : α ⊕ β` comes from the left component or not.
* `Sum.isRight`: Returns whether `x : α ⊕ β` comes from the right component or not.
* `Sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
* `Sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
* `Sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
* `Sum.Lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.

## Notes

The definition of `Sum` takes values in `Type _`. This effectively forbids `Prop`- valued sum types.
To this effect, we have `PSum`, which takes value in `Sort*` and carries a more complicated
universe signature in consequence. The `Prop` version is `or`.
-/


universe u v w x

variable {
α: Type u
α : 
Type u: Type (u+1)
Type u} {
α': Type w
α' : 
Type w: Type (w+1)
Type w} {
β: Type v
β : 
Type v: Type (v+1)
Type v} {
β': Type x
β' : 
Type x: Type (x+1)
Type x} {
γ: Type ?u.10
γ 
δ: Type ?u.9598
δ : 
Type _: Type (?u.4175+1)
Type _}

namespace Sum

deriving instance 
DecidableEq: Sort u → Sort (max1u)
DecidableEq for 
Sum: Type u → Type v → Type (maxuv)
Sum
deriving instance 
BEq: Type u → Type u
BEq for 
Sum: Type u → Type v → Type (maxuv)
Sum

@[simp]
theorem 
«forall»: ∀ {α : Type u} {β : Type v} {p : α ⊕ β → Prop}, (∀ (x : α ⊕ β), p x) ↔ (∀ (a : α), p (inl a)) ∧ ∀ (b : β), p (inr b)
«forall» {
p: α ⊕ β → Prop
p : 
Sum: Type ?u.2035 → Type ?u.2034 → Type (max?u.2035?u.2034)
Sum 
α: Type u
α 
β: Type v
β → 
Prop: Type
Prop} : (∀ 
x: ?m.2040
x, 
p: α ⊕ β → Prop
p 
x: ?m.2040
x) ↔ (∀ 
a: ?m.2045
a, 
p: α ⊕ β → Prop
p (
inl: {α : Type ?u.2049} → {β : Type ?u.2048} → α → α ⊕ β
inl 
a: ?m.2045
a)) ∧ ∀ 
b: ?m.2056
b, 
p: α ⊕ β → Prop
p (
inr: {α : Type ?u.2060} → {β : Type ?u.2059} → β → α ⊕ β
inr 
b: ?m.2056
b) :=
  ⟨fun 
h: ?m.2076
h ↦ ⟨fun 
_: ?m.2089
_ ↦ 
h: ?m.2076
h 
_: α ⊕ β
_, fun 
_: ?m.2095
_ ↦ 
h: ?m.2076
h 
_: α ⊕ β
_⟩, fun ⟨
h₁: ∀ (a : α), p (inl a)
h₁, 
h₂: ∀ (b : β), p (inr b)
h₂⟩ ↦ 
Sum.rec: ∀ {α : Type ?u.2134} {β : Type ?u.2133} {motive : α ⊕ β → Sort ?u.2135},
  (∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → ∀ (t : α ⊕ β), motive t
Sum.rec 
h₁: ∀ (a : α), p (inl a)
h₁ 
h₂: ∀ (b : β), p (inr b)
h₂⟩
#align sum.forall 
Sum.forall: ∀ {α : Type u} {β : Type v} {p : α ⊕ β → Prop}, (∀ (x : α ⊕ β), p x) ↔ (∀ (a : α), p (inl a)) ∧ ∀ (b : β), p (inr b)
Sum.forall

@[simp]
theorem 
«exists»: ∀ {α : Type u} {β : Type v} {p : α ⊕ β → Prop}, (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b)
«exists» {
p: α ⊕ β → Prop
p : 
Sum: Type ?u.2295 → Type ?u.2294 → Type (max?u.2295?u.2294)
Sum 
α: Type u
α 
β: Type v
β → 
Prop: Type
Prop} : (∃ 
x: ?m.2302
x, 
p: α ⊕ β → Prop
p 
x: ?m.2302
x) ↔ (∃ 
a: ?m.2309
a, 
p: α ⊕ β → Prop
p (
inl: {α : Type ?u.2312} → {β : Type ?u.2311} → α → α ⊕ β
inl 
a: ?m.2309
a)) ∨ ∃ 
b: ?m.2322
b, 
p: α ⊕ β → Prop
p (
inr: {α : Type ?u.2325} → {β : Type ?u.2324} → β → α ⊕ β
inr 
b: ?m.2322
b) :=
  ⟨ fun
    | ⟨
inl: {α : Type ?u.2345} → {β : Type ?u.2344} → α → α ⊕ β
inl 
a: α
a, 
h: p (inl a)
h⟩ => 
Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl ⟨
a: α
a, 
h: p (inl a)
h⟩
    | ⟨
inr: {α : Type ?u.2405} → {β : Type ?u.2404} → β → α ⊕ β
inr 
b: β
b, 
h: p (inr b)
h⟩ => 
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr ⟨
b: β
b, 
h: p (inr b)
h⟩,
    fun
    | 
Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl ⟨
a: α
a, 
h: p (inl a)
h⟩ => ⟨
inl: {α : Type ?u.2634} → {β : Type ?u.2633} → α → α ⊕ β
inl 
a: α
a, 
h: p (inl a)
h⟩
    | 
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr ⟨
b: β
b, 
h: p (inr b)
h⟩ => ⟨
inr: {α : Type ?u.2686} → {β : Type ?u.2685} → β → α ⊕ β
inr 
b: β
b, 
h: p (inr b)
h⟩⟩
#align sum.exists 
Sum.exists: ∀ {α : Type u} {β : Type v} {p : α ⊕ β → Prop}, (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b)
Sum.exists

theorem 
inl_injective: ∀ {α : Type u} {β : Type v}, Function.Injective inl
inl_injective : 
Function.Injective: {α : Sort ?u.2878} → {β : Sort ?u.2877} → (α → β) → Prop
Function.Injective (
inl: {α : Type ?u.2887} → {β : Type ?u.2886} → α → α ⊕ β
inl : 
α: Type u
α → 
Sum: Type ?u.2885 → Type ?u.2884 → Type (max?u.2885?u.2884)
Sum 
α: Type u
α 
β: Type v
β) := fun 
_: ?m.2898
_ 
_: ?m.2901
_ ↦ 
inl.inj: ∀ {α : Type ?u.2904} {β : Type ?u.2903} {val val_1 : α}, inl val = inl val_1 → val = val_1
inl.inj
#align sum.inl_injective 
Sum.inl_injective: ∀ {α : Type u} {β : Type v}, Function.Injective inl
Sum.inl_injective

theorem 
inr_injective: ∀ {α : Type u} {β : Type v}, Function.Injective inr
inr_injective : 
Function.Injective: {α : Sort ?u.2943} → {β : Sort ?u.2942} → (α → β) → Prop
Function.Injective (
inr: {α : Type ?u.2952} → {β : Type ?u.2951} → β → α ⊕ β
inr : 
β: Type v
β → 
Sum: Type ?u.2950 → Type ?u.2949 → Type (max?u.2950?u.2949)
Sum 
α: Type u
α 
β: Type v
β) := fun 
_: ?m.2963
_ 
_: ?m.2966
_ ↦ 
inr.inj: ∀ {α : Type ?u.2969} {β : Type ?u.2968} {val val_1 : β}, inr val = inr val_1 → val = val_1
inr.inj
#align sum.inr_injective 
Sum.inr_injective: ∀ {α : Type u} {β : Type v}, Function.Injective inr
Sum.inr_injective

section get

/-- Check if a sum is `inl` and if so, retrieve its contents. -/
def 
getLeft: {α : Type u} → {β : Type v} → α ⊕ β → Option α
getLeft : 
Sum: Type ?u.3009 → Type ?u.3008 → Type (max?u.3009?u.3008)
Sum 
α: Type u
α 
β: Type v
β → 
Option: Type ?u.3011 → Type ?u.3011
Option 
α: Type u
α
  | 
inl: {α : Type ?u.3017} → {β : Type ?u.3016} → α → α ⊕ β
inl 
a: α
a => 
some: {α : Type ?u.3036} → α → Option α
some 
a: α
a
  | 
inr: {α : Type ?u.3040} → {β : Type ?u.3039} → β → α ⊕ β
inr _ => 
none: {α : Type ?u.3058} → Option α
none
#align sum.get_left 
Sum.getLeft: {α : Type u} → {β : Type v} → α ⊕ β → Option α
Sum.getLeft

/-- Check if a sum is `inr` and if so, retrieve its contents. -/
def 
getRight: {α : Type u} → {β : Type v} → α ⊕ β → Option β
getRight : 
Sum: Type ?u.3238 → Type ?u.3237 → Type (max?u.3238?u.3237)
Sum 
α: Type u
α 
β: Type v
β → 
Option: Type ?u.3240 → Type ?u.3240
Option 
β: Type v
β
  | 
inr: {α : Type ?u.3246} → {β : Type ?u.3245} → β → α ⊕ β
inr 
b: β
b => 
some: {α : Type ?u.3265} → α → Option α
some 
b: β
b
  | 
inl: {α : Type ?u.3269} → {β : Type ?u.3268} → α → α ⊕ β
inl _ => 
none: {α : Type ?u.3287} → Option α
none
#align sum.get_right 
Sum.getRight: {α : Type u} → {β : Type v} → α ⊕ β → Option β
Sum.getRight

/-- Check if a sum is `inl`. -/
def 
isLeft: {α : Type u} → {β : Type v} → α ⊕ β → Bool
isLeft : 
Sum: Type ?u.3461 → Type ?u.3460 → Type (max?u.3461?u.3460)
Sum 
α: Type u
α 
β: Type v
β → 
Bool: Type
Bool
  | 
inl: {α : Type ?u.3468} → {β : Type ?u.3467} → α → α ⊕ β
inl _ => 
true: Bool
true
  | 
inr: {α : Type ?u.3489} → {β : Type ?u.3488} → β → α ⊕ β
inr _ => 
false: Bool
false
#align sum.is_left 
Sum.isLeft: {α : Type u} → {β : Type v} → α ⊕ β → Bool
Sum.isLeft

/-- Check if a sum is `inr`. -/
def 
isRight: α ⊕ β → Bool
isRight : 
Sum: Type ?u.3664 → Type ?u.3663 → Type (max?u.3664?u.3663)
Sum 
α: Type u
α 
β: Type v
β → 
Bool: Type
Bool
  | 
inl: {α : Type ?u.3671} → {β : Type ?u.3670} → α → α ⊕ β
inl _ => 
false: Bool
false
  | 
inr: {α : Type ?u.3692} → {β : Type ?u.3691} → β → α ⊕ β
inr _ => 
true: Bool
true
#align sum.is_right 
Sum.isRight: {α : Type u} → {β : Type v} → α ⊕ β → Bool
Sum.isRight

variable {
x: α ⊕ β
x 
y: α ⊕ β
y : 
Sum: Type ?u.4994 → Type ?u.4993 → Type (max?u.4994?u.4993)
Sum 
α: Type u
α 
β: Type v
β}

@[simp] theorem 
getLeft_inl: ∀ {α : Type u} {β : Type v} (x : α), getLeft (inl x) = some x
getLeft_inl (
x: α
x : 
α: Type u
α) : (
inl: {α : Type ?u.3902} → {β : Type ?u.3901} → α → α ⊕ β
inl 
x: α
x : 
α: Type u
α ⊕ 
β: Type v
β).
getLeft: {α : Type ?u.3908} → {β : Type ?u.3907} → α ⊕ β → Option α
getLeft = 
some: {α : Type ?u.3914} → α → Option α
some 
x: α
x := 
rfl: ∀ {α : Sort ?u.3920} {a : α}, a = a
rfl
@[simp] theorem 
getLeft_inr: ∀ {α : Type u} {β : Type v} (x : β), getLeft (inr x) = none
getLeft_inr (
x: β
x : 
β: Type v
β) : (
inr: {α : Type ?u.3981} → {β : Type ?u.3980} → β → α ⊕ β
inr 
x: β
x : 
α: Type u
α ⊕ 
β: Type v
β).
getLeft: {α : Type ?u.3987} → {β : Type ?u.3986} → α ⊕ β → Option α
getLeft = 
none: {α : Type ?u.3993} → Option α
none := 
rfl: ∀ {α : Sort ?u.4026} {a : α}, a = a
rfl
@[simp] theorem 
getRight_inl: ∀ {α : Type u} {β : Type v} (x : α), getRight (inl x) = none
getRight_inl (
x: α
x : 
α: Type u
α) : (
inl: {α : Type ?u.4087} → {β : Type ?u.4086} → α → α ⊕ β
inl 
x: α
x : 
α: Type u
α ⊕ 
β: Type v
β).
getRight: {α : Type ?u.4093} → {β : Type ?u.4092} → α ⊕ β → Option β
getRight = 
none: {α : Type ?u.4099} → Option α
none := 
rfl: ∀ {α : Sort ?u.4132} {a : α}, a = a
rfl
@[simp] theorem 
getRight_inr: ∀ {α : Type u} {β : Type v} (x : β), getRight (inr x) = some x
getRight_inr (
x: β
x : 
β: Type v
β) : (
inr: {α : Type ?u.4193} → {β : Type ?u.4192} → β → α ⊕ β
inr 
x: β
x : 
α: Type u
α ⊕ 
β: Type v
β).
getRight: {α : Type ?u.4199} → {β : Type ?u.4198} → α ⊕ β → Option β
getRight = 
some: {α : Type ?u.4205} → α → Option α
some 
x: β
x := 
rfl: ∀ {α : Sort ?u.4211} {a : α}, a = a
rfl

@[simp] theorem 
isLeft_inl: ∀ {α : Type u} {β : Type v} (x : α), isLeft (inl x) = true
isLeft_inl (
x: α
x : 
α: Type u
α) : (
inl: {α : Type ?u.4272} → {β : Type ?u.4271} → α → α ⊕ β
inl 
x: α
x : 
α: Type u
α ⊕ 
β: Type v
β).
isLeft: {α : Type ?u.4278} → {β : Type ?u.4277} → α ⊕ β → Bool
isLeft = 
true: Bool
true := 
rfl: ∀ {α : Sort ?u.4287} {a : α}, a = a
rfl
@[simp] theorem 
isLeft_inr: ∀ {α : Type u} {β : Type v} (x : β), isLeft (inr x) = false
isLeft_inr (
x: β
x : 
β: Type v
β) : (
inr: {α : Type ?u.4348} → {β : Type ?u.4347} → β → α ⊕ β
inr 
x: β
x : 
α: Type u
α ⊕ 
β: Type v
β).
isLeft: {α : Type ?u.4354} → {β : Type ?u.4353} → α ⊕ β → Bool
isLeft = 
false: Bool
false := 
rfl: ∀ {α : Sort ?u.4363} {a : α}, a = a
rfl
@[simp] theorem 
isRight_inl: ∀ {α : Type u} {β : Type v} (x : α), isRight (inl x) = false
isRight_inl (
x: α
x : 
α: Type u
α) : (
inl: {α : Type ?u.4424} → {β : Type ?u.4423} → α → α ⊕ β
inl 
x: α
x : 
α: Type u
α ⊕ 
β: Type v
β).
isRight: {α : Type ?u.4430} → {β : Type ?u.4429} → α ⊕ β → Bool
isRight = 
false: Bool
false := 
rfl: ∀ {α : Sort ?u.4439} {a : α}, a = a
rfl
@[simp] theorem 
isRight_inr: ∀ {α : Type u} {β : Type v} (x : β), isRight (inr x) = true
isRight_inr (
x: β
x : 
β: Type v
β) : (
inr: {α : Type ?u.4500} → {β : Type ?u.4499} → β → α ⊕ β
inr 
x: β
x : 
α: Type u
α ⊕ 
β: Type v
β).
isRight: {α : Type ?u.4506} → {β : Type ?u.4505} → α ⊕ β → Bool
isRight = 
true: Bool
true := 
rfl: ∀ {α : Sort ?u.4515} {a : α}, a = a
rfl

@[simp] theorem 
getLeft_eq_none_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, getLeft x = none ↔ isRight x = true
getLeft_eq_none_iff : 
x: α ⊕ β
x.
getLeft: {α : Type ?u.4571} → {β : Type ?u.4570} → α ⊕ β → Option α
getLeft = 
none: {α : Type ?u.4579} → Option α
none ↔ 
x: α ⊕ β
x.
isRight: {α : Type ?u.4611} → {β : Type ?u.4610} → α ⊕ β → Bool
isRight := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4555

δ: Type ?u.4558

x, y: α ⊕ β

getLeft x = none ↔ isRight x = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4555

δ: Type ?u.4558

y: α ⊕ β

val✝: α

inl
getLeft (inl val✝) = none ↔ isRight (inl val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4555

δ: Type ?u.4558

y: α ⊕ β

val✝: β

inr
getLeft (inr val✝) = none ↔ isRight (inr val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4555

δ: Type ?u.4558

x, y: α ⊕ β

getLeft x = none ↔ isRight x = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4555

δ: Type ?u.4558

y: α ⊕ β

val✝: α

inl
getLeft (inl val✝) = none ↔ isRight (inl val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4555

δ: Type ?u.4558

y: α ⊕ β

val✝: β

inr
getLeft (inr val✝) = none ↔ isRight (inr val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4555

δ: Type ?u.4558

x, y: α ⊕ β

getLeft x = none ↔ isRight x = true
Goals accomplished! 🐙

#align sum.get_left_eq_none_iff 
Sum.getLeft_eq_none_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, getLeft x = none ↔ isRight x = true
Sum.getLeft_eq_none_iff

@[simp] theorem 
getRight_eq_none_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, getRight x = none ↔ isLeft x = true
getRight_eq_none_iff : 
x: α ⊕ β
x.
getRight: {α : Type ?u.4999} → {β : Type ?u.4998} → α ⊕ β → Option β
getRight = 
none: {α : Type ?u.5007} → Option α
none ↔ 
x: α ⊕ β
x.
isLeft: {α : Type ?u.5039} → {β : Type ?u.5038} → α ⊕ β → Bool
isLeft := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4983

δ: Type ?u.4986

x, y: α ⊕ β

getRight x = none ↔ isLeft x = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4983

δ: Type ?u.4986

y: α ⊕ β

val✝: α

inl
getRight (inl val✝) = none ↔ isLeft (inl val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4983

δ: Type ?u.4986

y: α ⊕ β

val✝: β

inr
getRight (inr val✝) = none ↔ isLeft (inr val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4983

δ: Type ?u.4986

x, y: α ⊕ β

getRight x = none ↔ isLeft x = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4983

δ: Type ?u.4986

y: α ⊕ β

val✝: α

inl
getRight (inl val✝) = none ↔ isLeft (inl val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4983

δ: Type ?u.4986

y: α ⊕ β

val✝: β

inr
getRight (inr val✝) = none ↔ isLeft (inr val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.4983

δ: Type ?u.4986

x, y: α ⊕ β

getRight x = none ↔ isLeft x = true
Goals accomplished! 🐙

#align sum.get_right_eq_none_iff 
Sum.getRight_eq_none_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, getRight x = none ↔ isLeft x = true
Sum.getRight_eq_none_iff

@[simp] lemma 
getLeft_eq_some_iff: ∀ {a : α}, getLeft x = some a ↔ x = inl a
getLeft_eq_some_iff {
a: α
a : 
α: Type u
α} : 
x: α ⊕ β
x.
getLeft: {α : Type ?u.5424} → {β : Type ?u.5423} → α ⊕ β → Option α
getLeft = 
a: α
a ↔ 
x: α ⊕ β
x = 
inl: {α : Type ?u.5576} → {β : Type ?u.5575} → α → α ⊕ β
inl 
a: α
a := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5406

δ: Type ?u.5409

x, y: α ⊕ β

a: α

getLeft x = some a ↔ x = inl a
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5406

δ: Type ?u.5409

y: α ⊕ β

a, val✝: α

inl
getLeft (inl val✝) = some a ↔ inl val✝ = inl a
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5406

δ: Type ?u.5409

y: α ⊕ β

a: α

val✝: β

inr
getLeft (inr val✝) = some a ↔ inr val✝ = inl a
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5406

δ: Type ?u.5409

x, y: α ⊕ β

a: α

getLeft x = some a ↔ x = inl a
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5406

δ: Type ?u.5409

y: α ⊕ β

a, val✝: α

inl
getLeft (inl val✝) = some a ↔ inl val✝ = inl a
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5406

δ: Type ?u.5409

y: α ⊕ β

a: α

val✝: β

inr
getLeft (inr val✝) = some a ↔ inr val✝ = inl a
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5406

δ: Type ?u.5409

x, y: α ⊕ β

a: α

getLeft x = some a ↔ x = inl a
Goals accomplished! 🐙

#align sum.get_left_eq_some_iff 
Sum.getLeft_eq_some_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β} {a : α}, getLeft x = some a ↔ x = inl a
Sum.getLeft_eq_some_iff

@[simp] lemma 
getRight_eq_some_iff: ∀ {b : β}, getRight x = some b ↔ x = inr b
getRight_eq_some_iff {
b: β
b : 
β: Type v
β} : 
x: α ⊕ β
x.
getRight: {α : Type ?u.5944} → {β : Type ?u.5943} → α ⊕ β → Option β
getRight = 
b: β
b ↔ 
x: α ⊕ β
x = 
inr: {α : Type ?u.6096} → {β : Type ?u.6095} → β → α ⊕ β
inr 
b: β
b := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5926

δ: Type ?u.5929

x, y: α ⊕ β

b: β

getRight x = some b ↔ x = inr b
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5926

δ: Type ?u.5929

y: α ⊕ β

b: β

val✝: α

inl
getRight (inl val✝) = some b ↔ inl val✝ = inr b
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5926

δ: Type ?u.5929

y: α ⊕ β

b, val✝: β

inr
getRight (inr val✝) = some b ↔ inr val✝ = inr b
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5926

δ: Type ?u.5929

x, y: α ⊕ β

b: β

getRight x = some b ↔ x = inr b
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5926

δ: Type ?u.5929

y: α ⊕ β

b: β

val✝: α

inl
getRight (inl val✝) = some b ↔ inl val✝ = inr b
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5926

δ: Type ?u.5929

y: α ⊕ β

b, val✝: β

inr
getRight (inr val✝) = some b ↔ inr val✝ = inr b
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.5926

δ: Type ?u.5929

x, y: α ⊕ β

b: β

getRight x = some b ↔ x = inr b
Goals accomplished! 🐙

#align sum.get_right_eq_some_iff 
Sum.getRight_eq_some_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β} {b : β}, getRight x = some b ↔ x = inr b
Sum.getRight_eq_some_iff

@[simp]
theorem 
not_isLeft: ∀ {α : Type u} {β : Type v} (x : α ⊕ β), (!isLeft x) = isRight x
not_isLeft (
x: α ⊕ β
x : 
Sum: Type ?u.6466 → Type ?u.6465 → Type (max?u.6466?u.6465)
Sum 
α: Type u
α 
β: Type v
β) : 
not: Bool → Bool
not 
x: α ⊕ β
x.
isLeft: {α : Type ?u.6471} → {β : Type ?u.6470} → α ⊕ β → Bool
isLeft = 
x: α ⊕ β
x.
isRight: {α : Type ?u.6480} → {β : Type ?u.6479} → α ⊕ β → Bool
isRight := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6451

δ: Type ?u.6454

x✝, y, x: α ⊕ β

(!isLeft x) = isRight x
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6451

δ: Type ?u.6454

x, y: α ⊕ β

val✝: α

inl
(!isLeft (inl val✝)) = isRight (inl val✝)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6451

δ: Type ?u.6454

x, y: α ⊕ β

val✝: β

inr
(!isLeft (inr val✝)) = isRight (inr val✝)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6451

δ: Type ?u.6454

x✝, y, x: α ⊕ β

(!isLeft x) = isRight x
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6451

δ: Type ?u.6454

x, y: α ⊕ β

val✝: α

inl
(!isLeft (inl val✝)) = isRight (inl val✝)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6451

δ: Type ?u.6454

x, y: α ⊕ β

val✝: β

inr
(!isLeft (inr val✝)) = isRight (inr val✝)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6451

δ: Type ?u.6454

x✝, y, x: α ⊕ β

(!isLeft x) = isRight x
Goals accomplished! 🐙

#align sum.bnot_is_left 
Sum.not_isLeft: ∀ {α : Type u} {β : Type v} (x : α ⊕ β), (!isLeft x) = isRight x
Sum.not_isLeft

@[simp]
theorem 
isLeft_eq_false: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isLeft x = false ↔ isRight x = true
isLeft_eq_false : 
x: α ⊕ β
x.
isLeft: {α : Type ?u.6631} → {β : Type ?u.6630} → α ⊕ β → Bool
isLeft = 
false: Bool
false ↔ 
x: α ⊕ β
x.
isRight: {α : Type ?u.6641} → {β : Type ?u.6640} → α ⊕ β → Bool
isRight := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6615

δ: Type ?u.6618

x, y: α ⊕ β

isLeft x = false ↔ isRight x = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6615

δ: Type ?u.6618

y: α ⊕ β

val✝: α

inl
isLeft (inl val✝) = false ↔ isRight (inl val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6615

δ: Type ?u.6618

y: α ⊕ β

val✝: β

inr
isLeft (inr val✝) = false ↔ isRight (inr val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6615

δ: Type ?u.6618

x, y: α ⊕ β

isLeft x = false ↔ isRight x = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6615

δ: Type ?u.6618

y: α ⊕ β

val✝: α

inl
isLeft (inl val✝) = false ↔ isRight (inl val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6615

δ: Type ?u.6618

y: α ⊕ β

val✝: β

inr
isLeft (inr val✝) = false ↔ isRight (inr val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6615

δ: Type ?u.6618

x, y: α ⊕ β

isLeft x = false ↔ isRight x = true
Goals accomplished! 🐙

#align sum.is_left_eq_ff 
Sum.isLeft_eq_false: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isLeft x = false ↔ isRight x = true
Sum.isLeft_eq_false

theorem 
Not_isLeft: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, ¬isLeft x = true ↔ isRight x = true
Not_isLeft : ¬
x: α ⊕ β
x.
isLeft: {α : Type ?u.6997} → {β : Type ?u.6996} → α ⊕ β → Bool
isLeft ↔ 
x: α ⊕ β
x.
isRight: {α : Type ?u.7087} → {β : Type ?u.7086} → α ⊕ β → Bool
isRight := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.6982

δ: Type ?u.6985

x, y: α ⊕ β

¬isLeft x = true ↔ isRight x = true
Goals accomplished! 🐙

#align sum.not_is_left 
Sum.Not_isLeft: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, ¬isLeft x = true ↔ isRight x = true
Sum.Not_isLeft

@[simp]
theorem 
not_isRight: ∀ {α : Type u} {β : Type v} (x : α ⊕ β), (!decide (isRight x = isLeft x)) = true
not_isRight (
x: α ⊕ β
x : 
Sum: Type ?u.7263 → Type ?u.7262 → Type (max?u.7263?u.7262)
Sum 
α: Type u
α 
β: Type v
β) : !
x: α ⊕ β
x.
isRight: {α : Type ?u.7268} → {β : Type ?u.7267} → α ⊕ β → Bool
isRight = 
x: α ⊕ β
x.
isLeft: {α : Type ?u.7277} → {β : Type ?u.7276} → α ⊕ β → Bool
isLeft := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7248

δ: Type ?u.7251

x✝, y, x: α ⊕ β

(!decide (isRight x = isLeft x)) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7248

δ: Type ?u.7251

x, y: α ⊕ β

val✝: α

inl
(!decide (isRight (inl val✝) = isLeft (inl val✝))) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7248

δ: Type ?u.7251

x, y: α ⊕ β

val✝: β

inr
(!decide (isRight (inr val✝) = isLeft (inr val✝))) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7248

δ: Type ?u.7251

x✝, y, x: α ⊕ β

(!decide (isRight x = isLeft x)) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7248

δ: Type ?u.7251

x, y: α ⊕ β

val✝: α

inl
(!decide (isRight (inl val✝) = isLeft (inl val✝))) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7248

δ: Type ?u.7251

x, y: α ⊕ β

val✝: β

inr
(!decide (isRight (inr val✝) = isLeft (inr val✝))) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7248

δ: Type ?u.7251

x✝, y, x: α ⊕ β

(!decide (isRight x = isLeft x)) = true
Goals accomplished! 🐙

#align sum.bnot_is_right 
Sum.not_isRight: ∀ {α : Type u} {β : Type v} (x : α ⊕ β), (!decide (isRight x = isLeft x)) = true
Sum.not_isRight

@[simp]
theorem 
isRight_eq_false: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isRight x = false ↔ isLeft x = true
isRight_eq_false : 
x: α ⊕ β
x.
isRight: {α : Type ?u.7496} → {β : Type ?u.7495} → α ⊕ β → Bool
isRight = 
false: Bool
false ↔ 
x: α ⊕ β
x.
isLeft: {α : Type ?u.7506} → {β : Type ?u.7505} → α ⊕ β → Bool
isLeft := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7480

δ: Type ?u.7483

x, y: α ⊕ β

isRight x = false ↔ isLeft x = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7480

δ: Type ?u.7483

y: α ⊕ β

val✝: α

inl
isRight (inl val✝) = false ↔ isLeft (inl val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7480

δ: Type ?u.7483

y: α ⊕ β

val✝: β

inr
isRight (inr val✝) = false ↔ isLeft (inr val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7480

δ: Type ?u.7483

x, y: α ⊕ β

isRight x = false ↔ isLeft x = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7480

δ: Type ?u.7483

y: α ⊕ β

val✝: α

inl
isRight (inl val✝) = false ↔ isLeft (inl val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7480

δ: Type ?u.7483

y: α ⊕ β

val✝: β

inr
isRight (inr val✝) = false ↔ isLeft (inr val✝) = true
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7480

δ: Type ?u.7483

x, y: α ⊕ β

isRight x = false ↔ isLeft x = true
Goals accomplished! 🐙

#align sum.is_right_eq_ff 
Sum.isRight_eq_false: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isRight x = false ↔ isLeft x = true
Sum.isRight_eq_false

theorem 
Not_isRight: ¬isRight x = true ↔ isLeft x = true
Not_isRight : ¬
x: α ⊕ β
x.
isRight: {α : Type ?u.7862} → {β : Type ?u.7861} → α ⊕ β → Bool
isRight ↔ 
x: α ⊕ β
x.
isLeft: {α : Type ?u.7952} → {β : Type ?u.7951} → α ⊕ β → Bool
isLeft := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.7847

δ: Type ?u.7850

x, y: α ⊕ β

¬isRight x = true ↔ isLeft x = true
Goals accomplished! 🐙

#align sum.not_is_right 
Sum.Not_isRight: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, ¬isRight x = true ↔ isLeft x = true
Sum.Not_isRight

theorem 
isLeft_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isLeft x = true ↔ ∃ y, x = inl y
isLeft_iff : 
x: α ⊕ β
x.
isLeft: {α : Type ?u.8128} → {β : Type ?u.8127} → α ⊕ β → Bool
isLeft ↔ ∃ 
y: ?m.8220
y, 
x: α ⊕ β
x = 
Sum.inl: {α : Type ?u.8224} → {β : Type ?u.8223} → α → α ⊕ β
Sum.inl 
y: ?m.8220
y := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8113

δ: Type ?u.8116

x, y: α ⊕ β

isLeft x = true ↔ ∃ y, x = inl y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8113

δ: Type ?u.8116

y: α ⊕ β

val✝: α

inl
isLeft (inl val✝) = true ↔ ∃ y, inl val✝ = inl y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8113

δ: Type ?u.8116

y: α ⊕ β

val✝: β

inr
isLeft (inr val✝) = true ↔ ∃ y, inr val✝ = inl y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8113

δ: Type ?u.8116

x, y: α ⊕ β

isLeft x = true ↔ ∃ y, x = inl y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8113

δ: Type ?u.8116

y: α ⊕ β

val✝: α

inl
isLeft (inl val✝) = true ↔ ∃ y, inl val✝ = inl y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8113

δ: Type ?u.8116

y: α ⊕ β

val✝: β

inr
isLeft (inr val✝) = true ↔ ∃ y, inr val✝ = inl y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8113

δ: Type ?u.8116

x, y: α ⊕ β

isLeft x = true ↔ ∃ y, x = inl y
Goals accomplished! 🐙

#align sum.is_left_iff 
Sum.isLeft_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isLeft x = true ↔ ∃ y, x = inl y
Sum.isLeft_iff

theorem 
isRight_iff: isRight x = true ↔ ∃ y, x = inr y
isRight_iff : 
x: α ⊕ β
x.
isRight: {α : Type ?u.8813} → {β : Type ?u.8812} → α ⊕ β → Bool
isRight ↔ ∃ 
y: ?m.8905
y, 
x: α ⊕ β
x = 
Sum.inr: {α : Type ?u.8909} → {β : Type ?u.8908} → β → α ⊕ β
Sum.inr 
y: ?m.8905
y := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8798

δ: Type ?u.8801

x, y: α ⊕ β

isRight x = true ↔ ∃ y, x = inr y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8798

δ: Type ?u.8801

y: α ⊕ β

val✝: α

inl
isRight (inl val✝) = true ↔ ∃ y, inl val✝ = inr y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8798

δ: Type ?u.8801

y: α ⊕ β

val✝: β

inr
isRight (inr val✝) = true ↔ ∃ y, inr val✝ = inr y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8798

δ: Type ?u.8801

x, y: α ⊕ β

isRight x = true ↔ ∃ y, x = inr y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8798

δ: Type ?u.8801

y: α ⊕ β

val✝: α

inl
isRight (inl val✝) = true ↔ ∃ y, inl val✝ = inr y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8798

δ: Type ?u.8801

y: α ⊕ β

val✝: β

inr
isRight (inr val✝) = true ↔ ∃ y, inr val✝ = inr y
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type ?u.8798

δ: Type ?u.8801

x, y: α ⊕ β

isRight x = true ↔ ∃ y, x = inr y
Goals accomplished! 🐙

#align sum.is_right_iff 
Sum.isRight_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isRight x = true ↔ ∃ y, x = inr y
Sum.isRight_iff

end get

theorem 
inl.inj_iff: ∀ {α : Type u} {β : Type v} {a b : α}, inl a = inl b ↔ a = b
inl.inj_iff {
a: ?m.9489
a 
b: α
b} : (
inl: {α : Type ?u.9500} → {β : Type ?u.9499} → α → α ⊕ β
inl 
a: ?m.9489
a : 
Sum: Type ?u.9498 → Type ?u.9497 → Type (max?u.9498?u.9497)
Sum 
α: Type u
α 
β: Type v
β) = 
inl: {α : Type ?u.9506} → {β : Type ?u.9505} → α → α ⊕ β
inl 
b: ?m.9492
b ↔ 
a: ?m.9489
a = 
b: ?m.9492
b :=
  ⟨
inl.inj: ∀ {α : Type ?u.9554} {β : Type ?u.9553} {val val_1 : α}, inl val = inl val_1 → val = val_1
inl.inj, 
congr_arg: ∀ {α : Sort ?u.9572} {β : Sort ?u.9571} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
_: ?m.9573 → ?m.9574
_⟩
#align sum.inl.inj_iff 
Sum.inl.inj_iff: ∀ {α : Type u} {β : Type v} {a b : α}, inl a = inl b ↔ a = b
Sum.inl.inj_iff

theorem 
inr.inj_iff: ∀ {α : Type u} {β : Type v} {a b : β}, inr a = inr b ↔ a = b
inr.inj_iff {
a: β
a 
b: ?m.9604
b} : (
inr: {α : Type ?u.9612} → {β : Type ?u.9611} → β → α ⊕ β
inr 
a: ?m.9601
a : 
Sum: Type ?u.9610 → Type ?u.9609 → Type (max?u.9610?u.9609)
Sum 
α: Type u
α 
β: Type v
β) = 
inr: {α : Type ?u.9618} → {β : Type ?u.9617} → β → α ⊕ β
inr 
b: ?m.9604
b ↔ 
a: ?m.9601
a = 
b: ?m.9604
b :=
  ⟨
inr.inj: ∀ {α : Type ?u.9666} {β : Type ?u.9665} {val val_1 : β}, inr val = inr val_1 → val = val_1
inr.inj, 
congr_arg: ∀ {α : Sort ?u.9684} {β : Sort ?u.9683} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
_: ?m.9685 → ?m.9686
_⟩
#align sum.inr.inj_iff 
Sum.inr.inj_iff: ∀ {α : Type u} {β : Type v} {a b : β}, inr a = inr b ↔ a = b
Sum.inr.inj_iff

theorem 
inl_ne_inr: ∀ {a : α} {b : β}, inl a ≠ inr b
inl_ne_inr {
a: α
a : 
α: Type u
α} {
b: β
b : 
β: Type v
β} : 
inl: {α : Type ?u.9720} → {β : Type ?u.9719} → α → α ⊕ β
inl 
a: α
a ≠ 
inr: {α : Type ?u.9726} → {β : Type ?u.9725} → β → α ⊕ β
inr 
b: β
b :=
  
fun.: inl a = inr b → False
fun
fun.: inl a = inr b → False
.
#align sum.inl_ne_inr 
Sum.inl_ne_inr: ∀ {α : Type u} {β : Type v} {a : α} {b : β}, inl a ≠ inr b
Sum.inl_ne_inr

theorem 
inr_ne_inl: ∀ {a : α} {b : β}, inr b ≠ inl a
inr_ne_inl {
a: α
a : 
α: Type u
α} {
b: β
b : 
β: Type v
β} : 
inr: {α : Type ?u.9845} → {β : Type ?u.9844} → β → α ⊕ β
inr 
b: β
b ≠ 
inl: {α : Type ?u.9851} → {β : Type ?u.9850} → α → α ⊕ β
inl 
a: α
a :=
  
fun.: inr b = inl a → False
fun
fun.: inr b = inl a → False
.
#align sum.inr_ne_inl 
Sum.inr_ne_inl: ∀ {α : Type u} {β : Type v} {a : α} {b : β}, inr b ≠ inl a
Sum.inr_ne_inl

/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
protected def 
elim: {α : Type u_1} → {β : Type u_2} → {γ : Sort u_3} → (α → γ) → (β → γ) → α ⊕ β → γ
elim {
α: Type ?u.9982
α 
β: Type ?u.9981
β 
γ: Sort ?u.9969
γ : 
Sort _: Type ?u.9963
Sort
Sort _: Type ?u.9963
 _} (
f: α → γ
f : 
α: Sort ?u.9963
α → 
γ: Sort ?u.9969
γ) (
g: β → γ
g : 
β: Sort ?u.9966
β → 
γ: Sort ?u.9969
γ) : 
Sum: Type ?u.9982 → Type ?u.9981 → Type (max?u.9982?u.9981)
Sum 
α: Sort ?u.9963
α 
β: Sort ?u.9966
β → 
γ: Sort ?u.9969
γ :=
  fun 
x: ?m.9991
x ↦ 
Sum.casesOn: {α : Type ?u.9994} →
  {β : Type ?u.9993} →
    {motive : α ⊕ β → Sort ?u.9995} →
      (t : α ⊕ β) → ((val : α) → motive (inl val)) → ((val : β) → motive (inr val)) → motive t
Sum.casesOn 
x: ?m.9991
x 
f: α → γ
f 
g: β → γ
g
#align sum.elim 
Sum.elim: {α : Type u_1} → {β : Type u_2} → {γ : Sort u_3} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim

@[simp]
theorem 
elim_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) (x : α), Sum.elim f g (inl x) = f x
elim_inl {
α: Sort ?u.10166
α 
β: Type u_2
β 
γ: Sort ?u.10172
γ : 
Sort _: Type ?u.10166
Sort
Sort _: Type ?u.10166
 _} (
f: α → γ
f : 
α: Sort ?u.10166
α → 
γ: Sort ?u.10172
γ) (
g: β → γ
g : 
β: Sort ?u.10169
β → 
γ: Sort ?u.10172
γ) (
x: α
x : 
α: Sort ?u.10166
α) : 
Sum.elim: {α : Type ?u.10188} → {β : Type ?u.10187} → {γ : Sort ?u.10186} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f: α → γ
f 
g: β → γ
g (
inl: {α : Type ?u.10199} → {β : Type ?u.10198} → α → α ⊕ β
inl 
x: α
x) = 
f: α → γ
f 
x: α
x :=
  
rfl: ∀ {α : Sort ?u.10212} {a : α}, a = a
rfl
#align sum.elim_inl 
Sum.elim_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) (x : α), Sum.elim f g (inl x) = f x
Sum.elim_inl

@[simp]
theorem 
elim_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) (x : β), Sum.elim f g (inr x) = g x
elim_inr {
α: Type u_1
α 
β: Sort ?u.10267
β 
γ: Sort ?u.10270
γ : 
Sort _: Type ?u.10264
Sort
Sort _: Type ?u.10264
 _} (
f: α → γ
f : 
α: Sort ?u.10264
α → 
γ: Sort ?u.10270
γ) (
g: β → γ
g : 
β: Sort ?u.10267
β → 
γ: Sort ?u.10270
γ) (
x: β
x : 
β: Sort ?u.10267
β) : 
Sum.elim: {α : Type ?u.10286} → {β : Type ?u.10285} → {γ : Sort ?u.10284} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f: α → γ
f 
g: β → γ
g (
inr: {α : Type ?u.10297} → {β : Type ?u.10296} → β → α ⊕ β
inr 
x: β
x) = 
g: β → γ
g 
x: β
x :=
  
rfl: ∀ {α : Sort ?u.10310} {a : α}, a = a
rfl
#align sum.elim_inr 
Sum.elim_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) (x : β), Sum.elim f g (inr x) = g x
Sum.elim_inr

@[simp]
theorem 
elim_comp_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ), Sum.elim f g ∘ inl = f
elim_comp_inl {
α: Type u_1
α 
β: Sort ?u.10365
β 
γ: Sort ?u.10368
γ : 
Sort _: Type ?u.10368
Sort
Sort _: Type ?u.10368
 _} (
f: α → γ
f : 
α: Sort ?u.10362
α → 
γ: Sort ?u.10368
γ) (
g: β → γ
g : 
β: Sort ?u.10365
β → 
γ: Sort ?u.10368
γ) : 
Sum.elim: {α : Type ?u.10388} → {β : Type ?u.10387} → {γ : Sort ?u.10386} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f: α → γ
f 
g: β → γ
g ∘ 
inl: {α : Type ?u.10406} → {β : Type ?u.10405} → α → α ⊕ β
inl = 
f: α → γ
f :=
  
rfl: ∀ {α : Sort ?u.10422} {a : α}, a = a
rfl
#align sum.elim_comp_inl 
Sum.elim_comp_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ), Sum.elim f g ∘ inl = f
Sum.elim_comp_inl

@[simp]
theorem 
elim_comp_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ), Sum.elim f g ∘ inr = g
elim_comp_inr {
α: Type u_1
α 
β: Sort ?u.10486
β 
γ: Sort u_3
γ : 
Sort _: Type ?u.10489
Sort
Sort _: Type ?u.10489
 _} (
f: α → γ
f : 
α: Sort ?u.10483
α → 
γ: Sort ?u.10489
γ) (
g: β → γ
g : 
β: Sort ?u.10486
β → 
γ: Sort ?u.10489
γ) : 
Sum.elim: {α : Type ?u.10509} → {β : Type ?u.10508} → {γ : Sort ?u.10507} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f: α → γ
f 
g: β → γ
g ∘ 
inr: {α : Type ?u.10527} → {β : Type ?u.10526} → β → α ⊕ β
inr = 
g: β → γ
g :=
  
rfl: ∀ {α : Sort ?u.10543} {a : α}, a = a
rfl
#align sum.elim_comp_inr 
Sum.elim_comp_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ), Sum.elim f g ∘ inr = g
Sum.elim_comp_inr

@[simp]
theorem 
elim_inl_inr: ∀ {α : Type u_1} {β : Type u_2}, Sum.elim inl inr = id
elim_inl_inr {
α: Sort ?u.10604
α 
β: Sort ?u.10607
β : 
Sort _: Type ?u.10604
Sort
Sort _: Type ?u.10604
 _} : @
Sum.elim: {α : Type ?u.10613} → {β : Type ?u.10612} → {γ : Sort ?u.10611} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
α: Sort ?u.10604
α 
β: Sort ?u.10607
β 
_: Sort ?u.10611
_ 
inl: {α : Type ?u.10616} → {β : Type ?u.10615} → α → α ⊕ β
inl 
inr: {α : Type ?u.10625} → {β : Type ?u.10624} → β → α ⊕ β
inr = 
id: {α : Sort ?u.10633} → α → α
id :=
  
funext: ∀ {α : Sort ?u.10677} {β : α → Sort ?u.10676} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun 
x: ?m.10691
x ↦ 
Sum.casesOn: ∀ {α : Type ?u.10694} {β : Type ?u.10693} {motive : α ⊕ β → Sort ?u.10695} (t : α ⊕ β),
  (∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → motive t
Sum.casesOn 
x: ?m.10691
x (fun 
_: ?m.10738
_ ↦ 
rfl: ∀ {α : Sort ?u.10740} {a : α}, a = a
rfl) fun 
_: ?m.10746
_ ↦ 
rfl: ∀ {α : Sort ?u.10748} {a : α}, a = a
rfl
#align sum.elim_inl_inr 
Sum.elim_inl_inr: ∀ {α : Type u_1} {β : Type u_2}, Sum.elim inl inr = id
Sum.elim_inl_inr

theorem 
comp_elim: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} {δ : Sort u_4} (f : γ → δ) (g : α → γ) (h : β → γ),
  f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h)
comp_elim {
α: Sort ?u.10792
α 
β: Type u_2
β 
γ: Sort u_3
γ 
δ: Sort ?u.10801
δ : 
Sort _: Type ?u.10795
Sort
Sort _: Type ?u.10795
 _} (
f: γ → δ
f : 
γ: Sort ?u.10798
γ → 
δ: Sort ?u.10801
δ) (
g: α → γ
g : 
α: Sort ?u.10792
α → 
γ: Sort ?u.10798
γ) (
h: β → γ
h : 
β: Sort ?u.10795
β → 
γ: Sort ?u.10798
γ) :
    
f: γ → δ
f ∘ 
Sum.elim: {α : Type ?u.10828} → {β : Type ?u.10827} → {γ : Sort ?u.10826} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
g: α → γ
g 
h: β → γ
h = 
Sum.elim: {α : Type ?u.10848} → {β : Type ?u.10847} → {γ : Sort ?u.10846} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim (
f: γ → δ
f ∘ 
g: α → γ
g) (
f: γ → δ
f ∘ 
h: β → γ
h) :=
  
funext: ∀ {α : Sort ?u.10899} {β : α → Sort ?u.10898} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun 
x: ?m.10913
x ↦ 
Sum.casesOn: ∀ {α : Type ?u.10916} {β : Type ?u.10915} {motive : α ⊕ β → Sort ?u.10917} (t : α ⊕ β),
  (∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → motive t
Sum.casesOn 
x: ?m.10913
x (fun 
_: ?m.10963
_ ↦ 
rfl: ∀ {α : Sort ?u.10965} {a : α}, a = a
rfl) fun 
_: ?m.10972
_ ↦ 
rfl: ∀ {α : Sort ?u.10974} {a : α}, a = a
rfl
#align sum.comp_elim 
Sum.comp_elim: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} {δ : Sort u_4} (f : γ → δ) (g : α → γ) (h : β → γ),
  f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h)
Sum.comp_elim

@[simp]
theorem 
elim_comp_inl_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α ⊕ β → γ), Sum.elim (f ∘ inl) (f ∘ inr) = f
elim_comp_inl_inr {
α: Sort ?u.11009
α 
β: Sort ?u.11012
β 
γ: Sort u_3
γ : 
Sort _: Type ?u.11009
Sort
Sort _: Type ?u.11009
 _} (
f: α ⊕ β → γ
f : 
Sum: Type ?u.11020 → Type ?u.11019 → Type (max?u.11020?u.11019)
Sum 
α: Sort ?u.11009
α 
β: Sort ?u.11012
β → 
γ: Sort ?u.11015
γ) : 
Sum.elim: {α : Type ?u.11027} → {β : Type ?u.11026} → {γ : Sort ?u.11025} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim (
f: α ⊕ β → γ
f ∘ 
inl: {α : Type ?u.11043} → {β : Type ?u.11042} → α → α ⊕ β
inl) (
f: α ⊕ β → γ
f ∘ 
inr: {α : Type ?u.11066} → {β : Type ?u.11065} → β → α ⊕ β
inr) = 
f: α ⊕ β → γ
f :=
  
funext: ∀ {α : Sort ?u.11085} {β : α → Sort ?u.11084} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun 
x: ?m.11099
x ↦ 
Sum.casesOn: ∀ {α : Type ?u.11102} {β : Type ?u.11101} {motive : α ⊕ β → Sort ?u.11103} (t : α ⊕ β),
  (∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → motive t
Sum.casesOn 
x: ?m.11099
x (fun 
_: ?m.11149
_ ↦ 
rfl: ∀ {α : Sort ?u.11151} {a : α}, a = a
rfl) fun 
_: ?m.11157
_ ↦ 
rfl: ∀ {α : Sort ?u.11159} {a : α}, a = a
rfl
#align sum.elim_comp_inl_inr 
Sum.elim_comp_inl_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α ⊕ β → γ), Sum.elim (f ∘ inl) (f ∘ inr) = f
Sum.elim_comp_inl_inr

/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
protected def 
map: {α : Type u} → {α' : Type w} → {β : Type v} → {β' : Type x} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map (
f: α → α'
f : 
α: Type u
α → 
α': Type w
α') (
g: β → β'
g : 
β: Type v
β → 
β': Type x
β') : 
Sum: Type ?u.11234 → Type ?u.11233 → Type (max?u.11234?u.11233)
Sum 
α: Type u
α 
β: Type v
β → 
Sum: Type ?u.11237 → Type ?u.11236 → Type (max?u.11237?u.11236)
Sum 
α': Type w
α' 
β': Type x
β' :=
  
Sum.elim: {α : Type ?u.11243} → {β : Type ?u.11242} → {γ : Sort ?u.11241} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim (
inl: {α : Type ?u.11260} → {β : Type ?u.11259} → α → α ⊕ β
inl ∘ 
f: α → α'
f) (
inr: {α : Type ?u.11283} → {β : Type ?u.11282} → β → α ⊕ β
inr ∘ 
g: β → β'
g)
#align sum.map 
Sum.map: {α : Type u} → {α' : Type w} → {β : Type v} → {β' : Type x} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
Sum.map

@[simp]
theorem 
map_inl: ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : α → α') (g : β → β') (x : α),
  Sum.map f g (inl x) = inl (f x)
map_inl (
f: α → α'
f : 
α: Type u
α → 
α': Type w
α') (
g: β → β'
g : 
β: Type v
β → 
β': Type x
β') (
x: α
x : 
α: Type u
α) : (
inl: {α : Type ?u.11438} → {β : Type ?u.11437} → α → α ⊕ β
inl 
x: α
x).
map: {α : Type ?u.11444} →
  {α' : Type ?u.11442} → {β : Type ?u.11443} → {β' : Type ?u.11441} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map 
f: α → α'
f 
g: β → β'
g = 
inl: {α : Type ?u.11465} → {β : Type ?u.11464} → α → α ⊕ β
inl (
f: α → α'
f 
x: α
x) :=
  
rfl: ∀ {α : Sort ?u.11505} {a : α}, a = a
rfl
#align sum.map_inl 
Sum.map_inl: ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : α → α') (g : β → β') (x : α),
  Sum.map f g (inl x) = inl (f x)
Sum.map_inl

@[simp]
theorem 
map_inr: ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : α → α') (g : β → β') (x : β),
  Sum.map f g (inr x) = inr (g x)
map_inr (
f: α → α'
f : 
α: Type u
α → 
α': Type w
α') (
g: β → β'
g : 
β: Type v
β → 
β': Type x
β') (
x: β
x : 
β: Type v
β) : (
inr: {α : Type ?u.11573} → {β : Type ?u.11572} → β → α ⊕ β
inr 
x: β
x).
map: {α : Type ?u.11579} →
  {α' : Type ?u.11577} → {β : Type ?u.11578} → {β' : Type ?u.11576} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map 
f: α → α'
f 
g: β → β'
g = 
inr: {α : Type ?u.11600} → {β : Type ?u.11599} → β → α ⊕ β
inr (
g: β → β'
g 
x: β
x) :=
  
rfl: ∀ {α : Sort ?u.11640} {a : α}, a = a
rfl
#align sum.map_inr 
Sum.map_inr: ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : α → α') (g : β → β') (x : β),
  Sum.map f g (inr x) = inr (g x)
Sum.map_inr

@[simp]
theorem 
map_map: ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {α'' : Type u_1} {β'' : Type u_2} (f' : α' → α'')
  (g' : β' → β'') (f : α → α') (g : β → β') (x : α ⊕ β), Sum.map f' g' (Sum.map f g x) = Sum.map (f' ∘ f) (g' ∘ g) x
map_map {
α'': ?m.11696
α'' 
β'': ?m.11699
β''} (
f': α' → α''
f' : 
α': Type w
α' → 
α'': ?m.11696
α'') (
g': β' → β''
g' : 
β': Type x
β' → 
β'': ?m.11699
β'') (
f: α → α'
f : 
α: Type u
α → 
α': Type w
α') (
g: β → β'
g : 
β: Type v
β → 
β': Type x
β') :
    ∀ 
x: α ⊕ β
x : 
Sum: Type ?u.11720 → Type ?u.11719 → Type (max?u.11720?u.11719)
Sum 
α: Type u
α 
β: Type v
β, (
x: α ⊕ β
x.
map: {α : Type ?u.11727} →
  {α' : Type ?u.11725} → {β : Type ?u.11726} → {β' : Type ?u.11724} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map 
f: α → α'
f 
g: β → β'
g).
map: {α : Type ?u.11750} →
  {α' : Type ?u.11748} → {β : Type ?u.11749} → {β' : Type ?u.11747} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map 
f': α' → α''
f' 
g': β' → β''
g' = 
x: α ⊕ β
x.
map: {α : Type ?u.11773} →
  {α' : Type ?u.11771} → {β : Type ?u.11772} → {β' : Type ?u.11770} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map (
f': α' → α''
f' ∘ 
f: α → α'
f) (
g': β' → β''
g' ∘ 
g: β → β'
g)
  | 
inl: {α : Type ?u.11833} → {β : Type ?u.11832} → α → α ⊕ β
inl _ => 
rfl: ∀ {α : Sort ?u.11853} {a : α}, a = a
rfl
  | 
inr: {α : Type ?u.11938} → {β : Type ?u.11937} → β → α ⊕ β
inr _ => 
rfl: ∀ {α : Sort ?u.11956} {a : α}, a = a
rfl
#align sum.map_map 
Sum.map_map: ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {α'' : Type u_1} {β'' : Type u_2} (f' : α' → α'')
  (g' : β' → β'') (f : α → α') (g : β → β') (x : α ⊕ β), Sum.map f' g' (Sum.map f g x) = Sum.map (f' ∘ f) (g' ∘ g) x
Sum.map_map

@[simp]
theorem 
map_comp_map: ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {α'' : Type u_1} {β'' : Type u_2} (f' : α' → α'')
  (g' : β' → β'') (f : α → α') (g : β → β'), Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g)
map_comp_map {
α'': Type u_1
α'' 
β'': ?m.12129
β''} (
f': α' → α''
f' : 
α': Type w
α' → 
α'': ?m.12126
α'') (
g': β' → β''
g' : 
β': Type x
β' → 
β'': ?m.12129
β'') (
f: α → α'
f : 
α: Type u
α → 
α': Type w
α') (
g: β → β'
g : 
β: Type v
β → 
β': Type x
β') :
    
Sum.map: {α : Type ?u.12158} →
  {α' : Type ?u.12156} → {β : Type ?u.12157} → {β' : Type ?u.12155} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
Sum.map 
f': α' → α''
f' 
g': β' → β''
g' ∘ 
Sum.map: {α : Type ?u.12181} →
  {α' : Type ?u.12179} → {β : Type ?u.12180} → {β' : Type ?u.12178} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
Sum.map 
f: α → α'
f 
g: β → β'
g = 
Sum.map: {α : Type ?u.12203} →
  {α' : Type ?u.12201} → {β : Type ?u.12202} → {β' : Type ?u.12200} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
Sum.map (
f': α' → α''
f' ∘ 
f: α → α'
f) (
g': β' → β''
g' ∘ 
g: β → β'
g) :=
  
funext: ∀ {α : Sort ?u.12254} {β : α → Sort ?u.12253} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext <| 
map_map: ∀ {α : Type ?u.12270} {α' : Type ?u.12268} {β : Type ?u.12269} {β' : Type ?u.12267} {α'' : Type ?u.12271}
  {β'' : Type ?u.12272} (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') (x : α ⊕ β),
  Sum.map f' g' (Sum.map f g x) = Sum.map (f' ∘ f) (g' ∘ g) x
map_map 
f': α' → α''
f' 
g': β' → β''
g' 
f: α → α'
f 
g: β → β'
g
#align sum.map_comp_map 
Sum.map_comp_map: ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {α'' : Type u_1} {β'' : Type u_2} (f' : α' → α'')
  (g' : β' → β'') (f : α → α') (g : β → β'), Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g)
Sum.map_comp_map

@[simp]
theorem 
map_id_id: ∀ (α : Type u_1) (β : Type u_2), Sum.map id id = id
map_id_id (
α: ?m.12382
α 
β: Type u_2
β) : 
Sum.map: {α : Type ?u.12392} →
  {α' : Type ?u.12390} → {β : Type ?u.12391} → {β' : Type ?u.12389} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
Sum.map (@
id: {α : Sort ?u.12397} → α → α
id 
α: ?m.12382
α) (@
id: {α : Sort ?u.12400} → α → α
id 
β: ?m.12385
β) = 
id: {α : Sort ?u.12404} → α → α
id :=
  
funext: ∀ {α : Sort ?u.12450} {β : α → Sort ?u.12449} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun 
x: ?m.12464
x ↦ 
Sum.recOn: ∀ {α : Type ?u.12467} {β : Type ?u.12466} {motive : α ⊕ β → Sort ?u.12468} (t : α ⊕ β),
  (∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → motive t
Sum.recOn 
x: ?m.12464
x (fun 
_: ?m.12511
_ ↦ 
rfl: ∀ {α : Sort ?u.12513} {a : α}, a = a
rfl) fun 
_: ?m.12522
_ ↦ 
rfl: ∀ {α : Sort ?u.12524} {a : α}, a = a
rfl
#align sum.map_id_id 
Sum.map_id_id: ∀ (α : Type u_1) (β : Type u_2), Sum.map id id = id
Sum.map_id_id

theorem 
elim_map: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Sort u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ}
  {g₂ : δ → ε} {x : α ⊕ γ}, Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
elim_map {
α: Type u_1
α 
β: Sort ?u.12571
β 
γ: Type u_3
γ 
δ: Sort ?u.12577
δ 
ε: Sort u_5
ε : 
Sort _: Type ?u.12580
Sort
Sort _: Type ?u.12580
 _} {
f₁: α → β
f₁ : 
α: Sort ?u.12568
α → 
β: Sort ?u.12571
β} {
f₂: β → ε
f₂ : 
β: Sort ?u.12571
β → 
ε: Sort ?u.12580
ε} {
g₁: γ → δ
g₁ : 
γ: Sort ?u.12574
γ → 
δ: Sort ?u.12577
δ} {
g₂: δ → ε
g₂ : 
δ: Sort ?u.12577
δ → 
ε: Sort ?u.12580
ε} {
x: α ⊕ γ
x} :
    
Sum.elim: {α : Type ?u.12605} → {β : Type ?u.12604} → {γ : Sort ?u.12603} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f₂: β → ε
f₂ 
g₂: δ → ε
g₂ (
Sum.map: {α : Type ?u.12618} →
  {α' : Type ?u.12616} → {β : Type ?u.12617} → {β' : Type ?u.12615} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
Sum.map 
f₁: α → β
f₁ 
g₁: γ → δ
g₁ 
x: ?m.12599
x) = 
Sum.elim: {α : Type ?u.12635} → {β : Type ?u.12634} → {γ : Sort ?u.12633} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim (
f₂: β → ε
f₂ ∘ 
f₁: α → β
f₁) (
g₂: δ → ε
g₂ ∘ 
g₁: γ → δ
g₁) 
x: ?m.12599
x := 
Goals accomplished! 🐙
α✝: Type u

α': Type w

β✝: Type v

β': Type x

γ✝: Type ?u.12562

δ✝: Type ?u.12565

α: Type u_1

β: Type u_2

γ: Type u_3

δ: Type u_4

ε: Sort u_5

f₁: α → β

f₂: β → ε

g₁: γ → δ

g₂: δ → ε

x: α ⊕ γ

Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
α✝: Type u

α': Type w

β✝: Type v

β': Type x

γ✝: Type ?u.12562

δ✝: Type ?u.12565

α: Type u_1

β: Type u_2

γ: Type u_3

δ: Type u_4

ε: Sort u_5

f₁: α → β

f₂: β → ε

g₁: γ → δ

g₂: δ → ε

val✝: α

inl
Sum.elim f₂ g₂ (Sum.map f₁ g₁ (inl val✝)) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) (inl val✝)
α✝: Type u

α': Type w

β✝: Type v

β': Type x

γ✝: Type ?u.12562

δ✝: Type ?u.12565

α: Type u_1

β: Type u_2

γ: Type u_3

δ: Type u_4

ε: Sort u_5

f₁: α → β

f₂: β → ε

g₁: γ → δ

g₂: δ → ε

val✝: γ

inr
Sum.elim f₂ g₂ (Sum.map f₁ g₁ (inr val✝)) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) (inr val✝)
α✝: Type u

α': Type w

β✝: Type v

β': Type x

γ✝: Type ?u.12562

δ✝: Type ?u.12565

α: Type u_1

β: Type u_2

γ: Type u_3

δ: Type u_4

ε: Sort u_5

f₁: α → β

f₂: β → ε

g₁: γ → δ

g₂: δ → ε

x: α ⊕ γ

Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
α✝: Type u

α': Type w

β✝: Type v

β': Type x

γ✝: Type ?u.12562

δ✝: Type ?u.12565

α: Type u_1

β: Type u_2

γ: Type u_3

δ: Type u_4

ε: Sort u_5

f₁: α → β

f₂: β → ε

g₁: γ → δ

g₂: δ → ε

val✝: α

inl
Sum.elim f₂ g₂ (Sum.map f₁ g₁ (inl val✝)) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) (inl val✝)
α✝: Type u

α': Type w

β✝: Type v

β': Type x

γ✝: Type ?u.12562

δ✝: Type ?u.12565

α: Type u_1

β: Type u_2

γ: Type u_3

δ: Type u_4

ε: Sort u_5

f₁: α → β

f₂: β → ε

g₁: γ → δ

g₂: δ → ε

val✝: γ

inr
Sum.elim f₂ g₂ (Sum.map f₁ g₁ (inr val✝)) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) (inr val✝)
α✝: Type u

α': Type w

β✝: Type v

β': Type x

γ✝: Type ?u.12562

δ✝: Type ?u.12565

α: Type u_1

β: Type u_2

γ: Type u_3

δ: Type u_4

ε: Sort u_5

f₁: α → β

f₂: β → ε

g₁: γ → δ

g₂: δ → ε

x: α ⊕ γ

Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
Goals accomplished! 🐙

#align sum.elim_map 
Sum.elim_map: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Sort u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ}
  {g₂ : δ → ε} {x : α ⊕ γ}, Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
Sum.elim_map

theorem 
elim_comp_map: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Sort u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ}
  {g₂ : δ → ε}, Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁)
elim_comp_map {
α: Sort ?u.12808
α 
β: Sort ?u.12811
β 
γ: Sort ?u.12814
γ 
δ: Type u_4
δ 
ε: Sort ?u.12820
ε : 
Sort _: Type ?u.12817
Sort
Sort _: Type ?u.12817
 _} {
f₁: α → β
f₁ : 
α: Sort ?u.12808
α → 
β: Sort ?u.12811
β} {
f₂: β → ε
f₂ : 
β: Sort ?u.12811
β → 
ε: Sort ?u.12820
ε} {
g₁: γ → δ
g₁ : 
γ: Sort ?u.12814
γ → 
δ: Sort ?u.12817
δ} {
g₂: δ → ε
g₂ : 
δ: Sort ?u.12817
δ → 
ε: Sort ?u.12820
ε} :
    
Sum.elim: {α : Type ?u.12848} → {β : Type ?u.12847} → {γ : Sort ?u.12846} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f₂: β → ε
f₂ 
g₂: δ → ε
g₂ ∘ 
Sum.map: {α : Type ?u.12868} →
  {α' : Type ?u.12866} → {β : Type ?u.12867} → {β' : Type ?u.12865} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
Sum.map 
f₁: α → β
f₁ 
g₁: γ → δ
g₁ = 
Sum.elim: {α : Type ?u.12889} → {β : Type ?u.12888} → {γ : Sort ?u.12887} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim (
f₂: β → ε
f₂ ∘ 
f₁: α → β
f₁) (
g₂: δ → ε
g₂ ∘ 
g₁: γ → δ
g₁) :=
  
funext: ∀ {α : Sort ?u.12942} {β : α → Sort ?u.12941} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext $ fun 
_: ?m.12956
_ => 
elim_map: ∀ {α : Type ?u.12958} {β : Type ?u.12959} {γ : Type ?u.12960} {δ : Type ?u.12961} {ε : Sort ?u.12962} {f₁ : α → β}
  {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x : α ⊕ γ}, Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
elim_map
#align sum.elim_comp_map 
Sum.elim_comp_map: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Sort u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ}
  {g₂ : δ → ε}, Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁)
Sum.elim_comp_map

@[simp]
theorem 
isLeft_map: ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  isLeft (Sum.map f g x) = isLeft x
isLeft_map (
f: α → β
f : 
α: Type u
α → 
β: Type v
β) (
g: γ → δ
g : 
γ: Type ?u.13036
γ → 
δ: Type ?u.13039
δ) (
x: α ⊕ γ
x : 
Sum: Type ?u.13051 → Type ?u.13050 → Type (max?u.13051?u.13050)
Sum 
α: Type u
α 
γ: Type ?u.13036
γ) : 
isLeft: {α : Type ?u.13056} → {β : Type ?u.13055} → α ⊕ β → Bool
isLeft (
x: α ⊕ γ
x.
map: {α : Type ?u.13062} →
  {α' : Type ?u.13060} → {β : Type ?u.13061} → {β' : Type ?u.13059} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map 
f: α → β
f 
g: γ → δ
g) = 
isLeft: {α : Type ?u.13087} → {β : Type ?u.13086} → α ⊕ β → Bool
isLeft 
x: α ⊕ γ
x :=

Goals accomplished! 🐙
α: 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
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: α

inl
isLeft (Sum.map f g (inl val✝)) = isLeft (inl val✝)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: γ

inr
isLeft (Sum.map f g (inr val✝)) = isLeft (inr val✝)
α: 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
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: α

inl
isLeft (Sum.map f g (inl val✝)) = isLeft (inl val✝)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: γ

inr
isLeft (Sum.map f g (inr val✝)) = isLeft (inr val✝)
α: 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
Goals accomplished! 🐙

#align sum.is_left_map 
Sum.isLeft_map: ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  isLeft (Sum.map f g x) = isLeft x
Sum.isLeft_map

@[simp]
theorem 
isRight_map: ∀ (f : α → β) (g : γ → δ) (x : α ⊕ γ), isRight (Sum.map f g x) = isRight x
isRight_map (
f: α → β
f : 
α: Type u
α → 
β: Type v
β) (
g: γ → δ
g : 
γ: Type ?u.13254
γ → 
δ: Type ?u.13257
δ) (
x: α ⊕ γ
x : 
Sum: Type ?u.13269 → Type ?u.13268 → Type (max?u.13269?u.13268)
Sum 
α: Type u
α 
γ: Type ?u.13254
γ) : 
isRight: {α : Type ?u.13274} → {β : Type ?u.13273} → α ⊕ β → Bool
isRight (
x: α ⊕ γ
x.
map: {α : Type ?u.13280} →
  {α' : Type ?u.13278} → {β : Type ?u.13279} → {β' : Type ?u.13277} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map 
f: α → β
f 
g: γ → δ
g) = 
isRight: {α : Type ?u.13305} → {β : Type ?u.13304} → α ⊕ β → Bool
isRight 
x: α ⊕ γ
x :=

Goals accomplished! 🐙
α: 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
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: α

inl
isRight (Sum.map f g (inl val✝)) = isRight (inl val✝)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: γ

inr
isRight (Sum.map f g (inr val✝)) = isRight (inr val✝)
α: 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
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: α

inl
isRight (Sum.map f g (inl val✝)) = isRight (inl val✝)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: γ

inr
isRight (Sum.map f g (inr val✝)) = isRight (inr val✝)
α: 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
Goals accomplished! 🐙

#align sum.is_right_map 
Sum.isRight_map: ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  isRight (Sum.map f g x) = isRight x
Sum.isRight_map

@[simp]
theorem 
getLeft_map: ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  getLeft (Sum.map f g x) = Option.map f (getLeft x)
getLeft_map (
f: α → β
f : 
α: Type u
α → 
β: Type v
β) (
g: γ → δ
g : 
γ: Type ?u.13472
γ → 
δ: Type ?u.13475
δ) (
x: α ⊕ γ
x : 
Sum: Type ?u.13487 → Type ?u.13486 → Type (max?u.13487?u.13486)
Sum 
α: Type u
α 
γ: Type ?u.13472
γ) : (
x: α ⊕ γ
x.
map: {α : Type ?u.13494} →
  {α' : Type ?u.13492} → {β : Type ?u.13493} → {β' : Type ?u.13491} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map 
f: α → β
f 
g: γ → δ
g).
getLeft: {α : Type ?u.13515} → {β : Type ?u.13514} → α ⊕ β → Option α
getLeft = 
x: α ⊕ γ
x.
getLeft: {α : Type ?u.13524} → {β : Type ?u.13523} → α ⊕ β → Option α
getLeft.
map: {α : Type ?u.13528} → {β : Type ?u.13527} → (α → β) → Option α → Option β
map 
f: α → β
f :=

Goals accomplished! 🐙
α: 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)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: α

inl
getLeft (Sum.map f g (inl val✝)) = Option.map f (getLeft (inl val✝))
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: γ

inr
getLeft (Sum.map f g (inr val✝)) = Option.map f (getLeft (inr val✝))
α: 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)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: α

inl
getLeft (Sum.map f g (inl val✝)) = Option.map f (getLeft (inl val✝))
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: γ

inr
getLeft (Sum.map f g (inr val✝)) = Option.map f (getLeft (inr val✝))
α: 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)
Goals accomplished! 🐙

#align sum.get_left_map 
Sum.getLeft_map: ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  getLeft (Sum.map f g x) = Option.map f (getLeft x)
Sum.getLeft_map

@[simp]
theorem 
getRight_map: ∀ (f : α → β) (g : γ → δ) (x : α ⊕ γ), getRight (Sum.map f g x) = Option.map g (getRight x)
getRight_map (
f: α → β
f : 
α: Type u
α → 
β: Type v
β) (
g: γ → δ
g : 
γ: Type ?u.13702
γ → 
δ: Type ?u.13705
δ) (
x: α ⊕ γ
x : 
α: Type u
α ⊕ 
γ: Type ?u.13702
γ) :
  (
x: α ⊕ γ
x.
map: {α : Type ?u.13724} →
  {α' : Type ?u.13722} → {β : Type ?u.13723} → {β' : Type ?u.13721} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'
map 
f: α → β
f 
g: γ → δ
g).
getRight: {α : Type ?u.13745} → {β : Type ?u.13744} → α ⊕ β → Option β
getRight = 
x: α ⊕ γ
x.
getRight: {α : Type ?u.13754} → {β : Type ?u.13753} → α ⊕ β → Option β
getRight.
map: {α : Type ?u.13758} → {β : Type ?u.13757} → (α → β) → Option α → Option β
map 
g: γ → δ
g := 
Goals accomplished! 🐙
α: 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)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: α

inl
getRight (Sum.map f g (inl val✝)) = Option.map g (getRight (inl val✝))
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: γ

inr
getRight (Sum.map f g (inr val✝)) = Option.map g (getRight (inr val✝))
α: 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)
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: α

inl
getRight (Sum.map f g (inl val✝)) = Option.map g (getRight (inl val✝))
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type u_2

f: α → β

g: γ → δ

val✝: γ

inr
getRight (Sum.map f g (inr val✝)) = Option.map g (getRight (inr val✝))
α: 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)
Goals accomplished! 🐙

#align sum.get_right_map 
Sum.getRight_map: ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  getRight (Sum.map f g x) = Option.map g (getRight x)
Sum.getRight_map

open Function (update update_eq_iff update_comp_eq_of_injective update_comp_eq_of_forall_ne)

@[simp]
theorem 
update_elim_inl: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ}
  {i : α} {x : γ}, update (Sum.elim f g) (inl i) x = Sum.elim (update f i x) g
update_elim_inl [
DecidableEq: Sort ?u.13938 → Sort (max1?u.13938)
DecidableEq 
α: Type u
α] [
DecidableEq: Sort ?u.13947 → Sort (max1?u.13947)
DecidableEq (
Sum: Type ?u.13949 → Type ?u.13948 → Type (max?u.13949?u.13948)
Sum 
α: Type u
α 
β: Type v
β)] {
f: α → γ
f : 
α: Type u
α → 
γ: Type ?u.13932
γ} {
g: β → γ
g : 
β: Type v
β → 
γ: Type ?u.13932
γ} {
i: α
i : 
α: Type u
α}
    {
x: γ
x : 
γ: Type ?u.13932
γ} : 
update: {α : Sort ?u.13972} →
  {β : α → Sort ?u.13971} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update (
Sum.elim: {α : Type ?u.13978} → {β : Type ?u.13977} → {γ : Sort ?u.13976} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f: α → γ
f 
g: β → γ
g) (
inl: {α : Type ?u.14000} → {β : Type ?u.13999} → α → α ⊕ β
inl 
i: α
i) 
x: γ
x = 
Sum.elim: {α : Type ?u.14056} → {β : Type ?u.14055} → {γ : Sort ?u.14054} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim (
update: {α : Sort ?u.14061} →
  {β : α → Sort ?u.14060} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update 
f: α → γ
f 
i: α
i 
x: γ
x) 
g: β → γ
g :=
  
update_eq_iff: ∀ {α : Sort ?u.14177} {β : α → Sort ?u.14176} [inst : DecidableEq α] {a : α} {b : β a} {f g : (a : α) → β a},
  update f a b = g ↔ b = g a ∧ ∀ (x : α), x ≠ a → f x = g x
update_eq_iff.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.13935

inst✝¹: DecidableEq α

inst✝: DecidableEq (α ⊕ β)

f: α → γ

g: β → γ

i: α

x: γ

x = Sum.elim (update f i x) g (inl i)
Goals accomplished! 🐙
, 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.13935

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
Goals accomplished! 🐙
⟩
#align sum.update_elim_inl 
Sum.update_elim_inl: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ}
  {i : α} {x : γ}, update (Sum.elim f g) (inl i) x = Sum.elim (update f i x) g
Sum.update_elim_inl

@[simp]
theorem 
update_elim_inr: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq β] [inst_1 : DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ}
  {i : β} {x : γ}, update (Sum.elim f g) (inr i) x = Sum.elim f (update g i x)
update_elim_inr [
DecidableEq: Sort ?u.16305 → Sort (max1?u.16305)
DecidableEq 
β: Type v
β] [
DecidableEq: Sort ?u.16314 → Sort (max1?u.16314)
DecidableEq (
Sum: Type ?u.16316 → Type ?u.16315 → Type (max?u.16316?u.16315)
Sum 
α: Type u
α 
β: Type v
β)] {
f: α → γ
f : 
α: Type u
α → 
γ: Type ?u.16299
γ} {
g: β → γ
g : 
β: Type v
β → 
γ: Type ?u.16299
γ} {
i: β
i : 
β: Type v
β}
    {
x: γ
x : 
γ: Type ?u.16299
γ} : 
update: {α : Sort ?u.16339} →
  {β : α → Sort ?u.16338} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update (
Sum.elim: {α : Type ?u.16345} → {β : Type ?u.16344} → {γ : Sort ?u.16343} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f: α → γ
f 
g: β → γ
g) (
inr: {α : Type ?u.16367} → {β : Type ?u.16366} → β → α ⊕ β
inr 
i: β
i) 
x: γ
x = 
Sum.elim: {α : Type ?u.16423} → {β : Type ?u.16422} → {γ : Sort ?u.16421} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim 
f: α → γ
f (
update: {α : Sort ?u.16431} →
  {β : α → Sort ?u.16430} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update 
g: β → γ
g 
i: β
i 
x: γ
x) :=
  
update_eq_iff: ∀ {α : Sort ?u.16543} {β : α → Sort ?u.16542} [inst : DecidableEq α] {a : α} {b : β a} {f g : (a : α) → β a},
  update f a b = g ↔ b = g a ∧ ∀ (x : α), x ≠ a → f x = g x
update_eq_iff.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ⟨
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.16302

inst✝¹: DecidableEq β

inst✝: DecidableEq (α ⊕ β)

f: α → γ

g: β → γ

i: β

x: γ

x = Sum.elim f (update g i x) (inr i)
Goals accomplished! 🐙
, 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.16302

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
Goals accomplished! 🐙
⟩
#align sum.update_elim_inr 
Sum.update_elim_inr: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq β] [inst_1 : DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ}
  {i : β} {x : γ}, update (Sum.elim f g) (inr i) x = Sum.elim f (update g i x)
Sum.update_elim_inr

@[simp]
theorem 
update_inl_comp_inl: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α}
  {x : γ}, update f (inl i) x ∘ inl = update (f ∘ inl) i x
update_inl_comp_inl [
DecidableEq: Sort ?u.18671 → Sort (max1?u.18671)
DecidableEq 
α: Type u
α] [
DecidableEq: Sort ?u.18680 → Sort (max1?u.18680)
DecidableEq (
Sum: Type ?u.18682 → Type ?u.18681 → Type (max?u.18682?u.18681)
Sum 
α: Type u
α 
β: Type v
β)] {
f: α ⊕ β → γ
f : 
Sum: Type ?u.18693 → Type ?u.18692 → Type (max?u.18693?u.18692)
Sum 
α: Type u
α 
β: Type v
β → 
γ: Type ?u.18665
γ} {
i: α
i : 
α: Type u
α}
    {
x: γ
x : 
γ: Type ?u.18665
γ} : 
update: {α : Sort ?u.18709} →
  {β : α → Sort ?u.18708} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update 
f: α ⊕ β → γ
f (
inl: {α : Type ?u.18763} → {β : Type ?u.18762} → α → α ⊕ β
inl 
i: α
i) 
x: γ
x ∘ 
inl: {α : Type ?u.18824} → {β : Type ?u.18823} → α → α ⊕ β
inl = 
update: {α : Sort ?u.18832} →
  {β : α → Sort ?u.18831} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update (
f: α ⊕ β → γ
f ∘ 
inl: {α : Type ?u.18852} → {β : Type ?u.18851} → α → α ⊕ β
inl) 
i: α
i 
x: γ
x :=
  
update_comp_eq_of_injective: ∀ {α : Sort ?u.18920} {α' : Sort ?u.18919} [inst : DecidableEq α] [inst_1 : DecidableEq α'] {β : Sort ?u.18921}
  (g : α' → β) {f : α → α'}, Function.Injective f → ∀ (i : α) (a : β), update g (f i) a ∘ f = update (g ∘ f) i a
update_comp_eq_of_injective 
_: ?m.18923 → ?m.18926
_ 
inl_injective: ∀ {α : Type ?u.18930} {β : Type ?u.18929}, Function.Injective inl
inl_injective 
_: ?m.18922
_ 
_: ?m.18926
_
#align sum.update_inl_comp_inl 
Sum.update_inl_comp_inl: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α}
  {x : γ}, update f (inl i) x ∘ inl = update (f ∘ inl) i x
Sum.update_inl_comp_inl

@[simp]
theorem 
update_inl_apply_inl: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ}
  {i j : α} {x : γ}, update f (inl i) x (inl j) = update (f ∘ inl) i x j
update_inl_apply_inl [
DecidableEq: Sort ?u.19216 → Sort (max1?u.19216)
DecidableEq 
α: Type u
α] [
DecidableEq: Sort ?u.19225 → Sort (max1?u.19225)
DecidableEq (
Sum: Type ?u.19227 → Type ?u.19226 → Type (max?u.19227?u.19226)
Sum 
α: Type u
α 
β: Type v
β)] {
f: α ⊕ β → γ
f : 
Sum: Type ?u.19238 → Type ?u.19237 → Type (max?u.19238?u.19237)
Sum 
α: Type u
α 
β: Type v
β → 
γ: Type ?u.19210
γ} {
i: α
i 
j: α
j : 
α: Type u
α}
    {
x: γ
x : 
γ: Type ?u.19210
γ} : 
update: {α : Sort ?u.19250} →
  {β : α → Sort ?u.19249} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update 
f: α ⊕ β → γ
f (
inl: {α : Type ?u.19262} → {β : Type ?u.19261} → α → α ⊕ β
inl 
i: α
i) 
x: γ
x (
inl: {α : Type ?u.19266} → {β : Type ?u.19265} → α → α ⊕ β
inl 
j: α
j) = 
update: {α : Sort ?u.19325} →
  {β : α → Sort ?u.19324} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update (
f: α ⊕ β → γ
f ∘ 
inl: {α : Type ?u.19345} → {β : Type ?u.19344} → α → α ⊕ β
inl) 
i: α
i 
x: γ
x 
j: α
j := 
Goals accomplished! 🐙
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.19213

inst✝¹: DecidableEq α

inst✝: DecidableEq (α ⊕ β)

f: α ⊕ β → γ

i, j: α

x: γ

update f (inl i) x (inl j) = update (f ∘ inl) i x j
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.19213

inst✝¹: DecidableEq α

inst✝: DecidableEq (α ⊕ β)

f: α ⊕ β → γ

i, j: α

x: γ

update f (inl i) x (inl j) = update (f ∘ inl) i x j
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.19213

inst✝¹: DecidableEq α

inst✝: DecidableEq (α ⊕ β)

f: α ⊕ β → γ

i, j: α

x: γ

update f (inl i) x (inl j) = (update f (inl i) x ∘ inl) j
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.19213

inst✝¹: DecidableEq α

inst✝: DecidableEq (α ⊕ β)

f: α ⊕ β → γ

i, j: α

x: γ

update f (inl i) x (inl j) = update (f ∘ inl) i x j
α: Type u

α': Type w

β: Type v

β': Type x

γ: Type u_1

δ: Type ?u.19213

inst✝¹: DecidableEq α

inst✝: DecidableEq (α ⊕ β)

f: α ⊕ β → γ

i, j: α

x: γ

update f (inl i) x (inl j) = update f (inl i) x (inl j)
Goals accomplished! 🐙

#align sum.update_inl_apply_inl 
Sum.update_inl_apply_inl: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ}
  {i j : α} {x : γ}, update f (inl i) x (inl j) = update (f ∘ inl) i x j
Sum.update_inl_apply_inl

@[simp]
theorem 
update_inl_comp_inr: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {x : γ},
  update f (inl i) x ∘ inr = f ∘ inr
update_inl_comp_inr [
DecidableEq: Sort ?u.19792 → Sort (max1?u.19792)
DecidableEq (
Sum: Type ?u.19794 → Type ?u.19793 → Type (max?u.19794?u.19793)
Sum 
α: Type u
α 
β: Type v
β)] {
f: α ⊕ β → γ
f : 
Sum: Type ?u.19805 → Type ?u.19804 → Type (max?u.19805?u.19804)
Sum 
α: Type u
α 
β: Type v
β → 
γ: Type ?u.19786
γ} {
i: α
i : 
α: Type u
α} {
x: γ
x : 
γ: Type ?u.19786
γ} :
    
update: {α : Sort ?u.19821} →
  {β : α → Sort ?u.19820} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update 
f: α ⊕ β → γ
f (
inl: {α : Type ?u.19873} → {β : Type ?u.19872} → α → α ⊕ β
inl 
i: α
i) 
x: γ
x ∘ 
inr: {α : Type ?u.19932} → {β : Type ?u.19931} → β → α ⊕ β
inr = 
f: α ⊕ β → γ
f ∘ 
inr: {α : Type ?u.19949} → {β : Type ?u.19948} → β → α ⊕ β
inr :=
  (
update_comp_eq_of_forall_ne: ∀ {α' : Sort ?u.19966} [inst : DecidableEq α'] {α : Sort ?u.19967} {β : Sort ?u.19968} (g : α' → β) {f : α → α'}
  {i : α'} (a : β), (∀ (x : α), f x ≠ i) → update g i a ∘ f = g ∘ f
update_comp_eq_of_forall_ne 
_: ?m.19969 → ?m.19972
_ 
_: ?m.19972
_) fun 
_: ?m.20049
_ ↦ 
inr_ne_inl: ∀ {α : Type ?u.20052} {β : Type ?u.20051} {a : α} {b : β}, inr b ≠ inl a
inr_ne_inl
#align sum.update_inl_comp_inr 
Sum.update_inl_comp_inr: ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {x : γ},
  update f (inl i) x ∘ inr = f ∘ inr
Sum.update_inl_comp_inr

theorem 
update_inl_apply_inr: ∀ [inst : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ}, update f (inl i) x (inr j) = f (inr j)
update_inl_apply_inr [
DecidableEq: Sort ?u.20169 → Sort (max1?u.20169)
DecidableEq (
Sum: Type ?u.20171 → Type ?u.20170 → Type (max?u.20171?u.20170)
Sum 
α: Type u
α 
β: Type v
β)] {
f: α ⊕ β → γ
f : 
Sum: Type ?u.20182 → Type ?u.20181 → Type (max?u.20182?u.20181)
Sum 
α: Type u
α 
β: Type v
β → 
γ: Type ?u.20163
γ} {
i: α
i : 
α: Type u
α} {
j: β
j : 
β: Type v
β} {
x: γ
x : 
γ: Type ?u.20163
γ} :
    
update: {α : Sort ?u.20194} →
  {β : α → Sort ?u.20193} → [inst : DecidableEq α] → ((a : α) → β a) → (a' : α) → β a' → (a : α) → β a
update 
f: α ⊕ β → γ
f (
inl: {α : Type ?u.20206} → {β : Type ?u.20205} → α → α ⊕ β
inl 
i: α
i) 
x: γ
x (
inr: