awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
s : α ⊕' β
inl :
  ∀ (val : α),
    Eq (α := α ⊕' β)
      (Sum.elim PSum.inl PSum.inr
        ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl inr : α ⊕ β)) (PSum.inl val)))
      (PSum.inl val)
⊢ Sum.elim PSum.inl PSum.inr
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl inr : α ⊕ β)) s) =
    s
have inr : ∀ (val : β),
  Eq (α := α ⊕' β)
    (Sum.elim PSum.inl PSum.inr
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl inr : α ⊕ β)) (PSum.inr val)))
    (PSum.inr val)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
s : α ⊕ β
⊢ (fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s inl inr : α ⊕ β))
      (Sum.elim PSum.inl PSum.inr s) =
    s
have inl : ∀ (val : α),
  Eq (α := α ⊕ β)
    ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s inl inr : α ⊕ β))
      (Sum.elim PSum.inl PSum.inr (inl val)))
    (inl val)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
s : α ⊕ β
inl :
  ∀ (val : α),
    Eq (α := α ⊕ β)
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl inr : α ⊕ β))
        (Sum.elim PSum.inl PSum.inr (Sum.inl val)))
      (Sum.inl val)
⊢ (fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl inr : α ⊕ β))
      (Sum.elim PSum.inl PSum.inr s) =
    s
have inr : ∀ (val : β),
  Eq (α := α ⊕ β)
    ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl inr : α ⊕ β))
      (Sum.elim PSum.inl PSum.inr (inr val)))
    (inr val)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
⊢ (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)
have H : ∀ (i : α₁ ⊕ α₂),
  Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
    (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
    (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
have H : ∀ (val : α₁),
  Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inl val) : γ₁ ⊕ γ₂)
    (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inl val) : γ₁ ⊕ γ₂)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
H :
  ∀ (val : α₁),
    Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inl val) : γ₁ ⊕ γ₂)
      (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inl val) : γ₁ ⊕ γ₂)
⊢ Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
    (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
have H₁ : ∀ (val : α₂),
  Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inr val) : γ₁ ⊕ γ₂)
    (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inr val) : γ₁ ⊕ γ₂)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α : Type u_9
β : Type u_10
⊢ (Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)
have H : ∀ (i : α ⊕ β),
  Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
    ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α : Type u_9
β : Type u_10
i : α ⊕ β
⊢ Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
    ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
have H : ∀ (val : α),
  Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) (inl val) : α ⊕ β)
    ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) (inl val) : α ⊕ β)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α : Type u_9
β : Type u_10
i : α ⊕ β
H :
  ∀ (val : α),
    Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) (inl val) : α ⊕ β)
      ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) (inl val) : α ⊕ β)
⊢ Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
    ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) i : α ⊕ β)
have H₁ : ∀ (val : β),
  Eq (α := α ⊕ β) (((Equiv.refl α).sumCongr (Equiv.refl β) : (a : α ⊕ β) → α ⊕ β) (inr val) : α ⊕ β)
    ((Equiv.refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) (inr val) : α ⊕ β)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
⊢ 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))
        b) =
    b
have false : 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: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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}) ↦ 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
⊢ Sum.elim (fun (x : PUnit.{u + 1}) ↦ Bool.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))
        b) =
    b
have true : Sum.elim (fun (x : PUnit.{u + 1}) ↦ Bool.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: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
⊢ (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) s) =
    s
have inl : 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: rcases s with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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) (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)
⊢ (fun (b : Bool) ↦
        (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (Sum.inl PUnit.unit) (inr PUnit.unit) :
          PUnit ⊕ PUnit))
      (Sum.elim (fun (x : PUnit.{u + 1}) ↦ false) (fun (x : PUnit.{v + 1}) ↦ true) s) =
    s
have inr : Eq (α := PUnit ⊕ PUnit)
  ((fun (b : Bool) ↦
      (Bool.casesOn (motive := fun (x : Bool) ↦ PUnit ⊕ PUnit) b (Sum.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: rcases s with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
x : (α ⊕ β) ⊕ γ ⊕ δ
⊢ 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 : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
        x) =
    x
have inl : ∀ (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: rcases x with ((a | b) | (c | d))
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
x : (α ⊕ γ) ⊕ β ⊕ δ
⊢ 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 : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
      (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 : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
        x) =
    x
have inl : ∀ (a : α),
  Eq (α := (α ⊕ γ) ⊕ β ⊕ δ)
    (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 : (α ⊕ β) ⊕ γ ⊕ δ) → ((α ⊕ β) ⊕ γ) ⊕ δ))))
      (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 : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
        (inl (inl a))))
    (inl (inl a))
Tactic: rcases x with ((a | c) | (b | d))
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
inst : IsEmpty β
s : α ⊕ β
⊢ inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) s) = s
have inl : ∀ (val : α),
  Eq (α := α ⊕ β) (inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) (inl val))) (inl val)
Tactic: rcases s with (_ | x)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
inst : IsEmpty β
s : α ⊕ β
inl :
  ∀ (val : α),
    Eq (α := α ⊕ β) (Sum.inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) (Sum.inl val)))
      (Sum.inl val)
