feat(logic/function/basic): refine extend_apply (#16944)

Add `function.extend_apply_of_unique`
which allows to rewrite `function.extend f g e (f a) = g a` 
not only when `f` is injective, what `function.extend_apply` does, 
but when `f a = f b → g a = g b`.
Generalize a few similar lemmas in the same way.

TODO ? : rewrite `function.extend_apply` to use this function.



Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

src/data/polynomial/erase_lead.lean

@@ -310,10 +310,10 @@ begin
       { rw [fin.range_cast_succ, set.mem_def],
         exact lt_of_lt_of_le hij (nat.lt_succ_iff.mp j.2) },
       obtain ⟨i, rfl⟩ := hi,
-      rw function.extend_apply fin.cast_succ.injective,
+      rw fin.cast_succ.injective.extend_apply,
       by_cases hj : ∃ j₀, fin.cast_succ j₀ = j,
       { obtain ⟨j, rfl⟩ := hj,
-        rwa [function.extend_apply fin.cast_succ.injective, hk.lt_iff_lt,
+        rwa [fin.cast_succ.injective.extend_apply, hk.lt_iff_lt,
           ←fin.cast_succ_lt_cast_succ_iff] },
       { rw [function.extend_apply' _ _ _ hj],
         apply lt_nat_degree_of_mem_erase_lead_support,
@@ -326,13 +326,13 @@ begin
     { intro i,
       by_cases hi : ∃ i₀, fin.cast_succ i₀ = i,
       { obtain ⟨i, rfl⟩ := hi,
-        rw function.extend_apply fin.cast_succ.injective,
+        rw fin.cast_succ.injective.extend_apply,
         exact hx i },
       { rw [function.extend_apply' _ _ _ hi, ne, leading_coeff_eq_zero,
           ←card_support_eq_zero, h],
         exact n.succ_ne_zero } },
     { rw fin.sum_univ_cast_succ,
-      simp only [function.extend_apply fin.cast_succ.injective],
+      simp only [fin.cast_succ.injective.extend_apply],
       rw [←hf, function.extend_apply', function.extend_apply', erase_lead_add_C_mul_X_pow],
       all_goals { exact H } } },
 end

src/data/set/function.lean

@@ -109,7 +109,7 @@ lemma range_extend {f : α → β} (hf : injective f) (g : α → γ) (g' : β 
 begin
   refine (range_extend_subset _ _ _).antisymm _,
   rintro z (⟨x, rfl⟩|⟨y, hy, rfl⟩),
-  exacts [⟨f x, extend_apply hf _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]
+  exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]
 end
 
 /-- Restrict codomain of a function `f` to a set `s`. Same as `subtype.coind` but this version

src/logic/embedding/basic.lean

@@ -265,7 +265,7 @@ This embedding sends each `f : α → γ` to a function `g : β → γ` such tha
 noncomputable def arrow_congr_left {α : Sort u} {β : Sort v} {γ : Sort w} [inhabited γ]
   (e : α ↪ β) : (α → γ) ↪ (β → γ) :=
 ⟨λ f, extend e f default, λ f₁ f₂ h, funext $ λ x,
-  by simpa only [extend_apply e.injective] using congr_fun h (e x)⟩
+  by simpa only [e.injective.extend_apply] using congr_fun h (e x)⟩
 
 /-- Restrict both domain and codomain of an embedding. -/
 protected def subtype_map {α β} {p : α → Prop} {q : β → Prop} (f : α ↪ β)

src/logic/function/basic.lean

@@ -551,47 +551,76 @@ along a function `f : α → β` to a function `β → γ`,
 by using the values of `g` on the range of `f`
 and the values of an auxiliary function `e' : β → γ` elsewhere.
 
-Mostly useful when `f` is injective. -/
+Mostly useful when `f` is injective, more generally when `g.factors_through f`. -/
 def extend (f : α → β) (g : α → γ) (e' : β → γ) : β → γ :=
 λ b, if h : ∃ a, f a = b then g (classical.some h) else e' b
 
+/-- g factors through f : `f a = f b → g a = g b` -/
+def factors_through (g : α → γ) (f : α → β) : Prop :=
+∀ ⦃a b⦄, f a = f b → g a = g b
+
+lemma injective.factors_through (hf : injective f) (g : α → γ) : g.factors_through f :=
+λ a b h, congr_arg g (hf h)
+
 lemma extend_def (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [decidable (∃ a, f a = b)] :
   extend f g e' b = if h : ∃ a, f a = b then g (classical.some h) else e' b :=
 by { unfold extend, congr }
 
-@[simp] lemma extend_apply (hf : injective f) (g : α → γ) (e' : β → γ) (a : α) :
+lemma factors_through.extend_apply {g : α → γ} (hf : g.factors_through f) (e' : β → γ) (a : α) :
   extend f g e' (f a) = g a :=
 begin
   simp only [extend_def, dif_pos, exists_apply_eq_apply],
-  exact congr_arg g (hf $ classical.some_spec (exists_apply_eq_apply f a))
+  exact hf (classical.some_spec (exists_apply_eq_apply f a)),
 end
 
+@[simp] lemma injective.extend_apply (hf : f.injective) (g : α → γ) (e' : β → γ) (a : α) :
+  extend f g e' (f a) = g a :=
+(hf.factors_through g).extend_apply e' a
+
 @[simp] lemma extend_apply' (g : α → γ) (e' : β → γ) (b : β) (hb : ¬∃ a, f a = b) :
   extend f g e' b = e' b :=
 by simp [function.extend_def, hb]
 
-lemma apply_extend {δ} (hf : injective f) (F : γ → δ) (g : α → γ) (e' : β → γ) (b : β) :
+lemma factors_through_iff (g : α → γ) [nonempty γ] :
+  g.factors_through f ↔ ∃ (e : β → γ), g = e ∘ f :=
+⟨λ hf, ⟨extend f g (const β (classical.arbitrary γ)),
+      funext (λ x, by simp only [comp_app, hf.extend_apply])⟩,
+  λ h a b hf, by rw [classical.some_spec h, comp_apply, hf]⟩
+
+lemma factors_through.apply_extend {δ} {g : α → γ} (hf : factors_through g f)
+  (F : γ → δ) (e' : β → γ) (b : β) :
   F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b :=
 begin
   by_cases hb : ∃ a, f a = b,
   { cases hb with a ha, subst b,
-    rw [extend_apply hf, extend_apply hf] },
+    rw [factors_through.extend_apply, factors_through.extend_apply],
+    { intros a b h, simp only [comp_apply], apply congr_arg, exact hf h, },
+    { exact hf, }, },
   { rw [extend_apply' _ _ _ hb, extend_apply' _ _ _ hb] }
 end
 
+lemma injective.apply_extend {δ} (hf : injective f) (F : γ → δ) (g : α → γ) (e' : β → γ) (b : β) :
+  F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b :=
+(hf.factors_through g).apply_extend F e' b
+
 lemma extend_injective (hf : injective f) (e' : β → γ) :
   injective (λ g, extend f g e') :=
 begin
   intros g₁ g₂ hg,
   refine funext (λ x, _),
   have H := congr_fun hg (f x),
-  simp only [hf, extend_apply] at H,
+  simp only [hf.extend_apply] at H,
   exact H
 end
 
+lemma factors_through.extend_comp {g : α → γ} (e' : β → γ)
+  (hf : factors_through g f) :
+  extend f g e' ∘ f = g :=
+funext $ λ a, by simp only [comp_app, hf.extend_apply e']
+
 @[simp] lemma extend_comp (hf : injective f) (g : α → γ) (e' : β → γ) :
   extend f g e' ∘ f = g :=
-funext $ λ a, extend_apply hf g e' a
+(hf.factors_through g).extend_comp e'
 
 lemma injective.surjective_comp_right' (hf : injective f) (g₀ : β → γ) :
   surjective (λ g : β → γ, g ∘ f) :=

src/measure_theory/function/strongly_measurable/basic.lean

@@ -809,7 +809,8 @@ begin
   assume x,
   by_cases hx : ∃ y, g y = x,
   { rcases hx with ⟨y, rfl⟩,
-    simpa only [simple_func.extend_apply, hg.injective, extend_apply] using hf.tendsto_approx y },
+    simpa only [simple_func.extend_apply, hg.injective,
+      injective.extend_apply] using hf.tendsto_approx y },
   { simpa only [hx, simple_func.extend_apply', not_false_iff, extend_apply']
       using hg'.tendsto_approx x }
 end
@@ -821,7 +822,7 @@ lemma _root_.measurable_embedding.exists_strongly_measurable_extend
   ∃ f' : γ → β, strongly_measurable f' ∧ f' ∘ g = f :=
 ⟨function.extend g f (λ x, classical.choice (hne x)),
   hg.strongly_measurable_extend hf (strongly_measurable_const' $ λ _ _, rfl),
-  funext $ λ x, extend_apply hg.injective _ _ _⟩
+  funext $ λ x, hg.injective.extend_apply _ _ _⟩
 
 lemma measurable_set_eq_fun {m : measurable_space α} {E} [topological_space E] [metrizable_space E]
   {f g : α → E} (hf : strongly_measurable f) (hg : strongly_measurable g) :

src/measure_theory/integral/lebesgue.lean

@@ -292,7 +292,7 @@ def extend [measurable_space β] (f₁ : α →ₛ γ) (g : α → β)
 
 @[simp] lemma extend_apply [measurable_space β] (f₁ : α →ₛ γ) {g : α → β}
   (hg : measurable_embedding g) (f₂ : β →ₛ γ) (x : α) : (f₁.extend g hg f₂) (g x) = f₁ x :=
-function.extend_apply hg.injective _ _ _
+hg.injective.extend_apply _ _ _
 
 @[simp] lemma extend_apply' [measurable_space β] (f₁ : α →ₛ γ) {g : α → β}
   (hg : measurable_embedding g) (f₂ : β →ₛ γ) {y : β} (h : ¬∃ x, g x = y) :

src/measure_theory/measurable_space.lean

@@ -911,7 +911,7 @@ lemma exists_measurable_extend (hf : measurable_embedding f) {g : α → γ} (hg
   ∃ g' : β → γ, measurable g' ∧ g' ∘ f = g :=
 ⟨extend f g (λ x, classical.choice (hne x)),
   hf.measurable_extend hg (measurable_const' $ λ _ _, rfl),
-  funext $ λ x, extend_apply hf.injective _ _ _⟩
+  funext $ λ x, hf.injective.extend_apply _ _ _⟩
 
 lemma measurable_comp_iff (hg : measurable_embedding g) : measurable (g ∘ f) ↔ measurable f :=
 begin

src/measure_theory/measure/measure_space.lean

@@ -388,7 +388,7 @@ begin
   generalize ht : function.extend encodable.encode s ⊥ = t,
   replace hd : directed (⊆) t := ht ▸ hd.extend_bot encodable.encode_injective,
   suffices : μ (⋃ n, t n) = ⨆ n, μ (t n),
-  { simp only [← ht, apply_extend encodable.encode_injective μ, ← supr_eq_Union,
+  { simp only [← ht, encodable.encode_injective.apply_extend μ, ← supr_eq_Union,
       supr_extend_bot encodable.encode_injective, (∘), pi.bot_apply, bot_eq_empty,
       measure_empty] at this,
     exact this.trans (supr_extend_bot encodable.encode_injective _) },

src/measure_theory/pi_system.lean

@@ -311,14 +311,14 @@ begin
       intros h1 b h_b h_b_in_T,
       have h2 := h1 b h_b h_b_in_T,
       revert h2,
-      rw function.extend_apply subtype.val_injective,
+      rw subtype.val_injective.extend_apply,
       apply id } },
   { intros b h_b,
     simp_rw [finset.mem_image, exists_prop, subtype.exists,
              exists_and_distrib_right, exists_eq_right] at h_b,
     cases h_b,
     have h_b_alt : b = (subtype.mk b h_b_w).val := rfl,
-    rw [h_b_alt, function.extend_apply subtype.val_injective],
+    rw [h_b_alt, subtype.val_injective.extend_apply],
     apply h_t',
     apply h_b_h },
 end

src/model_theory/satisfiability.lean

@@ -142,8 +142,8 @@ begin
     refine λ a as b bs ab, _,
     rw [← subtype.coe_mk a as, ← subtype.coe_mk b bs, ← subtype.ext_iff],
     exact h.some.injective
-      ((function.extend_apply subtype.coe_injective h.some default ⟨a, as⟩).symm.trans
-      (ab.trans (function.extend_apply subtype.coe_injective h.some default ⟨b, bs⟩))), },
+      ((subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
+      (ab.trans (subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩))), },
   exact model.is_satisfiable M,
 end
 

src/order/complete_lattice.lean

@@ -1026,7 +1026,7 @@ theorem supr_extend_bot {e : ι → β} (he : injective e) (f : ι → α) :
   (⨆ j, extend e f ⊥ j) = ⨆ i, f i :=
 begin
   rw supr_split _ (λ j, ∃ i, e i = j),
-  simp [extend_apply he, extend_apply', @supr_comm _ β ι] { contextual := tt }
+  simp [he.extend_apply, extend_apply', @supr_comm _ β ι] { contextual := tt }
 end
 
 lemma infi_extend_top {e : ι → β} (he : injective e) (f : ι → α) : (⨅ j, extend e f ⊤ j) = infi f :=

src/order/directed.lean

@@ -97,7 +97,7 @@ begin
   { use e i, simp [function.extend_apply' _ _ _ hb] },
   rcases hf i j with ⟨k, hi, hj⟩,
   use (e k),
-  simp only [function.extend_apply he, *, true_and]
+  simp only [he.extend_apply, *, true_and]
 end
 
 /-- An antitone function on an inf-semilattice is directed. -/

src/topology/continuous_function/bounded.lean

@@ -361,7 +361,7 @@ def extend (f : α ↪ δ) (g : α →ᵇ β) (h : δ →ᵇ β) : δ →ᵇ β
 
 @[simp] lemma extend_apply (f : α ↪ δ) (g : α →ᵇ β) (h : δ →ᵇ β) (x : α) :
   extend f g h (f x) = g x :=
-extend_apply f.injective _ _ _
+f.injective.extend_apply _ _ _
 
 @[simp] lemma extend_comp (f : α ↪ δ) (g : α →ᵇ β) (h : δ →ᵇ β) : extend f g h ∘ f = g :=
 extend_comp f.injective _ _