case pos
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range (if p then f else g) ⊆ range f ∪ range g

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range (if p then f else g) ⊆ range f ∪ range g
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
⊢ range (if p then f else g) ⊆ range f ∪ range g
by_cases h : p
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range f ⊆ range f ∪ range g
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range (if p then f else g) ⊆ range f ∪ range g
rw [if_pos h]
no goals
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range f ⊆ range f ∪ range g
exact subset_union_left _ _
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range g ⊆ range f ∪ range g
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range (if p then f else g) ⊆ range f ∪ range g
rw [if_neg h]
no goals
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.93171
ι : Sort ?u.93174
ι' : Sort ?u.93177
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range g ⊆ range f ∪ range g
exact subset_union_right _ _