α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
⊢ ∃ a, f a = c
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
⊢ ∃ a, f a = c
inhabit δ
case intro.mk
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
a : α
b : β
h : map f g (a, b) = (c, default)
⊢ ∃ a, f a = c
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
⊢ ∃ a, f a = c
obtain ⟨⟨a, b⟩, h⟩ := h (c, default)
no goals
case intro.mk
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
a : α
b : β
h : map f g (a, b) = (c, default)
⊢ ∃ a, f a = c
exact ⟨a, congr_arg Prod.fst h⟩
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
⊢ ∃ a, g a = d
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
⊢ ∃ a, g a = d
inhabit γ
case intro.mk
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
a : α
b : β
h : map f g (a, b) = (default, d)
⊢ ∃ a, g a = d
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
⊢ ∃ a, g a = d
obtain ⟨⟨a, b⟩, h⟩ := h (default, d)
no goals
case intro.mk
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
a : α
b : β
h : map f g (a, b) = (default, d)
⊢ ∃ a, g a = d
exact ⟨b, congr_arg Prod.snd h⟩