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.
```/-
Authors: Mario Carneiro, Yury G. Kudryashov

! This file was ported from Lean 3 source module data.sum.basic
! 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 uBEq 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: α ⊕ β → Propp : Sum: Type ?u.2035 → Type ?u.2034 → Type (max?u.2035?u.2034)Sum α: Type uα β: Type vβ → Prop: TypeProp} : (∀ x: ?m.2040x, p: α ⊕ β → Propp x: ?m.2040x) ↔ (∀ a: ?m.2045a, p: α ⊕ β → Propp (inl: {α : Type ?u.2049} → {β : Type ?u.2048} → α → α ⊕ βinl a: ?m.2045a)) ∧ ∀ b: ?m.2056b, p: α ⊕ β → Propp (inr: {α : Type ?u.2060} → {β : Type ?u.2059} → β → α ⊕ βinr b: ?m.2056b) :=
⟨fun h: ?m.2076h ↦ ⟨fun _: ?m.2089_ ↦ h: ?m.2076h _: α ⊕ β_, fun _: ?m.2095_ ↦ h: ?m.2076h _: α ⊕ β_⟩, 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 tSum.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: α ⊕ β → Propp : Sum: Type ?u.2295 → Type ?u.2294 → Type (max?u.2295?u.2294)Sum α: Type uα β: Type vβ → Prop: TypeProp} : (∃ x: ?m.2302x, p: α ⊕ β → Propp x: ?m.2302x) ↔ (∃ a: ?m.2309a, p: α ⊕ β → Propp (inl: {α : Type ?u.2312} → {β : Type ?u.2311} → α → α ⊕ βinl a: ?m.2309a)) ∨ ∃ b: ?m.2322b, p: α ⊕ β → Propp (inr: {α : Type ?u.2325} → {β : Type ?u.2324} → β → α ⊕ βinr b: ?m.2322b) :=
⟨ fun
| ⟨inl: {α : Type ?u.2345} → {β : Type ?u.2344} → α → α ⊕ βinl a: αa, h: p (inl a)h⟩ => Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.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 ∨ bOr.inr ⟨b: βb, h: p (inr b)h⟩,
fun
| Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.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 ∨ bOr.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 inlinl_injective : Function.Injective: {α : Sort ?u.2878} → {β : Sort ?u.2877} → (α → β) → PropFunction.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_1inl.inj
#align sum.inl_injective Sum.inl_injective: ∀ {α : Type u} {β : Type v}, Function.Injective inlSum.inl_injective

theorem inr_injective: ∀ {α : Type u} {β : Type v}, Function.Injective inrinr_injective : Function.Injective: {α : Sort ?u.2943} → {β : Sort ?u.2942} → (α → β) → PropFunction.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_1inr.inj
#align sum.inr_injective Sum.inr_injective: ∀ {α : Type u} {β : Type v}, Function.Injective inrSum.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.3011Option α: 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.3240Option β: 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} → α ⊕ β → BoolisLeft : Sum: Type ?u.3461 → Type ?u.3460 → Type (max?u.3461?u.3460)Sum α: Type uα β: Type vβ → Bool: TypeBool
| inl: {α : Type ?u.3468} → {β : Type ?u.3467} → α → α ⊕ βinl _ => true: Booltrue
| inr: {α : Type ?u.3489} → {β : Type ?u.3488} → β → α ⊕ βinr _ => false: Boolfalse
#align sum.is_left Sum.isLeft: {α : Type u} → {β : Type v} → α ⊕ β → BoolSum.isLeft

/-- Check if a sum is `inr`. -/
def isRight: α ⊕ β → BoolisRight : Sum: Type ?u.3664 → Type ?u.3663 → Type (max?u.3664?u.3663)Sum α: Type uα β: Type vβ → Bool: TypeBool
| inl: {α : Type ?u.3671} → {β : Type ?u.3670} → α → α ⊕ βinl _ => false: Boolfalse
| inr: {α : Type ?u.3692} → {β : Type ?u.3691} → β → α ⊕ βinr _ => true: Booltrue
#align sum.is_right Sum.isRight: {α : Type u} → {β : Type v} → α ⊕ β → BoolSum.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 xgetLeft_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 = arfl
@[simp] theorem getLeft_inr: ∀ {α : Type u} {β : Type v} (x : β), getLeft (inr x) = nonegetLeft_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 = arfl
@[simp] theorem getRight_inl: ∀ {α : Type u} {β : Type v} (x : α), getRight (inl x) = nonegetRight_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 = arfl
@[simp] theorem getRight_inr: ∀ {α : Type u} {β : Type v} (x : β), getRight (inr x) = some xgetRight_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 = arfl

@[simp] theorem isLeft_inl: ∀ {α : Type u} {β : Type v} (x : α), isLeft (inl x) = trueisLeft_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} → α ⊕ β → BoolisLeft = true: Booltrue := rfl: ∀ {α : Sort ?u.4287} {a : α}, a = arfl
@[simp] theorem isLeft_inr: ∀ {α : Type u} {β : Type v} (x : β), isLeft (inr x) = falseisLeft_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} → α ⊕ β → BoolisLeft = false: Boolfalse := rfl: ∀ {α : Sort ?u.4363} {a : α}, a = arfl
@[simp] theorem isRight_inl: ∀ {α : Type u} {β : Type v} (x : α), isRight (inl x) = falseisRight_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} → α ⊕ β → BoolisRight = false: Boolfalse := rfl: ∀ {α : Sort ?u.4439} {a : α}, a = arfl
@[simp] theorem isRight_inr: ∀ {α : Type u} {β : Type v} (x : β), isRight (inr x) = trueisRight_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} → α ⊕ β → BoolisRight = true: Booltrue := rfl: ∀ {α : Sort ?u.4515} {a : α}, a = arfl

@[simp] theorem getLeft_eq_none_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, getLeft x = none ↔ isRight x = truegetLeft_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} → α ⊕ β → BoolisRight := byGoals accomplished! 🐙
α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4555δ: Type ?u.4558x, y: α ⊕ βgetLeft x = none ↔ isRight x = truecases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4555δ: Type ?u.4558y: α ⊕ βval✝: αinlgetLeft (inl val✝) = none ↔ isRight (inl val✝) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4555δ: Type ?u.4558y: α ⊕ βval✝: βinrgetLeft (inr val✝) = none ↔ isRight (inr val✝) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4555δ: Type ?u.4558x, y: α ⊕ βgetLeft x = none ↔ isRight x = true<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4555δ: Type ?u.4558y: α ⊕ βval✝: αinlgetLeft (inl val✝) = none ↔ isRight (inl val✝) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4555δ: Type ?u.4558y: α ⊕ βval✝: βinrgetLeft (inr val✝) = none ↔ isRight (inr val✝) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4555δ: Type ?u.4558x, y: α ⊕ βgetLeft x = none ↔ isRight x = truesimp only [getLeft: {α : Type ?u.4779} → {β : Type ?u.4778} → α ⊕ β → Option αgetLeft, isRight: {α : Type ?u.4911} → {β : Type ?u.4910} → α ⊕ β → BoolisRight, eq_self_iff_true: ∀ {α : Sort ?u.4784} (a : α), a = a ↔ Trueeq_self_iff_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 = trueSum.getLeft_eq_none_iff

@[simp] theorem getRight_eq_none_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, getRight x = none ↔ isLeft x = truegetRight_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} → α ⊕ β → BoolisLeft := byGoals accomplished! 🐙
α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4983δ: Type ?u.4986x, y: α ⊕ βgetRight x = none ↔ isLeft x = truecases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4983δ: Type ?u.4986y: α ⊕ βval✝: αinlgetRight (inl val✝) = none ↔ isLeft (inl val✝) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4983δ: Type ?u.4986y: α ⊕ βval✝: βinrgetRight (inr val✝) = none ↔ isLeft (inr val✝) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4983δ: Type ?u.4986x, y: α ⊕ βgetRight x = none ↔ isLeft x = true<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4983δ: Type ?u.4986y: α ⊕ βval✝: αinlgetRight (inl val✝) = none ↔ isLeft (inl val✝) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4983δ: Type ?u.4986y: α ⊕ βval✝: βinrgetRight (inr val✝) = none ↔ isLeft (inr val✝) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.4983δ: Type ?u.4986x, y: α ⊕ βgetRight x = none ↔ isLeft x = truesimp only [getRight: {α : Type ?u.5207} → {β : Type ?u.5206} → α ⊕ β → Option βgetRight, isLeft: {α : Type ?u.5291} → {β : Type ?u.5290} → α ⊕ β → BoolisLeft, eq_self_iff_true: ∀ {α : Sort ?u.5293} (a : α), a = a ↔ Trueeq_self_iff_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 = trueSum.getRight_eq_none_iff

@[simp] lemma getLeft_eq_some_iff: ∀ {a : α}, getLeft x = some a ↔ x = inl agetLeft_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 := byGoals accomplished! 🐙
α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5406δ: Type ?u.5409x, y: α ⊕ βa: αgetLeft x = some a ↔ x = inl acases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5406δ: Type ?u.5409y: α ⊕ βa, val✝: αinlgetLeft (inl val✝) = some a ↔ inl val✝ = inl aα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5406δ: Type ?u.5409y: α ⊕ βa: αval✝: βinrgetLeft (inr val✝) = some a ↔ inr val✝ = inl a α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5406δ: Type ?u.5409x, y: α ⊕ βa: αgetLeft x = some a ↔ x = inl a<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5406δ: Type ?u.5409y: α ⊕ βa, val✝: αinlgetLeft (inl val✝) = some a ↔ inl val✝ = inl aα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5406δ: Type ?u.5409y: α ⊕ βa: αval✝: βinrgetLeft (inr val✝) = some a ↔ inr val✝ = inl a α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5406δ: Type ?u.5409x, y: α ⊕ βa: αgetLeft x = some a ↔ x = inl asimp only [getLeft: {α : Type ?u.5821} → {β : Type ?u.5820} → α ⊕ β → Option αgetLeft, Option.some.injEq: ∀ {α : Type ?u.5695} (val val_1 : α), (some val = some val_1) = (val = val_1)Option.some.injEq, inl.injEq: ∀ {α : Type ?u.5710} {β : Type ?u.5709} (val val_1 : α), (inl val = inl val_1) = (val = val_1)inl.injEq]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 aSum.getLeft_eq_some_iff

@[simp] lemma getRight_eq_some_iff: ∀ {b : β}, getRight x = some b ↔ x = inr bgetRight_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 := byGoals accomplished! 🐙
α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5926δ: Type ?u.5929x, y: α ⊕ βb: βgetRight x = some b ↔ x = inr bcases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5926δ: Type ?u.5929y: α ⊕ βb: βval✝: αinlgetRight (inl val✝) = some b ↔ inl val✝ = inr bα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5926δ: Type ?u.5929y: α ⊕ βb, val✝: βinrgetRight (inr val✝) = some b ↔ inr val✝ = inr b α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5926δ: Type ?u.5929x, y: α ⊕ βb: βgetRight x = some b ↔ x = inr b<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5926δ: Type ?u.5929y: α ⊕ βb: βval✝: αinlgetRight (inl val✝) = some b ↔ inl val✝ = inr bα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5926δ: Type ?u.5929y: α ⊕ βb, val✝: βinrgetRight (inr val✝) = some b ↔ inr val✝ = inr b α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.5926δ: Type ?u.5929x, y: α ⊕ βb: βgetRight x = some b ↔ x = inr bsimp only [getRight: {α : Type ?u.6213} → {β : Type ?u.6212} → α ⊕ β → Option βgetRight, Option.some.injEq: ∀ {α : Type ?u.6215} (val val_1 : α), (some val = some val_1) = (val = val_1)Option.some.injEq, inr.injEq: ∀ {α : Type ?u.6230} {β : Type ?u.6229} (val val_1 : β), (inr val = inr val_1) = (val = val_1)inr.injEq]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 bSum.getRight_eq_some_iff

@[simp]
theorem not_isLeft: ∀ {α : Type u} {β : Type v} (x : α ⊕ β), (!isLeft x) = isRight xnot_isLeft (x: α ⊕ βx : Sum: Type ?u.6466 → Type ?u.6465 → Type (max?u.6466?u.6465)Sum α: Type uα β: Type vβ) : not: Bool → Boolnot x: α ⊕ βx.isLeft: {α : Type ?u.6471} → {β : Type ?u.6470} → α ⊕ β → BoolisLeft = x: α ⊕ βx.isRight: {α : Type ?u.6480} → {β : Type ?u.6479} → α ⊕ β → BoolisRight := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6451δ: Type ?u.6454x✝, y, x: α ⊕ β(!isLeft x) = isRight xcases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6451δ: Type ?u.6454x, y: α ⊕ βval✝: αinl(!isLeft (inl val✝)) = isRight (inl val✝)α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6451δ: Type ?u.6454x, y: α ⊕ βval✝: βinr(!isLeft (inr val✝)) = isRight (inr val✝) α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6451δ: Type ?u.6454x✝, y, x: α ⊕ β(!isLeft x) = isRight x<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6451δ: Type ?u.6454x, y: α ⊕ βval✝: αinl(!isLeft (inl val✝)) = isRight (inl val✝)α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6451δ: Type ?u.6454x, y: α ⊕ βval✝: βinr(!isLeft (inr val✝)) = isRight (inr val✝) α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6451δ: Type ?u.6454x✝, y, x: α ⊕ β(!isLeft x) = isRight xrflGoals accomplished! 🐙
#align sum.bnot_is_left Sum.not_isLeft: ∀ {α : Type u} {β : Type v} (x : α ⊕ β), (!isLeft x) = isRight xSum.not_isLeft

@[simp]
theorem isLeft_eq_false: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isLeft x = false ↔ isRight x = trueisLeft_eq_false : x: α ⊕ βx.isLeft: {α : Type ?u.6631} → {β : Type ?u.6630} → α ⊕ β → BoolisLeft = false: Boolfalse ↔ x: α ⊕ βx.isRight: {α : Type ?u.6641} → {β : Type ?u.6640} → α ⊕ β → BoolisRight := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6615δ: Type ?u.6618x, y: α ⊕ βisLeft x = false ↔ isRight x = truecases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6615δ: Type ?u.6618y: α ⊕ βval✝: αinlisLeft (inl val✝) = false ↔ isRight (inl val✝) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6615δ: Type ?u.6618y: α ⊕ βval✝: βinrisLeft (inr val✝) = false ↔ isRight (inr val✝) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6615δ: Type ?u.6618x, y: α ⊕ βisLeft x = false ↔ isRight x = true<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6615δ: Type ?u.6618y: α ⊕ βval✝: αinlisLeft (inl val✝) = false ↔ isRight (inl val✝) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6615δ: Type ?u.6618y: α ⊕ βval✝: βinrisLeft (inr val✝) = false ↔ isRight (inr val✝) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6615δ: Type ?u.6618x, y: α ⊕ βisLeft x = false ↔ isRight x = truesimpGoals accomplished! 🐙
#align sum.is_left_eq_ff Sum.isLeft_eq_false: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isLeft x = false ↔ isRight x = trueSum.isLeft_eq_false

theorem Not_isLeft: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, ¬isLeft x = true ↔ isRight x = trueNot_isLeft : ¬x: α ⊕ βx.isLeft: {α : Type ?u.6997} → {β : Type ?u.6996} → α ⊕ β → BoolisLeft ↔ x: α ⊕ βx.isRight: {α : Type ?u.7087} → {β : Type ?u.7086} → α ⊕ β → BoolisRight := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.6982δ: Type ?u.6985x, y: α ⊕ β¬isLeft x = true ↔ isRight x = truesimpGoals accomplished! 🐙
#align sum.not_is_left Sum.Not_isLeft: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, ¬isLeft x = true ↔ isRight x = trueSum.Not_isLeft

@[simp]
theorem not_isRight: ∀ {α : Type u} {β : Type v} (x : α ⊕ β), (!decide (isRight x = isLeft x)) = truenot_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} → α ⊕ β → BoolisRight = x: α ⊕ βx.isLeft: {α : Type ?u.7277} → {β : Type ?u.7276} → α ⊕ β → BoolisLeft := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7248δ: Type ?u.7251x✝, y, x: α ⊕ β(!decide (isRight x = isLeft x)) = truecases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7248δ: Type ?u.7251x, y: α ⊕ βval✝: αinl(!decide (isRight (inl val✝) = isLeft (inl val✝))) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7248δ: Type ?u.7251x, y: α ⊕ βval✝: βinr(!decide (isRight (inr val✝) = isLeft (inr val✝))) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7248δ: Type ?u.7251x✝, y, x: α ⊕ β(!decide (isRight x = isLeft x)) = true<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7248δ: Type ?u.7251x, y: α ⊕ βval✝: αinl(!decide (isRight (inl val✝) = isLeft (inl val✝))) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7248δ: Type ?u.7251x, y: α ⊕ βval✝: βinr(!decide (isRight (inr val✝) = isLeft (inr val✝))) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7248δ: Type ?u.7251x✝, y, x: α ⊕ β(!decide (isRight x = isLeft x)) = truerflGoals accomplished! 🐙
#align sum.bnot_is_right Sum.not_isRight: ∀ {α : Type u} {β : Type v} (x : α ⊕ β), (!decide (isRight x = isLeft x)) = trueSum.not_isRight

@[simp]
theorem isRight_eq_false: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isRight x = false ↔ isLeft x = trueisRight_eq_false : x: α ⊕ βx.isRight: {α : Type ?u.7496} → {β : Type ?u.7495} → α ⊕ β → BoolisRight = false: Boolfalse ↔ x: α ⊕ βx.isLeft: {α : Type ?u.7506} → {β : Type ?u.7505} → α ⊕ β → BoolisLeft := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7480δ: Type ?u.7483x, y: α ⊕ βisRight x = false ↔ isLeft x = truecases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7480δ: Type ?u.7483y: α ⊕ βval✝: αinlisRight (inl val✝) = false ↔ isLeft (inl val✝) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7480δ: Type ?u.7483y: α ⊕ βval✝: βinrisRight (inr val✝) = false ↔ isLeft (inr val✝) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7480δ: Type ?u.7483x, y: α ⊕ βisRight x = false ↔ isLeft x = true<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7480δ: Type ?u.7483y: α ⊕ βval✝: αinlisRight (inl val✝) = false ↔ isLeft (inl val✝) = trueα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7480δ: Type ?u.7483y: α ⊕ βval✝: βinrisRight (inr val✝) = false ↔ isLeft (inr val✝) = true α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7480δ: Type ?u.7483x, y: α ⊕ βisRight x = false ↔ isLeft x = truesimpGoals accomplished! 🐙
#align sum.is_right_eq_ff Sum.isRight_eq_false: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isRight x = false ↔ isLeft x = trueSum.isRight_eq_false

theorem Not_isRight: ¬isRight x = true ↔ isLeft x = trueNot_isRight : ¬x: α ⊕ βx.isRight: {α : Type ?u.7862} → {β : Type ?u.7861} → α ⊕ β → BoolisRight ↔ x: α ⊕ βx.isLeft: {α : Type ?u.7952} → {β : Type ?u.7951} → α ⊕ β → BoolisLeft := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.7847δ: Type ?u.7850x, y: α ⊕ β¬isRight x = true ↔ isLeft x = truesimpGoals accomplished! 🐙
#align sum.not_is_right Sum.Not_isRight: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, ¬isRight x = true ↔ isLeft x = trueSum.Not_isRight

theorem isLeft_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isLeft x = true ↔ ∃ y, x = inl yisLeft_iff : x: α ⊕ βx.isLeft: {α : Type ?u.8128} → {β : Type ?u.8127} → α ⊕ β → BoolisLeft ↔ ∃ y: ?m.8220y, x: α ⊕ βx = Sum.inl: {α : Type ?u.8224} → {β : Type ?u.8223} → α → α ⊕ βSum.inl y: ?m.8220y := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8113δ: Type ?u.8116x, y: α ⊕ βisLeft x = true ↔ ∃ y, x = inl ycases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8113δ: Type ?u.8116y: α ⊕ βval✝: αinlisLeft (inl val✝) = true ↔ ∃ y, inl val✝ = inl yα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8113δ: Type ?u.8116y: α ⊕ βval✝: βinrisLeft (inr val✝) = true ↔ ∃ y, inr val✝ = inl y α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8113δ: Type ?u.8116x, y: α ⊕ βisLeft x = true ↔ ∃ y, x = inl y<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8113δ: Type ?u.8116y: α ⊕ βval✝: αinlisLeft (inl val✝) = true ↔ ∃ y, inl val✝ = inl yα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8113δ: Type ?u.8116y: α ⊕ βval✝: βinrisLeft (inr val✝) = true ↔ ∃ y, inr val✝ = inl y α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8113δ: Type ?u.8116x, y: α ⊕ βisLeft x = true ↔ ∃ y, x = inl ysimpGoals accomplished! 🐙
#align sum.is_left_iff Sum.isLeft_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isLeft x = true ↔ ∃ y, x = inl ySum.isLeft_iff

theorem isRight_iff: isRight x = true ↔ ∃ y, x = inr yisRight_iff : x: α ⊕ βx.isRight: {α : Type ?u.8813} → {β : Type ?u.8812} → α ⊕ β → BoolisRight ↔ ∃ y: ?m.8905y, x: α ⊕ βx = Sum.inr: {α : Type ?u.8909} → {β : Type ?u.8908} → β → α ⊕ βSum.inr y: ?m.8905y := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8798δ: Type ?u.8801x, y: α ⊕ βisRight x = true ↔ ∃ y, x = inr ycases x: α ⊕ βxα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8798δ: Type ?u.8801y: α ⊕ βval✝: αinlisRight (inl val✝) = true ↔ ∃ y, inl val✝ = inr yα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8798δ: Type ?u.8801y: α ⊕ βval✝: βinrisRight (inr val✝) = true ↔ ∃ y, inr val✝ = inr y α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8798δ: Type ?u.8801x, y: α ⊕ βisRight x = true ↔ ∃ y, x = inr y<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8798δ: Type ?u.8801y: α ⊕ βval✝: αinlisRight (inl val✝) = true ↔ ∃ y, inl val✝ = inr yα: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8798δ: Type ?u.8801y: α ⊕ βval✝: βinrisRight (inr val✝) = true ↔ ∃ y, inr val✝ = inr y α: Type uα': Type wβ: Type vβ': Type xγ: Type ?u.8798δ: Type ?u.8801x, y: α ⊕ βisRight x = true ↔ ∃ y, x = inr ysimpGoals accomplished! 🐙
#align sum.is_right_iff Sum.isRight_iff: ∀ {α : Type u} {β : Type v} {x : α ⊕ β}, isRight x = true ↔ ∃ y, x = inr ySum.isRight_iff

end get

theorem inl.inj_iff: ∀ {α : Type u} {β : Type v} {a b : α}, inl a = inl b ↔ a = binl.inj_iff {a: ?m.9489a b: αb} : (inl: {α : Type ?u.9500} → {β : Type ?u.9499} → α → α ⊕ βinl a: ?m.9489a : 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.9492b ↔ a: ?m.9489a = b: ?m.9492b :=
⟨inl.inj: ∀ {α : Type ?u.9554} {β : Type ?u.9553} {val val_1 : α}, inl val = inl val_1 → val = val_1inl.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 = bSum.inl.inj_iff

theorem inr.inj_iff: ∀ {α : Type u} {β : Type v} {a b : β}, inr a = inr b ↔ a = binr.inj_iff {a: βa b: ?m.9604b} : (inr: {α : Type ?u.9612} → {β : Type ?u.9611} → β → α ⊕ βinr a: ?m.9601a : 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.9604b ↔ a: ?m.9601a = b: ?m.9604b :=
⟨inr.inj: ∀ {α : Type ?u.9666} {β : Type ?u.9665} {val val_1 : β}, inr val = inr val_1 → val = val_1inr.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 = bSum.inr.inj_iff

theorem inl_ne_inr: ∀ {a : α} {b : β}, inl a ≠ inr binl_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 → Falsefunfun.: inl a = inr b → False.
#align sum.inl_ne_inr Sum.inl_ne_inr: ∀ {α : Type u} {β : Type v} {a : α} {b : β}, inl a ≠ inr bSum.inl_ne_inr

theorem inr_ne_inl: ∀ {a : α} {b : β}, inr b ≠ inl ainr_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 → Falsefunfun.: inr b = inl a → False.
#align sum.inr_ne_inl Sum.inr_ne_inl: ∀ {α : Type u} {β : Type v} {a : α} {b : β}, inr b ≠ inl aSum.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.9963SortSort _: 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.9991x ↦ Sum.casesOn: {α : Type ?u.9994} →
{β : Type ?u.9993} →
{motive : α ⊕ β → Sort ?u.9995} →
(t : α ⊕ β) → ((val : α) → motive (inl val)) → ((val : β) → motive (inr val)) → motive tSum.casesOn x: ?m.9991x 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 xelim_inl {α: Sort ?u.10166α β: Type u_2β γ: Sort ?u.10172γ : Sort _: Type ?u.10166SortSort _: 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 = arfl
#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 xSum.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 xelim_inr {α: Type u_1α β: Sort ?u.10267β γ: Sort ?u.10270γ : Sort _: Type ?u.10264SortSort _: 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 = arfl
#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 xSum.elim_inr

@[simp]
theorem elim_comp_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ), Sum.elim f g ∘ inl = felim_comp_inl {α: Type u_1α β: Sort ?u.10365β γ: Sort ?u.10368γ : Sort _: Type ?u.10368SortSort _: 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 = arfl
#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 = fSum.elim_comp_inl

@[simp]
theorem elim_comp_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ), Sum.elim f g ∘ inr = gelim_comp_inr {α: Type u_1α β: Sort ?u.10486β γ: Sort u_3γ : Sort _: Type ?u.10489SortSort _: 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 = arfl
#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 = gSum.elim_comp_inr

@[simp]
theorem elim_inl_inr: ∀ {α : Type u_1} {β : Type u_2}, Sum.elim inl inr = idelim_inl_inr {α: Sort ?u.10604α β: Sort ?u.10607β : Sort _: Type ?u.10604SortSort _: 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 = gfunext fun x: ?m.10691x ↦ Sum.casesOn: ∀ {α : Type ?u.10694} {β : Type ?u.10693} {motive : α ⊕ β → Sort ?u.10695} (t : α ⊕ β),
(∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → motive tSum.casesOn x: ?m.10691x (fun _: ?m.10738_ ↦ rfl: ∀ {α : Sort ?u.10740} {a : α}, a = arfl) fun _: ?m.10746_ ↦ rfl: ∀ {α : Sort ?u.10748} {a : α}, a = arfl
#align sum.elim_inl_inr Sum.elim_inl_inr: ∀ {α : Type u_1} {β : Type u_2}, Sum.elim inl inr = idSum.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.10795SortSort _: 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 = gfunext fun x: ?m.10913x ↦ Sum.casesOn: ∀ {α : Type ?u.10916} {β : Type ?u.10915} {motive : α ⊕ β → Sort ?u.10917} (t : α ⊕ β),
(∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → motive tSum.casesOn x: ?m.10913x (fun _: ?m.10963_ ↦ rfl: ∀ {α : Sort ?u.10965} {a : α}, a = arfl) fun _: ?m.10972_ ↦ rfl: ∀ {α : Sort ?u.10974} {a : α}, a = arfl
#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) = felim_comp_inl_inr {α: Sort ?u.11009α β: Sort ?u.11012β γ: Sort u_3γ : Sort _: Type ?u.11009SortSort _: 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 = gfunext fun x: ?m.11099x ↦ Sum.casesOn: ∀ {α : Type ?u.11102} {β : Type ?u.11101} {motive : α ⊕ β → Sort ?u.11103} (t : α ⊕ β),
(∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → motive tSum.casesOn x: ?m.11099x (fun _: ?m.11149_ ↦ rfl: ∀ {α : Sort ?u.11151} {a : α}, a = arfl) fun _: ?m.11157_ ↦ rfl: ∀ {α : Sort ?u.11159} {a : α}, a = arfl
#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) = fSum.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 = arfl
#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 = arfl
#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) xmap_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 = arfl
| inr: {α : Type ?u.11938} → {β : Type ?u.11937} → β → α ⊕ βinr _ => rfl: ∀ {α : Sort ?u.11956} {a : α}, a = arfl
#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) xSum.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 = gfunext <| 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) xmap_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 = idmap_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 = gfunext fun x: ?m.12464x ↦ Sum.recOn: ∀ {α : Type ?u.12467} {β : Type ?u.12466} {motive : α ⊕ β → Sort ?u.12468} (t : α ⊕ β),
(∀ (val : α), motive (inl val)) → (∀ (val : β), motive (inr val)) → motive tSum.recOn x: ?m.12464x (fun _: ?m.12511_ ↦ rfl: ∀ {α : Sort ?u.12513} {a : α}, a = arfl) fun _: ?m.12522_ ↦ rfl: ∀ {α : Sort ?u.12524} {a : α}, a = arfl
#align sum.map_id_id Sum.map_id_id: ∀ (α : Type u_1) (β : Type u_2), Sum.map id id = idSum.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₁) xelim_map {α: Type u_1α β: Sort ?u.12571β γ: Type u_3γ δ: Sort ?u.12577δ ε: Sort u_5ε : Sort _: Type ?u.12580SortSort _: 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.12599x) = Sum.elim: {α : Type ?u.12635} → {β : Type ?u.12634} → {γ : Sort ?u.12633} → (α → γ) → (β → γ) → α ⊕ β → γSum.elim (f₂: β → εf₂ ∘ f₁: α → βf₁) (g₂: δ → εg₂ ∘ g₁: γ → δg₁) x: ?m.12599x := byGoals 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_5f₁: α → βf₂: β → εg₁: γ → δg₂: δ → εx: α ⊕ γSum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) xcases x: α ⊕ γ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_5f₁: α → βf₂: β → εg₁: γ → δg₂: δ → εval✝: αinlSum.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_5f₁: α → βf₂: β → εg₁: γ → δg₂: δ → εval✝: γinrSum.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_5f₁: α → β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_5f₁: α → βf₂: β → εg₁: γ → δg₂: δ → εval✝: αinlSum.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_5f₁: α → βf₂: β → εg₁: γ → δg₂: δ → εval✝: γinrSum.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_5f₁: α → βf₂: β → εg₁: γ → δg₂: δ → εx: α ⊕ γSum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) xrflGoals 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₁) xSum.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.12817SortSort _: 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 = gfunext \$ 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₁) xelim_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 xisLeft_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} → α ⊕ β → BoolisLeft (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} → α ⊕ β → BoolisLeft x: α ⊕ γx :=
byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δx: α ⊕ γisLeft (Sum.map f g x) = isLeft xcases x: α ⊕ γxα: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: αinlisLeft (Sum.map f g (inl val✝)) = isLeft (inl val✝)α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: γinrisLeft (Sum.map f g (inr val✝)) = isLeft (inr val✝) α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δx: α ⊕ γisLeft (Sum.map f g x) = isLeft x<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: αinlisLeft (Sum.map f g (inl val✝)) = isLeft (inl val✝)α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: γinrisLeft (Sum.map f g (inr val✝)) = isLeft (inr val✝) α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δx: α ⊕ γisLeft (Sum.map f g x) = isLeft xrflGoals 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 xSum.isLeft_map

@[simp]
theorem isRight_map: ∀ (f : α → β) (g : γ → δ) (x : α ⊕ γ), isRight (Sum.map f g x) = isRight xisRight_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} → α ⊕ β → BoolisRight (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} → α ⊕ β → BoolisRight x: α ⊕ γx :=
byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δx: α ⊕ γisRight (Sum.map f g x) = isRight xcases x: α ⊕ γxα: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: αinlisRight (Sum.map f g (inl val✝)) = isRight (inl val✝)α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: γinrisRight (Sum.map f g (inr val✝)) = isRight (inr val✝) α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δx: α ⊕ γisRight (Sum.map f g x) = isRight x<;>α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: αinlisRight (Sum.map f g (inl val✝)) = isRight (inl val✝)α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: γinrisRight (Sum.map f g (inr val✝)) = isRight (inr val✝) α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δx: α ⊕ γisRight (Sum.map f g x) = isRight xrflGoals 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 xSum.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 :=
byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δx: α ⊕ γgetLeft (Sum.map f g x) = Option.map f (getLeft x)cases x: α ⊕ γxα: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: αinlgetLeft (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_2f: α → βg: γ → δval✝: γinrgetLeft (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_2f: α → β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_2f: α → βg: γ → δval✝: αinlgetLeft (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_2f: α → βg: γ → δval✝: γinrgetLeft (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_2f: α → βg: γ → δx: α ⊕ γgetLeft (Sum.map f g x) = Option.map f (getLeft x)rflGoals 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 := byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δx: α ⊕ γgetRight (Sum.map f g x) = Option.map g (getRight x)cases x: α ⊕ γxα: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type u_2f: α → βg: γ → δval✝: αinlgetRight (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_2f: α → βg: γ → δval✝: γinrgetRight (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_2f: α → β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_2f: α → βg: γ → δval✝: αinlgetRight (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_2f: α → βg: γ → δval✝: γinrgetRight (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_2f: α → βg: γ → δx: α ⊕ γgetRight (Sum.map f g x) = Option.map g (getRight x)rflGoals 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) gupdate_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 : α) → β aupdate (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 : α) → β aupdate 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 xupdate_eq_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type ?u.13935inst✝¹: DecidableEq αinst✝: DecidableEq (α ⊕ β)f: α → γg: β → γi: αx: γx = Sum.elim (update f i x) g (inl i)simpGoals accomplished! 🐙, byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type ?u.13935inst✝¹: 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_1simp (config := { contextual := true: Booltrue })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) gSum.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 : α) → β aupdate (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 : α) → β aupdate 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 xupdate_eq_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type ?u.16302inst✝¹: DecidableEq βinst✝: DecidableEq (α ⊕ β)f: α → γg: β → γi: βx: γx = Sum.elim f (update g i x) (inr i)simpGoals accomplished! 🐙, byGoals accomplished! 🐙 α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type ?u.16302inst✝¹: 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_1simp (config := { contextual := true: Booltrue })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 xupdate_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 : α) → β aupdate 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 : α) → β aupdate (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 aupdate_comp_eq_of_injective _: ?m.18923 → ?m.18926_ inl_injective: ∀ {α : Type ?u.18930} {β : Type ?u.18929}, Function.Injective inlinl_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 xSum.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 jupdate_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 : α) → β aupdate 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 : α) → β aupdate (f: α ⊕ β → γf ∘ inl: {α : Type ?u.19345} → {β : Type ?u.19344} → α → α ⊕ βinl) i: αi x: γx j: αj := byGoals accomplished! 🐙
α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type ?u.19213inst✝¹: DecidableEq αinst✝: DecidableEq (α ⊕ β)f: α ⊕ β → γi, j: αx: γupdate f (inl i) x (inl j) = update (f ∘ inl) i x jrw [α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type ?u.19213inst✝¹: DecidableEq αinst✝: DecidableEq (α ⊕ β)f: α ⊕ β → γi, j: αx: γupdate f (inl i) x (inl j) = update (f ∘ inl) i x j← update_inl_comp_inl: ∀ {α : Type ?u.19413} {β : Type ?u.19412} {γ : Type ?u.19414} [inst : DecidableEq α] [inst_1 : DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ} {i : α} {x : γ}, update f (inl i) x ∘ inl = update (f ∘ inl) i xupdate_inl_comp_inl,α: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type ?u.19213inst✝¹: 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.19213inst✝¹: DecidableEq αinst✝: DecidableEq (α ⊕ β)f: α ⊕ β → γi, j: αx: γupdate f (inl i) x (inl j) = update (f ∘ inl) i x jFunction.comp_apply: ∀ {β : Sort ?u.19676} {δ : Sort ?u.19677} {α : Sort ?u.19678} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)Function.comp_applyα: Type uα': Type wβ: Type vβ': Type xγ: Type u_1δ: Type ?u.19213inst✝¹: 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 jSum.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 ∘ inrupdate_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 : α) → β aupdate 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 ∘ fupdate_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 ainr_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 ∘ inrSum.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 : α) → β aupdate f: α ⊕ β → γf (inl: {α : Type ?u.20206} → {β : Type ?u.20205} → α → α ⊕ βinl i: αi) x: γx (inr: ```