α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.4909
π : α → Type ?u.4914
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range g ∪ g' '' range fᶜ ⊆ range (extend f g g')
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.4909
π : α → Type ?u.4914
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range (extend f g g') = range g ∪ g' '' range fᶜ
refine' (range_extend_subset _ _ _).antisymm _
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.4909
π : α → Type ?u.4914
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')

case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.4909
π : α → Type ?u.4914
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
y : β
hy : y ∈ range fᶜ
⊢ g' y ∈ range (extend f g g')
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.4909
π : α → Type ?u.4914
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range g ∪ g' '' range fᶜ ⊆ range (extend f g g')
rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)
no goals
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.4909
π : α → Type ?u.4914
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')

case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.4909
π : α → Type ?u.4914
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
y : β
hy : y ∈ range fᶜ
⊢ g' y ∈ range (extend f g g')
exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]