-- Mathlib/Algebra/CharZero/Quotient.lean
theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) :
    z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + ((k : ℕ) • (p / z) : R)

Proof state:
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 • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Tactic:
have : (Quotient.mk _ : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl

Result:
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 (leftRel Zp) = mk
⊢ z • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Proof state:
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 (leftRel Zp) = mk
⊢ z • ↑a✝¹ = z • ↑a✝ ↔ ∃ k, ↑a✝¹ = ↑a✝ + ↑(↑k • (p / ↑z))

Tactic:
simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
  QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]

Result:
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 (leftRel Zp) = mk
⊢ z • (a✝¹ - a✝) ∈ AddSubgroup.zmultiples p ↔ ∃ k, a✝¹ - a✝ - ↑k • (p / ↑z) ∈ AddSubgroup.zmultiples p

Proof state:
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 (leftRel Zp) = mk
⊢ z • (a✝¹ - a✝) ∈ AddSubgroup.zmultiples p ↔ ∃ k, a✝¹ - a✝ - ↑k • (p / ↑z) ∈ AddSubgroup.zmultiples p

Tactic:
exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz

Result:
no goals

Proof state:
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 • ⟦a✝⟧ = z • θ ↔ ∃ k, ⟦a✝⟧ = θ + ↑(↑k • (p / ↑z))

Tactic:
induction θ using Quotient.inductionOn

Result:
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Proof state:
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 (leftRel Zp) = mk
⊢ z • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Tactic:
simp only [Zp, this]

Result:
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 (leftRel Zp) = mk
⊢ z • ↑a✝¹ = z • ↑a✝ ↔ ∃ k, ↑a✝¹ = ↑a✝ + ↑(↑k • (p / ↑z))

Proof state:
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Tactic:
let Zp := AddSubgroup.zmultiples p

Result:
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 • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Proof state:
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))

Tactic:
induction ψ using Quotient.inductionOn

Result:
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 • ⟦a✝⟧ = z • θ ↔ ∃ k, ⟦a✝⟧ = θ + ↑(↑k • (p / ↑z))