α : Type u_1
β : Type u_2
γ : Type u_4
δ : Type u_3
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this : Nonempty γ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
α : Type u_1
β : Type u_2
γ : Type u_4
δ : Type u_3
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
haveI := Nonempty.map f ‹_›
α : Type u_1
β : Type u_2
γ : Type u_4
δ : Type u_3
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this✝ : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
α : Type u_1
β : Type u_2
γ : Type u_4
δ : Type u_3
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this : Nonempty γ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
haveI := Nonempty.map g ‹_›
no goals
α : Type u_1
β : Type u_2
γ : Type u_4
δ : Type u_3
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this✝ : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
exact (map_injective.and map_surjective).trans (and_and_and_comm)