mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_hnot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝

Tactic:
rfl

Goal state after:
case map_hnot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ : α
⊢ e (￢a✝) = ￢e a✝
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
rfl

Goal state after:
case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
rfl

Goal state after:
case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
heytingAlgebra : HeytingAlgebra α := e.heytingAlgebra
coheytingAlgebra : CoheytingAlgebra α := e.coheytingAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e 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.17
β : Type ?u.16
val✝ : α
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) (PSum.inl val✝)) = PSum.inl val✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ≤ x
⊢ x \ (x \ y) = y

Tactic:
sdiff_sdiff_right_self,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ≤ x
⊢ x ⊓ y = y
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

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

Tactic:
rfl

Goal state after:
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⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
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:
rfl

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊔ x = ⊤

Tactic:
rw [sup_comm, sup_compl_eq_top]

Goal state after:
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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
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:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

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

Tactic:
by
  by_cases h : p a <;> simp [Perm.subtypeCongr, h]

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : p a
⊢ (x ∘ Subtype.val) ⟨a, h✝⟩ = x a

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case neg
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : ¬p a
⊢ x a = x a

Tactic:
rfl

Goal state after:
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⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
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:
rfl

Goal state after:
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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
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:
rfl

Goal state after:
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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
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:
rfl

Goal state after:
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✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
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:
rfl

Goal state after:
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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
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:
rfl

Goal state after:
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

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
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:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
p : α → Prop
h : ∀ (a : α), p a ↔ p ((Equiv.refl α) a)
x✝ : { a // p a }
⊢ ↑(((Equiv.refl α).subtypeEquiv h) x✝) = ↑((Equiv.refl { a // p a }) x✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ ∀ (a : β), q a ↔ p (e.symm a)

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → β a
h : ∀ (a : α), p a (f a)
⊢ (fun f ↦ ⟨fun a ↦ ↑(f a), ⋯⟩) ((fun f a ↦ ⟨↑f a, ⋯⟩) ⟨f, h⟩) = ⟨f, h⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α✝ : 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
β : Type u_10
γ : α → β → Type u_11
a' : α
b' : β
⊢ ⟨⟨a', b'⟩, ⋯⟩ = ⟨⟨a', b'⟩, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
⊢ (fun x' ↦ if h : x' ≠ x then f ⟨x', h⟩ else y) ∘ Subtype.val = f

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a✝ : α
ha : p₂ ⟦a✝⟧
⊢ (fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯)
      ((fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯) ⟨⟦a✝⟧, ha⟩) =
    ⟨⟦a✝⟧, ha⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a : { x // p₂ x }
⊢ (fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯)
      ((fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯) a) =
    a

Tactic:
obtain ⟨a, ha⟩ := a
    induction a using Quotient.inductionOn
    rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a✝ : Subtype p₁
⊢ (fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯)
      ((fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯) ⟦a✝⟧) =
    ⟦a✝⟧

Tactic:
rfl

Goal state after: