mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
val✝ : α
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) (PSum.inl val✝)) = PSum.inl val✝

pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
val✝ : β
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) (PSum.inr val✝)) = PSum.inr val✝

Tactic:
<;>

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
val✝ : α
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) (PSum.inl val✝)) = PSum.inl val✝

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
val✝ : β
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) (PSum.inr val✝)) = PSum.inr val✝
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
val✝ : α
⊢ (fun s ↦ PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inl val✝)) = inl val✝

pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
val✝ : β
⊢ (fun s ↦ PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inr val✝)) = inr val✝

Tactic:
<;>

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
val✝ : α
⊢ (fun s ↦ PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inl val✝)) = inl val✝

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
val✝ : β
⊢ (fun s ↦ PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inr val✝)) = inr val✝
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val✝ : α₁
⊢ ((e.sumCongr f).trans (g.sumCongr h)) (inl val✝) = ((e.trans g).sumCongr (f.trans h)) (inl val✝)

pp: case inr
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val✝ : α₂
⊢ ((e.sumCongr f).trans (g.sumCongr h)) (inr val✝) = ((e.trans g).sumCongr (f.trans h)) (inr val✝)

Tactic:
<;>

Goal state after:
case inl
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val✝ : α₁
⊢ ((e.sumCongr f).trans (g.sumCongr h)) (inl val✝) = ((e.trans g).sumCongr (f.trans h)) (inl val✝)

case inr
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val✝ : α₂
⊢ ((e.sumCongr f).trans (g.sumCongr h)) (inr val✝) = ((e.trans g).sumCongr (f.trans h)) (inr val✝)
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α : Type u_9
β : Type u_10
val✝ : α
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) (inl val✝) = (Equiv.refl (α ⊕ β)) (inl val✝)

pp: case inr
α : Type u_9
β : Type u_10
val✝ : β
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) (inr val✝) = (Equiv.refl (α ⊕ β)) (inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_9
β : Type u_10
val✝ : α
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) (inl val✝) = (Equiv.refl (α ⊕ β)) (inl val✝)

case inr
α : Type u_9
β : Type u_10
val✝ : β
⊢ ((Equiv.refl α).sumCongr (Equiv.refl β)) (inr val✝) = (Equiv.refl (α ⊕ β)) (inr val✝)
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : α
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)) (PSum.inl x)) =
    PSum.inl x

pp: case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : γ
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)) (PSum.inr x)) =
    PSum.inr x

Tactic:
<;>

Goal state after:
case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : α
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)) (PSum.inl x)) =
    PSum.inl x

case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : γ
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)) (PSum.inr x)) =
    PSum.inr x
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : β
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) (PSum.inl x)) =
    PSum.inl x

pp: case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : δ
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) (PSum.inr x)) =
    PSum.inr x

Tactic:
<;>

Goal state after:
case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : β
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) (PSum.inl x)) =
    PSum.inl x

case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : δ
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) (PSum.inr x)) =
    PSum.inr x
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
a : α
h : p (inl a)
⊢ (fun x ↦
        match x with
        | inl a => ⟨inl ↑a, ⋯⟩
        | inr b => ⟨inr ↑b, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨inl a, h⟩ => inl ⟨a, h⟩
          | ⟨inr b, h⟩ => inr ⟨b, h⟩)
        ⟨inl a, h⟩) =
    ⟨inl a, h⟩

pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
b : β
h : p (inr b)
⊢ (fun x ↦
        match x with
        | inl a => ⟨inl ↑a, ⋯⟩
        | inr b => ⟨inr ↑b, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨inl a, h⟩ => inl ⟨a, h⟩
          | ⟨inr b, h⟩ => inr ⟨b, h⟩)
        ⟨inr b, h⟩) =
    ⟨inr b, h⟩

