injective function composed with non zero function ne zero

Stream: Is there code for X?

[Chris Birkbeck]

I think I'm just being silly, but where is this in mathlib (or whatever the sensible version of this is):

lemma comp_inj_ne_zero {α β γ: Type*} [OfNat β 0] [ OfNat γ 0] (f : α → β) (hf : f ≠ 0) (g : β → γ)
  (hg : Injective g) (hg0 : g 0 = 0) : (g ∘ f) ≠ 0 := by

Thats a general version of what I need, in practice what I want is:

example (a : Fin 2 → ℤ) (ha : a ≠ 0) : (Int.cast (R := ℝ)) ∘ a ≠ 0 := by

[Yury G. Kudryashov]

You can use docs#Function.funext_iff and docs#Function.Injective.eq_iff'

[Chris Birkbeck]

Yes so I can prove them, using this. But it wasn't as quick as I thought, since in the case I care about Int.cast isn't a function from (Fin 2 → ℤ) → (Fin 2 → ℝ). Is there a quick way to show it extends to an injective function (or maybe we already have this, but i couldn't find it).

[Damiano Testa]

This does not seem so bad:

import Mathlib
open Function

lemma comp_inj_ne_zero {α β γ: Type*} [OfNat β 0] [ OfNat γ 0] (f : α → β) (hf : f ≠ 0) (g : β → γ)
    (hg : Injective g) (hg0 : g 0 = 0) : (g ∘ f) ≠ 0 := by
  simp only [ne_eq, funext_iff, Pi.zero_apply, not_forall, comp_apply] at hf ⊢
  rcases hf with ⟨a, ha⟩
  exact ⟨a, by rw [hg.eq_iff'] <;> assumption⟩

example (a : Fin 2 → ℤ) (ha : a ≠ 0) : (Int.cast (R := ℝ)) ∘ a ≠ 0 :=
  comp_inj_ne_zero _ ha _ Int.cast_injective Int.cast_zero

[Chris Birkbeck]

Ok fair, that's basically the proof I had, but it just felt that we would've already had "a non zero function composed with an injective function is non zero" in mathlib, since it seems pretty basic to me.

[Damiano Testa]

I agree and I'm sure no one would mind if you PRed it... :smiley:

[Chris Birkbeck]

I'm just really bad at finding these things in mathlib, so I thought I'd ask first, since its usually the case I've just done a bad job of finding things :)

[Eric Wieser]

Does docs#Function.ne_iff make the proof any shorter?

[Yury G. Kudryashov]

lemma comp_eq_zero_iff {α β γ: Type*} [OfNat β 0] [ OfNat γ 0] (f : α → β) (g : β → γ)
    (hg : Injective g) (hg0 : g 0 = 0) : g ∘ f = 0 ↔ f = 0 :=
  hg.comp_left.eq_iff' <| funext fun _ ↦ hg0

[Chris Birkbeck]

Oh very nice! I'll use that, thanks!

[Damiano Testa]

Yuri's version makes me wonder whether there should also be a version with just constant, not necessarily zero:

lemma comp_eq_const_iff {α β γ: Type*} (b : β) (c : γ) (f : α → β) (g : β → γ)
    (hg : Injective g) (hg0 : g b = c) : g ∘ f = (fun _ => c) ↔ f = (fun _ => b) :=
  hg.comp_left.eq_iff' <| funext fun _ ↦ hg0


lemma comp_eq_zero_iff {α β γ: Type*} [OfNat β 0] [ OfNat γ 0] (f : α → β) (g : β → γ)
    (hg : Injective g) (hg0 : g 0 = 0) : g ∘ f = 0 ↔ f = 0 :=
  comp_eq_const_iff _ _ _ _ ‹_› ‹_›

[Eric Wieser]

Or maybe even drop hg0:

lemma comp_eq_const_iff {α β γ: Type*} (b : β) (c : γ) (f : α → β) (g : β → γ)
    (hg : Injective g) : g ∘ f = Function.const _ (g b) ↔ f = Function.const _ b :=
  hg.comp_left.eq_iff' rfl

[Chris Birkbeck]

#11244