mathlib-initiative/mathlib-tactics huggingface dataset:
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✝

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✝

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✝

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✝

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

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

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

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✝

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✝

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✝

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

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

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

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

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

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

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

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

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

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

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

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

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

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✝)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: 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'

pp: 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'

Tactic:
<;>

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

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

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

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case fst
α✝ : 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 : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g))).fst =
    (f, g).fst

pp: case snd
α✝ : 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 : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g))).snd =
    (f, g).snd

Tactic:
<;>

Goal state after:
case fst
α✝ : 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 : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g))).fst =
    (f, g).fst

case snd
α✝ : 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 : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f ↦ (fun x ↦ f ↑x, fun x ↦ f ↑x)) ((fun f x ↦ if h : p x then f.fst ⟨x, h⟩ else f.snd ⟨x, h⟩) (f, g))).snd =
    (f, g).snd
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: case fst
α✝ : 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)).fst = f.fst

pp: case snd
α✝ : 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)
x : { j // j ≠ i }
⊢ ((fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f)).snd x = f.snd x

Tactic:
<;>

Goal state after:
case fst
α✝ : 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)).fst = f.fst

case snd
α✝ : 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)
x : { j // j ≠ i }
⊢ ((fun f ↦ (f i, fun j ↦ f ↑j)) ((fun f j ↦ if h : j = i then ⋯ ▸ f.fst else f.snd ⟨j, h⟩) f)).snd x = f.snd x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : ¬i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : ¬i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g = update (s.piecewise f g) j (f j)

Tactic:
simp +unfoldPartialApp only [piecewise, mem_insert_iff]
  ext i
  by_cases h : i = j
  · rw [h]
    simp
  · by_cases h' : i ∈ s <;> simp [h, h']

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

Goal state before:
pp: case h₁
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ ∀ (i : α), i ∈ s → f₁ i ≤ s.piecewise g₁ g₂ i

pp: case h₂
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ ∀ (i : α), ¬i ∈ s → f₂ i ≤ s.piecewise g₁ g₂ i

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ ∀ (i : α), i ∈ s → f₁ i ≤ s.piecewise g₁ g₂ i

case h₂
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ ∀ (i : α), ¬i ∈ s → f₂ i ≤ s.piecewise g₁ g₂ i
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case h₁
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : i✝ ∈ s
⊢ f₁ i✝ ≤ s.piecewise g₁ g₂ i✝

pp: case h₂
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : ¬i✝ ∈ s
⊢ f₂ i✝ ≤ s.piecewise g₁ g₂ i✝

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : i✝ ∈ s
⊢ f₁ i✝ ≤ s.piecewise g₁ g₂ i✝

case h₂
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : ¬i✝ ∈ s
⊢ f₂ i✝ ≤ s.piecewise g₁ g₂ i✝
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
h✝ : a ∈ s
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

pp: case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
h✝ : ¬a ∈ s
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
h✝ : a ∈ s
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
h✝ : ¬a ∈ s
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h✝ : x ∈ s
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

pp: case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h✝ : ¬x ∈ s
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h✝ : x ∈ s
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
h✝ : ¬x ∈ s
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x

pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x

pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x

case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inl ↔ Sum.inl val✝ ∈ {x | x.isLeft = true}

pp: case inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inl ↔ Sum.inr val✝ ∈ {x | x.isLeft = true}

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inl ↔ Sum.inl val✝ ∈ {x | x.isLeft = true}

case inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inl ↔ Sum.inr val✝ ∈ {x | x.isLeft = true}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inr ↔ Sum.inl val✝ ∈ {x | x.isRight = true}

pp: case inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inr ↔ Sum.inr val✝ ∈ {x | x.isRight = true}

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inr ↔ Sum.inl val✝ ∈ {x | x.isRight = true}

case inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inr ↔ Sum.inr val✝ ∈ {x | x.isRight = true}