mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Sum

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
x : (α ⊕ β) ⊕ γ ⊕ δ
⊢ (⇑(sumAssoc (α ⊕ β) γ δ) ∘
        Sum.map (⇑(sumAssoc α β γ).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
      ((⇑(sumAssoc (α ⊕ γ) β δ) ∘
          Sum.map (⇑(sumAssoc α γ β).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
        x) =
    x

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x)) = z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)

Tactic:
by

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

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
x : (α ⊕ γ) ⊕ β ⊕ δ
⊢ (⇑(sumAssoc (α ⊕ γ) β δ) ∘
        Sum.map (⇑(sumAssoc α γ β).symm) id ∘
          Sum.map (Sum.map id ⇑(sumComm β γ)) id ∘ Sum.map (⇑(sumAssoc α β γ)) id ∘ ⇑(sumAssoc (α ⊕ β) γ δ).symm)
      ((⇑(sumAssoc (α ⊕ β) γ δ) ∘
          Sum.map (⇑(sumAssoc α β γ).symm) id ∘
            Sum.map (Sum.map id ⇑(sumComm β γ).symm) id ∘ Sum.map (⇑(sumAssoc α γ β)) id ∘ ⇑(sumAssoc (α ⊕ γ) β δ).symm)
        x) =
    x

Tactic:
by

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

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.17
β : Type ?u.16
inst✝ : IsEmpty β
s : α ⊕ β
⊢ inl (Sum.elim id (fun a ↦ isEmptyElim a) s) = s

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y) ⊓ z \ (y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Tactic:
by

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

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.15
s : α ⊕ β
⊢ (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) s) =
    s

Tactic:
by

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

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.15
s : (b : Bool) × bif b 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)
        s) =
    s

Tactic:
by

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

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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
⊢ Option.elim' default Subtype.val ((fun a ↦ if h : a = default then none else some ⟨a, h⟩) a) = a

Tactic:
by

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

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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
⊢ (fun a ↦ if h : a = default then none else some ⟨a, h⟩) (Option.elim' default Subtype.val none) = none

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = (z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Tactic:
by

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

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
p : α → Prop
inst✝ : DecidablePred p
⊢ LeftInverse (fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) (Sum.elim Subtype.val Subtype.val)

Tactic:
by

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

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
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Sum.elim Subtype.val Subtype.val ((fun a ↦ if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩) a) = a

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x

Tactic:
by

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

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.20
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × (α i ⊕ β 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) p) =
    p

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y

Tactic:
by

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

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

Tactic:
by

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

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.20
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × α i ⊕ (i : ι) × β 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) p) =
    p

Tactic:
by

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

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.14
β : Type ?u.13
t : α ⊕ β → Type u_9
⊢ LeftInverse (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⟩

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)

Tactic:
by

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

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.14
β : Type ?u.13
t : α ⊕ β → Type u_9
⊢ RightInverse (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⟩

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x ⊓ x ⊓ (y ⊓ z ⊓ y \ z) = ⊥

Tactic:
by

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

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

Tactic:
inf_sdiff_assoc

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ y ⊓ x \ z = y ⊓ x \ z
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = b ⊓ a \ c

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ c

Tactic:
inf_sdiff_assoc

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = a ⊓ b \ c
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y) \ z = ⊥ ↔ x ⊓ y \ z = ⊥

Tactic:
inf_sdiff_assoc

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < z

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y ≤ z \ y ⊔ y

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : OrderTop α
a b : α
⊢ a \ b = a ⊓ ⊤ \ b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊔ a \ b = a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊓ a \ b = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a : α
⊢ ⊤ \ a = aᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl x y

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x y

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ = y ↔ yᶜ = x

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x = yᶜ ↔ y = xᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ xᶜ
⊢ x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ x
⊢ xᶜ ≤ y

Tactic:
by

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

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

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

Tactic:
by

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 : ε
h : p a
⊢ (ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u
x : α
inst✝¹ : BooleanAlgebra α
inst✝ : Nontrivial α
⊢ xᶜ < x ↔ x = ⊤

Tactic:
by

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 : ε
h : ¬p a
⊢ (ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x \ yᶜ = x ⊓ y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ Equiv.trans (ep.subtypeCongr en) (ep'.subtypeCongr en') = subtypeCongr (Equiv.trans ep ep') (Equiv.trans en en')

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ (x \ y)ᶜ = x ⇨ y

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ \ yᶜ = y \ x

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ Disjoint xᶜ y ↔ y ≤ x

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ Disjoint x yᶜ ↔ x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z

Tactic:
by

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
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
⊢ ↑((fun x ↦ ⟨fun a ↦ if h : p a then x₀ ⟨a, h⟩ else x ⟨a, h⟩, ⋯⟩) ((fun x a ↦ ↑x ↑a) ⟨x, hx⟩)) a = ↑⟨x, hx⟩ a

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ x ⊓ xᶜ ≤ ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤ ≤ x ⊔ xᶜ

Tactic:
by

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 u_9
β₂ : α → Sort u_10
F : (a : α) → β₁ a ≃ β₂ a
H : (a : α) → β₁ a
⊢ ∀ (x : α), Pi.map (fun a ↦ ⇑(F a).symm) (Pi.map (fun a ↦ ⇑(F a)) H) x = H x

Tactic:
by

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 u_9
β₂ : α → Sort u_10
F : (a : α) → β₁ a ≃ β₂ a
H : (a : α) → β₂ a
⊢ ∀ (x : α), Pi.map (fun a ↦ ⇑(F a)) (Pi.map (fun a ↦ ⇑(F a).symm) H) x = H x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
f : ℕ → Type u
⊢ LeftInverse (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⟩

Tactic:
by

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
f : ℕ → Type u
⊢ RightInverse (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⟩

Tactic:
by

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

Tactic:
by

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
⊢ RightInverse (Sum.elim succ fun x ↦ 0) fun n ↦ Nat.casesOn n (inr PUnit.unit) inl

Tactic:
by

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

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: ⊢ ∀ (p q : Bool), p ∆ q = (p ^^ q)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = b ∆ a

Tactic:
by

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 : { a // p a }
⊢ ↑((fun b ↦ ⟨e.symm ↑b, ⋯⟩) ((fun a ↦ ⟨e ↑a, ⋯⟩) a)) = ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ a = ⊥

Tactic:
by

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)
b : { b // q b }
⊢ ↑((fun a ↦ ⟨e ↑a, ⋯⟩) ((fun b ↦ ⟨e.symm ↑b, ⋯⟩) b)) = ↑b

Tactic:
by

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)
⊢ (Equiv.refl α).subtypeEquiv h = Equiv.refl { a // p a }

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ ⊥ = a

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ ⊥ ∆ a = a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f (a ⊓ b ⊔ a \ b) = f a

Tactic:
by

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
r : γ → Prop
e : α ≃ β
f : β ≃ γ
h : ∀ (a : α), p a ↔ q (e a)
h' : ∀ (b : β), q b ↔ r (f b)
⊢ ∀ (a : α), p a ↔ r ((e.trans f) a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = ⊥ ↔ a = b

Tactic:
by

Goal state after: