α : Type ?u.7362
α₁ : Type u_1
α₂ : Type u_2
β : α → Type ?u.7373
β₁ : α₁ → Type u_3
β₂ : α₂ → Type u_4
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = { fst := f₁ x, snd := b }
α : Type ?u.7362
α₁ : Type u_1
α₂ : Type u_2
β : α → Type ?u.7373
β₁ : α₁ → Type u_3
β₂ : α₂ → Type u_4
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ Surjective (Sigma.map f₁ f₂)
simp only [Function.Surjective, Sigma.forall, h₁.forall]
no goals
α : Type ?u.7362
α₁ : Type u_1
α₂ : Type u_2
β : α → Type ?u.7373
β₁ : α₁ → Type u_3
β₂ : α₂ → Type u_4
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = { fst := f₁ x, snd := b }
exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