doc-next-gen

Init.Data.Sum.Lemmas

Module docstring

{"# Disjoint union of types

Theorems about the definitions introduced in Init.Data.Sum.Basic. ","### Sum.elim ","### Sum.map ","### Sum.swap "}

Sum.forall theorem
{p : α ⊕ β → Prop} : (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b)
Full source 
protected theorem «forall» {p : α ⊕ β → Prop} :
    (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
  ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨h₁, h₂⟩ => Sum.rec h₁ h₂⟩
Universal Quantifier over Disjoint Union Decomposes into Conjunction
Informal description
For any predicate $p$ defined on the disjoint union $\alpha \oplus \beta$, the statement that $p(x)$ holds for all $x \in \alpha \oplus \beta$ is equivalent to the conjunction of the statements that $p(\text{inl}(a))$ holds for all $a \in \alpha$ and $p(\text{inr}(b))$ holds for all $b \in \beta$. In other words: \[ (\forall x \in \alpha \oplus \beta, p(x)) \leftrightarrow (\forall a \in \alpha, p(\text{inl}(a))) \land (\forall b \in \beta, p(\text{inr}(b))) \]
Sum.exists theorem
{p : α ⊕ β → Prop} : (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b)
Full source 
protected theorem «exists» {p : α ⊕ β → Prop} :
    (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
  ⟨ fun
    | ⟨inl a, h⟩ => Or.inl ⟨a, h⟩
    | ⟨inr b, h⟩ => Or.inr ⟨b, h⟩,
    fun
    | Or.inl ⟨a, h⟩ => ⟨inl a, h⟩
    | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩
Existential Quantifier over Disjoint Union Decomposes into Disjunction
Informal description
For any predicate $p$ defined on the disjoint union $\alpha \oplus \beta$, the existence of an element $x \in \alpha \oplus \beta$ satisfying $p(x)$ is equivalent to the existence of an element $a \in \alpha$ satisfying $p(\text{inl}(a))$ or the existence of an element $b \in \beta$ satisfying $p(\text{inr}(b))$. In other words: \[ (\exists x \in \alpha \oplus \beta, p(x)) \leftrightarrow (\exists a \in \alpha, p(\text{inl}(a))) \lor (\exists b \in \beta, p(\text{inr}(b))) \]
Sum.forall_sum theorem
{γ : α ⊕ β → Sort _} {p : (∀ ab, γ ab) → Prop} : (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb))
Full source 
theorem forall_sum {γ : α ⊕ β → Sort _} {p : (∀ ab, γ ab) → Prop} :
    (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) := by
  refine ⟨fun h fa fb => h _, fun h fab => ?_⟩
  have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
    apply funext
    rintro (_ | _) <;> rfl
  rw [h1]; exact h _ _
Universal Quantifier over Dependent Functions on Disjoint Union Decomposes via Sum Recursion
Informal description
For any family of types $\gamma$ indexed by the disjoint union $\alpha \oplus \beta$ and any predicate $p$ on dependent functions $\forall ab, \gamma(ab)$, the statement that $p$ holds for all such functions is equivalent to $p$ holding for all functions constructed via the sum recursion operator $\text{Sum.rec}$ from pairs of functions $f_a : \forall a, \gamma(\text{inl}(a))$ and $f_b : \forall b, \gamma(\text{inr}(b))$. In other words: \[ (\forall f : \forall ab, \gamma(ab), p(f)) \leftrightarrow (\forall f_a f_b, p(\text{Sum.rec}(f_a, f_b))) \]
Sum.inl_getLeft theorem
: ∀ (x : α ⊕ β) (h : x.isLeft), inl (x.getLeft h) = x
Full source 
@[simp] theorem inl_getLeft : ∀ (x : α ⊕ β) (h : x.isLeft), inl (x.getLeft h) = x
  | inl _, _ => rfl
Left Injection Equals Original Element in Disjoint Union
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$ and a proof $h$ that $x$ is of the form $\text{inl}(a)$, the left injection of the extracted element $\text{inl}(x.\text{getLeft}\ h)$ equals $x$.
Sum.inr_getRight theorem
: ∀ (x : α ⊕ β) (h : x.isRight), inr (x.getRight h) = x
Full source 
@[simp] theorem inr_getRight : ∀ (x : α ⊕ β) (h : x.isRight), inr (x.getRight h) = x
  | inr _, _ => rfl
Right Injection Equals Original Element in Disjoint Union
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$ and a proof $h$ that $x$ is of the form $\text{inr}(b)$, the right injection of the extracted element $\text{inr}(x.\text{getRight}\ h)$ equals $x$.
Sum.getLeft?_eq_none_iff theorem
{x : α ⊕ β} : x.getLeft? = none ↔ x.isRight
Full source 
@[simp] theorem getLeft?_eq_none_iff {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight := by
  cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]
Left Component is None if and only if Element is Right Injection in Disjoint Union
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the left component of $x$ as an optional value is `none` if and only if $x$ is a right injection (i.e., of the form $\text{inr}(b)$ for some $b \in \beta$).
Sum.getRight?_eq_none_iff theorem
{x : α ⊕ β} : x.getRight? = none ↔ x.isLeft
Full source 
@[simp] theorem getRight?_eq_none_iff {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft := by
  cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]
Right Component is None if and only if Element is Left Injection in Disjoint Union
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the right component of $x$ as an optional value is `none` if and only if $x$ is a left injection (i.e., of the form $\text{inl}(a)$ for some $a \in \alpha$).
Sum.getLeft_eq_iff theorem
(h : x.isLeft) : x.getLeft h = a ↔ x = inl a
Full source 
@[simp] theorem getLeft_eq_iff (h : x.isLeft) : x.getLeft h = a ↔ x = inl a := by
  cases x <;> simp at h ⊢
Left Component Extraction Characterization in Disjoint Union
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$ and a proof $h$ that $x$ is a left injection (i.e., $x.\text{isLeft}$ holds), the extracted left component $\text{getLeft}\ x\ h$ equals $a$ if and only if $x$ is equal to the left injection $\text{inl}(a)$.
Sum.getRight_eq_iff theorem
(h : x.isRight) : x.getRight h = b ↔ x = inr b
Full source 
@[simp] theorem getRight_eq_iff (h : x.isRight) : x.getRight h = b ↔ x = inr b := by
  cases x <;> simp at h ⊢
Right Component Extraction Equivalence in Disjoint Union
Informal description
For an element $x$ of the disjoint union $\alpha \oplus \beta$ and a proof $h$ that $x$ is of the form $\text{inr}(b)$, the extracted right component $\text{getRight}\ x\ h$ equals $b$ if and only if $x$ is equal to $\text{inr}(b)$.
Sum.getLeft?_eq_some_iff theorem
: x.getLeft? = some a ↔ x = inl a
Full source 
@[simp] theorem getLeft?_eq_some_iff : x.getLeft? = some a ↔ x = inl a := by
  cases x <;> simp only [getLeft?, Option.some.injEq, inl.injEq, reduceCtorEq]
Equivalence: $\text{getLeft?}(x) = \text{some}(a) \leftrightarrow x = \text{inl}(a)$
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the optional left component `x.getLeft?` equals `some a` if and only if $x$ is of the form $\text{inl}(a)$.
Sum.getRight?_eq_some_iff theorem
: x.getRight? = some b ↔ x = inr b
Full source 
@[simp] theorem getRight?_eq_some_iff : x.getRight? = some b ↔ x = inr b := by
  cases x <;> simp only [getRight?, Option.some.injEq, inr.injEq, reduceCtorEq]
Right Component Extraction Yields Some if and only if Element is Right Injection
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the right component extraction function $\text{getRight?}$ returns $\text{some}(b)$ if and only if $x$ is the right injection $\text{inr}(b)$.
Sum.bnot_isLeft theorem
(x : α ⊕ β) : !x.isLeft = x.isRight
Full source 
@[simp] theorem bnot_isLeft (x : α ⊕ β) : !x.isLeft = x.isRight := by cases x <;> rfl
Negation of Left Injection Check Equals Right Injection Check in Disjoint Union
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the negation of the left injection check equals the right injection check, i.e., $\neg(\text{isLeft}(x)) = \text{isRight}(x)$.
Sum.isLeft_eq_false theorem
{x : α ⊕ β} : x.isLeft = false ↔ x.isRight
Full source 
@[simp] theorem isLeft_eq_false {x : α ⊕ β} : x.isLeft = false ↔ x.isRight := by cases x <;> simp
Left Injection Check is False if and only if Right Injection Check is True
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the predicate `x.isLeft` evaluates to `false` if and only if `x.isRight` evaluates to `true`. In other words, $x$ is not a left injection if and only if it is a right injection.
Sum.not_isLeft theorem
{x : α ⊕ β} : ¬x.isLeft ↔ x.isRight
Full source 
theorem not_isLeft {x : α ⊕ β} : ¬x.isLeft¬x.isLeft ↔ x.isRight := by simp
Negation of Left Injection in Disjoint Union is Right Injection
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the negation of `x.isLeft` is equivalent to `x.isRight`. In other words, $x$ is not a left injection if and only if it is a right injection.
Sum.bnot_isRight theorem
(x : α ⊕ β) : !x.isRight = x.isLeft
Full source 
@[simp] theorem bnot_isRight (x : α ⊕ β) : !x.isRight = x.isLeft := by cases x <;> rfl
Negation of Right Injection Check Equals Left Injection Check in Disjoint Union
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the negation of the right injection check `x.isRight` equals the left injection check `x.isLeft`. In other words, $\neg(\text{isRight}(x)) = \text{isLeft}(x)$.
Sum.isRight_eq_false theorem
{x : α ⊕ β} : x.isRight = false ↔ x.isLeft
Full source 
@[simp] theorem isRight_eq_false {x : α ⊕ β} : x.isRight = false ↔ x.isLeft := by cases x <;> simp
Right Injection Check Equals False if and only if Left Injection Holds
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the boolean check `x.isRight` equals `false` if and only if `x.isLeft` holds. In other words, $x$ is not a right injection if and only if it is a left injection.
Sum.not_isRight theorem
{x : α ⊕ β} : ¬x.isRight ↔ x.isLeft
Full source 
theorem not_isRight {x : α ⊕ β} : ¬x.isRight¬x.isRight ↔ x.isLeft := by simp
Negation of Right Injection in Disjoint Union is Left Injection
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the negation of `x.isRight` is equivalent to `x.isLeft`. In other words, $x$ is not a right injection if and only if it is a left injection.
Sum.isLeft_iff theorem
: x.isLeft ↔ ∃ y, x = Sum.inl y
Full source 
theorem isLeft_iff : x.isLeft ↔ ∃ y, x = Sum.inl y := by cases x <;> simp
Left Injection Check is Equivalent to Existence of Preimage in First Component
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the boolean check `x.isLeft` is true if and only if there exists an element $y \in \alpha$ such that $x = \text{inl}(y)$.
Sum.isRight_iff theorem
: x.isRight ↔ ∃ y, x = Sum.inr y
Full source 
theorem isRight_iff : x.isRight ↔ ∃ y, x = Sum.inr y := by cases x <;> simp
Characterization of Right Injection in Disjoint Union
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the predicate `x.isRight` holds if and only if there exists an element $y \in \beta$ such that $x = \text{inr}(y)$.
Sum.inl.inj_iff theorem
: (inl a : α ⊕ β) = inl b ↔ a = b
Full source 
theorem inl.inj_iff : (inl a : α ⊕ β) = inl b ↔ a = b := ⟨inl.inj, congrArg _⟩
Injectivity of Left Injection in Disjoint Union: $\operatorname{inl}(a) = \operatorname{inl}(b) \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the left injections $\operatorname{inl}(a)$ and $\operatorname{inl}(b)$ in the disjoint union $\alpha \oplus \beta$ are equal if and only if $a = b$.
Sum.inr.inj_iff theorem
: (inr a : α ⊕ β) = inr b ↔ a = b
Full source 
theorem inr.inj_iff : (inr a : α ⊕ β) = inr b ↔ a = b := ⟨inr.inj, congrArg _⟩
Injectivity of Right Injection in Disjoint Union: $\operatorname{inr}(a) = \operatorname{inr}(b) \leftrightarrow a = b$
Informal description
For any elements $a, b$ of type $\beta$, the right injection $\operatorname{inr}(a)$ in the disjoint union $\alpha \oplus \beta$ equals $\operatorname{inr}(b)$ if and only if $a = b$.
Sum.inl_ne_inr theorem
: inl a ≠ inr b
Full source 
theorem inl_ne_inr : inlinl a ≠ inr b := nofun
Non-equality of Left and Right Injections in Disjoint Union
Informal description
For any elements $a$ of type $\alpha$ and $b$ of type $\beta$, the left injection $\operatorname{inl}(a)$ in the disjoint union $\alpha \oplus \beta$ is not equal to the right injection $\operatorname{inr}(b)$.
Sum.inr_ne_inl theorem
: inr b ≠ inl a
Full source 
theorem inr_ne_inl : inrinr b ≠ inl a := nofun
Non-equality of left and right injections in disjoint union
Informal description
For any elements $a$ of type $\alpha$ and $b$ of type $\beta$, the right injection $\operatorname{inr}(b)$ in the disjoint union $\alpha \oplus \beta$ is not equal to the left injection $\operatorname{inl}(a)$.
Sum.elim_comp_inl theorem
(f : α → γ) (g : β → γ) : Sum.elim f g ∘ inl = f
Full source 
@[simp] theorem elim_comp_inl (f : α → γ) (g : β → γ) : Sum.elimSum.elim f g ∘ inl = f :=
  rfl
Composition of Sum Elimination with Left Injection Yields First Function
Informal description
For any functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, the composition of the case analysis function $\operatorname{Sum.elim}\,f\,g$ with the left injection $\operatorname{inl} \colon \alpha \to \alpha \oplus \beta$ equals $f$, i.e., $(\operatorname{Sum.elim}\,f\,g) \circ \operatorname{inl} = f$.
Sum.elim_comp_inr theorem
(f : α → γ) (g : β → γ) : Sum.elim f g ∘ inr = g
Full source 
@[simp] theorem elim_comp_inr (f : α → γ) (g : β → γ) : Sum.elimSum.elim f g ∘ inr = g :=
  rfl
Right Injection Composition with Case Analysis
Informal description
For any functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, the composition of the case analysis function $\operatorname{Sum.elim}\,f\,g$ with the right injection $\operatorname{inr}$ equals $g$, i.e., $(\operatorname{Sum.elim}\,f\,g) \circ \operatorname{inr} = g$.
Sum.elim_inl_inr theorem
: @Sum.elim α β _ inl inr = id
Full source 
@[simp] theorem elim_inl_inr : @Sum.elim α β _ inl inr = id :=
  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
Case Analysis on Disjoint Union Yields Identity
Informal description
For any types $\alpha$ and $\beta$, the case analysis function $\text{Sum.elim}$ applied to the left injection $\text{inl} \colon \alpha \to \alpha \oplus \beta$ and the right injection $\text{inr} \colon \beta \to \alpha \oplus \beta$ yields the identity function on $\alpha \oplus \beta$, i.e., $\text{Sum.elim}\, \text{inl}\, \text{inr} = \text{id}$.
Sum.comp_elim theorem
(f : γ → δ) (g : α → γ) (h : β → γ) : f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h)
Full source 
theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
    f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h) :=
  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
Composition with Sum Elimination Commutes
Informal description
For any functions $f \colon \gamma \to \delta$, $g \colon \alpha \to \gamma$, and $h \colon \beta \to \gamma$, the composition of $f$ with the case analysis function $\text{Sum.elim}\,g\,h$ is equal to the case analysis of the compositions $f \circ g$ and $f \circ h$. In other words, the following diagram commutes: $$f \circ (\text{Sum.elim}\,g\,h) = \text{Sum.elim}\,(f \circ g)\,(f \circ h).$$
Sum.elim_comp_inl_inr theorem
(f : α ⊕ β → γ) : Sum.elim (f ∘ inl) (f ∘ inr) = f
Full source 
@[simp] theorem elim_comp_inl_inr (f : α ⊕ β → γ) :
    Sum.elim (f ∘ inl) (f ∘ inr) = f :=
  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
Case Analysis on Disjoint Union Recovers Original Function
Informal description
For any function $f \colon \alpha \oplus \beta \to \gamma$, the case analysis function $\text{Sum.elim}$ applied to the compositions $f \circ \text{inl}$ and $f \circ \text{inr}$ is equal to $f$ itself, i.e., $$\text{Sum.elim}\,(f \circ \text{inl})\,(f \circ \text{inr}) = f.$$
Sum.elim_eq_iff theorem
{u u' : α → γ} {v v' : β → γ} : Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v'
Full source 
theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
    Sum.elimSum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' := by
  simp [funext_iff, Sum.forall]