Tactic:
<;>

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
a : α
h : p (inl a)
⊢ (fun x ↦
        match x with
        | inl a => ⟨inl ↑a, ⋯⟩
        | inr b => ⟨inr ↑b, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨inl a, h⟩ => inl ⟨a, h⟩
          | ⟨inr b, h⟩ => inr ⟨b, h⟩)
        ⟨inl a, h⟩) =
    ⟨inl a, h⟩

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
b : β
h : p (inr b)
⊢ (fun x ↦
        match x with
        | inl a => ⟨inl ↑a, ⋯⟩
        | inr b => ⟨inr ↑b, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨inl a, h⟩ => inl ⟨a, h⟩
          | ⟨inr b, h⟩ => inr ⟨b, h⟩)
        ⟨inr b, h⟩) =
    ⟨inr b, h⟩
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
a : { a // p (inl a) }
⊢ (fun x ↦
        match x with
        | ⟨inl a, h⟩ => inl ⟨a, h⟩
        | ⟨inr b, h⟩ => inr ⟨b, h⟩)
      ((fun x ↦
          match x with
          | inl a => ⟨inl ↑a, ⋯⟩
          | inr b => ⟨inr ↑b, ⋯⟩)
        (inl a)) =
    inl a

pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
b : { b // p (inr b) }
⊢ (fun x ↦
        match x with
        | ⟨inl a, h⟩ => inl ⟨a, h⟩
        | ⟨inr b, h⟩ => inr ⟨b, h⟩)
      ((fun x ↦
          match x with
          | inl a => ⟨inl ↑a, ⋯⟩
          | inr b => ⟨inr ↑b, ⋯⟩)
        (inr b)) =
    inr b

Tactic:
<;>

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
a : { a // p (inl a) }
⊢ (fun x ↦
        match x with
        | ⟨inl a, h⟩ => inl ⟨a, h⟩
        | ⟨inr b, h⟩ => inr ⟨b, h⟩)
      ((fun x ↦
          match x with
          | inl a => ⟨inl ↑a, ⋯⟩
          | inr b => ⟨inr ↑b, ⋯⟩)
        (inl a)) =
    inl a

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.14
β : Type ?u.13
p : α ⊕ β → Prop
b : { b // p (inr b) }
⊢ (fun x ↦
        match x with
        | ⟨inl a, h⟩ => inl ⟨a, h⟩
        | ⟨inr b, h⟩ => inr ⟨b, h⟩)
      ((fun x ↦
          match x with
          | inl a => ⟨inl ↑a, ⋯⟩
          | inr b => ⟨inr ↑b, ⋯⟩)
        (inr b)) =
    inr b
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case false
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ Sum.elim (fun x ↦ false) (fun x ↦ true) ((fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) false) = false

pp: case true
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ Sum.elim (fun x ↦ false) (fun x ↦ true) ((fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) true) = true

Tactic:
<;>

Goal state after:
case false
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ Sum.elim (fun x ↦ false) (fun x ↦ true) ((fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) false) = false

case true
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ Sum.elim (fun x ↦ false) (fun x ↦ true) ((fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit)) true) = true
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ (fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit))
      (Sum.elim (fun x ↦ false) (fun x ↦ true) (inl PUnit.unit)) =
    inl PUnit.unit

pp: case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ (fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit))
      (Sum.elim (fun x ↦ false) (fun x ↦ true) (inr PUnit.unit)) =
    inr PUnit.unit

Tactic:
<;>

Goal state after:
case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ (fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit))
      (Sum.elim (fun x ↦ false) (fun x ↦ true) (inl PUnit.unit)) =
    inl PUnit.unit

case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ (fun b ↦ Bool.casesOn b (inl PUnit.unit) (inr PUnit.unit))
      (Sum.elim (fun x ↦ false) (fun x ↦ true) (inr PUnit.unit)) =
    inr PUnit.unit
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl.inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : α
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inl val✝))) =
    inl (inl val✝)

pp: case inl.inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : β
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inr val✝))) =
    inl (inr val✝)

pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : γ
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inr val✝)) =
    inr val✝

Tactic:
<;>

Goal state after:
case inl.inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : α
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inl val✝))) =
    inl (inl val✝)

case inl.inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : β
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inr val✝))) =
    inl (inr val✝)

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : γ
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inr val✝)) =
    inr val✝
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : α
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inl val✝)) =
    inl val✝

pp: case inr.inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : β
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inl val✝))) =
    inr (inl val✝)

pp: case inr.inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : γ
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inr val✝))) =
    inr (inr val✝)

Tactic:
<;>

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : α
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inl val✝)) =
    inl val✝

case inr.inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : β
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inl val✝))) =
    inr (inl val✝)

case inr.inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
val✝ : γ
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inr val✝))) =
    inr (inr val✝)
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
val✝ : α
⊢ (fun s ↦
        match s with
        | ⟨false, a⟩ => inl a
        | ⟨true, b⟩ => inr b)
      ((fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) (inl val✝)) =
    inl val✝

pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
val✝ : β
⊢ (fun s ↦
        match s with
        | ⟨false, a⟩ => inl a
        | ⟨true, b⟩ => inr b)
      ((fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) (inr val✝)) =
    inr val✝

Tactic:
<;>

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
val✝ : α
⊢ (fun s ↦
        match s with
        | ⟨false, a⟩ => inl a
        | ⟨true, b⟩ => inr b)
      ((fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) (inl val✝)) =
    inl val✝

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
val✝ : β
⊢ (fun s ↦
        match s with
        | ⟨false, a⟩ => inl a
        | ⟨true, b⟩ => inr b)
      ((fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) (inr val✝)) =
    inr val✝
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case false
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
snd✝ : bif false then β else α
⊢ (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s)
      ((fun s ↦
          match s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b)
        ⟨false, snd✝⟩) =
    ⟨false, snd✝⟩

pp: case true
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
snd✝ : bif true then β else α
⊢ (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s)
      ((fun s ↦
          match s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b)
        ⟨true, snd✝⟩) =
    ⟨true, snd✝⟩

Tactic:
<;>

Goal state after:
case false
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
snd✝ : bif false then β else α
⊢ (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s)
      ((fun s ↦
          match s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b)
        ⟨false, snd✝⟩) =
    ⟨false, snd✝⟩

case true
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
snd✝ : bif true then β else α
⊢ (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s)
      ((fun s ↦
          match s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b)
        ⟨true, snd✝⟩) =
    ⟨true, snd✝⟩
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case pos
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
h✝ : a = default
⊢ Option.elim' default Subtype.val none = a

pp: case neg
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
h✝ : ¬a = default
⊢ Option.elim' default Subtype.val (some ⟨a, h✝⟩) = a

Tactic:
<;>

Goal state after:
case pos
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
h✝ : a = default
⊢ Option.elim' default Subtype.val none = a

case neg
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
h✝ : ¬a = default
⊢ Option.elim' default Subtype.val (some ⟨a, h✝⟩) = a
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val (Sum.inl ⟨x, hx⟩)) =
    Sum.inl ⟨x, hx⟩

pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val (Sum.inr ⟨x, hx⟩)) =
    Sum.inr ⟨x, hx⟩

Tactic:
<;>

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val (Sum.inl ⟨x, hx⟩)) =
    Sum.inl ⟨x, hx⟩

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val (Sum.inr ⟨x, hx⟩)) =
    Sum.inr ⟨x, hx⟩
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case pos
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
a : α
h✝ : p a
⊢ Sum.elim Subtype.val Subtype.val (Sum.inl ⟨a, h✝⟩) = a

pp: case neg
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
a : α
h✝ : ¬p a
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, h✝⟩) = a

Tactic:
<;>

Goal state after:
case pos
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
a : α
h✝ : p a
⊢ Sum.elim Subtype.val Subtype.val (Sum.inl ⟨a, h✝⟩) = a

case neg
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
inst✝ : DecidablePred p
a : α
h✝ : ¬p a
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr ⟨a, h✝⟩) = a
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.20
α : ι → Type u_9
β : ι → Type u_10
i : ι
a : α i
⊢ Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr)
      ((fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) ⟨i, inl a⟩) =
    ⟨i, inl a⟩

pp: case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.20
α : ι → Type u_9
β : ι → Type u_10
i : ι
b : β i
⊢ Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr)
      ((fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) ⟨i, inr b⟩) =
    ⟨i, inr b⟩

Tactic:
<;>

Goal state after:
case inl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.20
α : ι → Type u_9
β : ι → Type u_10
i : ι
a : α i
⊢ Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr)
      ((fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) ⟨i, inl a⟩) =
    ⟨i, inl a⟩

case inr
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.20
α : ι → Type u_9
β : ι → Type u_10
i : ι
b : β i
⊢ Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr)
      ((fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) ⟨i, inr b⟩) =
    ⟨i, inr b⟩