awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
a : M
this_1 : Nonempty.{u_1 + 1} (↑{m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑a : M ⧸ S)} : Type u_1)
b : M
this : Nonempty.{u_1 + 1} (↑{m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑b : M ⧸ S)} : Type u_1)
refine :
  dist 1
      (↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) {m : M | (↑m : M ⧸ S) = HMul.hMul (α := M ⧸ S) (↑a : M ⧸ S) (↑b : M ⧸ S)} x)
            (a * b) ⋯) :
        M) ≤
    dist 1
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑a : M ⧸ S)} x) a ⋯) :
          M) +
      dist 1
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑b : M ⧸ S)} x) b ⋯) :
          M)
⊢ ⨅ (y : (↑{m : M | (↑m : M ⧸ S) = HMul.hMul (α := M ⧸ S) (↑a : M ⧸ S) (↑b : M ⧸ S)} : Type u_1)), dist 1 (↑y : M) ≤
    dist 1
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑a : M ⧸ S)} x) a ⋯) :
          M) +
      dist 1
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑b : M ⧸ S)} x) b ⋯) :
          M)

Tactic:
refine ciInf_le_of_le ⟨0, forall_mem_range.2 fun _ ↦ dist_nonneg⟩ ⟨a * b, rfl⟩ ?_

Premises used: Iff.mpr, Set.forall_mem_range, dist_nonneg, ciInf_le_of_le, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
a : M
this_1 : Nonempty.{u_1 + 1} (↑{m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑a : M ⧸ S)} : Type u_1)
b : M
this : Nonempty.{u_1 + 1} (↑{m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑b : M ⧸ S)} : Type u_1)
⊢ dist 1
      (↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) {m : M | (↑m : M ⧸ S) = HMul.hMul (α := M ⧸ S) (↑a : M ⧸ S) (↑b : M ⧸ S)} x)
            (a * b) ⋯) :
        M) ≤
    dist 1
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑a : M ⧸ S)} x) a ⋯) :
          M) +
      dist 1
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑b : M ⧸ S)} x) b ⋯) :
          M)

Tactic:
simpa using norm_mul_le' _ _

Premises used: norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r_1 ε : ℝ
x : M ⧸ S
r : ℝ
simp :
  (∀ ⦃y : M⦄, Membership.mem (γ := Set M) {m : M | (↑m : M ⧸ S) = x⁻¹} y → r ≤ dist 1 y) ↔
    ∀ ⦃y : M⦄, Membership.mem (γ := Set M) {m : M | (↑m : M ⧸ S) = x} y → r ≤ dist 1 y
⊢ r ≤ infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x⁻¹} ↔ r ≤ infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x}

Tactic:
simp only [le_infDist (norm_aux _)]

Premises used: _private.0.QuotientGroup.norm_aux, Metric.le_infDist
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r_1 ε : ℝ
x : M ⧸ S
r : ℝ
⊢ ∀ (a : M),
    Membership.mem (γ := Set M) {m : M | (↑m : M ⧸ S) = x⁻¹} a → r ≤ dist 1 a ↔
      Membership.mem (α := M) (γ := Set M) {m : M | (↑m : M ⧸ S) = x} ((Equiv.inv M : (a : M) → M) a : M) →
        r ≤ dist (α := M) (1 : M) ((Equiv.inv M : (a : M) → M) a : M)

Tactic:
simp [← inv_eq_iff_eq_inv]

Premises used: inv_eq_iff_eq_inv
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r_1 ε : ℝ
x : M ⧸ S
r : ℝ
⊢ (∀ ⦃y : M⦄, Membership.mem (γ := Set M) {m : M | (↑m : M ⧸ S) = x⁻¹} y → r ≤ dist 1 y) ↔
    ∀ ⦃y : M⦄, Membership.mem (γ := Set M) {m : M | (↑m : M ⧸ S) = x} y → r ≤ dist 1 y

Tactic:
exact (Equiv.inv _).forall_congr (by simp [← inv_eq_iff_eq_inv])