Equality of Sum Elimination Functions is Equivalent to Componentwise Equality
Informal description
For any functions $u, u' \colon \alpha \to \gamma$ and $v, v' \colon \beta \to \gamma$, the case analysis functions $\text{Sum.elim}\,u\,v$ and $\text{Sum.elim}\,u'\,v'$ are equal if and only if $u = u'$ and $v = v'$.
Sum.map_map theorem
(f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') : ∀ x : Sum α β, (x.map f g).map f' g' = x.map (f' ∘ f) (g' ∘ g)
Full source 
@[simp] theorem map_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
    ∀ x : Sum α β, (x.map f g).map f' g' = x.map (f' ∘ f) (g' ∘ g)
  | inl _ => rfl
  | inr _ => rfl
Composition of Component-wise Mappings on Disjoint Unions
Informal description
For any functions $f' \colon \alpha' \to \alpha''$, $g' \colon \beta' \to \beta''$, $f \colon \alpha \to \alpha'$, and $g \colon \beta \to \beta'$, and for any element $x \in \alpha \oplus \beta$, the following equality holds: $$(x.\text{map}\,f\,g).\text{map}\,f'\,g' = x.\text{map}\,(f' \circ f)\,(g' \circ g).$$
Sum.map_comp_map theorem
(f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') : Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g)
Full source 
@[simp] theorem map_comp_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
    Sum.mapSum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g) :=
  funext <| map_map f' g' f g
Composition of Sum Mappings Equals Sum of Compositions
Informal description
For any functions $f \colon \alpha \to \alpha'$, $g \colon \beta \to \beta'$, $f' \colon \alpha' \to \alpha''$, and $g' \colon \beta' \to \beta''$, the composition of the sum mappings satisfies: \[ \text{Sum.map}\, f'\, g' \circ \text{Sum.map}\, f\, g = \text{Sum.map}\, (f' \circ f)\, (g' \circ g). \]
Sum.map_id_id theorem
: Sum.map (@id α) (@id β) = id
Full source 
@[simp] theorem map_id_id : Sum.map (@id α) (@id β) = id :=
  funext fun x => Sum.recOn x (fun _ => rfl) fun _ => rfl
Identity Mapping Preserved Under Sum Construction
Informal description
The component-wise mapping of the identity functions on types $\alpha$ and $\beta$ is equal to the identity function on the disjoint union $\alpha \oplus \beta$. That is, $\text{Sum.map}\, \text{id}\, \text{id} = \text{id}$.
Sum.elim_map theorem
{f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x} : Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
Full source 
theorem elim_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x} :
    Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x := by
  cases x <;> rfl
Compatibility of Sum Elimination with Sum Mapping
Informal description
For any functions $f_1 \colon \alpha \to \beta$, $f_2 \colon \beta \to \varepsilon$, $g_1 \colon \gamma \to \delta$, $g_2 \colon \delta \to \varepsilon$, and any element $x$ in the disjoint union $\alpha \oplus \gamma$, the following equality holds: \[ \text{Sum.elim}\, f_2\, g_2\, (\text{Sum.map}\, f_1\, g_1\, x) = \text{Sum.elim}\, (f_2 \circ f_1)\, (g_2 \circ g_1)\, x. \]
Sum.elim_comp_map theorem
{f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} : Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁)
Full source 
theorem elim_comp_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} :
    Sum.elimSum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) :=
  funext fun _ => elim_map
Composition of Sum Elimination and Sum Mapping Equals Sum Elimination of Compositions
Informal description
For any functions $f_1 \colon \alpha \to \beta$, $f_2 \colon \beta \to \varepsilon$, $g_1 \colon \gamma \to \delta$, and $g_2 \colon \delta \to \varepsilon$, the composition of the sum elimination function $\text{Sum.elim}\,f_2\,g_2$ with the sum mapping function $\text{Sum.map}\,f_1\,g_1$ is equal to the sum elimination function applied to the compositions $f_2 \circ f_1$ and $g_2 \circ g_1$. That is, \[ \text{Sum.elim}\,f_2\,g_2 \circ \text{Sum.map}\,f_1\,g_1 = \text{Sum.elim}\,(f_2 \circ f_1)\,(g_2 \circ g_1). \]
Sum.isLeft_map theorem
(f : α → β) (g : γ → δ) (x : α ⊕ γ) : isLeft (x.map f g) = isLeft x
Full source 
@[simp] theorem isLeft_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
    isLeft (x.map f g) = isLeft x := by
  cases x <;> rfl
