-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) (k • e)
inr :
  Membership.mem (γ := Set E) (ball 0 ‖e‖)
      (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
        E) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₁ :
  ‖(↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
          E)‖ <
      ‖e‖ ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₂ :
  ‖k • e‖ < ‖e‖ ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
inr₃ :
  ‖k • e‖ < ‖e‖ ↔
    Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx = 0
inr₄ :
  ‖k • e‖ < ‖e‖ ↔
    (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) :
        E) =
      (↑0 : E)
inr₅ : ‖k • e‖ < ‖e‖ ↔ k • e = (↑0 : E)
inr₆ : ‖k • e‖ < ‖e‖ ↔ k • e = 0
inr₇ : norm (E := ℚ) (↑k : ℚ) * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₈ : ‖k‖ * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₉ : |(↑k : ℝ)| * ‖e‖ < ‖e‖ ↔ k • e = 0
inr₁₀ : LT.lt (α := ℝ) |(↑k : ℝ)| 1 ↔ k • e = 0
inr₁₁ : LT.lt (α := ℝ) |(↑k : ℝ)| (↑1 : ℝ) ↔ k • e = 0
inr₁₂ : LT.lt (α := ℝ) (↑|k| : ℝ) (↑1 : ℝ) ↔ k • e = 0
inr₁₃ : |k| < 1 ↔ k • e = 0
inr₁₄ : k = 0 ↔ k • e = 0
inr₁₅ : k = 0 ↔ k = 0 ∨ e = 0
inr₁₆ inr₁₇ : k = 0 ↔ k = 0
⊢ Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' ball 0 ‖e‖)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)

Tactic:
rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff,
      AddSubgroup.coe_mk, AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat,
      Int.norm_eq_abs, mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _,
      ← Int.cast_abs, Int.cast_lt, Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]

Premises used: Iff.mpr, norm_zsmul, norm_pos_iff, Int.cast_abs, AddSubgroup.coe_zero, Rat, Int.cast_lt, Int.norm_eq_abs, mul_lt_iff_lt_one_left, AddSubgroup.coe_mk, Subtype.ext_iff, Set.mem_singleton_iff, Int.norm_cast_rat, Int.abs_lt_one_iff, or_iff_left, Int.cast_one, Set.mem_preimage, mem_ball_zero_iff, smul_eq_zero