awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
rw : s * HSMul.hSMul (β := Set E) x (closedBall 1 δ) = x • cthickening δ s
⊢ s * closedBall x δ = x • cthickening δ s
have rw₁ : x • (s * closedBall 1 δ) = x • cthickening δ s
Tactic: rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
rw : s * HSMul.hSMul (β := Set E) x (closedBall 1 δ) = x • cthickening δ s
rw₁ : x • (s * closedBall 1 δ) = x • cthickening δ s
⊢ s * closedBall x δ = x • cthickening δ s
have rw₂ : x • cthickening δ s = x • cthickening δ s
Tactic: rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s
have rw : s * closedBall x δ = x • cthickening δ s
Tactic: rw [mul_comm, hs.mul_closedBall hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Pointwise (goal)
Goal:
E : Type u_1
inst : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
rw : s * closedBall x δ = x • cthickening δ s
⊢ closedBall x δ * s = x • cthickening δ s
have rw₁ : x • cthickening δ s = x • cthickening δ s
Tactic: rw [mul_comm, hs.mul_closedBall hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
⊢ infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x * y} ≤
    infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x} + infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = y}
have simp : ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤
  HAdd.hAdd (α := ℝ) (⨅ (y : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)), dist 1 (↑y : M))
    (⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)), dist 1 (↑y_1 : M))
Tactic: simp only [infDist_eq_iInf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
⊢ ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤
    HAdd.hAdd (α := ℝ) (⨅ (y : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)), dist 1 (↑y : M))
      (⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)), dist 1 (↑y_1 : M))
have this : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)
Tactic: have := (norm_aux x).to_subtype
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
this : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)
⊢ ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤
    HAdd.hAdd (α := ℝ) (⨅ (y : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)), dist 1 (↑y : M))
      (⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)), dist 1 (↑y_1 : M))
have this₁ : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)
Tactic: have := (norm_aux y).to_subtype
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r ε : ℝ
x y : M ⧸ S
this_1 : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)
this : Nonempty.{u_1 + 1} (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)
⊢ ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤
    HAdd.hAdd (α := ℝ) (⨅ (y : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)), dist 1 (↑y : M))
      (⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)), dist 1 (↑y_1 : M))
have refine : ∀ (i : (↑{m : M | (↑m : M ⧸ S) = x} : Type u_1)) (j : (↑{m : M | (↑m : M ⧸ S) = y} : Type u_1)),
  ⨅ (y_1 : (↑{m : M | (↑m : M ⧸ S) = x * y} : Type u_1)), dist 1 (↑y_1 : M) ≤ dist 1 (↑i : M) + dist 1 (↑j : M)
Tactic: refine le_ciInf_add_ciInf ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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)
⊢ ⨅ (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)
have 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) sorry) :
      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 sorry) :
        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 sorry) :
        M)