Preservation of Left Injection Under Sum Mapping
Informal description
For any functions $f \colon \alpha \to \beta$ and $g \colon \gamma \to \delta$, and any element $x$ in the disjoint union $\alpha \oplus \gamma$, the boolean value indicating whether $\text{Sum.map}\,f\,g\,x$ is a left injection (`inl`) is equal to the boolean value indicating whether $x$ itself is a left injection. In other words, mapping preserves the left/right structure of the sum type.
Sum.isRight_map theorem
(f : α → β) (g : γ → δ) (x : α ⊕ γ) : isRight (x.map f g) = isRight x
Full source 
@[simp] theorem isRight_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
    isRight (x.map f g) = isRight x := by
  cases x <;> rfl
Preservation of Right Injection Property under Sum Mapping
Informal description
For any functions $f \colon \alpha \to \beta$ and $g \colon \gamma \to \delta$, and any element $x \in \alpha \oplus \gamma$, the property of being a right injection is preserved under the mapping $\text{Sum.map}\,f\,g$. That is, $\text{isRight}(\text{Sum.map}\,f\,g\,x) = \text{isRight}(x)$.
Sum.getLeft?_map theorem
(f : α → β) (g : γ → δ) (x : α ⊕ γ) : (x.map f g).getLeft? = x.getLeft?.map f
Full source 
@[simp] theorem getLeft?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
    (x.map f g).getLeft? = x.getLeft?.map f := by
  cases x <;> rfl
Left Component Preservation under Sum Mapping
Informal description
For any functions $f \colon \alpha \to \beta$ and $g \colon \gamma \to \delta$, and any element $x \in \alpha \oplus \gamma$, the left component of the mapped sum $\text{Sum.map}\,f\,g\,x$ is equal to the mapped left component of $x$. That is, $(\text{Sum.map}\,f\,g\,x).\text{getLeft?} = x.\text{getLeft?}.\text{map}\,f$.
Sum.getRight?_map theorem
(f : α → β) (g : γ → δ) (x : α ⊕ γ) : (x.map f g).getRight? = x.getRight?.map g
Full source 
@[simp] theorem getRight?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
    (x.map f g).getRight? = x.getRight?.map g := by cases x <;> rfl
