awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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
fb' : ‖f‖ ≤ (↑1 : ℝ)
⊢ norm.{u_3} (E := N) ((lift S f hf : (a : M ⧸ S) → N) x : N) ≤ ‖x‖

Tactic:
simpa using le_of_opNorm_le _ (f.lift_norm_le _ _ fb') _

Premises used: NormedAddGroupHom.le_of_opNorm_le, NormedAddGroupHom.lift_norm_le
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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
inst_4 : CompleteSpace M
⊢ CompleteSpace.{u_1} (M ⧸ S)

Tactic:
QuotientAddGroup.completeSpace_left M S.toAddSubgroup

Premises used: QuotientAddGroup.completeSpace_left, Submodule.toAddSubgroup, Submodule.quotientRel
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
R : Type u_3
inst_1 : Ring R
inst_2 : Module R M
S : Submodule R M
x : M ⧸ S
ε : ℝ
hε : 0 < ε
⊢ ∃ (m : M), mk m = x ∧ ‖m‖ < ‖x‖ + ε

Tactic:
exists_norm_mk_lt x hε

Premises used: QuotientAddGroup.exists_norm_mk_lt, Submodule.Quotient.mk, Submodule.quotientRel
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
R : Type u_3
inst_1 : Ring R
inst_2 : Module R M
S : Submodule R M
m : M
⊢ norm (E := M ⧸ S) (mk m) ≤ ‖m‖

Tactic:
norm_mk_le_norm

Premises used: Submodule.Quotient.mk, setOf, QuotientAddGroup.norm_mk_le_norm, Submodule.quotientRel
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 < ε
⊢ ∃ (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ε
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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‖) ε
⊢ ∃ (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

Premises used: abs_sub_lt_iff, Metric.mem_ball, Dist.dist
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 < ε
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‖ + ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε

Tactic:
rcases this with ⟨δ, hδ, h⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 < ε
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) + ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε

Tactic:
obtain ⟨a, rfl, ha⟩ := Submodule.Quotient.norm_mk_lt x hδ

Premises used: Submodule.Quotient.norm_mk_lt, rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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) + δ
linarith :
  δ ≤ ‖a‖ - norm (E := M ⧸ S) (mk a) → ‖a‖ - (norm (E := M ⧸ S) (mk a) + δ) + (δ - (‖a‖ - norm (E := M ⧸ S) (mk a))) = 0
⊢ ‖a‖ - norm (E := M ⧸ S) (mk a) < δ

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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) + δ
linarith :
  δ ≤ norm (E := M ⧸ S) (mk a) - ‖a‖ →
    0 - δ + (δ - (norm (E := M ⧸ S) (mk a) - ‖a‖)) + (norm (E := M ⧸ S) (mk a) - ‖a‖) = 0
⊢ norm (E := M ⧸ S) (mk a) - ‖a‖ < δ

Tactic:
linarith [Submodule.Quotient.norm_mk_le S a]

Premises used: Submodule.Quotient.norm_mk_le
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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) + δ
⊢ ‖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]⟩

Premises used: Norm.norm, And.intro
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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
ha : ‖a‖ < norm (E := M ⧸ S) (mk a) + δ
h : ‖k‖ * ‖a‖ - ‖k‖ * norm (E := M ⧸ S) (mk a) < ε ∧ ‖k‖ * norm (E := M ⧸ S) (mk a) - ‖k‖ * ‖a‖ < ε
⊢ norm (E := M ⧸ S) (mk (k • a)) ≤ ‖k‖ * ‖a‖

Tactic:
(norm_mk_le ..).trans (norm_smul_le k a)

Premises used: norm_smul_le, LE.le.trans, Submodule.Quotient.norm_mk_le
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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
ha : ‖a‖ < norm (E := M ⧸ S) (mk a) + δ
h : ‖k‖ * ‖a‖ - ‖k‖ * norm (E := M ⧸ S) (mk a) < ε ∧ ‖k‖ * norm (E := M ⧸ S) (mk a) - ‖k‖ * ‖a‖ < ε
⊢ ‖k‖ * ‖a‖ ≤ ‖k‖ * norm (E := M ⧸ S) (mk a) + ε

