-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem liftMonoidWithZeroHom_injective [Nontrivial R] (φ : R[X] →*₀ G₀) (hφ : Function.Injective φ)
    (hφ' : R[X]⁰ ≤ G₀⁰.comap φ := nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ hφ) :
    Function.Injective (liftMonoidWithZeroHom φ hφ')

Proof state:
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_2
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ φ ↑a'.2 ≠ 0

Tactic:
exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)

Result:
no goals

Proof state:
case ofFractionRing.ofFractionRing.H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.1 a.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.1 a'.2 } →
    { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }

Tactic:
simp_rw [liftMonoidWithZeroHom_apply_ofFractionRing_mk]

Result:
case ofFractionRing.ofFractionRing.H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
⊢ φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2 →
    { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }

Proof state:
case ofFractionRing.ofFractionRing
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
x y : FractionRing R[X]
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := x } = (liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := x } = { toFractionRing := y }

Tactic:
induction' x using Localization.induction_on with a

Result:
case ofFractionRing.ofFractionRing.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
y : FractionRing R[X]
a : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.1 a.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := y }

Proof state:
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_1
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ φ ↑a.2 ≠ 0

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_2
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ φ ↑a'.2 ≠ 0

Tactic:
all_goals exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)

Result:
no goals

Proof state:
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_3
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
this : φ a.1 * φ ↑a'.2 = φ a'.1 * φ ↑a.2
⊢ ↑(a'.1, a'.2).2 * (a.1, a.2).1 = ↑(a.1, a.2).2 * (a'.1, a'.2).1

Tactic:
rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this

Result:
no goals

Proof state:
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ Localization.mk a.1 a.2 = Localization.mk a'.1 a'.2

Tactic:
refine Localization.mk_eq_mk_iff.mpr (Localization.r_of_eq (M := R[X]) ?_)

Result:
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ ↑(a'.1, a'.2).2 * (a.1, a.2).1 = ↑(a.1, a.2).2 * (a'.1, a'.2).1

Proof state:
case ofFractionRing.ofFractionRing.H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
⊢ φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2 →
    { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }

Tactic:
intro h

Result:
case ofFractionRing.ofFractionRing.H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2
⊢ { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }

Proof state:
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
⊢ Function.Injective ⇑(liftMonoidWithZeroHom φ hφ')

Tactic:
rintro ⟨x⟩ ⟨y⟩

Result:
case ofFractionRing.ofFractionRing
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
x y : FractionRing R[X]
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := x } = (liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := x } = { toFractionRing := y }

Proof state:
case ofFractionRing.ofFractionRing.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
y : FractionRing R[X]
a : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.1 a.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := y }

Tactic:
induction' y using Localization.induction_on with a'

Result:
case ofFractionRing.ofFractionRing.H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯
a a' : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.1 a.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.1 a'.2 } →
    { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }