# Documentation

Std.Data.Sum.Lemmas

# Disjoint union of types #

Theorems about the definitions introduced in Std.Data.Sum.Basic.

@[simp]
theorem Sum.forall {α : Type u_1} {β : Type u_2} {p : α βProp} :
((x : α β) → p x) ((a : α) → p ()) ((b : β) → p ())
@[simp]
theorem Sum.exists {α : Type u_1} {β : Type u_2} {p : α βProp} :
(x, p x) (a, p ()) b, p ()
theorem Sum.forall_sum {α : Type u_1} {β : Type u_2} {γ : α βSort u_3} (p : ((ab : α β) → γ ab) → Prop) :
((fab : (ab : α β) → γ ab) → p fab) (fa : (val : α) → γ (Sum.inl val)) → (fb : (val : β) → γ (Sum.inr val)) → p fun t => Sum.rec fa fb t
@[simp]
theorem Sum.inl_getLeft {α : Type u_1} {β : Type u_2} (x : α β) (h : ) :
Sum.inl () = x
@[simp]
theorem Sum.inr_getRight {α : Type u_1} {β : Type u_2} (x : α β) (h : ) :
Sum.inr () = x
@[simp]
theorem Sum.getLeft?_eq_none_iff {α : Type u_1} {β : Type u_2} {x : α β} :
= none
@[simp]
theorem Sum.getRight?_eq_none_iff {α : Type u_1} {β : Type u_2} {x : α β} :
= none
theorem Sum.eq_left_getLeft_of_isLeft {α : Type u_1} {β : Type u_2} {x : α β} (h : ) :
x = Sum.inl ()
@[simp]
theorem Sum.getLeft_eq_iff :
∀ {α : Type u_1} {a : α} {β : Type u_2} {x : α β} (h : ), = a x =
theorem Sum.eq_right_getRight_of_isRight {α : Type u_1} {β : Type u_2} {x : α β} (h : ) :
x = Sum.inr ()
@[simp]
theorem Sum.getRight_eq_iff :
∀ {β : Type u_1} {b : β} {α : Type u_2} {x : α β} (h : ), = b x =
@[simp]
theorem Sum.getLeft?_eq_some_iff :
∀ {α : Type u_1} {a : α} {β : Type u_2} {x : α β}, x =
@[simp]
theorem Sum.getRight?_eq_some_iff :
∀ {β : Type u_1} {b : β} {α : Type u_2} {x : α β}, x =
@[simp]
theorem Sum.bnot_isLeft {α : Type u_1} {β : Type u_2} (x : α β) :
@[simp]
theorem Sum.isLeft_eq_false {α : Type u_1} {β : Type u_2} {x : α β} :
theorem Sum.not_isLeft {α : Type u_1} {β : Type u_2} {x : α β} :
@[simp]
theorem Sum.bnot_isRight {α : Type u_1} {β : Type u_2} (x : α β) :
@[simp]
theorem Sum.isRight_eq_false {α : Type u_1} {β : Type u_2} {x : α β} :
theorem Sum.not_isRight {α : Type u_1} {β : Type u_2} {x : α β} :
theorem Sum.isLeft_iff :
∀ {α : Type u_1} {β : Type u_2} {x : α β}, y, x =
theorem Sum.isRight_iff :
∀ {α : Type u_1} {β : Type u_2} {x : α β}, y, x =
theorem Sum.inl.inj_iff {α : Type u_1} {β : Type u_2} {a : α} {b : α} :
= a = b
theorem Sum.inr.inj_iff {α : Type u_1} {β : Type u_2} {a : β} {b : β} :
= a = b
theorem Sum.inl_ne_inr :
∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β},
theorem Sum.inr_ne_inl :
∀ {β : Type u_1} {b : β} {α : Type u_2} {a : α},

### Sum.elim#

