case intro.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c

case intro.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ a, f a = c
obtain ⟨a | b, h⟩ := h (inl c)
no goals
case intro.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c
exact ⟨a, inl_injective h⟩
no goals
case intro.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c
cases h
case intro.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d

case intro.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
⊢ ∃ a, g a = d
obtain ⟨a | b, h⟩ := h (inr d)
no goals
case intro.inl
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d
cases h
no goals
case intro.inr
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_2
δ : Type u_1
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d
exact ⟨b, inr_injective h⟩