Premises used: Equiv.inv, Equiv.forall_congr
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
⊢ ‖x‖ = (groupSeminorm : (a : M ⧸ S) → ℝ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
⊢ ‖x‖ = infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x}

Tactic:
rfl

Premises used: Metric.infDist, ENNReal.toReal, NNReal.toReal, rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
r : ℝ
⊢ r ≤ ‖x‖ ↔ ∀ (m : M), (↑m : M ⧸ S) = x → r ≤ ‖m‖

Tactic:
simp [norm_eq_infDist, le_infDist (norm_aux _)]

Premises used: _private.0.QuotientGroup.norm_aux, Metric.le_infDist, QuotientGroup.norm_eq_infDist
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
r : ℝ
⊢ ‖x‖ < r ↔ ∃ (m : M), (↑m : M ⧸ S) = x ∧ ‖m‖ < r

Tactic:
simp [norm_eq_infDist, infDist_lt_iff (norm_aux _)]

Premises used: _private.0.QuotientGroup.norm_aux, Metric.infDist_lt_iff, QuotientGroup.norm_eq_infDist
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
⊢ ∀ (ε : ℝ), Eq.{u_1 + 1} (α := Set (M ⧸ S)) (mk '' ball 1 ε) {x : M ⧸ S | ‖x‖ < ε}

Tactic:
fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_

Premises used: Iff.mpr, Set.ext, QuotientGroup.forall_mk
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
refine :
  ∀ (ε : ℝ) (x : M),
    Membership.mem (γ := Set (M ⧸ S)) (mk '' ball 1 ε) (↑x : M ⧸ S) ↔
      Membership.mem (γ := Set (M ⧸ S)) {x : M ⧸ S | ‖x‖ < ε} (↑x : M ⧸ S)
⊢ ∀ (ε : ℝ), Eq.{u_1 + 1} (α := Set (M ⧸ S)) (mk '' ball 1 ε) {x : M ⧸ S | ‖x‖ < ε}

Tactic:
refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_

Premises used: Iff.mpr, Set.ext, QuotientGroup.forall_mk
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
rw :
  (∃ (x_1 : M), Membership.mem (γ := Set M) {x : M | ‖x‖ < ε} x_1 ∧ Eq (α := M ⧸ S) (↑x_1 : M ⧸ S) (↑x : M ⧸ S)) ↔
    ∃ (m : M), Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑x : M ⧸ S) ∧ ‖m‖ < ε
⊢ Membership.mem (γ := Set (M ⧸ S)) (mk '' ball 1 ε) (↑x : M ⧸ S) ↔
    Membership.mem (γ := Set (M ⧸ S)) {x : M ⧸ S | ‖x‖ < ε} (↑x : M ⧸ S)

Tactic:
rw [ball_one_eq, mem_setOf_eq, norm_lt_iff, mem_image]

Premises used: Set.mem_image, ball_one_eq, Set.mem_setOf_eq, QuotientGroup.norm_lt_iff
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ (∃ (x_1 : M), Membership.mem (γ := Set M) {x : M | ‖x‖ < ε} x_1 ∧ Eq (α := M ⧸ S) (↑x_1 : M ⧸ S) (↑x : M ⧸ S)) ↔
    ∃ (m : M), Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑x : M ⧸ S) ∧ ‖m‖ < ε

Tactic:
exists_congr fun _ ↦ and_comm

Premises used: and_comm, exists_congr
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ (∃ (x_1 : M), Membership.mem (γ := Set M) {x : M | ‖x‖ < ε} x_1 ∧ Eq (α := M ⧸ S) (↑x_1 : M ⧸ S) (↑x : M ⧸ S)) ↔
    ∃ (m : M), Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑x : M ⧸ S) ∧ ‖m‖ < ε

Tactic:
exact exists_congr fun _ ↦ and_comm

Premises used: and_comm, exists_congr
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
⊢ ∀ (ε : ℝ), Eq.{u_1 + 1} (α := Set (M ⧸ S)) (mk '' ball 1 ε) {x : M ⧸ S | ‖x‖ < ε}

