awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β γ) : (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:
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 β γ) : (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 (inr c))))
    (inl (inr 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
b : β
⊢ 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 : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
        (inr (inl b))))
    (inr (inl 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
d : δ
⊢ 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 : (α ⊕ γ) ⊕ β ⊕ δ) → ((α ⊕ γ) ⊕ β) ⊕ δ))))
        (inr (inr d))))
    (inr (inr d))

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
δ : Type u_12
⊢ (sumSumSumComm α β γ δ).symm = sumSumSumComm α γ β δ

Tactic:
rfl

Premises used: Sum.swap, Equiv.sumSumSumComm, 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
γ : 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)
inr :
  ∀ (x : β),
    Eq (α := α ⊕ β) (Sum.inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) (Sum.inr x))) (Sum.inr x)
⊢ Sum.inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) s) = s

Tactic:
rcases s with (_ | x)
-- 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
inst : IsEmpty β
val : α
⊢ Eq (α := α ⊕ β) (inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) (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
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
inst : IsEmpty β
x : β
⊢ Eq (α := α ⊕ β) (inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) (inr x))) (inr x)

Tactic:
isEmptyElim x

Premises used: isEmptyElim
-- 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
inst : IsEmpty β
x : β
⊢ Eq (α := α ⊕ β) (inl (Sum.elim id (fun (a : β) ↦ isEmptyElim (p := fun (x : β) ↦ α) a) (inr x))) (inr x)

Tactic:
exact isEmptyElim x
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
inst : IsEmpty β
a : α
⊢ (sumEmpty α β : (a : α ⊕ β) → α) (inl a) = a

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
inst : IsEmpty α
b : β
⊢ (emptySum α β : (a : α ⊕ β) → β) (inr b) = b

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
γ : 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⟩ => Sum.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)
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⟩ => Sum.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.inr val)))
      (Sum.inr 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⟩ => Sum.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

Tactic:
cases s
-- 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
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:
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
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 α))
        (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
γ : 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 Bool.true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.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
              | ⟨Bool.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)
true :
  ∀ (snd : bif Bool.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 Bool.true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.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
              | ⟨Bool.true, b⟩ => inr b :
              α ⊕ β))
          (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.true snd)))
      (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.true 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 Bool.true then β else α) ↦ Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) Bool.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
            | ⟨Bool.true, b⟩ => inr b :
            α ⊕ β))
        s) =
    s

Tactic:
rcases s with ⟨_ | _, _⟩
-- 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
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:
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
snd : bif true 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 α) true snd)))
    (Sigma.mk (β := fun (b : Bool) ↦ bif b then β else α) true snd)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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 : α
pos :
  a = default →
    Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default)) none = a
neg :
  ∀ (h : ¬a = default),
    Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default))
        (some (Subtype.mk (p := fun (a : α) ↦ a ≠ default) a h)) =
      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

Tactic:
split_ifs
-- Module: Mathlib.Logic.Equiv.Sum
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 : α
h : a = default
⊢ Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default)) none = a

Tactic:
simp [*]
-- Module: Mathlib.Logic.Equiv.Sum
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 : α
h : ¬a = default
⊢ Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default))
      (some (Subtype.mk (p := fun (a : α) ↦ a ≠ default) a h)) =
    a

