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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrLeft e).trans (prodComm β₂ α₁) = (prodComm β₁ α₁).trans (prodCongrRight e)

Tactic:
by

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) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrRight e).trans (prodComm α₁ β₂) = (prodComm α₁ β₁).trans (prodCongrLeft e)

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂) = (sigmaEquivProd α₁ β₁).trans (prodCongrRight e)

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e) = (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm

Tactic:
by

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

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)

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ Set.image (⇑(swap i j)) s ↔ a ∈ insert j s \ {i}

Tactic:
by

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

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

Goal state before:
pp: α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
⊢ (swap i j).sumCongr (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)

Tactic:
by

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 β₁
⊢ 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:
by

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

Goal state before:
pp: α : Type u_9
β : Type u_10
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
⊢ sumCongr (Equiv.refl α) (swap i j) = swap (Sum.inr i) (Sum.inr j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : (prodExtendRight a e) (a', b) ≠ (a', b)
⊢ a' = a

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
f : α ≃ β
a : α
b : β
⊢ (f.setValue a b) a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ ((prodExtendRight a e) ab).fst = ab.fst

Tactic:
by

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

Goal state after:
Module: Mathlib.Order.SymmDiff

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

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

Tactic:
by

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

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
⊢ (piCongrLeft' (fun x ↦ P) e).symm = piCongrLeft' (fun a ↦ P) e.symm

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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.14
ι' : Type ?u.13
π : ι ⊕ ι' → Type u_9
f : (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) = f

Tactic:
by

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

Tactic:
by

Goal state after:
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 : β
⊢ (piCongrLeft' P e).symm g (e.symm b) = g b

Tactic:
by

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))
i : ι
⊢ (piCongrLeft π e) ((sumPiEquivProdPi fun x ↦ π (e x)).symm (f, g)) (e (inl i)) = f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ b ⇔ c = a ⇔ c ⇔ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

Goal state after:
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₁.piCongr h₂) f (h₁ a) = (h₂ a) (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
⊢ BooleanAlgebra α

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ

Tactic:
by

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.18
β : Type ?u.17
γ : Type ?u.15
⊢ LeftInverse (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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s t : Set α
⊢ a ∈ s ⇔ t ↔ (a ∈ s ↔ a ∈ t)

Tactic:
by

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

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

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

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
x : α
hx : x ∈ t
⊢ x ∈ s

Tactic:
by

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

Goal state before:
pp: α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
⊢ ⇑ε₂.symm ∘ f ∘ ⇑ε₁.symm = f' ↔ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_11
β₁ : Type u_12
e : α₁ ≃ β₁
f : α₁ → α₁
x : α₁
⊢ e (f x) = e.conj f (e x)

Tactic:
by

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

Goal state before:
pp: α₁ : Type u_11
β₁ : Type u_12
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
x y : α₁
⊢ e (f x y) = (e.arrowCongr e.conj) f (e x) (e y)

Tactic:
by

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.18
β : Type ?u.17
γ : Type ?u.15
⊢ RightInverse (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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
α' : Sort u_9
inst✝¹ : DecidableEq α'
inst✝ : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
⊢ update f a v ∘ ⇑g = update (f ∘ ⇑g) (g.symm a) v

Tactic:
by

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

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P (e.symm b)
b' : β
⊢ (Equiv.piCongrLeft' P e) (update f (e.symm b) x) b' = update ((Equiv.piCongrLeft' P e) f) b x b'

Tactic:
rcases eq_or_ne b' b with (rfl | h)

Goal state after:
case inl
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b' : β
x : P (e.symm b')
⊢ (Equiv.piCongrLeft' P e) (update f (e.symm b') x) b' = update ((Equiv.piCongrLeft' P e) f) b' x b'

case inr
α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P (e.symm b)
b' : β
h : b' ≠ b
⊢ (Equiv.piCongrLeft' P e) (update f (e.symm b) x) b' = update ((Equiv.piCongrLeft' P e) f) b x b'
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P (e.symm b)
⊢ (Equiv.piCongrLeft' P e) (update f (e.symm b) x) = update ((Equiv.piCongrLeft' P e) f) b x

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (b : β) → P (e.symm b)
b : β
x : P (e.symm b)
⊢ (Equiv.piCongrLeft' P e).symm (update f b x) = update ((Equiv.piCongrLeft' P e).symm f) (e.symm b) x

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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

Tactic:
by

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
x✝ : Bool → α
⊢ (fun p b ↦ if b = true then p.snd else p.fst) ((fun f ↦ (f false, f true)) x✝) = x✝

Tactic:
by

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
p : α → Prop
β : α → Type u_10
inst✝ : DecidablePred p
f : (i : α) → β i
⊢ (fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

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
p : α → Prop
β : α → Type u_10
inst✝ : DecidablePred p
⊢ RightInverse (fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)

Tactic:
by

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
inst✝ : DecidableEq α
i : α
β : α → Type u_10
f : (j : α) → β j
⊢ (fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) ((fun f ↦ (f i, fun j ↦ f ↑j)) f) = f

Tactic:
by

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
inst✝ : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j // j ≠ i }) → β ↑j)
⊢ (fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ a ∆ c ⊔ b ∆ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Set β
h : ∀ (x : α), f x = g x
⊢ f ⁻¹' s = g ⁻¹' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
⊢ (fun x ↦ b) ⁻¹' s = if b ∈ s then univ else ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
⊢ preimage f^[n] = (preimage f)^[n]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Set (Subtype p)
t : Set α
⊢ s = Subtype.val ⁻¹' t ↔ ∀ (x : α) (h : p x), ⟨x, h⟩ ∈ s ↔ x ∈ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
f : α → β
⊢ (f ⁻¹' s).Nonempty ↔ (s ∩ range f).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ p ⁻¹' {True} = {a | p a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
⊢ p ⁻¹' {False} = {a | ¬p a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
⊢ Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
⊢ f ⁻¹' s ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
a : α
⊢ a ∈ s → f a ∈ f '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : β → Prop
⊢ (∀ (y : β), y ∈ f '' s → p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : β → Prop
⊢ (∃ y, y ∈ f '' s ∧ p y) ↔ ∃ x, x ∈ s ∧ p (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
⊢ f '' s = g '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ (x : α), f x = g x
⊢ f '' s = g '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : s ⊆ t
⊢ f '' s ⊆ f '' t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
a : Set α
⊢ f ∘ g '' a = f '' g '' a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ image (g ∘ f) = image g ∘ image f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ image g ∘ image f = image (g ∘ f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
β' : Type u_5
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ f '' g '' s = g' '' f' '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' (s ∪ t) = f '' s ∪ f '' t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ f '' ∅ = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ s → f x = f y → x = y
b : β
x✝ : b ∈ f '' s ∩ f '' t
a₁ : α
ha₁ : a₁ ∈ s
h₁ : f a₁ = b
a₂ : α
ha₂ : a₂ ∈ t
h₂ : f a₂ = b
⊢ f a₂ = f a₁

Tactic:
by

Goal state after: