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_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ Sum.inl ⟨x, ?inl.hc⟩ = Sum.inl ⟨x, hx⟩

pp: case inl.hc
α✝ : 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
⊢ p x

Tactic:
]

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_9
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ Sum.inr ⟨x, ?inr.hnc⟩ = Sum.inr ⟨x, hx⟩

pp: case inr.hnc
α✝ : 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
⊢ ¬p x

Tactic:
]

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:
← sup_inf_right

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x = z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x
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 ⊓ z \ y ⊔ z ⊓ y ⊓ x

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)
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 rcases p with (⟨i, a⟩ | ⟨i, b⟩) <;> rfl

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) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

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 ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y)

Tactic:
]

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 < x ⊔ z \ x

Tactic:
]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < x ⊔ z \ x
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ (z \ x) \ x ≤ y
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:
]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z \ y ⊔ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
]

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
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x

Tactic:
]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x
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:
]

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

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

Tactic:
]

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 = a

Tactic:
]

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

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

Tactic:
]

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

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

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 rw [sdiff_eq, top_inf_eq]

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

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

Tactic:
]

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl yᶜ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
]

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x xᶜ
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state after:
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
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ y ≤ z → (xᶜ ≤ z ↔ Codisjoint x z)

Tactic:
]

Goal state after:
α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ y ≤ z → (xᶜ ≤ z ↔ Codisjoint x z)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
]

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤
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 : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ x ⟨a, h⟩ = x ⟨a, h⟩

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

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 = f a

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : a ≤ b
⊢ b \ a = b \ a

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a \ b = a \ b

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : Disjoint a b
⊢ a ⊔ b = a ⊔ b

Tactic:
]

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 : α
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)

Tactic:
]

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.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π (↑f i).fst

Tactic:
]

Goal state after:
α : 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.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π (↑f i).fst
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a

Tactic:
]

Goal state after:
case refine_1
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)

Tactic:
]

Goal state after:
case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)
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✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
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_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊥ = ⊥

Tactic:
]

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
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
h : p ⟨a, b⟩
⊢ γ (↑⟨⟨a, b⟩, h⟩).fst (↑⟨⟨a, b⟩, h⟩).snd = γ a b

Tactic:
]

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

Goal state before:
pp: α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
c : γ a b
h : p ⟨a, b⟩
⊢ c = (sigmaSigmaSubtype p h) ⟨⟨a, ⟨b, c⟩⟩, h⟩

Tactic:
]

Goal state after:
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
c : γ a b
h : p ⟨a, b⟩
⊢ c = (sigmaSigmaSubtype p h) ⟨⟨a, ⟨b, c⟩⟩, h⟩
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b)

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
h : IsCompl a b
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
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 }
a b : α
hab : a ≈ b
⊢ p₂ ⟦b⟧ = p₂ ⟦b⟧

Tactic:
]

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✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
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_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b \ a = b \ a

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a \ b = a \ b

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b ⊓ a = b ⊓ a

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b
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✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
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_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
⊢ f a ⊓ (f b)ᶜ = f a ⊓ (f b)ᶜ

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint a b ↔ Disjoint a b

Tactic:
]

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✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
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_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
⊢ f b ⊔ (f a)ᶜ = f b ⊔ (f a)ᶜ

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a c d : α
h : swap a c = swap a d
⊢ d = d

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

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

Goal state before:
pp: case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ j ∈ insert j s \ {a}

Tactic:
]

Goal state after:
case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ j ∈ insert j s \ {a}
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}

Tactic:
]

Goal state after:
case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ g (e (e.symm b)) ≍ g b

Tactic:
]

Goal state after:
α : Sort u_1
β : Sort u_4
P : α → Sort u_9
e : α ≃ β
g : (b : β) → P (e.symm b)
b : β
⊢ g (e (e.symm b)) ≍ g b
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ (h₂ a) (f a) = (h₂ a) (f a)

Tactic:
]

Goal state after: