awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
n : N
⊢ ∃ (m : M), (f : (a : M) → N) m = n ∧ ‖m‖ < ‖n‖ + ε
have obtain : ∀ (m : M),
  ∃ (m_1 : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m_1 : N) ((f : (a : M) → N) m : N) ∧
      ‖m_1‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε
Tactic: obtain ⟨m, rfl⟩ := hquot.surjective n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
have rw : (↑f.ker : Set M).Nonempty
Tactic: rw [Set.image_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ (m_1 : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m_1 : N) ((f : (a : M) → N) m : N) ∧
      ‖m_1‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε
have nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
Tactic: have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty := by
    rw [Set.image_nonempty]
    exact ⟨0, f.ker.zero_mem⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
⊢ ∃ (m_1 : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m_1 : N) ((f : (a : M) → N) m : N) ∧
      ‖m_1‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε
have rcases : ∀ (x : M) (hx : x ∈ (↑f.ker : Set M)) (H : ‖m + x‖ < sInf ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M)) + ε),
  ∃ (m_1 : M),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m_1 : N) ((f : (a : M) → N) m : N) ∧
      ‖m_1‖ < norm.{u_2} (E := N) ((f : (a : M) → N) m : N) + ε
Tactic: rcases Real.lt_sInf_add_pos nonemp hε
    with ⟨_, ⟨⟨x, hx, rfl⟩, H : ‖m + x‖ < sInf ((fun m' : M => ‖m + m'‖) '' f.ker) + ε⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
x : M
hx : x ∈ (↑f.ker : Set M)
H : ‖m + x‖ < sInf ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M)) + ε
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (m + x) : N) ((f : (a : M) → N) m : N)
have rw : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) x : N) = (f : (a : M) → N) m
Tactic: rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
x : M
hx : x ∈ (↑f.ker : Set M)
H : ‖m + x‖ < sInf ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M)) + ε
rw : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) x : N) = (f : (a : M) → N) m
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (m + x) : N) ((f : (a : M) → N) m : N)
have rw₁ : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) m : N) (0 : N) = (f : (a : M) → N) m
Tactic: rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty (α := ℝ) ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M))
x : M
hx : x ∈ (↑f.ker : Set M)
H : ‖m + x‖ < sInf ((fun (m' : M) ↦ ‖m + m'‖) '' (↑f.ker : Set M)) + ε
rw : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) x : N) = (f : (a : M) → N) m
rw₁ : HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) m : N) (0 : N) = (f : (a : M) → N) m
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (m + x) : N) ((f : (a : M) → N) m : N)
have rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) ((f : (a : M) → N) m : N)
Tactic: rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ norm.{u_2} (E := N) ((f : (a : M) → N) m : N) ≤ ‖m‖
have rw : sInf ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) ≤ ‖m‖
Tactic: rw [hquot.norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ sInf ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) ≤ ‖m‖
have h₁ : BddBelow (α := ℝ) ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M))
Tactic: apply csInf_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
h₁ : BddBelow (α := ℝ) ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M))
⊢ sInf ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) ≤ ‖m‖
have h₂ : Membership.mem (γ := Set ℝ) ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M)) ‖m‖
Tactic: apply csInf_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
m : M
⊢ BddBelow (α := ℝ) ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M))
have h : Membership.mem (γ := Set ℝ) (lowerBounds ((fun (m_1 : M) ↦ ‖m + m_1‖) '' (↑f.ker : Set M))) 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
fb : f.NormNoninc
x : M ⧸ S
⊢ norm.{u_3} (E := N) ((lift S f hf : (a : M ⧸ S) → N) x : N) ≤ ‖x‖
have fb' : ‖f‖ ≤ (↑1 : ℝ)
Tactic: have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : Ring R
inst_3 : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst_4 : SeminormedCommRing 𝕜
inst_5 : Module 𝕜 M
inst_6 : IsBoundedSMul 𝕜 M
inst_7 : SMul 𝕜 R
inst_8 : IsScalarTower 𝕜 R M
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
have this : ∃ (ia : ℝ), 0 < ia ∧ ∀ x_1 ∈ ball ‖x‖ ia, ‖k‖ * x_1 ∈ ball (‖k‖ * ‖x‖) ε
Tactic: have := (nhds_basis_ball.tendsto_iff nhds_basis_ball).mp
        ((@Real.uniformContinuous_const_mul ‖k‖).continuous.tendsto ‖x‖) ε hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : Ring R
