chore(*): a few lemmas about `range_splitting (#10016)

src/data/equiv/set.lean

@@ -447,6 +447,10 @@ begin
   simp [apply_of_injective_symm f hf],
 end
 
+lemma coe_of_injective_symm {α β} (f : α → β) (hf : injective f) :
+  ((of_injective f hf).symm : range f → α) = range_splitting f :=
+by { ext ⟨y, x, rfl⟩, apply hf, simp [apply_range_splitting f] }
+
 @[simp] lemma self_comp_of_injective_symm {α β} (f : α → β) (hf : injective f) :
   f ∘ ((of_injective f hf).symm) = coe :=
 funext (λ x, apply_of_injective_symm f hf x)

src/data/set/basic.lean

@@ -1846,6 +1846,8 @@ funext $ λ i, rfl
 @[simp] lemma range_factorization_coe (f : ι → β) (a : ι) :
   (range_factorization f a : β) = f a := rfl
 
+@[simp] lemma coe_comp_range_factorization (f : ι → β) : coe ∘ range_factorization f = f := rfl
+
 lemma surjective_onto_range : surjective (range_factorization f) :=
 λ ⟨_, ⟨i, rfl⟩⟩, ⟨i, rfl⟩
 
@@ -1916,6 +1918,16 @@ lemma left_inverse_range_splitting (f : α → β) :
 lemma range_splitting_injective (f : α → β) : injective (range_splitting f) :=
 (left_inverse_range_splitting f).injective
 
+lemma right_inverse_range_splitting {f : α → β} (h : injective f) :
+  right_inverse (range_factorization f) (range_splitting f) :=
+(left_inverse_range_splitting f).right_inverse_of_injective $
+  λ x y hxy, h $ subtype.ext_iff.1 hxy
+
+lemma preimage_range_splitting {f : α → β} (hf : injective f) :
+  preimage (range_splitting f) = image (range_factorization f) :=
+(image_eq_preimage_of_inverse (right_inverse_range_splitting hf)
+  (left_inverse_range_splitting f)).symm
+
 lemma is_compl_range_some_none (α : Type*) :
   is_compl (range (some : α → option α)) {none} :=
 ⟨λ x ⟨⟨a, ha⟩, (hn : x = none)⟩, option.some_ne_none _ (ha.trans hn),

src/logic/function/basic.lean

@@ -231,6 +231,16 @@ theorem right_inverse.injective {f : α → β} {g : β → α} (h : right_inver
   injective f :=
 h.left_inverse.injective
 
+theorem left_inverse.right_inverse_of_injective {f : α → β} {g : β → α} (h : left_inverse f g)
+  (hf : injective f) :
+  right_inverse f g :=
+λ x, hf $ h (f x)
+
+theorem left_inverse.right_inverse_of_surjective {f : α → β} {g : β → α} (h : left_inverse f g)
+  (hg : surjective g) :
+  right_inverse f g :=
+λ x, let ⟨y, hy⟩ := hg x in hy ▸ congr_arg g (h y)
+
 theorem left_inverse.eq_right_inverse {f : α → β} {g₁ g₂ : β → α} (h₁ : left_inverse g₁ f)
   (h₂ : right_inverse g₂ f) :
   g₁ = g₂ :=
@@ -316,8 +326,7 @@ lemma inv_fun_comp (hf : injective f) : inv_fun f ∘ f = id := funext $ left_in
 end inv_fun
 
 section inv_fun
-variables {α : Type u} [i : nonempty α] {β : Sort v} {f : α → β}
-include i
+variables {α : Type u} [nonempty α] {β : Sort v} {f : α → β}
 
 lemma injective.has_left_inverse (hf : injective f) : has_left_inverse f :=
 ⟨inv_fun f, left_inverse_inv_fun hf⟩