-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem map_injective [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap φ)
    (hf : Function.Injective φ) : Function.Injective (map φ hφ)

Proof state:
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
⊢ Function.Injective ⇑(map φ hφ)

Tactic:
rintro ⟨x⟩ ⟨y⟩ h

Result:
case ofFractionRing.ofFractionRing
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
x y : FractionRing R[X]
h : (map φ hφ) { toFractionRing := x } = (map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := x } = { toFractionRing := y }

Proof state:
case ofFractionRing.ofFractionRing.H
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
y : FractionRing R[X]
y✝ : R[X] × ↥R[X]⁰
h : (map φ hφ) { toFractionRing := Localization.mk y✝.1 y✝.2 } = (map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := y }

Tactic:
induction y using Localization.induction_on

Result:
case ofFractionRing.ofFractionRing.H.H
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
y✝¹ y✝ : R[X] × ↥R[X]⁰
h :
  (map φ hφ) { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } =
    (map φ hφ) { toFractionRing := Localization.mk y✝.1 y✝.2 }
⊢ { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } = { toFractionRing := Localization.mk y✝.1 y✝.2 }

Proof state:
case ofFractionRing.ofFractionRing.H.H
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
y✝¹ y✝ : R[X] × ↥R[X]⁰
h :
  (map φ hφ) { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } =
    (map φ hφ) { toFractionRing := Localization.mk y✝.1 y✝.2 }
⊢ { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } = { toFractionRing := Localization.mk y✝.1 y✝.2 }

Tactic:
simpa only [map_apply_ofFractionRing_mk, ofFractionRing_injective.eq_iff,
  Localization.mk_eq_mk_iff, Localization.r_iff_exists, mul_cancel_left_coe_nonZeroDivisors,
  exists_const, ← map_mul, hf.eq_iff] using h

Result:
no goals

Proof state:
case ofFractionRing.ofFractionRing
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
x y : FractionRing R[X]
h : (map φ hφ) { toFractionRing := x } = (map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := x } = { toFractionRing := y }

Tactic:
induction x using Localization.induction_on

Result:
case ofFractionRing.ofFractionRing.H
R : Type u_3
S : Type u_4
F : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ⇑φ
y : FractionRing R[X]
y✝ : R[X] × ↥R[X]⁰
h : (map φ hφ) { toFractionRing := Localization.mk y✝.1 y✝.2 } = (map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := y }