Tactic:
(sub_lt_iff_lt_add'.mp h.1).le

Premises used: LT.lt.le, sub_lt_iff_lt_add', And.left, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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
ha : ‖a‖ < norm (E := M ⧸ S) (mk a) + δ
h : ‖k‖ * ‖a‖ - ‖k‖ * norm (E := M ⧸ S) (mk a) < ε ∧ ‖k‖ * norm (E := M ⧸ S) (mk a) - ‖k‖ * ‖a‖ < ε
⊢ ‖HSMul.hSMul (β := M ⧸ S) k (mk a)‖ ≤ ‖k‖ * norm (E := M ⧸ S) (mk a) + ε

Tactic:
calc
        _ ≤ ‖k‖ * ‖a‖ := (norm_mk_le ..).trans (norm_smul_le k a)
        _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le

Premises used: norm_smul_le, LT.lt.le, sub_lt_iff_lt_add', And.left, Iff.mp, LE.le.trans, Submodule.Quotient.norm_mk_le
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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
subst : ∀ (x : M ⧸ S), norm (E := M ⧸ S) ((S.quotEquivOfEq S ⋯ : (a : M ⧸ S) → M ⧸ S) x : M ⧸ S) = ‖x‖
⊢ ∀ (x : M ⧸ S), norm (E := M ⧸ T) ((S.quotEquivOfEq T h : (a : M ⧸ S) → M ⧸ T) x : M ⧸ T) = ‖x‖

Tactic:
subst h
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 : Submodule R M
__spread.0 : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
x : M ⧸ S
a : M
⊢ norm (E := M ⧸ S) ((S.quotEquivOfEq S ⋯ : (a : M ⧸ S) → M ⧸ S) (Quot.mk (⇑S.quotientRel : M → M → Prop) a) : M ⧸ S) =
    norm (E := M ⧸ S) (Quot.mk (⇑S.quotientRel : M → M → Prop) a)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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
⊢ map S.mkQ T = map S.mkQ (S ⊔ T)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
R : Type u_3
inst : SeminormedCommRing R
I : Ideal R
x : R ⧸ I
ε : ℝ
hε : 0 < ε
⊢ ∃ (r : R), (mk I : (a : R) → R ⧸ I) r = x ∧ ‖r‖ < ‖x‖ + ε

Tactic:
exists_norm_mk_lt x hε

Premises used: QuotientAddGroup.exists_norm_mk_lt, Submodule.Quotient.mk, setOf, Submodule.quotientRel
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
R : Type u_3
inst : SeminormedCommRing R
I : Ideal R
r : R
⊢ norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) r : R ⧸ I) ≤ ‖r‖

Tactic:
norm_mk_le_norm

Premises used: Submodule.Quotient.mk, setOf, QuotientAddGroup.norm_mk_le_norm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 < ε
⊢ ∃ (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ε
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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) ε
⊢ ∃ (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

Premises used: and_imp, Metric.mem_ball, Set.mem_prod, Prod.forall, Prod.exists
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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‖) < ε
rcases :
  ∀ (ε₁ ε₂ : ℝ) (h : ∀ (a b : ℝ), dist a ‖x‖ < ε₁ → dist b ‖y‖ < ε₂ → dist (a * b) (‖x‖ * ‖y‖) < ε) (h₁ : 0 < ε₁)
    (h₂ : 0 < ε₂), ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε

Tactic:
rcases this with ⟨ε₁, ε₂, ⟨h₁, h₂⟩, h⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 < ε₂
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) +
        ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε

Tactic:
obtain ⟨⟨a, rfl, ha⟩, ⟨b, rfl, hb⟩⟩ := Ideal.Quotient.norm_mk_lt x h₁,
      Ideal.Quotient.norm_mk_lt y h₂

Premises used: Ideal.Quotient.norm_mk_lt, rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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) + ε₂
⊢ ∀ (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

Premises used: abs_sub_lt_iff, Dist.dist
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 <
            ε
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
⊢ ‖a‖ - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) < ε₁

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 <
            ε
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
⊢ norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) a : R ⧸ I) - ‖a‖ < ε₁

Tactic:
linarith [Ideal.Quotient.norm_mk_le I a]

Premises used: Ideal.Quotient.norm_mk_le
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 <
            ε
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
⊢ ‖b‖ - norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) < ε₂

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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 <
            ε
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
⊢ norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) b : R ⧸ I) - ‖b‖ < ε₂

Tactic:
linarith [Ideal.Quotient.norm_mk_le I b]

Premises used: Ideal.Quotient.norm_mk_le
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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‖ * ‖b‖ -
        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‖ * ‖b‖ <
      ε

Tactic:
specialize h ‖a‖ ‖b‖ ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I a]⟩
      ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I b]⟩

Premises used: Norm.norm, And.intro
-- Module: Mathlib.Analysis.Normed.Group.Quotient
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‖ * ‖b‖ -
        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‖ * ‖b‖ <
      ε
⊢ norm (E := R ⧸ I) ((mk I : (a : R) → R ⧸ I) (a * b) : R ⧸ I) ≤ ‖a‖ * ‖b‖

Tactic:
(Ideal.Quotient.norm_mk_le I (a * b)).trans (norm_mul_le a b)

Premises used: HMul.hMul, LE.le.trans, norm_mul_le, Ideal.Quotient.norm_mk_le