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))
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))
induction ψ using Quotient.inductionOn'
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))
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))
induction θ using Quotient.inductionOn'
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))
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))
let Zp := AddSubgroup.zmultiples p
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))
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))
have : (Quotient.mk'' : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
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))
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))
simp only [this]
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
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))
simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
  QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
no goals
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
exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz