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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a b : α
⊢ (swap a b) b = a

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a b x : α
⊢ x ≠ a → x ≠ b → (swap a b) x = x

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
x y : α
h : swap x y = Equiv.refl α
⊢ (Equiv.refl α) x = (Equiv.refl α) y

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
x y : α
⊢ x = y → swap x y = Equiv.refl α

Tactic:
grind

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

Goal state before:
pp: case mk
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
toFun✝ invFun✝ : α → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ ({ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (swap a b)) x =
    if { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = a then b
    else
      if { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = b then a
      else { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x

Tactic:
rfl

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
i j : α
⊢ ⇑(swap i j) = update (update id j i) i j

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
i j : α
f : α → β
⊢ f ∘ ⇑(swap i j) = update (update f j (f i)) i (f j)

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
e : α ≃ β
⊢ (e.symm.trans (swap a b)).trans e = swap (e a) (e b)

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
i j a : α
⊢ (swap i j) ((swap i j) a) = a

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
⊢ v ((swap i j) k) = v k

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
x y z w : α
⊢ (swap x y) z = w ↔ z = (swap x y) w

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a b x : α
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case lt
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rfl

Goal state after:
case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rfl

Goal state after:
case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
distribLattice : DistribLattice α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rfl

Goal state after:
case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Logic.Equiv.Prod

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
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ LeftInverse (fun x ↦ ⟨e₁.symm x.fst, e₂.symm x.snd⟩) fun x ↦ ⟨e₁ x.fst, e₂ x.snd⟩

Tactic:
grind

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

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
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ RightInverse (fun x ↦ ⟨e₁.symm x.fst, e₂.symm x.snd⟩) fun x ↦ ⟨e₁ x.fst, e₂ x.snd⟩

Tactic:
grind

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

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
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun ab ↦ ((e ab.snd).symm ab.fst, ab.snd)) fun ab ↦ ((e ab.snd) ab.fst, ab.snd)

Tactic:
grind

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

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
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ RightInverse (fun ab ↦ ((e ab.snd).symm ab.fst, ab.snd)) fun ab ↦ ((e ab.snd) ab.fst, ab.snd)

Tactic:
grind

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

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
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun ab ↦ (ab.fst, (e ab.fst).symm ab.snd)) fun ab ↦ (ab.fst, (e ab.fst) ab.snd)

Tactic:
grind

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

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
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ RightInverse (fun ab ↦ (ab.fst, (e ab.fst).symm ab.snd)) fun ab ↦ (ab.fst, (e ab.fst) ab.snd)

Tactic:
grind

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ⟨((sigmaEquivProd α₁ β₁).symm (a, b)).fst,
      (e ((sigmaEquivProd α₁ β₁).symm (a, b)).fst) ((sigmaEquivProd α₁ β₁).symm (a, b)).snd⟩ =
    (sigmaEquivProd α₁ β₂).symm (a, (e a) b)

Tactic:
rfl

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

Goal state before:
pp: case le
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

Tactic:
rfl

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

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
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun y ↦ (e₁.symm y.fst, (e₂ (e₁.symm y.fst)).symm y.snd)) fun x ↦ (e₁ x.fst, (e₂ x.fst) x.snd)

Tactic:
grind

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

Goal state before:
pp: case lt
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

Tactic:
rfl

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

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
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
⊢ RightInverse (fun y ↦ (e₁.symm y.fst, (e₂ (e₁.symm y.fst)).symm y.snd)) fun x ↦ (e₁ x.fst, (e₂ x.fst) x.snd)

Tactic:
grind

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)

Tactic:
by
  simp_rw [← symmDiff_assoc, symmDiff_comm]

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

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
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
⊢ LeftInverse (fun ab ↦ if ab.fst = a then (a, (Equiv.symm e) ab.snd) else ab) fun ab ↦
    if ab.fst = a then (a, e ab.snd) else ab

Tactic:
grind

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

Goal state before:
pp: case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

Tactic:
rfl

Goal state after:
case map_sup
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Logic.Equiv.Prod

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
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
⊢ RightInverse (fun ab ↦ if ab.fst = a then (a, (Equiv.symm e) ab.snd) else ab) fun ab ↦
    if ab.fst = a then (a, e ab.snd) else ab

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)

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
P : α → Sort u_9
e : α ≃ β
f : (a : α) → P a
⊢ (fun f x ↦ ⋯ ▸ f (e x)) ((fun f x ↦ f (e.symm x)) f) = f

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
P : α → Sort u_9
e : α ≃ β
f : (b : β) → P (e.symm b)
⊢ (fun f x ↦ f (e.symm x)) ((fun f x ↦ ⋯ ▸ f (e x)) f) = f

Tactic:
grind

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

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
π : ι ⊕ ι' → Type u_9
f : (i : ι ⊕ ι') → π i
i : ι
⊢ (fun g t ↦ Sum.rec g.fst g.snd t) ((fun f ↦ (fun i ↦ f (inl i), fun i' ↦ f (inr i'))) f) (inl i) = f (inl i)

Tactic:
rfl

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

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
π : ι ⊕ ι' → Type u_9
f : (i : ι ⊕ ι') → π i
i : ι'
⊢ (fun g t ↦ Sum.rec g.fst g.snd t) ((fun f ↦ (fun i ↦ f (inl i), fun i' ↦ f (inr i'))) f) (inr i) = f (inr i)

Tactic:
rfl

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

Goal state before:
pp: case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

