instance diamond in algebra.id for subtypes

Stream: general

[Eric Wieser]

We can add a stupid id_explode field to every ring which sends x to {foo := x.foo}

[Eric Wieser]

And then change algebra.id to use that

[María Inés de Frutos Fernández]

Is this the same kind of issue?

import ring_theory.ideal.local_ring
import ring_theory.valuation.integers

universes u v

variables {K : Type u} [field K] [nontrivial K] {Γ₀ : Type v}
  [linear_ordered_comm_group_with_zero Γ₀] (v : valuation K Γ₀)

lemma is_unit_iff_valuation_one (r : v.integer) : is_unit r ↔ v r = 1 :=
begin
  refine ⟨λ h, valuation.integers.one_of_is_unit (valuation.integer.integers v) h, λ h, _⟩,
  { apply @valuation.integers.is_unit_of_one K Γ₀ _ _ v v.integer _ _,
    { exact valuation.integer.integers v },
    { rw [is_unit_iff_ne_zero, ← (algebra_map _ _).map_zero],
      rw function.injective.ne_iff ((algebra_map _ _ ).injective), --here
      sorry, },
    { exact h, }}
end

[Kevin Buzzard]

The rewrite is failing because Lean can't even make the term you want to rewrite:

lemma is_unit_iff_valuation_one (r : v.integer) : is_unit r ↔ v r = 1 :=
begin
  have foo := function.injective.ne_iff ((algebra_map _ _ ).injective),
end
/-
term
  algebra_map ?m_1 ?m_2
has type
  @ring_hom ?m_1 ?m_2 (@semiring.to_non_assoc_semiring ?m_1 (@comm_semiring.to_semiring ?m_1 ?m_3))
    (@semiring.to_non_assoc_semiring ?m_2 ?m_4) : Type (max ? ?)
but is expected to have type
  @ring_hom ?m_1 ?m_2 (@semiring.to_non_assoc_semiring ?m_1 (@ring.to_semiring ?m_1 (@division_ring.to_ring ?m_1 ?m_3)))
    (@semiring.to_non_assoc_semiring ?m_2 ?m_4) : Type (max ? ?)
-/

[Kevin Buzzard]

oh wait -- this rewrite is failing because ring_hom.injective needs that the source is a field, and your source is ↥(v.integer)

[María Inés de Frutos Fernández]

Thanks!