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.20
α : ι → Type u_9
β : ι → Type u_10
i : ι
a : α i
⊢ (fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd)
      (Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr) (inl ⟨i, a⟩)) =
    inl ⟨i, 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
⊢ (fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd)
      (Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr) (inr ⟨i, b⟩)) =
    inr ⟨i, 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
⊢ (fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd)
      (Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr) (inl ⟨i, a⟩)) =
    inl ⟨i, 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
⊢ (fun p ↦ Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd)
      (Sum.elim (Sigma.map id fun x ↦ inl) (Sigma.map id fun x ↦ inr) (inr ⟨i, b⟩)) =
    inr ⟨i, b⟩
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
t : α ⊕ β → Type u_9
x : α
y : t (inl x)
⊢ Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩)
      ((fun x ↦
          match x with
          | ⟨inl x, y⟩ => inl ⟨x, y⟩
          | ⟨inr x, y⟩ => inr ⟨x, y⟩)
        ⟨inl x, y⟩) =
    ⟨inl x, y⟩

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
t : α ⊕ β → Type u_9
x : β
y : t (inr x)
⊢ Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩)
      ((fun x ↦
          match x with
          | ⟨inl x, y⟩ => inl ⟨x, y⟩
          | ⟨inr x, y⟩ => inr ⟨x, y⟩)
        ⟨inr x, y⟩) =
    ⟨inr x, y⟩

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
t : α ⊕ β → Type u_9
x : α
y : t (inl x)
⊢ Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩)
      ((fun x ↦
          match x with
          | ⟨inl x, y⟩ => inl ⟨x, y⟩
          | ⟨inr x, y⟩ => inr ⟨x, y⟩)
        ⟨inl x, y⟩) =
    ⟨inl x, y⟩

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
t : α ⊕ β → Type u_9
x : β
y : t (inr x)
⊢ Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩)
      ((fun x ↦
          match x with
          | ⟨inl x, y⟩ => inl ⟨x, y⟩
          | ⟨inr x, y⟩ => inr ⟨x, y⟩)
        ⟨inr x, y⟩) =
    ⟨inr x, y⟩
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
t : α ⊕ β → Type u_9
x : α
y : t (inl x)
⊢ (fun x ↦
        match x with
        | ⟨inl x, y⟩ => inl ⟨x, y⟩
        | ⟨inr x, y⟩ => inr ⟨x, y⟩)
      (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩) (inl ⟨x, y⟩)) =
    inl ⟨x, y⟩

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
t : α ⊕ β → Type u_9
x : β
y : t (inr x)
⊢ (fun x ↦
        match x with
        | ⟨inl x, y⟩ => inl ⟨x, y⟩
        | ⟨inr x, y⟩ => inr ⟨x, y⟩)
      (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩) (inr ⟨x, y⟩)) =
    inr ⟨x, y⟩

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
t : α ⊕ β → Type u_9
x : α
y : t (inl x)
⊢ (fun x ↦
        match x with
        | ⟨inl x, y⟩ => inl ⟨x, y⟩
        | ⟨inr x, y⟩ => inr ⟨x, y⟩)
      (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩) (inl ⟨x, y⟩)) =
    inl ⟨x, y⟩

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
t : α ⊕ β → Type u_9
x : β
y : t (inr x)
⊢ (fun x ↦
        match x with
        | ⟨inl x, y⟩ => inl ⟨x, y⟩
        | ⟨inr x, y⟩ => inr ⟨x, y⟩)
      (Sum.elim (fun a ↦ ⟨inl a.fst, a.snd⟩) (fun b ↦ ⟨inr b.fst, b.snd⟩) (inr ⟨x, y⟩)) =
    inr ⟨x, y⟩
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case none
α✝ : 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.12
β : Option α → Type u_9
f : (a : Option α) → β a
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) none = f none

pp: case some
α✝ : 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.12
β : Option α → Type u_9
f : (a : Option α) → β a
val✝ : α
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) (some val✝) = f (some val✝)

Tactic:
<;>

Goal state after:
case none
α✝ : 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.12
β : Option α → Type u_9
f : (a : Option α) → β a
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) none = f none

case some
α✝ : 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.12
β : Option α → Type u_9
f : (a : Option α) → β a
val✝ : α
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) (some val✝) = f (some val✝)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : p a
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

pp: case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

Tactic:
<;>

Goal state after:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : p a
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)

case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
h : p x
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x

pp: case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
h : ¬p x
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x

Tactic:
<;>

Goal state after:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
h : p x
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x

case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
h : ¬p x
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case left
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ (x ⊓ xᶜ).fst ≤ ⊥.fst

pp: case right
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ (x ⊓ xᶜ).snd ≤ ⊥.snd

Tactic:
<;>

Goal state after:
case left
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ (x ⊓ xᶜ).fst ≤ ⊥.fst

case right
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ (x ⊓ xᶜ).snd ≤ ⊥.snd
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case left
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤.fst ≤ (x ⊔ xᶜ).fst

pp: case right
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤.snd ≤ (x ⊔ xᶜ).snd

Tactic:
<;>

Goal state after:
case left
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤.fst ≤ (x ⊔ xᶜ).fst

case right
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤.snd ≤ (x ⊔ xᶜ).snd
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case fst
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x \ y).fst = (x ⊓ yᶜ).fst

pp: case snd
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x \ y).snd = (x ⊓ yᶜ).snd

Tactic:
<;>

Goal state after:
case fst
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x \ y).fst = (x ⊓ yᶜ).fst

case snd
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x \ y).snd = (x ⊓ yᶜ).snd
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case fst
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x ⇨ y).fst = (y ⊔ xᶜ).fst

pp: case snd
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x ⇨ y).snd = (y ⊔ xᶜ).snd

Tactic:
<;>

Goal state after:
case fst
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x ⇨ y).fst = (y ⊔ xᶜ).fst

case snd
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x ⇨ y).snd = (y ⊔ xᶜ).snd
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case zero
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
x : f 0
⊢ Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)
      ((fun x ↦
          Sigma.casesOn x fun n ↦
            Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
        ⟨0, x⟩) =
    ⟨0, x⟩

pp: case succ
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)
      ((fun x ↦
          Sigma.casesOn x fun n ↦
            Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
        ⟨n + 1, x⟩) =
    ⟨n + 1, x⟩

Tactic:
<;>

Goal state after:
case zero
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
x : f 0
⊢ Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)
      ((fun x ↦
          Sigma.casesOn x fun n ↦
            Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
        ⟨0, x⟩) =
    ⟨0, x⟩

case succ
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)
      ((fun x ↦
          Sigma.casesOn x fun n ↦
            Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
        ⟨n + 1, x⟩) =
    ⟨n + 1, x⟩
Module: Mathlib.Logic.Equiv.Basic

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
f : ℕ → Type u
x : f 0
⊢ (fun x ↦
        Sigma.casesOn x fun n ↦
          Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
      (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id) (inl x)) =
    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
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ (fun x ↦
        Sigma.casesOn x fun n ↦
          Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
      (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id) (inr ⟨n, x⟩)) =
    inr ⟨n, 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
f : ℕ → Type u
x : f 0
⊢ (fun x ↦
        Sigma.casesOn x fun n ↦
          Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
      (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id) (inl x)) =
    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
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ (fun x ↦
        Sigma.casesOn x fun n ↦
          Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩)
      (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id) (inr ⟨n, x⟩)) =
    inr ⟨n, x⟩
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case zero
α : 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 succ (fun x ↦ 0) ((fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) 0) = 0

pp: case succ
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
n✝ : ℕ
⊢ Sum.elim succ (fun x ↦ 0) ((fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) (n✝ + 1)) = n✝ + 1

Tactic:
<;>

Goal state after:
case zero
α : 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 succ (fun x ↦ 0) ((fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) 0) = 0

case succ
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
n✝ : ℕ
⊢ Sum.elim succ (fun x ↦ 0) ((fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) (n✝ + 1)) = n✝ + 1
Module: Mathlib.Logic.Equiv.Basic

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
val✝ : ℕ
⊢ (fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) (Sum.elim succ (fun x ↦ 0) (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
val✝ : PUnit
⊢ (fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) (Sum.elim succ (fun x ↦ 0) (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
val✝ : ℕ
⊢ (fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) (Sum.elim succ (fun x ↦ 0) (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
val✝ : PUnit
⊢ (fun n ↦ Nat.casesOn n (inr PUnit.unit) inl) (Sum.elim succ (fun x ↦ 0) (inr val✝)) = inr val✝
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case ofNat
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
m : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc ((fun z ↦ Int.casesOn z inl inr) (Int.ofNat m)) = Int.ofNat m

pp: case negSucc
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
n : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc ((fun z ↦ Int.casesOn z inl inr) (Int.negSucc n)) = Int.negSucc n

Tactic:
<;>

Goal state after:
case ofNat
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
m : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc ((fun z ↦ Int.casesOn z inl inr) (Int.ofNat m)) = Int.ofNat m

case negSucc
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
n : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc ((fun z ↦ Int.casesOn z inl inr) (Int.negSucc n)) = Int.negSucc n
Module: Mathlib.Logic.Equiv.Basic

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
m : ℕ
⊢ (fun z ↦ Int.casesOn z inl inr) (Sum.elim Int.ofNat Int.negSucc (inl m)) = inl m

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
n : ℕ
⊢ (fun z ↦ Int.casesOn z inl inr) (Sum.elim Int.ofNat Int.negSucc (inr n)) = inr n

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
m : ℕ
⊢ (fun z ↦ Int.casesOn z inl inr) (Sum.elim Int.ofNat Int.negSucc (inl m)) = inl m

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
n : ℕ
⊢ (fun z ↦ Int.casesOn z inl inr) (Sum.elim Int.ofNat Int.negSucc (inr n)) = inr n
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case e'_3
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a = a ∆ ⊥

pp: case e'_4
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b = b ∆ ⊥

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a = a ∆ ⊥

case e'_4
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b = b ∆ ⊥
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : r = a
⊢ a = r

pp: case neg
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : ¬r = a
⊢ r = r

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : r = a
⊢ a = r

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : ¬r = a
⊢ r = r
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : b = a
⊢ b = r

pp: case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : r = a
h✝¹ : ¬b = a
h✝ : b = b
⊢ a = r

pp: case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : r = a
h✝¹ : ¬b = a
h✝ : ¬b = b
⊢ b = r

pp: case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : ¬r = a
h✝¹ : r = b
h✝ : a = a
⊢ b = r

pp: case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝³ : ¬r = a
h✝² : r = b
h✝¹ : ¬a = a
h✝ : a = b
⊢ a = r

pp: case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝³ : ¬r = a
h✝² : r = b
h✝¹ : ¬a = a
h✝ : ¬a = b
⊢ a = r

pp: case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : ¬r = b
⊢ r = r

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : b = a
⊢ b = r

case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : r = a
h✝¹ : ¬b = a
h✝ : b = b
⊢ a = r

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : r = a
h✝¹ : ¬b = a
h✝ : ¬b = b
⊢ b = r

case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝² : ¬r = a
h✝¹ : r = b
h✝ : a = a
⊢ b = r

case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝³ : ¬r = a
h✝² : r = b
h✝¹ : ¬a = a
h✝ : a = b
⊢ a = r

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝³ : ¬r = a
h✝² : r = b
h✝¹ : ¬a = a
h✝ : ¬a = b
⊢ a = r

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : ¬r = b
⊢ r = r
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : r = b
⊢ b = a

pp: case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : ¬r = b
⊢ b = b

pp: case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : r = b
⊢ a = a

pp: case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : ¬r = b
⊢ r = r

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : r = b
⊢ b = a

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : r = a
h✝ : ¬r = b
⊢ b = b

case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : r = b
⊢ a = a

case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h✝¹ : ¬r = a
h✝ : ¬r = b
⊢ r = r
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case le
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

pp: case lt
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

pp: case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

pp: case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

pp: case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ e ⊥ = ⊥

pp: case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b

Tactic:
<;>

Goal state after:
case le
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ e ⊥ = ⊥

case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b