no goals
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' range fᶜ
classical
rintro _ ⟨y, rfl⟩
rw [extend_def]
split_ifs with h
exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]
case intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ extend f g g' y ∈ range g ∪ g' '' range fᶜ
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
⊢ range (extend f g g') ⊆ range g ∪ g' '' range fᶜ
rintro _ ⟨y, rfl⟩
case intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ (if h : ∃ a, f a = y then g (Classical.choose h) else g' y) ∈ range g ∪ g' '' range fᶜ
case intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ extend f g g' y ∈ range g ∪ g' '' range fᶜ
rw [extend_def]
case intro.inl
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ a, f a = y
⊢ g (Classical.choose h) ∈ range g ∪ g' '' range fᶜ

case intro.inr
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
y : β
h : ¬∃ a, f a = y
⊢ g' y ∈ range g ∪ g' '' range fᶜ
case intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ (if h : ∃ a, f a = y then g (Classical.choose h) else g' y) ∈ range g ∪ g' '' range fᶜ
split_ifs with h
no goals
case intro.inl
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ a, f a = y
⊢ g (Classical.choose h) ∈ range g ∪ g' '' range fᶜ

case intro.inr
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.4057
π : α → Type ?u.4062
f : α → β
g : α → γ
g' : β → γ
y : β
h : ¬∃ a, f a = y
⊢ g' y ∈ range g ∪ g' '' range fᶜ
exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]