Right Component Preservation under Sum Mapping: $(\text{map}\,f\,g\,x).\text{getRight?} = x.\text{getRight?}.\text{map}\,g$
Informal description
For any functions $f \colon \alpha \to \beta$ and $g \colon \gamma \to \delta$, and any element $x \in \alpha \oplus \gamma$, the right component of the mapped sum $\text{Sum.map}\,f\,g\,x$ as an optional value is equal to mapping $g$ over the right component of $x$ as an optional value. That is, $$(\text{Sum.map}\,f\,g\,x).\text{getRight?} = x.\text{getRight?}.\text{map}\,g.$$
Sum.swap_swap theorem
(x : α ⊕ β) : swap (swap x) = x
Full source 
@[simp] theorem swap_swap (x : α ⊕ β) : swap (swap x) = x := by cases x <;> rfl
Double Swap of Disjoint Union is Identity
Informal description
For any element $x$ of the disjoint union type $\alpha \oplus \beta$, applying the swap operation twice returns $x$ itself, i.e., $\text{swap}(\text{swap}(x)) = x$.
Sum.swap_swap_eq theorem
: swap ∘ swap = @id (α ⊕ β)
Full source 
@[simp] theorem swap_swap_eq : swapswap ∘ swap = @id (α ⊕ β) := funext <| swap_swap
Double Swap Equals Identity on Disjoint Union
Informal description
The composition of the swap operation with itself on the disjoint union type $\alpha \oplus \beta$ is equal to the identity function, i.e., $\text{swap} \circ \text{swap} = \text{id}$.
Sum.isLeft_swap theorem
(x : α ⊕ β) : x.swap.isLeft = x.isRight
Full source 
@[simp] theorem isLeft_swap (x : α ⊕ β) : x.swap.isLeft = x.isRight := by cases x <;> rfl
Left Injection Check of Swap Equals Right Injection Check
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the result of checking whether the swapped version of $x$ (via `Sum.swap`) is a left injection (`Sum.isLeft`) is equal to checking whether $x$ itself is a right injection (`Sum.isRight$).
Sum.isRight_swap theorem
(x : α ⊕ β) : x.swap.isRight = x.isLeft
Full source 
@[simp] theorem isRight_swap (x : α ⊕ β) : x.swap.isRight = x.isLeft := by cases x <;> rfl
Swap Preserves Injection Checks: $\text{isRight}(\text{swap}(x)) = \text{isLeft}(x)$
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the result of checking whether the swapped version $\text{swap}(x)$ is a right injection equals the result of checking whether $x$ is a left injection. That is, $\text{isRight}(\text{swap}(x)) = \text{isLeft}(x)$.
Sum.getLeft?_swap theorem
(x : α ⊕ β) : x.swap.getLeft? = x.getRight?
Full source 
@[simp] theorem getLeft?_swap (x : α ⊕ β) : x.swap.getLeft? = x.getRight? := by cases x <;> rfl
Equality of Left Component of Swapped Sum and Right Component: $\mathrm{getLeft?}(x.\mathrm{swap}) = \mathrm{getRight?}(x)$
Informal description
For any element $x$ in the disjoint union $\alpha \oplus \beta$, the left component of the swapped sum $x.\mathrm{swap}$ (viewed as an optional value) is equal to the right component of $x$ (also viewed as an optional value). In other words, $\mathrm{getLeft?}(x.\mathrm{swap}) = \mathrm{getRight?}(x)$.
Sum.getRight?_swap theorem
(x : α ⊕ β) : x.swap.getRight? = x.getLeft?
Full source 
@[simp] theorem getRight?_swap (x : α ⊕ β) : x.swap.getRight? = x.getLeft? := by cases x <;> rfl
Equality of Right Component of Swapped Sum and Left Component: $\mathrm{getRight?}(x.\mathrm{swap}) = \mathrm{getLeft?}(x)$
Informal description
For any element $x$ of the disjoint union $\alpha \oplus \beta$, the right component of the swapped sum $x.\mathrm{swap}$ as an optional value is equal to the left component of $x$ as an optional value. In other words, $\mathrm{getRight?}(x.\mathrm{swap}) = \mathrm{getLeft?}(x)$.
Sum.LiftRel.mono theorem
(hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y
Full source 
theorem LiftRel.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b)
  (h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y := by
  cases h
  · exact LiftRel.inl (hr _ _ ‹_›)
  · exact LiftRel.inr (hs _ _ ‹_›)
Monotonicity of Lifted Relations on Disjoint Unions
Informal description
Given relations $r_1, r_2 : \alpha \to \gamma \to \mathrm{Prop}$ and $s_1, s_2 : \beta \to \delta \to \mathrm{Prop}$ such that: 1. For all $a \in \alpha$ and $b \in \gamma$, $r_1(a, b)$ implies $r_2(a, b)$, 2. For all $a \in \beta$ and $b \in \delta$, $s_1(a, b)$ implies $s_2(a, b)$, and given elements $x \in \alpha \oplus \beta$ and $y \in \gamma \oplus \delta$ such that $\mathrm{LiftRel}\, r_1\, s_1\, x\, y$ holds, then $\mathrm{LiftRel}\, r_2\, s_2\, x\, y$ also holds.
Sum.LiftRel.mono_left theorem
(hr : ∀ a b, r₁ a b → r₂ a b) (h : LiftRel r₁ s x y) : LiftRel r₂ s x y
Full source 
theorem LiftRel.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : LiftRel r₁ s x y) :
    LiftRel r₂ s x y :=
  (h.mono hr) fun _ _ => id
Monotonicity of Lifted Relations on the Left Component
Informal description
Given relations $r_1, r_2 : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$ such that for all $a \in \alpha$ and $b \in \gamma$, $r_1(a, b)$ implies $r_2(a, b)$, and given elements $x \in \alpha \oplus \beta$ and $y \in \gamma \oplus \delta$ such that $\mathrm{LiftRel}\, r_1\, s\, x\, y$ holds, then $\mathrm{LiftRel}\, r_2\, s\, x\, y$ also holds.
Sum.LiftRel.mono_right theorem
(hs : ∀ a b, s₁ a b → s₂ a b) (h : LiftRel r s₁ x y) : LiftRel r s₂ x y
Full source 
theorem LiftRel.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : LiftRel r s₁ x y) :
    LiftRel r s₂ x y :=
  h.mono (fun _ _ => id) hs
Monotonicity of Lifted Relations on Disjoint Unions (Right)
Informal description
Given relations $s_1, s_2 : \beta \to \delta \to \mathrm{Prop}$ such that for all $a \in \beta$ and $b \in \delta$, $s_1(a, b)$ implies $s_2(a, b)$, and given elements $x \in \alpha \oplus \beta$ and $y \in \gamma \oplus \delta$ such that $\mathrm{LiftRel}\, r\, s_1\, x\, y$ holds, then $\mathrm{LiftRel}\, r\, s_2\, x\, y$ also holds.
Sum.LiftRel.swap theorem
(h : LiftRel r s x y) : LiftRel s r x.swap y.swap
Full source 
protected theorem LiftRel.swap (h : LiftRel r s x y) : LiftRel s r x.swap y.swap := by
  cases h
  · exact LiftRel.inr ‹_›
  · exact LiftRel.inl ‹_›
Swap of Lifted Relations on Disjoint Unions
Informal description
Given relations $r : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$, if $\mathrm{LiftRel}\, r\, s$ holds for elements $x \in \alpha \oplus \beta$ and $y \in \gamma \oplus \delta$, then $\mathrm{LiftRel}\, s\, r$ holds for the swapped elements $x.\mathrm{swap} \in \beta \oplus \alpha$ and $y.\mathrm{swap} \in \delta \oplus \gamma$.
Sum.liftRel_swap_iff theorem
: LiftRel s r x.swap y.swap ↔ LiftRel r s x y
Full source 
@[simp] theorem liftRel_swap_iff : LiftRelLiftRel s r x.swap y.swap ↔ LiftRel r s x y :=
  ⟨fun h => by rw [← swap_swap x, ← swap_swap y]; exact h.swap, LiftRel.swap⟩
Equivalence of Lifted Relations under Swap: $\mathrm{LiftRel}\, s\, r\, (x.\mathrm{swap})\, (y.\mathrm{swap}) \leftrightarrow \mathrm{LiftRel}\, r\, s\, x\, y$
Informal description
For any relations $r : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$, and any elements $x \in \alpha \oplus \beta$ and $y \in \gamma \oplus \delta$, the lifted relation $\mathrm{LiftRel}\, s\, r$ holds for the swapped elements $x.\mathrm{swap}$ and $y.\mathrm{swap}$ if and only if $\mathrm{LiftRel}\, r\, s$ holds for $x$ and $y$.
Sum.LiftRel.lex theorem
{a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b
Full source 
protected theorem LiftRel.lex {a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b := by
  cases h
  · exact Lex.inl ‹_›
  · exact Lex.inr ‹_›
Lifted Relation Implies Lexicographic Order on Disjoint Union
Informal description
For any elements $a, b$ in the disjoint union $\alpha \oplus \beta$, if the lifted relation $\text{LiftRel}\, r\, s$ holds between $a$ and $b$, then the lexicographic order $\text{Lex}\, r\, s$ also holds between $a$ and $b$.
Sum.liftRel_subrelation_lex theorem
: Subrelation (LiftRel r s) (Lex r s)
Full source 
theorem liftRel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex
Lifted Relation is Subrelation of Lexicographic Order on Disjoint Union
Informal description
For any relations $r$ on type $\alpha$ and $s$ on type $\beta$, the lifted relation $\text{LiftRel}\, r\, s$ is a subrelation of the lexicographic order $\text{Lex}\, r\, s$ on the disjoint union $\alpha \oplus \beta$. That is, whenever $\text{LiftRel}\, r\, s\, x\, y$ holds for $x, y \in \alpha \oplus \beta$, then $\text{Lex}\, r\, s\, x\, y$ also holds.
Sum.Lex.mono theorem
(hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) : Lex r₂ s₂ x y
Full source 
theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) :
    Lex r₂ s₂ x y := by
  cases h
  · exact Lex.inl (hr _ _ ‹_›)
  · exact Lex.inr (hs _ _ ‹_›)
  · exact Lex.sep _ _
Monotonicity of Lexicographic Order on Disjoint Union
Informal description
For any relations $r_1, r_2$ on type $\alpha$ and $s_1, s_2$ on type $\beta$, if $r_1$ implies $r_2$ (i.e., $r_1(a, b) \to r_2(a, b)$ for all $a, b \in \alpha$) and $s_1$ implies $s_2$ (i.e., $s_1(a, b) \to s_2(a, b)$ for all $a, b \in \beta$), then the lexicographic order $\text{Lex}(r_1, s_1)$ on $\alpha \oplus \beta$ implies $\text{Lex}(r_2, s_2)$. In other words, if $x \leq y$ under $\text{Lex}(r_1, s_1)$, then $x \leq y$ under $\text{Lex}(r_2, s_2)$.
Sum.Lex.mono_left theorem
(hr : ∀ a b, r₁ a b → r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y
Full source 
theorem Lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y :=
  (h.mono hr) fun _ _ => id
Monotonicity of Lexicographic Order in Left Component
Informal description
For any relations $r_1, r_2$ on type $\alpha$ and $s$ on type $\beta$, if $r_1$ implies $r_2$ (i.e., $r_1(a, b) \to r_2(a, b)$ for all $a, b \in \alpha$), then the lexicographic order $\text{Lex}(r_1, s)$ on $\alpha \oplus \beta$ implies $\text{Lex}(r_2, s)$. In other words, if $x \leq y$ under $\text{Lex}(r_1, s)$, then $x \leq y$ under $\text{Lex}(r_2, s)$.
Sum.Lex.mono_right theorem
(hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y
Full source 
theorem Lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y :=
  h.mono (fun _ _ => id) hs
Monotonicity of Lexicographic Order with Respect to Right Relation
Informal description
For any relations $s_1, s_2$ on type $\beta$, if $s_1$ implies $s_2$ (i.e., $s_1(a, b) \to s_2(a, b)$ for all $a, b \in \beta$), then the lexicographic order $\text{Lex}(r, s_1)$ on $\alpha \oplus \beta$ implies $\text{Lex}(r, s_2)$. In other words, if $x \leq y$ under $\text{Lex}(r, s_1)$, then $x \leq y$ under $\text{Lex}(r, s_2)$.
Sum.lex_acc_inl theorem
(aca : Acc r a) : Acc (Lex r s) (inl a)
Full source 
theorem lex_acc_inl (aca : Acc r a) : Acc (Lex r s) (inl a) := by
  induction aca with
  | intro _ _ IH =>
    constructor
    intro y h
    cases h with
    | inl h' => exact IH _ h'
Accessibility of Left Injection in Lexicographic Order on Disjoint Union
Informal description
Given a relation $r$ on a type $\alpha$ and a relation $s$ on a type $\beta$, if an element $a \in \alpha$ is accessible with respect to $r$ (i.e., $\text{Acc } r \, a$ holds), then the element $\text{inl } a \in \alpha \oplus \beta$ is accessible with respect to the lexicographic order $\text{Lex } r \, s$ on the disjoint union $\alpha \oplus \beta$.
Sum.lex_acc_inr theorem
(aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) : Acc (Lex r s) (inr b)
Full source 
theorem lex_acc_inr (aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
    Acc (Lex r s) (inr b) := by
  induction acb with
  | intro _ _ IH =>
    constructor
    intro y h
    cases h with
    | inr h' => exact IH _ h'
    | sep => exact aca _
Accessibility of Right Injection in Lexicographic Order on Disjoint Union
Informal description
Given relations $r$ on $\alpha$ and $s$ on $\beta$, if: 1. For every $a \in \alpha$, the element $\text{inl } a$ is accessible under the lexicographic order $\text{Lex } r s$, and 2. For some $b \in \beta$, $b$ is accessible under $s$, then the element $\text{inr } b$ is accessible under the lexicographic order $\text{Lex } r s$.
Sum.lex_wf theorem
(ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s)
Full source 
theorem lex_wf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s) :=
  have aca : ∀ a, Acc (Lex r s) (inl a) := fun a => lex_acc_inl (ha.apply a)
  ⟨fun x => Sum.recOn x aca fun b => lex_acc_inr aca (hb.apply b)⟩
Well-Foundedness of Lexicographic Order on Disjoint Union
Informal description
Given well-founded relations $r$ on $\alpha$ and $s$ on $\beta$, the lexicographic order $\text{Lex } r s$ on the disjoint union $\alpha \oplus \beta$ is also well-founded.
Sum.elim_const_const theorem
(c : γ) : Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c
Full source 
theorem elim_const_const (c : γ) :
    Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c := by
  apply funext
  rintro (_ | _) <;> rfl
Sum Elimination of Constant Functions Yields Constant Function
Informal description
For any type $\gamma$ and element $c \in \gamma$, the case analysis function $\text{Sum.elim}$ applied to the constant functions $\lambda (x : \alpha), c$ and $\lambda (x : \beta), c$ is equal to the constant function $\lambda (x : \alpha \oplus \beta), c$.
Sum.elim_lam_const_lam_const theorem
(c : γ) : Sum.elim (fun _ : α => c) (fun _ : β => c) = fun _ => c
Full source 
@[simp] theorem elim_lam_const_lam_const (c : γ) :
    Sum.elim (fun _ : α => c) (fun _ : β => c) = fun _ => c :=
  Sum.elim_const_const c
Sum Elimination of Constant Functions Yields Constant Function
Informal description
For any type $\gamma$ and element $c \in \gamma$, the case analysis function $\text{Sum.elim}$ applied to the constant functions $\lambda (x : \alpha), c$ and $\lambda (x : \beta), c$ is equal to the constant function $\lambda (x : \alpha \oplus \beta), c$.