Tactic:
rfl

Goal state after:
case map_inf
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: ι : Type u_10
ι' : Type u_11
ι'' : Sort u_12
π : ι'' → Type u_9
e : ι ⊕ ι' ≃ ι''
f : (i : ι) → π (e (inl i))
g : (i : ι') → π (e (inr i))
i : ι
⊢ (piCongrLeft π e) ((sumPiEquivProdPi fun x ↦ π (e x)).symm (f, g)) (e (inl i)) = f i

Tactic:
grind

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

Goal state before:
pp: ι : Type u_10
ι' : Type u_11
ι'' : Sort u_12
π : ι'' → Type u_9
e : ι ⊕ ι' ≃ ι''
f : (i : ι) → π (e (inl i))
g : (i : ι') → π (e (inr i))
j : ι'
⊢ (piCongrLeft π e) ((sumPiEquivProdPi fun x ↦ π (e x)).symm (f, g)) (e (inr j)) = g j

Tactic:
grind

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

Goal state before:
pp: case map_top
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤

Tactic:
rfl

Goal state after:
case map_top
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊤ = ⊤
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥

Tactic:
rfl

Goal state after:
case map_bot
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := ⋯
compl : Compl α := ⋯
himp : HImp α := ⋯
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := ⋯
⊢ e ⊥ = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case map_compl
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

Tactic:
rfl

Goal state after:
case map_compl
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ
Module: Mathlib.Logic.Equiv.Prod

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
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
val✝ : α
⊢ (fun p ↦ Sum.elim p.fst p.snd) ((fun f ↦ (f ∘ inl, f ∘ inr)) f) (inl val✝) = f (inl val✝)

Tactic:
rfl

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

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
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
val✝ : β
⊢ (fun p ↦ Sum.elim p.fst p.snd) ((fun f ↦ (f ∘ inl, f ∘ inr)) f) (inr val✝) = f (inr val✝)

Tactic:
rfl

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

Goal state before:
pp: case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝

Tactic:
rfl

Goal state after:
case map_sdiff
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: case map_himp
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝

Tactic:
rfl

Goal state after:
case map_himp
α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
top : Top α := e.top
compl : Compl α := e.compl
himp : HImp α := e.himp
generalizedBooleanAlgebra : GeneralizedBooleanAlgebra α := e.generalizedBooleanAlgebra
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: case mk
α✝ : 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
fst✝ : α → γ
snd✝ : β → γ
⊢ (fun f ↦ (f ∘ inl, f ∘ inr)) ((fun p ↦ Sum.elim p.fst p.snd) (fst✝, snd✝)) = (fst✝, snd✝)

Tactic:
rfl

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

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
snd✝ : γ
val✝ : α
⊢ (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s)
      ((fun p ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst) (inl val✝, snd✝)) =
    (inl val✝, snd✝)

Tactic:
rfl

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

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
snd✝ : γ
val✝ : β
⊢ (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s)
      ((fun p ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst) (inr val✝, snd✝)) =
    (inr val✝, snd✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Set.SymmDiff

Goal state before:
pp: α : Type u
s t u : Set α
⊢ (s ∪ t) ∆ u ⊆ s ∆ u ∪ t ∆ u

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Set.SymmDiff

Goal state before:
pp: α : Type u
s t u : Set α
⊢ s ∆ (t ∪ u) ⊆ s ∆ t ∪ s ∆ u

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Set.SymmDiff

Goal state before:
pp: α : Type u
s t u v : Set α
⊢ (s ∪ t) ∆ (u ∪ v) ⊆ s ∆ u ∪ t ∆ v

Tactic:
grind

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

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
fst✝ : α
snd✝ : γ
⊢ (fun p ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst)
      ((fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) (inl (fst✝, snd✝))) =
    inl (fst✝, snd✝)

Tactic:
rfl

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

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
fst✝ : β
snd✝ : γ
⊢ (fun p ↦ Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst)
      ((fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) (inr (fst✝, snd✝))) =
    inr (fst✝, snd✝)

Tactic:
rfl

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

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
⊢ LeftInverse (fun p ↦ (⟨p.fst, p.snd.fst⟩, p.snd.snd)) fun p ↦ ⟨p.fst.fst, (p.fst.snd, p.snd)⟩

Tactic:
grind

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

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
⊢ RightInverse (fun p ↦ (⟨p.fst, p.snd.fst⟩, p.snd.snd)) fun p ↦ ⟨p.fst.fst, (p.fst.snd, p.snd)⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
compl_sup_distrib,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a \ b)ᶜ ⊓ (b \ a)ᶜ = a ⇔ b
Module: Mathlib.Logic.Equiv.Prod

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.13
snd✝ : α
⊢ Sum.elim (Prod.mk false) (Prod.mk true) ((fun p ↦ if p.fst = true then inr p.snd else inl p.snd) (false, snd✝)) =
    (false, snd✝)

Tactic:
rfl

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

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.13
snd✝ : α
⊢ Sum.elim (Prod.mk false) (Prod.mk true) ((fun p ↦ if p.fst = true then inr p.snd else inl p.snd) (true, snd✝)) =
    (true, snd✝)

Tactic:
rfl

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

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.13
val✝ : α
⊢ (fun p ↦ if p.fst = true then inr p.snd else inl p.snd) (Sum.elim (Prod.mk false) (Prod.mk true) (inl val✝)) =
    inl val✝

Tactic:
rfl

Goal state after: