[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ z • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p
[PROOFSTEP]
rw [AddSubgroup.mem_zmultiples_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p
[PROOFSTEP]
simp_rw [AddSubgroup.mem_zmultiples_iff, div_eq_mul_inv, ← smul_mul_assoc, eq_sub_iff_add_eq]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
have hz' : (z : R) ≠ 0 := Int.cast_ne_zero.mpr hz
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
conv_rhs => simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
| ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
| ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
| ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r
[PROOFSTEP]
simp (config := { singlePass := true }) only [← (mul_right_injective₀ hz').eq_iff]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔
    ∃ k k_1, (fun x x_1 => x * x_1) (↑z) (k_1 • p + ↑k • p * (↑z)⁻¹) = (fun x x_1 => x * x_1) (↑z) r
[PROOFSTEP]
simp_rw [← zsmul_eq_mul, smul_add, ← mul_smul_comm, zsmul_eq_mul (z : R)⁻¹, mul_inv_cancel hz', mul_one, ←
  coe_nat_zsmul, smul_smul, ← add_smul]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) → ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r
[PROOFSTEP]
rintro ⟨k, h⟩
[GOAL]
case mp.intro
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r
[PROOFSTEP]
simp_rw [← h]
[GOAL]
case mp.intro
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ ∃ k_1 k_2, (z * k_2 + ↑↑k_1) • p = k • p
[PROOFSTEP]
refine' ⟨⟨(k % z).toNat, _⟩, k / z, _⟩
[GOAL]
case mp.intro.refine'_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ Int.toNat (k % z) < Int.natAbs z
[PROOFSTEP]
rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
[GOAL]
case mp.intro.refine'_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ k % z < ↑(Int.natAbs z)
[PROOFSTEP]
exact (Int.emod_lt _ hz).trans_eq (Int.abs_eq_natAbs _)
[GOAL]
case mp.intro.refine'_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + ↑↑{ val := Int.toNat (k % z), isLt := (_ : Int.toNat (k % z) < Int.natAbs z) }) • p = k • p
[PROOFSTEP]
rw [Fin.val_mk, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
[GOAL]
case mp.intro.refine'_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = k • p
[PROOFSTEP]
nth_rewrite 3 [← Int.div_add_mod k z]
[GOAL]
case mp.intro.refine'_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = (z * Int.div k z + Int.mod k z) • p
[PROOFSTEP]
rw [Int.mod_def, ← Int.div_def', Int.emod_def]
[GOAL]
case mp.intro.refine'_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + (k - z * (k / z))) • p = (z * (k / z) + (k - z * (k / z))) • p
[PROOFSTEP]
simp only [add_sub_cancel'_right, zsmul_eq_mul, Int.div_def']
[GOAL]
case mpr
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k k_1, (z * k_1 + ↑↑k) • p = z • r) → ∃ k, k • p = z • r
[PROOFSTEP]
rintro ⟨k, n, h⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : Fin (Int.natAbs z)
n : ℤ
h : (z * n + ↑↑k) • p = z • r
⊢ ∃ k, k • p = z • r
[PROOFSTEP]
exact ⟨_, h⟩
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
[PROOFSTEP]
rw [← coe_nat_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.coe_nat_ne_zero.mpr hn), Int.cast_ofNat]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ (∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p) ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
⊢ z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
induction ψ using Quotient.inductionOn'
[GOAL]
case h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
θ : R ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
a✝ : R
⊢ z • Quotient.mk'' a✝ = z • θ ↔ ∃ k, Quotient.mk'' a✝ = θ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
induction θ using Quotient.inductionOn'
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • Quotient.mk'' a✝¹ = z • Quotient.mk'' a✝ ↔ ∃ k, Quotient.mk'' a✝¹ = Quotient.mk'' a✝ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
let Zp := AddSubgroup.zmultiples p
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
Zp : AddSubgroup R := AddSubgroup.zmultiples p
⊢ z • Quotient.mk'' a✝¹ = z • Quotient.mk'' a✝ ↔ ∃ k, Quotient.mk'' a✝¹ = Quotient.mk'' a✝ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
have : (Quotient.mk'' : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
Zp : AddSubgroup R := AddSubgroup.zmultiples p
this : Quotient.mk'' = mk
⊢ z • Quotient.mk'' a✝¹ = z • Quotient.mk'' a✝ ↔ ∃ k, Quotient.mk'' a✝¹ = Quotient.mk'' a✝ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
simp only [this]
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
Zp : AddSubgroup R := AddSubgroup.zmultiples p
this : Quotient.mk'' = mk
⊢ z • ↑a✝¹ = z • ↑a✝ ↔ ∃ k, ↑a✝¹ = ↑a✝ + ↑(↑k • (p / ↑z))
[PROOFSTEP]
simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add, QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
[GOAL]
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
Zp : AddSubgroup R := AddSubgroup.zmultiples p
this : Quotient.mk'' = mk
⊢ z • (a✝¹ - a✝) ∈ AddSubgroup.zmultiples p ↔ ∃ k, a✝¹ - a✝ - ↑k • (p / ↑z) ∈ AddSubgroup.zmultiples p
[PROOFSTEP]
exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑n))
[PROOFSTEP]
rw [← coe_nat_zsmul ψ, ← coe_nat_zsmul θ, zmultiples_zsmul_eq_zsmul_iff (Int.coe_nat_ne_zero.mpr hz), Int.cast_ofNat]
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ (∃ k, ψ = θ + ↑(↑k • (p / ↑n))) ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑n))
[PROOFSTEP]
rfl