Tactic:
have : ∀ ε : ℝ, mk '' ball (1 : M) ε = {x : M ⧸ S | ‖x‖ < ε} := by
    refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
    rw [ball_one_eq, mem_setOf_eq, norm_lt_iff, mem_image]
    exact exists_congr fun _ ↦ and_comm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), Eq.{u_1 + 1} (α := Set (M ⧸ S)) (mk '' ball 1 ε) {x : M ⧸ S | ‖x‖ < ε}
rw : Filter.HasBasis.{u_1, 1} (α := M ⧸ S) (Filter.map mk (𝓝 1)) (fun (ε : ℝ) ↦ 0 < ε) fun (x : ℝ) ↦ mk '' ball 1 x
⊢ Filter.HasBasis.{u_1, 1} (α := M ⧸ S) (𝓝 1) (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {x : M ⧸ S | ‖x‖ < ε}

Tactic:
rw [← mk_one, nhds_eq, ← funext this]

Premises used: QuotientGroup.mk_one, QuotientGroup.nhds_eq, funext
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), Eq.{u_1 + 1} (α := Set (M ⧸ S)) (mk '' ball 1 ε) {x : M ⧸ S | ‖x‖ < ε}
⊢ Filter.HasBasis.{u_1, 1} (α := M ⧸ S) (Filter.map mk (𝓝 1)) (fun (ε : ℝ) ↦ 0 < ε) fun (x : ℝ) ↦ mk '' ball 1 x

Tactic:
.map _ Metric.nhds_basis_ball

Premises used: Filter.HasBasis.map, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), Eq.{u_1 + 1} (α := Set (M ⧸ S)) (mk '' ball 1 ε) {x : M ⧸ S | ‖x‖ < ε}
⊢ Filter.HasBasis.{u_1, 1} (α := M ⧸ S) (Filter.map mk (𝓝 1)) (fun (ε : ℝ) ↦ 0 < ε) fun (x : ℝ) ↦ mk '' ball 1 x

Tactic:
exact .map _ Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M
rw :
  infDist (α := M) ((IsometryEquiv.divLeft x : (a : M) → M) 1 : M)
      (preimage (β := M) (⇑(IsometryEquiv.symm (IsometryEquiv.divLeft x)) : (a : M) → M)
          {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑x : M ⧸ S)} :
        Set M) =
    infDist x (↑S : Set M)
⊢ norm (E := M ⧸ S) (↑x : M ⧸ S) = infDist x (↑S : Set M)

Tactic:
rw [norm_eq_infDist, ← infDist_image (IsometryEquiv.divLeft x).isometry,
    ← IsometryEquiv.preimage_symm]

Premises used: Metric.infDist_image, QuotientGroup.norm_eq_infDist, IsometryEquiv.divLeft, IsometryEquiv.preimage_symm, IsometryEquiv.isometry
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ infDist (α := M) ((IsometryEquiv.divLeft x : (a : M) → M) 1 : M)
      (preimage (β := M) (⇑(IsometryEquiv.symm (IsometryEquiv.divLeft x)) : (a : M) → M)
          {m : M | Eq (α := M ⧸ S) (↑m : M ⧸ S) (↑x : M ⧸ S)} :
        Set M) =
    infDist x (↑S : Set M)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ Membership.mem (γ := Set M) {m_1 : M | Eq (α := M ⧸ S) (↑m_1 : M ⧸ S) (↑m : M ⧸ S)} m

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
rw : (↑S : Set M).Nonempty
⊢ norm (E := M ⧸ S) (↑m : M ⧸ S) = 0 ↔ m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set M)

Tactic:
rw [norm_mk, ← mem_closure_iff_infDist_zero]

Premises used: QuotientGroup.norm_mk, Metric.mem_closure_iff_infDist_zero
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ (↑S : Set M).Nonempty

Tactic:
⟨1, S.one_mem⟩

Premises used: Subgroup.one_mem, Set.Nonempty, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ (↑S : Set M).Nonempty

Tactic:
exact ⟨1, S.one_mem⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set M)
rw : m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set M) ↔ m ∈ S
rw₁ : m ∈ (↑S : Set M) ↔ m ∈ S
rw₂ rw₃ : m ∈ S ↔ m ∈ S
⊢ norm (E := M ⧸ S) (↑m : M ⧸ S) = 0 ↔ m ∈ S

