re-casting to nat

Stream: Is there code for X?

[Will Midwood]

Hi all, hopefully just a quick one.
I'm trying to prove this goal with these hypotheses:

a : ℤ,
p : ℕ,
hp : irreducible p
⊢ irreducible ↑p

In previous parts of the proof lean casted p to an integer, is there a way I can cast it back so I can useexact hp? Thanks

[Adam Topaz]

tactic#norm_cast and tactic#push_cast are your friends

[Adam Topaz]

actually maybe these don't help directly in this case.

[Junyan Xu]

Yeah I don't think those tactics know about the lemmas docs#irreducible_iff_nat_prime, docs#nat.prime_iff_prime_int, docs#unique_factorization_monoid.irreducible_iff_prime, which is the shortest path I could find.

[Adam Topaz]

We do have something for units though...

[Adam Topaz]

docs#int.of_nat_is_unit

[Adam Topaz]

That's tagged with norm_cast. Presumably we should do something similar for irreducible.

[Junyan Xu]

Maybe that could make this (squarefree) automatic as well.

[Alex J. Best]

I have the following in a project somewhere, where I think I had this in mind, not sure I ever PRed it though

lemma irreducible_of_map_irreducible {α β : Type*} [monoid α] [monoid β] [unique βˣ] {p : α}
  {F : Type*} [monoid_hom_class F α β] (f : F) (hf : ∀ x, f x = 1 → x = 1)
  (h : irreducible $ f p) : irreducible p :=
{ not_unit := λ hn, h.not_unit (hn.map f),
  is_unit_or_is_unit' := λ a b hab, begin
    have := map_mul f a b,
    rw ← hab at this,
    apply or.imp _ _ (h.is_unit_or_is_unit this);
    rintro ⟨ua, ha⟩;
    [rw hf a, rw hf b];
    { exact is_unit_one } <|>
    { simp [← ha], },
  end }

[Eric Rodriguez]

that should probably be called irreducible.of_map; also we can write that with more familar injective hypotheses for stricter restrictions on alpha, beta I guess

[Alex J. Best]

What do you mean more precisely? (btw it turns out I was using it for something else but I think it applies here)