mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.BooleanAlgebra.Defs

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
⊢ ∀ (x y z : PUnit), min (max x y) (max x z) ≤ max x (min y z)

Tactic:
simp

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: case e'_3
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ x = map (e.trans e.symm) x

Tactic:
simp

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: case e'_3
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ y = map (e.symm.trans e) y

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
x : α
⊢ x ∈ s ∧ ¬x ∈ t ↔ x ∈ s ∩ tᶜ

Tactic:
simp

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

Goal state before:
pp: case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (e (some x)) = some x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ s \ {a} ⊆ t ↔ s ⊆ insert a t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
x : α
⊢ e.optionCongr (some x) = some (e x)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ ↑((fun a ↦ ⟨↑e (some a), ⋯⟩) ((fun b ↦ ((↑e).symm ↑b).get ⋯) b)) = ↑b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ s \ {a} ⊂ s ↔ a ∈ s

Tactic:
simp

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
⊢ (fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) ((fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) none) = none

Tactic:
simp

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
val✝ : α
⊢ ↑((fun e ↦
            ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
              ⋯⟩)
          ((fun e ↦
              { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                right_inv := ⋯ })
            e))
      (some val✝) =
    ↑e (some val✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ some
      (({
              toFun := fun e ↦
                { toFun := fun a ↦ ⟨↑e (some a), ⋯⟩, invFun := fun b ↦ ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                  right_inv := ⋯ },
              invFun := fun e ↦
                ⟨{ toFun := fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e),
                    invFun := fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯, right_inv := ⋯ },
                  ⋯⟩,
              left_inv := ⋯, right_inv := ⋯ }
            e).symm
        b) =
    (↑e).symm ↑b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : { y // y ≠ x }
⊢ (↑((optionSubtype x).symm e)).symm ↑b = some (e.symm b)

Tactic:
by
  simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk,
             Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
  exact fun h => False.elim (b.property h)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (optionSubtypeNe a).symm a = none

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_4
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
⊢ ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ b₁ ≍ b₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: case inl
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
jb : β ia
⊢ update f ⟨ia, ib⟩ x ⟨ia, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ia jb

Tactic:
simp

Goal state after:
case inl
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
jb : β ia
⊢ update f ⟨ia, ib⟩ x ⟨ia, jb⟩ = update (fun y ↦ f ⟨ia, y⟩) ib x jb
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
⊢ GeneralizedCoheytingAlgebra α

Tactic:
apply e.injective.generalizedCoheytingAlgebra

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ e ⊥ = ⊥

case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ ∀ (a b : α), e (a \ b) = e a \ e b
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
simp

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

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

Tactic:
simp

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.23
α₂ : Type ?u.25
β₁ : Type ?u.22
β₂ : Type ?u.24
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
x : α₁ ⊕ β₁
⊢ Sum.map (⇑ea.symm) (⇑eb.symm) (Sum.map (⇑ea) (⇑eb) x) = x

Tactic:
simp

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.23
α₂ : Type ?u.25
β₁ : Type ?u.22
β₂ : Type ?u.24
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
x : α₂ ⊕ β₂
⊢ Sum.map (⇑ea) (⇑eb) (Sum.map (⇑ea.symm) (⇑eb.symm) x) = x

Tactic:
simp

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
e₁ : α ≃ β
e₂ : γ ≃ δ
x : α
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)) (PSum.inl x)) =
    PSum.inl x

Tactic:
simp

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
e₁ : α ≃ β
e₂ : γ ≃ δ
x : γ
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)) (PSum.inr x)) =
    PSum.inr x

Tactic:
simp

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
e₁ : α ≃ β
e₂ : γ ≃ δ
x : β
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) (PSum.inl x)) =
    PSum.inl x

Tactic:
simp

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
e₁ : α ≃ β
e₂ : γ ≃ δ
x : δ
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) (PSum.inr x)) =
    PSum.inr x

Tactic:
simp

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.18
β : Type ?u.17
γ : Type ?u.15
⊢ RightInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr)) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))

Tactic:
rintro (_ | ⟨_ | _⟩)

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.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✝

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✝)

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✝)
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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
a : α
⊢ (⇑(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)
        (inl (inl a))) =
    inl (inl a)

Tactic:
simp

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
b : β
⊢ (⇑(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)
        (inl (inr b))) =
    inl (inr b)

Tactic:
simp

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
c : γ
⊢ (⇑(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)
        (inr (inl c))) =
    inr (inl c)

Tactic:
simp

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
d : δ
⊢ (⇑(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)
        (inr (inr d))) =
    inr (inr d)

Tactic:
simp

Goal state after:
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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
a : α
⊢ (⇑(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)
        (inl (inl a))) =
    inl (inl a)

Tactic:
simp

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
c : γ
⊢ (⇑(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)
        (inl (inr c))) =
    inl (inr c)

Tactic:
simp

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
b : β
⊢ (⇑(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)
        (inr (inl b))) =
    inr (inl b)

Tactic:
simp

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.19
β : Type ?u.18
γ : Type ?u.21
δ : Type ?u.20
d : δ
⊢ (⇑(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)
        (inr (inr d))) =
    inr (inr d)

Tactic:
simp

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

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
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⟩

Tactic:
simp

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

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
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⟩

Tactic:
simp

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

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 ⊓ y \ z

Tactic:
sup_inf_left

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

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

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

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

Tactic:
by
  simpa using lt_compl_self (a := xᶜ)

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

Tactic:
simp

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

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

Tactic:
simp

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:
constructor <;> simp

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

Tactic:
simp

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

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

Tactic:
simp

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:
constructor <;> simp

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

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

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

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

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
e : α ≃ β
⊢ ∀ (a : α), p (e a) ↔ p (e a)

Tactic:
simp

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
x✝ : { f // ∀ (i : ι), (f i).fst = i }
f : ι → (i : ι) × π i
hf : ∀ (i : ι), (f i).fst = i
i : ι
⊢ (↑((fun f ↦ ⟨fun i ↦ ⟨i, f i⟩, ⋯⟩) ((fun f i ↦ ⋯.mpr (↑f i).snd) ⟨f, hf⟩)) i).snd ≍ (↑⟨f, hf⟩ i).snd

Tactic:
simp

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

Goal state before:
pp: case refl
α✝ : 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 : Sigma β
x✝ : { s // s.fst = a.fst }
⊢ (fun b ↦ ⟨⟨a.fst, b⟩, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨⟨fst, b⟩, h⟩ => h ▸ b)
        ⟨a, ⋯⟩) =
    ⟨a, ⋯⟩

Tactic:
simp

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 : α
b : β a
⊢ (fun x ↦
        match x with
        | ⟨⟨fst, b⟩, h⟩ => h ▸ b)
      ((fun b ↦ ⟨⟨a, b⟩, ⋯⟩) b) =
    b

Tactic:
simp

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

Goal state after: