awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val : α₁
⊢ Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inl val) : γ₁ ⊕ γ₂)
    (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inl val) : γ₁ ⊕ γ₂)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val : α₂
⊢ Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inr val) : γ₁ ⊕ γ₂)
    (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inr val) : γ₁ ⊕ γ₂)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
δ : Type u_12
e : α ≃ β
f : γ ≃ δ
⊢ (e.sumCongr f).symm = e.symm.sumCongr f.symm

Tactic:
rfl

Premises used: Sum.map, Equiv.sumCongr, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
H :
  ∀ (i : α ⊕ β),
    Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
      ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
⊢ (Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)

Tactic:
ext i
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
i : α ⊕ β
H :
  ∀ (val : α),
    Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) (inl val) : α ⊕ β)
      ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) (inl val) : α ⊕ β)
H₁ :
  ∀ (val : β),
    Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) (inr val) : α ⊕ β)
      ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) (inr val) : α ⊕ β)
⊢ Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
    ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)

Tactic:
cases i
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
val : α
⊢ Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) (inl val) : α ⊕ β)
    ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) (inl val) : α ⊕ β)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
val : β
⊢ Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) (inr val) : α ⊕ β)
    ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) (inr val) : α ⊕ β)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : 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 : α
⊢ Eq (α := α ⊕' γ)
    ((fun (x : β ⊕' δ) ↦
        (PSum.casesOn (motive := fun (x : β ⊕' δ) ↦ α ⊕' γ) x (PSum.inl ∘ (⇑e₁.symm : (a : β) → α))
            (PSum.inr ∘ (⇑e₂.symm : (a : δ) → γ)) :
          α ⊕' γ))
      ((fun (x : α ⊕' γ) ↦
          (PSum.casesOn (motive := fun (x : α ⊕' γ) ↦ β ⊕' δ) x (PSum.inl ∘ (⇑e₁ : (a : α) → β))
              (PSum.inr ∘ (⇑e₂ : (a : γ) → δ)) :
            β ⊕' δ))
        (PSum.inl x)))
    (PSum.inl x)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : 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 : γ
⊢ Eq (α := α ⊕' γ)
    ((fun (x : β ⊕' δ) ↦
        (PSum.casesOn (motive := fun (x : β ⊕' δ) ↦ α ⊕' γ) x (PSum.inl ∘ (⇑e₁.symm : (a : β) → α))
            (PSum.inr ∘ (⇑e₂.symm : (a : δ) → γ)) :
          α ⊕' γ))
      ((fun (x : α ⊕' γ) ↦
          (PSum.casesOn (motive := fun (x : α ⊕' γ) ↦ β ⊕' δ) x (PSum.inl ∘ (⇑e₁ : (a : α) → β))
              (PSum.inr ∘ (⇑e₂ : (a : γ) → δ)) :
            β ⊕' δ))
        (PSum.inr x)))
    (PSum.inr x)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : 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 : β
⊢ Eq (α := β ⊕' δ)
    ((fun (x : α ⊕' γ) ↦
        (PSum.casesOn (motive := fun (x : α ⊕' γ) ↦ β ⊕' δ) x (PSum.inl ∘ (⇑e₁ : (a : α) → β))
            (PSum.inr ∘ (⇑e₂ : (a : γ) → δ)) :
          β ⊕' δ))
      ((fun (x : β ⊕' δ) ↦
          (PSum.casesOn (motive := fun (x : β ⊕' δ) ↦ α ⊕' γ) x (PSum.inl ∘ (⇑e₁.symm : (a : β) → α))
              (PSum.inr ∘ (⇑e₂.symm : (a : δ) → γ)) :
            α ⊕' γ))
        (PSum.inl x)))
    (PSum.inl x)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : 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 : δ
⊢ Eq (α := β ⊕' δ)
    ((fun (x : α ⊕' γ) ↦
        (PSum.casesOn (motive := fun (x : α ⊕' γ) ↦ β ⊕' δ) x (PSum.inl ∘ (⇑e₁ : (a : α) → β))
            (PSum.inr ∘ (⇑e₂ : (a : γ) → δ)) :
          β ⊕' δ))
      ((fun (x : β ⊕' δ) ↦
          (PSum.casesOn (motive := fun (x : β ⊕' δ) ↦ α ⊕' γ) x (PSum.inl ∘ (⇑e₁.symm : (a : β) → α))
              (PSum.inr ∘ (⇑e₂.symm : (a : δ) → γ)) :
            α ⊕' γ))
        (PSum.inr x)))
    (PSum.inr x)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
p : α ⊕ β → Prop
a : α
h : p (inl a)
⊢ (fun (x : Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }) ↦
        (match (motive := Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) } → { c : α ⊕ β // p c }) x with
          | inl a => Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inl (↑a : α)) ⋯
          | inr b => Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inr (↑b : β)) ⋯ :
          { c : α ⊕ β // p c }))
      ((fun (x : { c : α ⊕ β // p c }) ↦
          (match (motive := { c : α ⊕ β // p c } → Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }) x with
            | ⟨inl a, h⟩ => inl (Subtype.mk (p := fun (a : α) ↦ p (inl a)) a h)
            | ⟨inr b, h⟩ => inr (Subtype.mk (p := fun (b : β) ↦ p (inr b)) b h) :
            Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }))
        (Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inl a) h)) =
    Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inl a) h

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
p : α ⊕ β → Prop
b : β
h : p (inr b)
⊢ (fun (x : Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }) ↦
        (match (motive := Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) } → { c : α ⊕ β // p c }) x with
          | inl a => Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inl (↑a : α)) ⋯
          | inr b => Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inr (↑b : β)) ⋯ :
          { c : α ⊕ β // p c }))
      ((fun (x : { c : α ⊕ β // p c }) ↦
          (match (motive := { c : α ⊕ β // p c } → Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }) x with
            | ⟨inl a, h⟩ => inl (Subtype.mk (p := fun (a : α) ↦ p (inl a)) a h)
            | ⟨inr b, h⟩ => inr (Subtype.mk (p := fun (b : β) ↦ p (inr b)) b h) :
            Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }))
        (Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inr b) h)) =
    Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inr b) h

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
p : α ⊕ β → Prop
a : { a : α // p (inl a) }
⊢ Eq (α := Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) })
    ((fun (x : { c : α ⊕ β // p c }) ↦
        (match (motive := { c : α ⊕ β // p c } → Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }) x with
          | ⟨inl a, h⟩ => inl (Subtype.mk (p := fun (a : α) ↦ p (inl a)) a h)
          | ⟨inr b, h⟩ => inr (Subtype.mk (p := fun (b : β) ↦ p (inr b)) b h) :
          Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }))
      ((fun (x : Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }) ↦
          (match (motive := Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) } → { c : α ⊕ β // p c }) x with
            | inl a => Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inl (↑a : α)) ⋯
            | inr b => Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inr (↑b : β)) ⋯ :
            { c : α ⊕ β // p c }))
        (inl a)))
    (inl a)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
p : α ⊕ β → Prop
b : { b : β // p (inr b) }
⊢ Eq (α := Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) })
    ((fun (x : { c : α ⊕ β // p c }) ↦
        (match (motive := { c : α ⊕ β // p c } → Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }) x with
          | ⟨inl a, h⟩ => inl (Subtype.mk (p := fun (a : α) ↦ p (inl a)) a h)
          | ⟨inr b, h⟩ => inr (Subtype.mk (p := fun (b : β) ↦ p (inr b)) b h) :
          Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }))
      ((fun (x : Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) }) ↦
          (match (motive := Sum.{u_9, u_10} { a : α // p (inl a) } { b : β // p (inr b) } → { c : α ⊕ β // p c }) x with
            | inl a => Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inl (↑a : α)) ⋯
            | inr b => Subtype.mk (p := fun (c : α ⊕ β) ↦ p c) (inr (↑b : β)) ⋯ :
            { c : α ⊕ β // p c }))
        (inr b)))
    (inr b)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
ea : Perm α
eb : Perm β
x : α ⊕ β
⊢ Eq (α := α ⊕ β) ((ea.sumCongr eb : (a : α ⊕ β) → α ⊕ β) x : α ⊕ β)
    (Sum.map (⇑ea : (a : α) → α) (⇑eb : (a : β) → β) x : α ⊕ β)

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
e : Perm α
f : Perm β
g : Perm α
h : Perm β
⊢ Equiv.trans (e.sumCongr f) (g.sumCongr h) = sumCongr (Equiv.trans e g) (Equiv.trans f h)

Tactic:
Equiv.sumCongr_trans e f g h

Premises used: Equiv.sumCongr_trans
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
e : Perm α
f : Perm β
⊢ Equiv.symm (e.sumCongr f) = sumCongr (Equiv.symm e) (Equiv.symm f)

Tactic:
Equiv.sumCongr_symm e f

Premises used: Equiv.sumCongr_symm
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
⊢ sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)

Tactic:
Equiv.sumCongr_refl

Premises used: Equiv.sumCongr_refl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
b : Bool
false :
  Sum.elim (fun (x : PUnit.{u + 1}) ↦ Bool.false) (fun (x : PUnit.{v + 1}) ↦ Bool.true)
      ((fun (b : Bool) ↦
          (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (inl PUnit.unit) (inr PUnit.unit) : PUnit ⊕ PUnit))
        Bool.false) =
    Bool.false
true :
  Sum.elim (fun (x : PUnit.{u + 1}) ↦ Bool.false) (fun (x : PUnit.{v + 1}) ↦ Bool.true)
      ((fun (b : Bool) ↦
          (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (inl PUnit.unit) (inr PUnit.unit) : PUnit ⊕ PUnit))
        Bool.true) =
    Bool.true
⊢ Sum.elim (fun (x : PUnit.{u + 1}) ↦ Bool.false) (fun (x : PUnit.{v + 1}) ↦ Bool.true)
      ((fun (b : Bool) ↦
          (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (inl PUnit.unit) (inr PUnit.unit) : PUnit ⊕ PUnit))
        b) =
    b

Tactic:
cases b
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : 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 : PUnit.{u + 1}) ↦ false) (fun (x : PUnit.{v + 1}) ↦ true)
      ((fun (b : Bool) ↦
          (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (inl PUnit.unit) (inr PUnit.unit) : PUnit ⊕ PUnit))
        false) =
    false

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : 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 : PUnit.{u + 1}) ↦ false) (fun (x : PUnit.{v + 1}) ↦ true)
      ((fun (b : Bool) ↦
          (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (inl PUnit.unit) (inr PUnit.unit) : PUnit ⊕ PUnit))
        true) =
    true

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
s : PUnit ⊕ PUnit
inl :
  Eq (α := PUnit ⊕ PUnit)
    ((fun (b : Bool) ↦
        (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (Sum.inl PUnit.unit) (Sum.inr PUnit.unit) :
          PUnit ⊕ PUnit))
      (Sum.elim (fun (x : PUnit.{u + 1}) ↦ false) (fun (x : PUnit.{v + 1}) ↦ true) (Sum.inl PUnit.unit)))
    (Sum.inl PUnit.unit)
inr :
  Eq (α := PUnit ⊕ PUnit)
    ((fun (b : Bool) ↦
        (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (Sum.inl PUnit.unit) (Sum.inr PUnit.unit) :
          PUnit ⊕ PUnit))
      (Sum.elim (fun (x : PUnit.{u + 1}) ↦ false) (fun (x : PUnit.{v + 1}) ↦ true) (Sum.inr PUnit.unit)))
    (Sum.inr PUnit.unit)
⊢ (fun (b : Bool) ↦
        (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (Sum.inl PUnit.unit) (Sum.inr PUnit.unit) :
          PUnit ⊕ PUnit))
      (Sum.elim (fun (x : PUnit.{u + 1}) ↦ false) (fun (x : PUnit.{v + 1}) ↦ true) s) =
    s

Tactic:
rcases s with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ Eq (α := PUnit ⊕ PUnit)
    ((fun (b : Bool) ↦
        (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (inl PUnit.unit) (inr PUnit.unit) : PUnit ⊕ PUnit))
      (Sum.elim (fun (x : PUnit.{u + 1}) ↦ false) (fun (x : PUnit.{v + 1}) ↦ true) (inl PUnit.unit)))
    (inl PUnit.unit)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
⊢ Eq (α := PUnit ⊕ PUnit)
    ((fun (b : Bool) ↦
        (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (inl PUnit.unit) (inr PUnit.unit) : PUnit ⊕ PUnit))
      (Sum.elim (fun (x : PUnit.{u + 1}) ↦ false) (fun (x : PUnit.{v + 1}) ↦ true) (inr PUnit.unit)))
    (inr PUnit.unit)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
⊢ (sumComm α β).symm = sumComm β α

Tactic:
rfl

Premises used: Sum.swap, Equiv.sumComm, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
val : α
⊢ Eq (α := (α ⊕ β) ⊕ γ)
    (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inl val))))
    (inl (inl val))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
val : β
⊢ Eq (α := (α ⊕ β) ⊕ γ)
    (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inr val))))
    (inl (inr val))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
val : γ
⊢ Eq (α := (α ⊕ β) ⊕ γ)
    (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inr val)))
    (inr val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
val : α
⊢ Eq (α := α ⊕ β ⊕ γ)
    (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inl val)))
    (inl val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
val : β
⊢ Eq (α := α ⊕ β ⊕ γ)
    (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inl val))))
    (inr (inl val))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
val : γ
⊢ Eq (α := α ⊕ β ⊕ γ)
    (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:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
a : α
⊢ Eq (α := α ⊕ β ⊕ γ) ((sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl a)) : α ⊕ β ⊕ γ) (inl a : α ⊕ β ⊕ γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
b : β
⊢ Eq (α := α ⊕ β ⊕ γ) ((sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr b)) : α ⊕ β ⊕ γ)
    (inr (inl b) : α ⊕ β ⊕ γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
c : γ
⊢ Eq (α := α ⊕ β ⊕ γ) ((sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr c) : α ⊕ β ⊕ γ) (inr (inr c) : α ⊕ β ⊕ γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
a : α
⊢ Eq (α := (α ⊕ β) ⊕ γ) (((sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) (inl a) : (α ⊕ β) ⊕ γ)
    (inl (inl a) : (α ⊕ β) ⊕ γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
b : β
⊢ Eq (α := (α ⊕ β) ⊕ γ) (((sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) (inr (inl b)) : (α ⊕ β) ⊕ γ)
    (inl (inr b) : (α ⊕ β) ⊕ γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
c : γ
⊢ Eq (α := (α ⊕ β) ⊕ γ) (((sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) (inr (inr c)) : (α ⊕ β) ⊕ γ)
    (inr c : (α ⊕ β) ⊕ γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ_1 : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
δ : Type u_12
a : α
⊢ Eq (α := (α ⊕ β) ⊕ γ ⊕ δ)
    (comp (α := (α ⊕ γ) ⊕ β ⊕ δ) (β := ((α ⊕ β) ⊕ γ) ⊕ δ)
      (⇑(sumAssoc (α ⊕ β) γ δ) : (a : ((α ⊕ β) ⊕ γ) ⊕ δ) → (α ⊕ β) ⊕ γ ⊕ δ)
      (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) id)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ).symm : (a : γ ⊕ β) → β ⊕ γ)) id)
          (comp (β := ((α ⊕ γ) ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β) : (a : (α ⊕ γ) ⊕ β) → α ⊕ γ ⊕ β) id)
            (⇑(Equiv.symm (sumAssoc (α ⊕ γ) β δ)) : (a : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
      (comp (α := (α ⊕ β) ⊕ γ ⊕ δ) (β := ((α ⊕ γ) ⊕ β) ⊕ δ)
        (⇑(sumAssoc (α ⊕ γ) β δ) : (a : ((α ⊕ γ) ⊕ β) ⊕ δ) → (α ⊕ γ) ⊕ β ⊕ δ)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β).symm : (a : α ⊕ γ ⊕ β) → (α ⊕ γ) ⊕ β) id)
          (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ) : (a : β ⊕ γ) → γ ⊕ β)) id)
            (comp (β := ((α ⊕ β) ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ) : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) id)
              (⇑(Equiv.symm (sumAssoc (α ⊕ β) γ δ)) : (a : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
        (inl (inl a))))
    (inl (inl a))

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ_1 : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
δ : Type u_12
b : β
⊢ Eq (α := (α ⊕ β) ⊕ γ ⊕ δ)
    (comp (α := (α ⊕ γ) ⊕ β ⊕ δ) (β := ((α ⊕ β) ⊕ γ) ⊕ δ)
      (⇑(sumAssoc (α ⊕ β) γ δ) : (a : ((α ⊕ β) ⊕ γ) ⊕ δ) → (α ⊕ β) ⊕ γ ⊕ δ)
      (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) id)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ).symm : (a : γ ⊕ β) → β ⊕ γ)) id)
          (comp (β := ((α ⊕ γ) ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β) : (a : (α ⊕ γ) ⊕ β) → α ⊕ γ ⊕ β) id)
            (⇑(Equiv.symm (sumAssoc (α ⊕ γ) β δ)) : (a : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
      (comp (α := (α ⊕ β) ⊕ γ ⊕ δ) (β := ((α ⊕ γ) ⊕ β) ⊕ δ)
        (⇑(sumAssoc (α ⊕ γ) β δ) : (a : ((α ⊕ γ) ⊕ β) ⊕ δ) → (α ⊕ γ) ⊕ β ⊕ δ)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β).symm : (a : α ⊕ γ ⊕ β) → (α ⊕ γ) ⊕ β) id)
          (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ) : (a : β ⊕ γ) → γ ⊕ β)) id)
            (comp (β := ((α ⊕ β) ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ) : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) id)
              (⇑(Equiv.symm (sumAssoc (α ⊕ β) γ δ)) : (a : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
        (inl (inr b))))
    (inl (inr b))

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ_1 : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
δ : Type u_12
c : γ
⊢ Eq (α := (α ⊕ β) ⊕ γ ⊕ δ)
    (comp (α := (α ⊕ γ) ⊕ β ⊕ δ) (β := ((α ⊕ β) ⊕ γ) ⊕ δ)
      (⇑(sumAssoc (α ⊕ β) γ δ) : (a : ((α ⊕ β) ⊕ γ) ⊕ δ) → (α ⊕ β) ⊕ γ ⊕ δ)
      (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) id)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ).symm : (a : γ ⊕ β) → β ⊕ γ)) id)
          (comp (β := ((α ⊕ γ) ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β) : (a : (α ⊕ γ) ⊕ β) → α ⊕ γ ⊕ β) id)
            (⇑(Equiv.symm (sumAssoc (α ⊕ γ) β δ)) : (a : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
      (comp (α := (α ⊕ β) ⊕ γ ⊕ δ) (β := ((α ⊕ γ) ⊕ β) ⊕ δ)
        (⇑(sumAssoc (α ⊕ γ) β δ) : (a : ((α ⊕ γ) ⊕ β) ⊕ δ) → (α ⊕ γ) ⊕ β ⊕ δ)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β).symm : (a : α ⊕ γ ⊕ β) → (α ⊕ γ) ⊕ β) id)
          (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ) : (a : β ⊕ γ) → γ ⊕ β)) id)
            (comp (β := ((α ⊕ β) ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ) : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) id)
              (⇑(Equiv.symm (sumAssoc (α ⊕ β) γ δ)) : (a : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
        (inr (inl c))))
    (inr (inl c))

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ_1 : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
δ : Type u_12
d : δ
⊢ Eq (α := (α ⊕ β) ⊕ γ ⊕ δ)
    (comp (α := (α ⊕ γ) ⊕ β ⊕ δ) (β := ((α ⊕ β) ⊕ γ) ⊕ δ)
      (⇑(sumAssoc (α ⊕ β) γ δ) : (a : ((α ⊕ β) ⊕ γ) ⊕ δ) → (α ⊕ β) ⊕ γ ⊕ δ)
      (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ).symm : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) id)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ).symm : (a : γ ⊕ β) → β ⊕ γ)) id)
          (comp (β := ((α ⊕ γ) ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β) : (a : (α ⊕ γ) ⊕ β) → α ⊕ γ ⊕ β) id)
            (⇑(Equiv.symm (sumAssoc (α ⊕ γ) β δ)) : (a : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
      (comp (α := (α ⊕ β) ⊕ γ ⊕ δ) (β := ((α ⊕ γ) ⊕ β) ⊕ δ)
        (⇑(sumAssoc (α ⊕ γ) β δ) : (a : ((α ⊕ γ) ⊕ β) ⊕ δ) → (α ⊕ γ) ⊕ β ⊕ δ)
        (comp (β := (α ⊕ γ ⊕ β) ⊕ δ) (Sum.map (⇑(sumAssoc α γ β).symm : (a : α ⊕ γ ⊕ β) → (α ⊕ γ) ⊕ β) id)
          (comp (β := (α ⊕ β ⊕ γ) ⊕ δ) (Sum.map (Sum.map id (⇑(sumComm β γ) : (a : β ⊕ γ) → γ ⊕ β)) id)
            (comp (β := ((α ⊕ β) ⊕ γ) ⊕ δ) (Sum.map (⇑(sumAssoc α β γ) : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) id)
              (⇑(Equiv.symm (sumAssoc (α ⊕ β) γ δ)) : (a : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
        (inr (inr d))))
    (inr (inr d))

Tactic:
simp