Tactic:
rw [norm_mk_eq_zero_iff_mem_closure, hS.closure_eq, SetLike.mem_coe]

Premises used: QuotientGroup.norm_mk_eq_zero_iff_mem_closure, IsClosed.closure_eq, SetLike.mem_coe
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M ⧸ S
hε : 0 < ε
⊢ ∃ (m : M), (↑m : M ⧸ S) = x ∧ ‖m‖ < ‖x‖ + ε

Tactic:
norm_lt_iff.1 <| lt_add_of_pos_right _ hε

Premises used: lt_add_of_pos_right, Iff.mp, QuotientGroup.norm_lt_iff
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
obtain :
  ∀ (n : M) (hn : Eq (α := M ⧸ S) (↑n : M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m))
    (hn' : ‖n‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε),
    ∃ s ∈ S, ‖m * s‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε
⊢ ∃ s ∈ S, ‖m * s‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε

Tactic:
obtain ⟨n : M, hn, hn'⟩ := exists_norm_mk_lt (QuotientGroup.mk' S m) hε

Premises used: QuotientGroup.exists_norm_mk_lt, QuotientGroup.mk', DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : Eq (α := M ⧸ S) (↑n : M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m)
hn' : ‖n‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε
⊢ m⁻¹ * n ∈ S

Tactic:
simpa [eq_comm, QuotientGroup.eq] using hn

Premises used: QuotientGroup.eq, eq_comm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : Eq (α := M ⧸ S) (↑n : M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m)
hn' : ‖n‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε
⊢ ‖m * (m⁻¹ * n)‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : Eq (α := M ⧸ S) (↑n : M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m)
hn' : ‖n‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε
⊢ ∃ s ∈ S, ‖m * s‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε

Tactic:
exact ⟨m⁻¹ * n, by simpa [eq_comm, QuotientGroup.eq] using hn, by simpa⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
rw :
  Eq.{u_1 + 1} (α := Filter ((M ⧸ S) × M ⧸ S))
    (⨅ (i : ℝ),
      ⨅ (_ : 0 < i),
        Filter.principal (preimage (β := M ⧸ S) (fun (p : (M ⧸ S) × M ⧸ S) ↦ p.1⁻¹ * p.2) {x : M ⧸ S | ‖x‖ < i}))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : (M ⧸ S) × M ⧸ S | dist p.1 p.2 < ε})
⊢ Eq.{u_1 + 1} (α := Filter ((M ⧸ S) × M ⧸ S)) (uniformity (M ⧸ S))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : (M ⧸ S) × M ⧸ S | dist p.1 p.2 < ε})

Tactic:
rw [uniformity_eq_comap_nhds_one_left, (nhds_one_hasBasis.comap _).eq_biInf]

Premises used: QuotientGroup.nhds_one_hasBasis, Filter.HasBasis.eq_biInf, Filter.HasBasis.comap, uniformity_eq_comap_nhds_one_left
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ Eq.{u_1 + 1} (α := Filter ((M ⧸ S) × M ⧸ S))
    (⨅ (i : ℝ),
      ⨅ (_ : 0 < i),
        Filter.principal (preimage (β := M ⧸ S) (fun (p : (M ⧸ S) × M ⧸ S) ↦ p.1⁻¹ * p.2) {x : M ⧸ S | ‖x‖ < i}))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : (M ⧸ S) × M ⧸ S | dist p.1 p.2 < ε})

Tactic:
simp only [dist, preimage_setOf_eq, norm_eq_groupSeminorm]

Premises used: Set.preimage_setOf_eq, Dist.dist, QuotientGroup.norm_eq_groupSeminorm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ Eq.{u_1 + 1} (α := TopologicalSpace (Quotient (leftRel S))) instTopologicalSpaceQuotient
    UniformSpace.toTopologicalSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
inst_1 : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set M)
⊢ instSeminormedCommGroup S = NormedCommGroup.toSeminormedCommGroup

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S = T
subst : Isometry (Subgroup.quotientEquivOfEq ⋯).toFun
⊢ Isometry (Subgroup.quotientEquivOfEq h).toFun