Tactic:
simp [*]
-- Module: Mathlib.Logic.Equiv.Sum
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 α
⊢ Eq.{u + 1} (α := Option { a : α // a ≠ default })
    ((fun (a : α) ↦
        (if h : a = default then none else some (Subtype.mk (p := fun (a : α) ↦ a ≠ default) a h) :
          Option { a : α // a ≠ default }))
      (Option.elim' (α := { a : α // a ≠ default }) default (Subtype.val (p := fun (a : α) ↦ a ≠ default)) none))
    none

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
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_9
p : α → Prop
inst : DecidablePred p
x : α
hx : p x
inl :
  Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (if h : p x then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x h)
    else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h))
    (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    ((fun (a : α) ↦
        (if h : p a then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)
          else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) :
          { a : α // p a } ⊕ { a : α // ¬p a }))
      (Sum.elim (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.val (p := fun (a : α) ↦ ¬p a))
        (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))))
    (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))

Tactic:
dsimp
-- Module: Mathlib.Logic.Equiv.Sum
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_9
p : α → Prop
inst : DecidablePred p
x : α
hx : ¬p x
inr :
  Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (if h : p x then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x h)
    else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h))
    (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    ((fun (a : α) ↦
        (if h : p a then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)
          else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) :
          { a : α // p a } ⊕ { a : α // ¬p a }))
      (Sum.elim (α := { a : α // p a }) (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a))
        (Subtype.val (p := fun (a : α) ↦ ¬p a)) (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))))
    (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))

Tactic:
dsimp
-- Module: Mathlib.Logic.Equiv.Sum
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_9
p : α → Prop
inst : DecidablePred p
x : α
hx : p x
inl :
  Eq (α := { a : α // p a } ⊕ { a : α // ¬p a }) (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
    (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
inl₁ : p x
inl₂ :
  Eq (α := { a : α // p a } ⊕ { a : α // ¬p a }) (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
    (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))
inl₃ : p x
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (if h : p x then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x h)
    else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h))
    (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x hx))

Tactic:
rw [dif_pos]

Premises used: dif_pos
-- Module: Mathlib.Logic.Equiv.Sum
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_9
p : α → Prop
inst : DecidablePred p
x : α
hx : ¬p x
inr :
  Eq (α := { a : α // p a } ⊕ { a : α // ¬p a }) (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
    (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
inr₁ : ¬p x
inr₂ :
  Eq (α := { a : α // p a } ⊕ { a : α // ¬p a }) (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
    (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))
inr₃ : ¬p x
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (if h : p x then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) x h)
    else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x h))
    (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx))

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- Module: Mathlib.Logic.Equiv.Sum
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_9
p : α → Prop
inst : DecidablePred p
a : α
pos :
  ∀ (h : p a),
    Sum.elim (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.val (p := fun (a : α) ↦ ¬p a))
        (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)) =
      a
neg :
  ∀ (h : ¬p a),
    Sum.elim (α := { a : α // p a }) (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a))
        (Subtype.val (p := fun (a : α) ↦ ¬p a)) (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
      a
⊢ Sum.elim (α := { a : α // p a }) (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a))
      (Subtype.val (p := fun (a : α) ↦ ¬p a))
      (if h : p a then Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)
      else Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
    a

Tactic:
split_ifs
-- Module: Mathlib.Logic.Equiv.Sum
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_9
p : α → Prop
inst : DecidablePred p
a : α
h : p a
⊢ Sum.elim (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.val (p := fun (a : α) ↦ ¬p a))
      (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h)) =
    a

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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_9
p : α → Prop
inst : DecidablePred p
a : α
h : ¬p a
⊢ Sum.elim (α := { a : α // p a }) (β := { a : α // ¬p a }) (Subtype.val (p := fun (a : α) ↦ p a))
      (Subtype.val (p := fun (a : α) ↦ ¬p a)) (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
    a

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
p : α → Prop
inst : DecidablePred p
x : { a : α // p a }
⊢ (sumCompl p : (a : { a : α // p a } ⊕ { a : α // ¬p a }) → α) (Sum.inl x) = (↑x : α)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
p : α → Prop
inst : DecidablePred p
x : { a : α // ¬p a }
⊢ (sumCompl p : (a : { a : α // p a } ⊕ { a : α // ¬p a }) → α) (Sum.inr x) = (↑x : α)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
p : α → Prop
inst : DecidablePred p
a : α
h : p a
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (((sumCompl p).symm : (a : α) → { a : α // p a } ⊕ { a : α // ¬p a }) a : { a : α // p a } ⊕ { a : α // ¬p a })
    (Sum.inl (Subtype.mk (p := fun (a : α) ↦ p a) a h) : { a : α // p a } ⊕ { a : α // ¬p a })

Tactic:
dif_pos h

Premises used: dif_pos, dite