⊢ Sum.inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) s) = s
have inr : ∀ (x : β), Eq (α := α ⊕ β) (Sum.inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) (inr x))) (inr x)
Tactic: rcases s with (_ | x)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
s : α ⊕ β
⊢ (fun (s : (b : Bool) × bif b then β else α) ↦
        (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b :
          α ⊕ β))
      ((fun (s : α ⊕ β) ↦
          (Sum.elim (fun (x : bif false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false x)
              (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
            (b : Bool) × bif b then β else α))
        s) =
    s
have inl : ∀ (val : α),
  Eq (α := α ⊕ β)
    ((fun (s : (b : Bool) × bif b then β else α) ↦
        (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
          | ⟨false, a⟩ => inl a
          | ⟨true, b⟩ => inr b :
          α ⊕ β))
      ((fun (s : α ⊕ β) ↦
          (Sum.elim (fun (x : bif false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false x)
              (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
            (b : Bool) × bif b then β else α))
        (inl val)))
    (inl val)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
s : α ⊕ β
inl :
  ∀ (val : α),
    Eq (α := α ⊕ β)
      ((fun (s : (b : Bool) × bif b then β else α) ↦
          (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
            | ⟨false, a⟩ => Sum.inl a
            | ⟨true, b⟩ => inr b :
            α ⊕ β))
        ((fun (s : α ⊕ β) ↦
            (Sum.elim (fun (x : bif false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false x)
                (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
              (b : Bool) × bif b then β else α))
          (Sum.inl val)))
      (Sum.inl val)
⊢ (fun (s : (b : Bool) × bif b then β else α) ↦
        (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
          | ⟨false, a⟩ => Sum.inl a
          | ⟨true, b⟩ => inr b :
          α ⊕ β))
      ((fun (s : α ⊕ β) ↦
          (Sum.elim (fun (x : bif false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false x)
              (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
            (b : Bool) × bif b then β else α))
        s) =
    s
have inr : ∀ (val : β),
  Eq (α := α ⊕ β)
    ((fun (s : (b : Bool) × bif b then β else α) ↦
        (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
          | ⟨false, a⟩ => Sum.inl a
          | ⟨true, b⟩ => inr b :
          α ⊕ β))
      ((fun (s : α ⊕ β) ↦
          (Sum.elim (fun (x : bif false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false x)
              (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
            (b : Bool) × bif b then β else α))
        (inr val)))
    (inr val)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
s : (b : Bool) × bif b then β else α
⊢ (fun (s : α ⊕ β) ↦
        (Sum.elim (fun (x : bif false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false x)
            (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
          (b : Bool) × bif b then β else α))
      ((fun (s : (b : Bool) × bif b then β else α) ↦
          (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
            | ⟨false, a⟩ => inl a
            | ⟨true, b⟩ => inr b :
            α ⊕ β))
        s) =
    s
have false : ∀ (snd : bif false then β else α),
  Eq.{u_9 + 1} (α := (b : Bool) × bif b then β else α)
    ((fun (s : α ⊕ β) ↦
        (Sum.elim (fun (x : bif false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false x)
            (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
          (b : Bool) × bif b then β else α))
      ((fun (s : (b : Bool) × bif b then β else α) ↦
          (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
            | ⟨false, a⟩ => inl a
            | ⟨true, b⟩ => inr b :
            α ⊕ β))
        (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false snd)))
    (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) false snd)
Tactic: rcases s with ⟨_ | _, _⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
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
s : (b : Bool) × bif b then β else α
false :
  ∀ (snd : bif Bool.false then β else α),
    Eq.{u_9 + 1} (α := (b : Bool) × bif b then β else α)
      ((fun (s : α ⊕ β) ↦
          (Sum.elim
              (fun (x : bif Bool.false then β else α) ↦
                Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.false x)
              (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
            (b : Bool) × bif b then β else α))
        ((fun (s : (b : Bool) × bif b then β else α) ↦
            (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
              | ⟨Bool.false, a⟩ => inl a
              | ⟨true, b⟩ => inr b :
              α ⊕ β))
          (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.false snd)))
      (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.false snd)
⊢ (fun (s : α ⊕ β) ↦
        (Sum.elim
            (fun (x : bif Bool.false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.false x)
            (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
          (b : Bool) × bif b then β else α))
      ((fun (s : (b : Bool) × bif b then β else α) ↦
          (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
            | ⟨Bool.false, a⟩ => inl a
            | ⟨true, b⟩ => inr b :
            α ⊕ β))
        s) =
    s
have true : ∀ (snd : bif true then β else α),
  Eq.{u_9 + 1} (α := (b : Bool) × bif b then β else α)
    ((fun (s : α ⊕ β) ↦
        (Sum.elim
            (fun (x : bif Bool.false then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.false x)
            (fun (x : bif true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true x) s :
          (b : Bool) × bif b then β else α))
      ((fun (s : (b : Bool) × bif b then β else α) ↦
          (match (motive := ((b : Bool) × bif b then β else α) → α ⊕ β) s with
            | ⟨Bool.false, a⟩ => inl a
            | ⟨true, b⟩ => inr b :
            α ⊕ β))
        (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true snd)))
    (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true snd)
Tactic: rcases s with ⟨_ | _, _⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (goal)
Goal:
α_1 : 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_1 : DecidableEq α
a : α
⊢ Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default))
      (if h : a = default then none else some (Subtype.mk (p := fun (a : α) ↦ a ≠ default) a h)) =
    a
have pos : a = default →
  Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default)) none = a
Tactic: split_ifs