Tactic:
subst h
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
__spread.0 : M ⧸ S ≃ M ⧸ S := Subgroup.quotientEquivOfEq ⋯
x1 : M ⧸ S
a : M
x2 : M ⧸ S
a_1 : M
⊢ edist ((Subgroup.quotientEquivOfEq ⋯).toFun (Quot.mk (⇑(leftRel S) : M → M → Prop) a))
      ((Subgroup.quotientEquivOfEq ⋯).toFun (Quot.mk (⇑(leftRel S) : M → M → Prop) a_1)) =
    edist (α := M ⧸ S) (Quot.mk (⇑(leftRel S) : M → M → Prop) a) (Quot.mk (⇑(leftRel S) : M → M → Prop) a_1)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
rw : ∀ (x : HasQuotient.Quotient M (B := Subgroup M) ⊥), norm (E := M) ((quotientBot : (a : M ⧸ ⊥) → M) x : M) = ‖x‖
⊢ Isometry.{u_1, u_1} (α := HasQuotient.Quotient M (B := Subgroup M) ⊥) (β := M) (⇑quotientBot : (a : M ⧸ ⊥) → M)

Tactic:
rw [MonoidHomClass.isometry_iff_norm]

Premises used: MonoidHomClass.isometry_iff_norm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x_2 : HasQuotient.Quotient M (B := Subgroup M) ⊥
x : M
mk : ‖x‖ = norm (E := HasQuotient.Quotient M (B := Subgroup M) ⊥) (↑x : M ⧸ ⊥)
⊢ norm (E := M) ((quotientBot : (a : M ⧸ ⊥) → M) (Quot.mk (⇑(leftRel ⊥) : M → M → Prop) x) : M) =
    norm (E := HasQuotient.Quotient M (B := Subgroup M) ⊥) (Quot.mk (⇑(leftRel ⊥) : M → M → Prop) x)

Tactic:
change ‖x‖ = ‖QuotientGroup.mk x‖

Premises used: QuotientGroup.mk
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x_2 : HasQuotient.Quotient M (B := Subgroup M) ⊥
x : M
⊢ ‖x‖ = norm (E := HasQuotient.Quotient M (B := Subgroup M) ⊥) (↑x : M ⧸ ⊥)

Tactic:
simp [norm_mk]

Premises used: QuotientGroup.norm_mk
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S ≤ T
rw :
  ∀ (x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T),
    norm (E := M ⧸ T)
        ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x : M ⧸ T) =
      ‖x‖
⊢ Isometry (α := (M ⧸ S) ⧸ Subgroup.map (mk' S) T) (β := M ⧸ T)
    (⇑(quotientQuotientEquivQuotient S T h) : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T)

Tactic:
rw [MonoidHomClass.isometry_iff_norm]

Premises used: MonoidHomClass.isometry_iff_norm
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S ≤ T
⊢ ∀ (x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T),
    norm (E := M ⧸ T)
        ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x : M ⧸ T) =
      ‖x‖

Tactic:
fun x => eq_of_forall_le_iff fun r => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S ≤ T
refine :
  ∀ (x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) (r : ℝ),
    r ≤
        norm (E := M ⧸ T)
          ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x : M ⧸ T) ↔
      r ≤ ‖x‖
⊢ ∀ (x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T),
    norm (E := M ⧸ T)
        ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x : M ⧸ T) =
      ‖x‖

Tactic:
refine fun x => eq_of_forall_le_iff fun r => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r_1 ε : ℝ
h : S ≤ T
x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T
r : ℝ
simp :
  (∀ (m : M),
      Eq (α := M ⧸ T) (↑m : M ⧸ T)
          ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x) →
        r ≤ ‖m‖) ↔
    ∀ (m : M ⧸ S), (↑m : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) = x → ∀ (m_1 : M), (↑m_1 : M ⧸ S) = m → r ≤ ‖m_1‖
⊢ r ≤
      norm (E := M ⧸ T)
        ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x : M ⧸ T) ↔
    r ≤ ‖x‖