inst_3 : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst_4 : SeminormedCommRing 𝕜
inst_5 : Module 𝕜 M
inst_6 : IsBoundedSMul 𝕜 M
inst_7 : SMul 𝕜 R
inst_8 : IsScalarTower 𝕜 R M
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
this : ∃ (ia : ℝ), 0 < ia ∧ ∀ x_1 ∈ ball ‖x‖ ia, ‖k‖ * x_1 ∈ ball (‖k‖ * ‖x‖) ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
have this₁ : ∃ (ia : ℝ),
  0 < ia ∧ ∀ (x_1 : ℝ), x_1 - ‖x‖ < ia ∧ ‖x‖ - x_1 < ia → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε
Tactic: simp only [mem_ball, dist, abs_sub_lt_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : Ring R
inst_3 : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst_4 : SeminormedCommRing 𝕜
inst_5 : Module 𝕜 M
inst_6 : IsBoundedSMul 𝕜 M
inst_7 : SMul 𝕜 R
inst_8 : IsScalarTower 𝕜 R M
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
this :
  ∃ (ia : ℝ),
    0 < ia ∧ ∀ (x_1 : ℝ), x_1 - ‖x‖ < ia ∧ ‖x‖ - x_1 < ia → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
have rcases : ∀ (δ : ℝ) (hδ : 0 < δ)
  (h : ∀ (x_1 : ℝ), x_1 - ‖x‖ < δ ∧ ‖x‖ - x_1 < δ → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε),
  ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
Tactic: rcases this with ⟨δ, hδ, h⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : Ring R
inst_3 : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst_4 : SeminormedCommRing 𝕜
inst_5 : Module 𝕜 M
inst_6 : IsBoundedSMul 𝕜 M
inst_7 : SMul 𝕜 R
inst_8 : IsScalarTower 𝕜 R M
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
h : ∀ (x_1 : ℝ), x_1 - ‖x‖ < δ ∧ ‖x‖ - x_1 < δ → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
have obtain : ∀ (a : M)
  (h :
    ∀ (x : ℝ),
      x - norm (E := M ⧸ S) (mk a) < δ ∧ norm (E := M ⧸ S) (mk a) - x < δ →
        ‖k‖ * x - ‖k‖ * norm (E := M ⧸ S) (mk a) < ε ∧ ‖k‖ * norm (E := M ⧸ S) (mk a) - ‖k‖ * x < ε)
  (ha : ‖a‖ < norm (E := M ⧸ S) (mk a) + δ), ‖HSMul.hSMul (β := M ⧸ S) k (mk a)‖ ≤ ‖k‖ * norm (E := M ⧸ S) (mk a) + ε
Tactic: obtain ⟨a, rfl, ha⟩ := Submodule.Quotient.norm_mk_lt x hδ
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : Ring R
inst_3 : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst_4 : SeminormedCommRing 𝕜
inst_5 : Module 𝕜 M
inst_6 : IsBoundedSMul 𝕜 M
inst_7 : SMul 𝕜 R
inst_8 : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h :
  ∀ (x : ℝ),
    x - norm (E := M ⧸ S) (mk a) < δ ∧ norm (E := M ⧸ S) (mk a) - x < δ →
      ‖k‖ * x - ‖k‖ * norm (E := M ⧸ S) (mk a) < ε ∧ ‖k‖ * norm (E := M ⧸ S) (mk a) - ‖k‖ * x < ε
ha : ‖a‖ < norm (E := M ⧸ S) (mk a) + δ
⊢ ‖a‖ - norm (E := M ⧸ S) (mk a) < δ
have linarith : δ ≤ ‖a‖ - norm (E := M ⧸ S) (mk a) → ‖a‖ - (norm (E := M ⧸ S) (mk a) + δ) + (δ - (‖a‖ - norm (E := M ⧸ S) (mk a))) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : Ring R
inst_3 : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst_4 : SeminormedCommRing 𝕜
inst_5 : Module 𝕜 M
inst_6 : IsBoundedSMul 𝕜 M
inst_7 : SMul 𝕜 R
inst_8 : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h :
  ∀ (x : ℝ),
    x - norm (E := M ⧸ S) (mk a) < δ ∧ norm (E := M ⧸ S) (mk a) - x < δ →
      ‖k‖ * x - ‖k‖ * norm (E := M ⧸ S) (mk a) < ε ∧ ‖k‖ * norm (E := M ⧸ S) (mk a) - ‖k‖ * x < ε
ha : ‖a‖ < norm (E := M ⧸ S) (mk a) + δ
⊢ norm (E := M ⧸ S) (mk a) - ‖a‖ < δ
have linarith : δ ≤ norm (E := M ⧸ S) (mk a) - ‖a‖ →
  0 - δ + (δ - (norm (E := M ⧸ S) (mk a) - ‖a‖)) + (norm (E := M ⧸ S) (mk a) - ‖a‖) = 0
Tactic: linarith [Submodule.Quotient.norm_mk_le S a]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : Ring R
inst_3 : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst_4 : SeminormedCommRing 𝕜
inst_5 : Module 𝕜 M
inst_6 : IsBoundedSMul 𝕜 M
inst_7 : SMul 𝕜 R
inst_8 : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h :
  ∀ (x : ℝ),
    x - norm (E := M ⧸ S) (mk a) < δ ∧ norm (E := M ⧸ S) (mk a) - x < δ →
      ‖k‖ * x - ‖k‖ * norm (E := M ⧸ S) (mk a) < ε ∧ ‖k‖ * norm (E := M ⧸ S) (mk a) - ‖k‖ * x < ε
ha : ‖a‖ < norm (E := M ⧸ S) (mk a) + δ
⊢ ‖HSMul.hSMul (β := M ⧸ S) k (mk a)‖ ≤ ‖k‖ * norm (E := M ⧸ S) (mk a) + ε
have h₁ : ‖k‖ * ‖a‖ - ‖k‖ * norm (E := M ⧸ S) (mk a) < ε ∧ ‖k‖ * norm (E := M ⧸ S) (mk a) - ‖k‖ * ‖a‖ < ε
Tactic: specialize h ‖a‖ ⟨by linarith, by linarith [Submodule.Quotient.norm_mk_le S a]⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : Ring R
inst_3 : Module R M
S T : Submodule R M
h : S = T
⊢ ∀ (x : M ⧸ S), norm (E := M ⧸ T) ((S.quotEquivOfEq T h : (a : M ⧸ S) → M ⧸ T) x : M ⧸ T) = ‖x‖
have subst : ∀ (x : M ⧸ S), norm (E := M ⧸ S) ((S.quotEquivOfEq S sorry : (a : M ⧸ S) → M ⧸ S) x : M ⧸ S) = ‖x‖
Tactic: subst h
Cleared hypotheses: T, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
have this : ∃ (ia : ℝ × ℝ),
  (0 < ia.1 ∧ 0 < ia.2) ∧ ∀ x_1 ∈ ball ‖x‖ ia.1 ×ˢ ball ‖y‖ ia.2, x_1.1 * x_1.2 ∈ ball ((‖x‖, ‖y‖).1 * (‖x‖, ‖y‖).2) ε
Tactic: have := ((nhds_basis_ball.prod_nhds nhds_basis_ball).tendsto_iff nhds_basis_ball).mp
      (continuous_mul.tendsto (‖x‖, ‖y‖)) ε hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
this :
  ∃ (ia : ℝ × ℝ),
    (0 < ia.1 ∧ 0 < ia.2) ∧ ∀ x_1 ∈ ball ‖x‖ ia.1 ×ˢ ball ‖y‖ ia.2, x_1.1 * x_1.2 ∈ ball ((‖x‖, ‖y‖).1 * (‖x‖, ‖y‖).2) ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
have this₁ : ∃ (a : ℝ) (b : ℝ),
  (0 < a ∧ 0 < b) ∧ ∀ (a_1 b_1 : ℝ), dist a_1 ‖x‖ < a → dist b_1 ‖y‖ < b → dist (a_1 * b_1) (‖x‖ * ‖y‖) < ε
Tactic: simp only [Set.mem_prod, mem_ball, and_imp, Prod.forall, Prod.exists] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
this :
  ∃ (a : ℝ) (b : ℝ),
    (0 < a ∧ 0 < b) ∧ ∀ (a_1 b_1 : ℝ), dist a_1 ‖x‖ < a → dist b_1 ‖y‖ < b → dist (a_1 * b_1) (‖x‖ * ‖y‖) < ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
have rcases : ∀ (ε₁ ε₂ : ℝ) (h : ∀ (a b : ℝ), dist a ‖x‖ < ε₁ → dist b ‖y‖ < ε₂ → dist (a * b) (‖x‖ * ‖y‖) < ε) (h₁ : 0 < ε₁)
  (h₂ : 0 < ε₂), ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
Tactic: rcases this with ⟨ε₁, ε₂, ⟨h₁, h₂⟩, h⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h : ∀ (a b : ℝ), dist a ‖x‖ < ε₁ → dist b ‖y‖ < ε₂ → dist (a * b) (‖x‖ * ‖y‖) < ε
h₁ : 0 < ε₁
h₂ : 0 < ε₂
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
have obtain : ∀ (a : R) (ha : ‖a‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) + ε₁) (b : R)
  (h :
    ∀ (a_1 b_1 : ℝ),
      dist a_1 (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I)) < ε₁ →
        dist b_1 (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I)) < ε₂ →
          dist (a_1 * b_1)
              (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I)) <
            ε)
  (hb : ‖b‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε₂),
  ‖HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I)‖ ≤
    norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) * norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε
Tactic: obtain ⟨⟨a, rfl, ha⟩, ⟨b, rfl, hb⟩⟩ := Ideal.Quotient.norm_mk_lt x h₁,
      Ideal.Quotient.norm_mk_lt y h₂
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) + ε₁
b : R
h :
  ∀ (a_1 b_1 : ℝ),
    dist a_1 (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I)) < ε₁ →
      dist b_1 (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I)) < ε₂ →
        dist (a_1 * b_1)
            (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
              norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I)) <
          ε
hb : ‖b‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε₂
⊢ ‖HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I)‖ ≤
    norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) * norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε
have h₃ : ∀ (a_1 b_1 : ℝ),
  a_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) < ε₁ ∧
      norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - a_1 < ε₁ →
    b_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) < ε₂ ∧
        norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - b_1 < ε₂ →
      a_1 * b_1 -
            norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
              norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) <
          ε ∧
        norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
              norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) -
            a_1 * b_1 <
          ε
Tactic: simp only [dist, abs_sub_lt_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) + ε₁
b : R
hb : ‖b‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) < ε₁ ∧
        norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - a_1 < ε₁ →
      b_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) < ε₂ ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - b_1 < ε₂ →
        a_1 * b_1 -
              norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) <
            ε ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) -
              a_1 * b_1 <
            ε
⊢ ‖a‖ - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) < ε₁
have linarith : ε₁ ≤ ‖a‖ - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) →
  ‖a‖ - (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) + ε₁) +
      (ε₁ - (‖a‖ - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I))) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) + ε₁
b : R
hb : ‖b‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) < ε₁ ∧
        norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - a_1 < ε₁ →
      b_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) < ε₂ ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - b_1 < ε₂ →
        a_1 * b_1 -
              norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) <
            ε ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) -
              a_1 * b_1 <
            ε
⊢ norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - ‖a‖ < ε₁
have linarith : ε₁ ≤ norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - ‖a‖ →
  0 - ε₁ + (ε₁ - (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - ‖a‖)) +
      (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - ‖a‖) =
    0
Tactic: linarith [Ideal.Quotient.norm_mk_le I a]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) + ε₁
b : R
hb : ‖b‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) < ε₁ ∧
        norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - a_1 < ε₁ →
      b_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) < ε₂ ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - b_1 < ε₂ →
        a_1 * b_1 -
              norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) <
            ε ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) -
              a_1 * b_1 <
            ε
⊢ ‖b‖ - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) < ε₂
have linarith : ε₂ ≤ ‖b‖ - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) →
  ‖b‖ - (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε₂) +
      (ε₂ - (‖b‖ - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I))) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
R : Type u_3
inst_2 : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) + ε₁
b : R
hb : ‖b‖ < norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) < ε₁ ∧
        norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - a_1 < ε₁ →
      b_1 - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) < ε₂ ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - b_1 < ε₂ →
        a_1 * b_1 -
              norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) <
            ε ∧
          norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) *
                norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) -
              a_1 * b_1 <
            ε
⊢ norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - ‖b‖ < ε₂
have linarith : ε₂ ≤ norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - ‖b‖ →
  0 - ε₂ + (ε₂ - (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - ‖b‖)) +
      (norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - ‖b‖) =
    0
Tactic: linarith [Ideal.Quotient.norm_mk_le I b]