Tactic: refine ciInf_le_of_le ⟨0, forall_mem_range.2 fun _ ↦ dist_nonneg⟩ ⟨a * b, rfl⟩ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x_1 : M ⧸ S
m : M
r_1 ε : ℝ
x : M ⧸ S
r : ℝ
⊢ r ≤ infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x⁻¹} ↔ r ≤ infDist.{u_1} (α := M) 1 {m : M | (↑m : M ⧸ S) = x}
have 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
Tactic: simp only [le_infDist (norm_aux _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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‖ < ε}
have 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)
Tactic: refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
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)
have 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‖ < ε
Tactic: rw [ball_one_eq, mem_setOf_eq, norm_lt_iff, mem_image]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
⊢ Filter.HasBasis.{u_1, 1} (α := M ⧸ S) (𝓝 1) (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {x : M ⧸ S | ‖x‖ < ε}
have this : ∀ (ε : ℝ), 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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) (𝓝 1) (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {x : M ⧸ S | ‖x‖ < ε}
have rw : Filter.HasBasis.{u_1, 1} (α := M ⧸ S) (Filter.map mk (𝓝 1)) (fun (ε : ℝ) ↦ 0 < ε) fun (x : ℝ) ↦ mk '' ball 1 x
Tactic: rw [← mk_one, nhds_eq, ← funext this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
x : M
⊢ norm (E := M ⧸ S) (↑x : M ⧸ S) = infDist x (↑S : Set M)
have 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)
Tactic: rw [norm_eq_infDist, ← infDist_image (IsometryEquiv.divLeft x).isometry,
    ← IsometryEquiv.preimage_symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
⊢ norm (E := M ⧸ S) (↑m : M ⧸ S) = 0 ↔ m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set M)
have rw : (↑S : Set M).Nonempty
Tactic: rw [norm_mk, ← mem_closure_iff_infDist_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set M)
⊢ norm (E := M ⧸ S) (↑m : M ⧸ S) = 0 ↔ m ∈ S
have rw : m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set M) ↔ m ∈ S
Tactic: rw [norm_mk_eq_zero_iff_mem_closure, hS.closure_eq, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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
⊢ norm (E := M ⧸ S) (↑m : M ⧸ S) = 0 ↔ m ∈ S
have rw₁ : m ∈ (↑S : Set M) ↔ m ∈ S
Tactic: rw [norm_mk_eq_zero_iff_mem_closure, hS.closure_eq, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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
⊢ norm (E := M ⧸ S) (↑m : M ⧸ S) = 0 ↔ m ∈ S
have rw₂ : m ∈ S ↔ m ∈ S
Tactic: rw [norm_mk_eq_zero_iff_mem_closure, hS.closure_eq, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
⊢ ∃ s ∈ S, ‖m * s‖ < norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) + ε
have 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) + ε
Tactic: obtain ⟨n : M, hn, hn'⟩ := exists_norm_mk_lt (QuotientGroup.mk' S m) hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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)) (uniformity (M ⧸ S))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : (M ⧸ S) × M ⧸ S | dist p.1 p.2 < ε})
have 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 < ε})
Tactic: rw [uniformity_eq_comap_nhds_one_left, (nhds_one_hasBasis.comap _).eq_biInf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S = T
⊢ Isometry (Subgroup.quotientEquivOfEq h).toFun
have subst : Isometry (Subgroup.quotientEquivOfEq sorry).toFun
Tactic: subst h
Cleared hypotheses: T, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ Isometry.{u_1, u_1} (α := HasQuotient.Quotient M (B := Subgroup M) ⊥) (β := M) (⇑quotientBot : (a : M ⧸ ⊥) → M)
have rw : ∀ (x : HasQuotient.Quotient M (B := Subgroup M) ⊥), norm (E := M) ((quotientBot : (a : M ⧸ ⊥) → M) x : M) = ‖x‖
Tactic: rw [MonoidHomClass.isometry_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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
⊢ 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)
have mk : ‖x‖ = norm (E := HasQuotient.Quotient M (B := Subgroup M) ⊥) (↑x : M ⧸ ⊥)
Tactic: change ‖x‖ = ‖QuotientGroup.mk x‖
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
h : S ≤ T
⊢ Isometry (α := (M ⧸ S) ⧸ Subgroup.map (mk' S) T) (β := M ⧸ T)
    (⇑(quotientQuotientEquivQuotient S T h) : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T)
have 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‖
Tactic: rw [MonoidHomClass.isometry_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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‖
have 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‖
Tactic: refine fun x => eq_of_forall_le_iff fun r => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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 : ℝ
⊢ r ≤
      norm (E := M ⧸ T)
        ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x : M ⧸ T) ↔
    r ≤ ‖x‖
have 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‖
Tactic: simp only [le_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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
⊢ Eq (α := M ⧸ T) (↑z : M ⧸ T)
    ((quotientQuotientEquivQuotient S T h : (a : (M ⧸ S) ⧸ Subgroup.map (mk' S) T) → M ⧸ T) x)
have 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))
Tactic: subst_vars
Cleared hypotheses: x, h₁, y, h₂, h₃
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ norm (E := M ⧸ S) ((mk' S : (a : M) → M ⧸ S) m : M ⧸ S) = sInf ((fun (x : M) ↦ ‖m + x‖) '' (↑S : Set M))
have rw : Eq (α := ℝ) (⨅ (y : (↑(↑S : Set M) : Type u_1)), dist (-m) (↑y : M))
  (⨅ (a : (↑(↑S : Set M) : Type u_1)), ‖m + (↑a : 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]
-- 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
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : M ⧸ S
h : ‖f‖ = 0
⊢ norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) x : N) ≤ ‖f‖ * ‖x‖
have inl : ∀ (x : M),
  norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) (↑x : M ⧸ S) : N) ≤
    ‖f‖ * norm (E := M ⧸ S) (↑x : M ⧸ S)
Tactic: rcases mk_surjective x with ⟨x, rfl⟩
Cleared hypotheses: x
-- 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
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : M ⧸ S
h : 0 < ‖f‖
⊢ norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) x : N) ≤ ‖f‖ * ‖x‖
have inr : ¬∃ (m : M), (↑m : M ⧸ S) = x ∧ ‖m‖ < norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) x : N) / ‖f‖
Tactic: rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff]
-- 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
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : M ⧸ S
⊢ norm.{u_2} (E := N) ((lift S f.toAddMonoidHom hf : (a : M ⧸ S) → N) x : N) ≤ ‖f‖ * ‖x‖
have x₁ : ‖f‖ = 0 ∨ 0 < ‖f‖
Tactic: cases (norm_nonneg f).eq_or_lt' with
  | inl h =>
    rcases mk_surjective x with ⟨x, rfl⟩
    simpa [h] using le_opNorm f x
  | inr h =>
    rw [← not_lt, ← lt_div_iff₀' h, norm_lt_iff]
    rintro ⟨x, rfl, hx⟩
    exact ((lt_div_iff₀' h).1 hx).not_ge (le_opNorm f x)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
⊢ ‖S.normedMk‖ = 1
have refine : 1 ≤ ‖S.normedMk‖
Tactic: refine le_antisymm (norm_normedMk_le S) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
⊢ ∃ (x : M), 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)
have refine : ∀ (x : M) (hx : x ∈ (↑S.topologicalClosure : Set M)ᶜ), 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)
Tactic: refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
⊢ 1 ≤ ‖S.normedMk‖
have obtain : ∀ (x : M) (hx : 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)), 1 ≤ ‖S.normedMk‖
Tactic: obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖ := by
    refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
    exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) ≠ univ
