α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ ∀ (y : α), (if p y then f y else g y) ∈ range f ∪ range g
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ (range fun x => if p x then f x else g x) ⊆ range f ∪ range g
rw [range_subset_iff]
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
⊢ (if p x then f x else g x) ∈ range f ∪ range g
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ ∀ (y : α), (if p y then f y else g y) ∈ range f ∪ range g
intro x
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : ¬p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
⊢ (if p x then f x else g x) ∈ range f ∪ range g
by_cases h : p x
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : ¬p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : ¬p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g
simp [if_pos h, mem_union, mem_range_self]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.93493
ι : Sort ?u.93496
ι' : Sort ?u.93499
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : ¬p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g
simp [if_neg h, mem_union, mem_range_self]