awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
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
⊢ 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)
have inr₇ : norm (E := ℚ) (↑k : ℚ) * ‖e‖ < ‖e‖ ↔ k • e = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
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
⊢ 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)
have inr₈ : ‖k‖ * ‖e‖ < ‖e‖ ↔ k • e = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
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
⊢ 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)
have inr₉ : |(↑k : ℝ)| * ‖e‖ < ‖e‖ ↔ k • e = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
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
⊢ 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)
have inr₁₀ : LT.lt (α := ℝ) |(↑k : ℝ)| 1 ↔ k • e = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
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
⊢ 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)
have inr₁₁ : LT.lt (α := ℝ) |(↑k : ℝ)| (↑1 : ℝ) ↔ k • e = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
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
⊢ 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)
have inr₁₂ : LT.lt (α := ℝ) (↑|k| : ℝ) (↑1 : ℝ) ↔ k • e = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
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
⊢ 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)
have inr₁₃ : |k| < 1 ↔ k • e = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Basic (goal)
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
⊢ 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)
have inr₁₄ : k = 0 ↔ k • e = 0
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]