@[simp]
theorem Sum.elim_comp_inl {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : αγ) (g : βγ) :
Sum.elim f g Sum.inl = f
@[simp]
theorem Sum.elim_comp_inr {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : αγ) (g : βγ) :
Sum.elim f g Sum.inr = g
@[simp]
theorem Sum.elim_inl_inr {α : Type u_1} {β : Type u_2} :
Sum.elim Sum.inl Sum.inr = id
theorem Sum.comp_elim {γ : Sort u_1} {δ : Sort u_2} {α : Type u_3} {β : Type u_4} (f : γδ) (g : αγ) (h : βγ) :
f Sum.elim g h = Sum.elim (f g) (f h)
@[simp]
theorem Sum.elim_comp_inl_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α βγ) :
Sum.elim (f Sum.inl) (f Sum.inr) = f

### Sum.map#

@[simp]
theorem Sum.map_map {α' : Type u_1} {α'' : Type u_2} {β' : Type u_3} {β'' : Type u_4} {α : Type u_5} {β : Type u_6} (f' : α'α'') (g' : β'β'') (f : αα') (g : ββ') (x : α β) :
Sum.map f' g' (Sum.map f g x) = Sum.map (f' f) (g' g) x
@[simp]
theorem Sum.map_comp_map {α' : Type u_1} {α'' : Type u_2} {β' : Type u_3} {β'' : Type u_4} {α : Type u_5} {β : Type u_6} (f' : α'α'') (g' : β'β'') (f : αα') (g : ββ') :
Sum.map f' g' Sum.map f g = Sum.map (f' f) (g' g)
@[simp]
theorem Sum.map_id_id {α : Type u_1} {β : Type u_2} :
Sum.map id id = id
theorem Sum.elim_map {α : Type u_1} {β : Type u_2} {ε : Sort u_3} {γ : Type u_4} {δ : Type u_5} {f₁ : αβ} {f₂ : βε} {g₁ : γδ} {g₂ : δε} {x : α γ} :
Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ f₁) (g₂ g₁) x
theorem Sum.elim_comp_map {α : Type u_1} {β : Type u_2} {ε : Sort u_3} {γ : Type u_4} {δ : Type u_5} {f₁ : αβ} {f₂ : βε} {g₁ : γδ} {g₂ : δε} :
Sum.elim f₂ g₂ Sum.map f₁ g₁ = Sum.elim (f₂ f₁) (g₂ g₁)
@[simp]
theorem Sum.isLeft_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (x : α γ) :
@[simp]
theorem Sum.isRight_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (x : α γ) :
@[simp]
theorem Sum.getLeft?_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (x : α γ) :
@[simp]
theorem Sum.getRight?_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (x : α γ) :

### Sum.swap#

@[simp]
theorem Sum.swap_swap {α : Type u_1} {β : Type u_2} (x : α β) :
Sum.swap () = x
@[simp]
theorem Sum.swap_swap_eq {α : Type u_1} {β : Type u_2} :
Sum.swap Sum.swap = id
@[simp]
theorem Sum.isLeft_swap {α : Type u_1} {β : Type u_2} (x : α β) :
@[simp]
theorem Sum.isRight_swap {α : Type u_1} {β : Type u_2} (x : α β) :
@[simp]
theorem Sum.getLeft?_swap {α : Type u_1} {β : Type u_2} (x : α β) :
@[simp]
theorem Sum.getRight?_swap {α : Type u_1} {β : Type u_2} (x : α β) :
theorem Sum.LiftRel.mono :
∀ {α : Type u_1} {α_1 : Type u_2} {r₁ r₂ : αα_1Prop} {β : Type u_3} {β_1 : Type u_4} {s₁ s₂ : ββ_1Prop} {x : α β} {y : α_1 β_1}, (∀ (a : α) (b : α_1), r₁ a br₂ a b) → (∀ (a : β) (b : β_1), s₁ a bs₂ a b) → Sum.LiftRel r₁ s₁ x ySum.LiftRel r₂ s₂ x y
theorem Sum.LiftRel.mono_left :
∀ {α : Type u_1} {α_1 : Type u_2} {r₁ r₂ : αα_1Prop} {β : Type u_3} {β_1 : Type u_4} {s : ββ_1Prop} {x : α β} {y : α_1 β_1}, (∀ (a : α) (b : α_1), r₁ a br₂ a b) → Sum.LiftRel r₁ s x ySum.LiftRel r₂ s x y
theorem Sum.LiftRel.mono_right :
∀ {β : Type u_1} {β_1 : Type u_2} {s₁ s₂ : ββ_1Prop} {α : Type u_3} {α_1 : Type u_4} {r : αα_1Prop} {x : α β} {y : α_1 β_1}, (∀ (a : β) (b : β_1), s₁ a bs₂ a b) → Sum.LiftRel r s₁ x ySum.LiftRel r s₂ x y
theorem Sum.LiftRel.swap :
∀ {α : Type u_1} {α_1 : Type u_2} {r : αα_1Prop} {β : Type u_3} {β_1 : Type u_4} {s : ββ_1Prop} {x : α β} {y : α_1 β_1}, Sum.LiftRel r s x ySum.LiftRel s r () ()
@[simp]
theorem Sum.liftRel_swap_iff :
∀ {β : Type u_1} {β_1 : Type u_2} {s : ββ_1Prop} {α : Type u_3} {α_1 : Type u_4} {r : αα_1Prop} {x : α β} {y : α_1 β_1}, Sum.LiftRel s r () () Sum.LiftRel r s x y
theorem Sum.LiftRel.lex {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {a : α β} {b : α β} (h : Sum.LiftRel r s a b) :
Sum.Lex r s a b
theorem Sum.liftRel_subrelation_lex :
∀ {α : Type u_1} {r : ααProp} {β : Type u_2} {s : ββProp}, Subrelation () (Sum.Lex r s)
theorem Sum.Lex.mono :
∀ {α : Type u_1} {r₁ r₂ : ααProp} {β : Type u_2} {s₁ s₂ : ββProp} {x y : α β}, (∀ (a b : α), r₁ a br₂ a b) → (∀ (a b : β), s₁ a bs₂ a b) → Sum.Lex r₁ s₁ x ySum.Lex r₂ s₂ x y
theorem Sum.Lex.mono_left :
∀ {α : Type u_1} {r₁ r₂ : ααProp} {β : Type u_2} {s : ββProp} {x y : α β}, (∀ (a b : α), r₁ a br₂ a b) → Sum.Lex r₁ s x ySum.Lex r₂ s x y
theorem Sum.Lex.mono_right :
∀ {β : Type u_1} {s₁ s₂ : ββProp} {α : Type u_2} {r : ααProp} {x y : α β}, (∀ (a b : β), s₁ a bs₂ a b) → Sum.Lex r s₁ x ySum.Lex r s₂ x y
theorem Sum.lex_acc_inl :
∀ {α : Type u_1} {r : ααProp} {a : α} {β : Type u_2} {s : ββProp}, Acc r aAcc (Sum.Lex r s) ()
theorem Sum.lex_acc_inr :
∀ {α : Type u_1} {r : ααProp} {β : Type u_2} {s : ββProp}, (∀ (a : α), Acc (Sum.Lex r s) ()) → ∀ {b : β}, Acc s bAcc (Sum.Lex r s) ()
theorem Sum.lex_wf :
∀ {α : Type u_1} {r : ααProp} {α_1 : Type u_2} {s : α_1α_1Prop}, WellFounded (Sum.Lex r s)
theorem Sum.elim_const_const {γ : Sort u_1} {α : Type u_2} {β : Type u_3} (c : γ) :
Sum.elim () () = Function.const (α β) c
@[simp]
theorem Sum.elim_lam_const_lam_const {γ : Sort u_1} {α : Type u_2} {β : Type u_3} (c : γ) :
(Sum.elim (fun x => c) fun x => c) = fun x => c