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
⊢ DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples e)
have inl : DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples 0)
Tactic: rcases eq_or_ne e 0 with (rfl | he)
Cleared hypotheses: e
-- 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
inl : DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples 0)
⊢ DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples e)
have inr : ∀ (he : e ≠ 0), DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples e)
Tactic: rcases eq_or_ne e 0 with (rfl | 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
this : IsAddTorsionFree E
⊢ DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples 0)
have inl : DiscreteTopology.{u_6} ↥⊥
Tactic: rw [AddSubgroup.zmultiples_zero_eq_bot]
-- 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
⊢ DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples e)
have inr : ∃ (t : Set E),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
    Eq (α := Set ↥(AddSubgroup.zmultiples e))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' t) {0}
Tactic: rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
-- 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
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      Eq (α := Set ↥(AddSubgroup.zmultiples e))
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' t) {0}
have inr : Eq (α := Set ↥(AddSubgroup.zmultiples e))
  (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' ball 0 ‖e‖) {0}
Tactic: refine ⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, ?_⟩
-- 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
⊢ Eq (α := Set ↥(AddSubgroup.zmultiples e))
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' ball 0 ‖e‖)
    {0}
have inr : ∀ (x : E) (hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x),
  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) x hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) x hx)
Tactic: ext ⟨x, hx⟩
-- 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
x : E
hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x
⊢ 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) x hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) x hx)
have inr : ∀ (k : ℤ) (hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) (k • e)),
  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: obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
Cleared hypotheses: x, hx
-- 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)
⊢ 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 : 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)
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)
⊢ 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₁ : ‖(↑(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)
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)
⊢ 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‖ ↔
  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]
-- 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)
⊢ 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‖ ↔
  Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx = 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
⊢ 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‖ ↔
  (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) : E) =
    (↑0 : E)
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)
⊢ 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 : E)
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)
⊢ 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]