Tactic:
simp only [le_norm_iff]

Premises used: QuotientGroup.le_norm_iff
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r_1 ε : ℝ
h : S ≤ T
x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T
r : ℝ
h₁ :
  ∀ (m : M),
    Eq (α := M ⧸ T) (↑m : M ⧸ T)
        ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x) →
      r ≤ ‖m‖
y : M ⧸ S
h₂ : (↑y : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) = x
z : M
h₃ : (↑z : M ⧸ S) = y
subst_vars :
  ∀
    (h₁ :
      ∀ (m : M),
        Eq (α := M ⧸ T) (↑m : M ⧸ T)
            ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T)
              (↑(↑z : M ⧸ S) : (M ⧸ S) ⧸ Subgroup.map (mk' S) T)) →
          r ≤ ‖m‖),
    Eq (α := M ⧸ T) (↑z : M ⧸ T)
      ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T)
        (↑(↑z : M ⧸ S) : (M ⧸ S) ⧸ Subgroup.map (mk' S) T))
⊢ Eq (α := M ⧸ T) (↑z : M ⧸ T)
    ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x)

Tactic:
subst_vars
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r_1 ε : ℝ
h : S ≤ T
r : ℝ
z : M
h₁ :
  ∀ (m : M),
    Eq (α := M ⧸ T) (↑m : M ⧸ T)
        ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T)
          (↑(↑z : M ⧸ S) : (M ⧸ S) ⧸ Subgroup.map (mk' S) T)) →
      r ≤ ‖m‖
⊢ Eq (α := M ⧸ T) (↑z : M ⧸ T)
    ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T)
      (↑(↑z : M ⧸ S) : (M ⧸ S) ⧸ Subgroup.map (mk' S) T))

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r_1 ε : ℝ
h : S ≤ T
x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T
r : ℝ
⊢ (∀ (m : M),
      Eq (α := M ⧸ T) (↑m : M ⧸ T)
          ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x) →
        r ≤ ‖m‖) ↔
    ∀ (m : M ⧸ S), (↑m : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) = x → ∀ (m_1 : M), (↑m_1 : M ⧸ S) = m → r ≤ ‖m_1‖

Tactic:
exact ⟨
      fun h₁ y h₂ z h₃ => h₁ z <| by subst_vars; rfl,
      fun h₁ y h₂ => h₁ y ((quotientQuotientEquivQuotient S T h).injective h₂) y rfl⟩
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
rw :
  Eq (α := ℝ) (⨅ (y : (↑(↑S : Set M) : Type u_1)), dist (-m) (↑y : M))
    (⨅ (a : (↑(↑S : Set M) : Type u_1)), ‖m + (↑a : M)‖)
⊢ norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) = sInf ((fun (x : M) ↦ ‖m + x‖) '' (↑S : Set M))

Tactic:
rw [mk'_apply, norm_mk, sInf_image', ← infDist_image isometry_neg, image_neg_eq_neg,
    neg_coe_set (H := S), infDist_eq_iInf]

Premises used: Set.image_neg_eq_neg, Metric.infDist_image, QuotientAddGroup.norm_mk, neg_coe_set, sInf_image', Metric.infDist_eq_iInf, isometry_neg, QuotientAddGroup.mk'_apply
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ Eq (α := ℝ) (⨅ (y : (↑(↑S : Set M) : Type u_1)), dist (-m) (↑y : M))
    (⨅ (a : (↑(↑S : Set M) : Type u_1)), ‖m + (↑a : M)‖)

Tactic:
simp only [dist_eq_norm', sub_neg_eq_add, add_comm]

Premises used: dist_eq_norm', add_comm, sub_neg_eq_add
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M ⧸ S
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
norm_add_le x y

Premises used: setOf, norm_add_le
-- Module: Mathlib.Analysis.Normed.Group.Quotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖ZeroHom.toFun (↑(mk' S) : ZeroHom M (M ⧸ S)) m‖ ≤ 1 * ‖m‖

Tactic:
simpa [one_mul] using norm_mk_le_norm

Premises used: QuotientAddGroup.norm_mk_le_norm, one_mul