x : M
hx : 0 < norm (E := M ⧸ S) (↑x : M ⧸ S)
⊢ 1 ≤ ‖S.normedMk‖
have refine : norm (E := M ⧸ S) (↑x : M ⧸ S) ≤ ‖S.normedMk‖ * norm (E := M ⧸ S) (↑x : M ⧸ S)
Tactic: refine (le_mul_iff_one_le_left hx).1 ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
⊢ ‖S.normedMk‖ = 0
have refine : ∀ (x : M), norm (E := M ⧸ S) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) ≤ 0 * ‖x‖
Tactic: refine le_antisymm (opNorm_le_bound _ le_rfl fun x => ?_) (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
x : M
⊢ x ∈ S.normedMk.ker.topologicalClosure
have rw : Membership.mem (γ := Set M) univ x
Tactic: rw [S.ker_normedMk, ← SetLike.mem_coe, h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
x : M
⊢ norm (E := M ⧸ S) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) ≤ 0 * ‖x‖
have hker : x ∈ S.normedMk.ker.topologicalClosure
Tactic: have hker : x ∈ S.normedMk.ker.topologicalClosure := by
    rw [S.ker_normedMk, ← SetLike.mem_coe, h]
    trivial
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (hypothesis)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
S : AddSubgroup M
h : (↑S.topologicalClosure : Set M) = univ
x : M
hker : x ∈ S.normedMk.ker.topologicalClosure
⊢ norm (E := M ⧸ S) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) ≤ 0 * ‖x‖
have hker₁ : x ∈ S.topologicalClosure
Tactic: rw [ker_normedMk] at hker
Cleared hypotheses: hker
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
⊢ g = lift S f hf
have H : ∀ (x : M ⧸ S), Eq.{u_3 + 1} (α := N) ((g : (a : M ⧸ S) → N) x : N) ((lift S f hf : (a : M ⧸ S) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
x : M ⧸ S
⊢ Eq.{u_3 + 1} (α := N) ((g : (a : M ⧸ S) → N) x : N) ((lift S f hf : (a : M ⧸ S) → N) x : N)
have H : ∀ (x : M),
  Eq.{u_3 + 1} (α := N) ((g : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
    ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
Tactic: rcases AddSubgroup.surjective_normedMk _ x with ⟨x, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ Eq.{u_3 + 1} (α := N) ((g : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
    ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
have H : Eq.{u_3 + 1} (α := N) ((g.comp S.normedMk : (a : M) → N) x : N)
  ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
Tactic: change g.comp S.normedMk x = _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Quotient (goal)
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)
g : NormedAddGroupHom.{u_1, u_3} (M ⧸ S) N
h : g.comp S.normedMk = f
x : M
⊢ Eq.{u_3 + 1} (α := N) ((g.comp S.normedMk : (a : M) → N) x : N)
    ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
have H : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N)
  ((lift S f hf : (a : M ⧸ S) → N) ((S.normedMk : (a : M) → M ⧸ S) x : M ⧸ S) : N)
Tactic: simp only [h]