awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : SeparationQuotient M
obtain :
  ∀ (x : M),
    norm.{u_2} (E := N) ((liftNormedAddGroupHom f hf : (a : SeparationQuotient M) → N) (mk x) : N) ≤
      ‖f‖ * norm (E := SeparationQuotient M) (mk x)
⊢ norm.{u_2} (E := N) ((liftNormedAddGroupHom f hf : (a : SeparationQuotient M) → N) x : N) ≤ ‖f‖ * ‖x‖

Tactic:
obtain ⟨x, rfl⟩ := surjective_mk x

Premises used: SeparationQuotient.surjective_mk, rfl
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : M
⊢ norm.{u_2} (E := N) ((liftNormedAddGroupHom f hf : (a : SeparationQuotient M) → N) (mk x) : N) ≤
    ‖f‖ * norm (E := SeparationQuotient M) (mk x)

Tactic:
le_opNorm f x

Premises used: Quotient.liftOn', NormedAddGroupHom.le_opNorm, SeparationQuotient.lift
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x : M
⊢ norm.{u_2} (E := N) ((liftNormedAddGroupHom f hf : (a : SeparationQuotient M) → N) (mk x) : N) ≤
    ‖f‖ * norm (E := SeparationQuotient M) (mk x)

Tactic:
exact le_opNorm f x

Premises used: NormedAddGroupHom.le_opNorm
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N_1 : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N_1
N : Type u_3
inst_2 : SeminormedAddCommGroup N
g : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N
x : M
hx : ‖x‖ = 0
⊢ Eq (α := SeparationQuotient M) (mk x) 0

Tactic:
rw [← norm_mk, norm_eq_zero] at hx

Premises used: norm_eq_zero, SeparationQuotient.norm_mk
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N_1 : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N_1
N : Type u_3
inst_2 : SeminormedAddCommGroup N
g : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N
x : M
hx : Eq (α := SeparationQuotient M) (mk x) 0
⊢ Eq.{u_3 + 1} (α := N) ((g.comp normedMk : (a : M) → N) x : N) (0 : N)

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N_1 : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N_1
N : Type u_3
inst_2 : SeminormedAddCommGroup N
x : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N
H :
  ∀ (x_1 : SeparationQuotient M),
    Eq.{u_3 + 1} (α := N)
      (((fun
                  (f :
                    { f : NormedAddGroupHom M N //
                      ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }) ↦
                liftNormedAddGroupHom (↑f : NormedAddGroupHom M N) ⋯)
              ((fun (g : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N) ↦
                  (Subtype.mk (p := fun (f : NormedAddGroupHom M N) ↦
                      ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)) (g.comp normedMk)
                      ⋯ :
                    { f : NormedAddGroupHom M N //
                      ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }))
                x) :
            (a : SeparationQuotient M) → N)
          x_1 :
        N)
      ((x : (a : SeparationQuotient M) → N) x_1 : N)
⊢ (fun
          (f :
            { f : NormedAddGroupHom M N //
              ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }) ↦
        liftNormedAddGroupHom (↑f : NormedAddGroupHom M N) ⋯)
      ((fun (g : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N) ↦
          (Subtype.mk (p := fun (f : NormedAddGroupHom M N) ↦
              ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)) (g.comp normedMk) ⋯ :
            { f : NormedAddGroupHom M N //
              ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }))
        x) =
    x

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N_1 : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N_1
N : Type u_3
inst_2 : SeminormedAddCommGroup N
x_1 : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N
x : SeparationQuotient M
H :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := N)
      (((fun
                  (f :
                    { f : NormedAddGroupHom M N //
                      ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }) ↦
                liftNormedAddGroupHom (↑f : NormedAddGroupHom M N) ⋯)
              ((fun (g : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N) ↦
                  (Subtype.mk (p := fun (f : NormedAddGroupHom M N) ↦
                      ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)) (g.comp normedMk)
                      ⋯ :
                    { f : NormedAddGroupHom M N //
                      ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }))
                x_1) :
            (a : SeparationQuotient M) → N)
          (mk x) :
        N)
      ((x_1 : (a : SeparationQuotient M) → N) (mk x) : N)
⊢ Eq.{u_3 + 1} (α := N)
    (((fun
                (f :
                  { f : NormedAddGroupHom M N //
                    ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }) ↦
              liftNormedAddGroupHom (↑f : NormedAddGroupHom M N) ⋯)
            ((fun (g : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N) ↦
                (Subtype.mk (p := fun (f : NormedAddGroupHom M N) ↦
                    ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)) (g.comp normedMk) ⋯ :
                  { f : NormedAddGroupHom M N //
                    ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }))
              x_1) :
          (a : SeparationQuotient M) → N)
        x :
      N)
    ((x_1 : (a : SeparationQuotient M) → N) x : N)

Tactic:
obtain ⟨x, rfl⟩ := surjective_mk x

Premises used: SeparationQuotient.surjective_mk, rfl
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N_1 : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N_1
N : Type u_3
inst_2 : SeminormedAddCommGroup N
x_1 : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N
x : M
⊢ Eq.{u_3 + 1} (α := N)
    (((fun
                (f :
                  { f : NormedAddGroupHom M N //
                    ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }) ↦
              liftNormedAddGroupHom (↑f : NormedAddGroupHom M N) ⋯)
            ((fun (g : NormedAddGroupHom.{u_1, u_3} (SeparationQuotient M) N) ↦
                (Subtype.mk (p := fun (f : NormedAddGroupHom M N) ↦
                    ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)) (g.comp normedMk) ⋯ :
                  { f : NormedAddGroupHom M N //
                    ∀ (x : M), ‖x‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N) }))
              x_1) :
          (a : SeparationQuotient M) → N)
        (mk x) :
      N)
    ((x_1 : (a : SeparationQuotient M) → N) (mk x) : N)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (s : M), ‖s‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
⊢ ‖liftNormedAddGroupHom f hf‖ ≤ ‖f‖

Tactic:
NormedAddGroupHom.opNorm_le_bound _ (norm_nonneg f) (norm_liftNormedAddGroupHom_apply_le f hf)

Premises used: SeparationQuotient.norm_liftNormedAddGroupHom_apply_le, NormedAddGroupHom.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (s : M), ‖s‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
c : ℝ≥0
fb : ‖f‖ ≤ (↑c : ℝ)
⊢ ‖liftNormedAddGroupHom f hf‖ ≤ (↑c : ℝ)

Tactic:
(norm_liftNormedAddGroupHom_le f hf).trans fb

Premises used: SeparationQuotient.norm_liftNormedAddGroupHom_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (s : M), ‖s‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
fb : f.NormNoninc
x : SeparationQuotient M
⊢ ‖f‖ ≤ 1

Tactic:
have fb' : ‖f‖ ≤ 1 := NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.mp fb
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (s : M), ‖s‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
fb : f.NormNoninc
x : SeparationQuotient M
fb' : ‖f‖ ≤ 1
⊢ norm.{u_3} (E := N) ((liftNormedAddGroupHom f hf : (a : SeparationQuotient M) → N) x : N) ≤ ‖x‖

Tactic:
le_trans (norm_liftNormedAddGroupHom_apply_le f hf x)
    (mul_le_of_le_one_left (norm_nonneg x) fb')

Premises used: SeparationQuotient.norm_liftNormedAddGroupHom_apply_le, mul_le_of_le_one_left, norm_nonneg, le_trans
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
N : Type u_3
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (s : M), ‖s‖ = 0 → Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) s : N) (0 : N)
fb : f.NormNoninc
x : SeparationQuotient M
fb' : ‖f‖ ≤ 1
⊢ norm.{u_3} (E := N) ((liftNormedAddGroupHom f hf : (a : SeparationQuotient M) → N) x : N) ≤ ‖x‖

Tactic:
exact le_trans (norm_liftNormedAddGroupHom_apply_le f hf x)
    (mul_le_of_le_one_left (norm_nonneg x) fb')

Premises used: SeparationQuotient.norm_liftNormedAddGroupHom_apply_le, mul_le_of_le_one_left, norm_nonneg, le_trans
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
inst_1 : NontrivialTopology M
h_above :
  ∀ (x : M),
    norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤ 1 * ‖x‖
h_below :
  ∀ N ≥ 0,
    (∀ (x : M),
        norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤
          N * ‖x‖) →
      1 ≤ N
⊢ norm.{u_1} (E := NormedAddGroupHom M (SeparationQuotient M)) normedMk = 1

Tactic:
apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one

Premises used: NormedAddGroupHom.opNorm_eq_of_bounds, zero_le_one
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
inst_1 : NontrivialTopology M
⊢ ∀ (x : M),
    norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤ 1 * ‖x‖

Tactic:
simpa only [normedMk_apply, one_mul] using fun _ ↦ le_rfl

Premises used: le_rfl, SeparationQuotient.normedMk_apply, one_mul
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
inst_1 : NontrivialTopology M
N : ℝ
h_below :
  N ≥ 0 →
    (∀ (x : M),
        norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤
          N * ‖x‖) →
      1 ≤ N
⊢ N ≥ 0 →
    (∀ (x : M),
        norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤
          N * ‖x‖) →
      1 ≤ N

Tactic:
_
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
inst_1 : NontrivialTopology M
N : ℝ
h : N ≥ 0
hle :
  ∀ (x : M),
    norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤ N * ‖x‖
h_below : ∀ (x : M), ‖x‖ ≠ 0 → 1 ≤ N
⊢ 1 ≤ N

Tactic:
obtain ⟨x, _⟩ := exists_norm_ne_zero M

Premises used: exists_norm_ne_zero
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
inst_1 : NontrivialTopology M
N : ℝ
h : N ≥ 0
hle :
  ∀ (x : M),
    norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤ N * ‖x‖
x : M
h_1 : ‖x‖ ≠ 0
⊢ 0 < norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M)

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
inst_1 : NontrivialTopology M
N : ℝ
h : N ≥ 0
hle :
  ∀ (x : M),
    norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤ N * ‖x‖
x : M
h_1 : ‖x‖ ≠ 0
⊢ 1 ≤ N

Tactic:
exact one_le_of_le_mul_right₀ (by positivity) (hle x)

Premises used: one_le_of_le_mul_right₀
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
mp : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0 → ∀ (x : M), ‖x‖ = 0
mpr : (∀ (x : M), ‖x‖ = 0) → Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
⊢ Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0 ↔ ∀ (x : M), ‖x‖ = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
x : M
mp : Eq (α := SeparationQuotient M) (mk x) 0
⊢ ‖x‖ = 0

Tactic:
rw [SeparationQuotient.mk_eq_zero_iff.mp]

Premises used: SeparationQuotient.mk_eq_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
x : M
rw :
  Eq (α := SeparationQuotient M) ((0 : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
    (0 : SeparationQuotient M)
⊢ Eq (α := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
    (0 : SeparationQuotient M)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
x : M
⊢ Eq (α := SeparationQuotient M) ((0 : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
    (0 : SeparationQuotient M)

Tactic:
simp only [zero_apply]

Premises used: NormedAddGroupHom.zero_apply
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
x : M
⊢ Eq (α := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
    (0 : SeparationQuotient M)

Tactic:
have : normedMk x = 0 := by
      rw [h]
      simp only [zero_apply]
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
x : M
this :
  Eq (α := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
    (0 : SeparationQuotient M)
mp : Eq (α := SeparationQuotient M) (mk x) ((normedMk : (a : M) → SeparationQuotient M) x)
⊢ Eq (α := SeparationQuotient M) (mk x) 0

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
x : M
this :
  Eq (α := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
    (0 : SeparationQuotient M)
⊢ Eq (α := SeparationQuotient M) (mk x) ((normedMk : (a : M) → SeparationQuotient M) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
mpr :
  ∀ (x : M),
    Eq (α := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
      ((0 : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
⊢ Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
x : M
⊢ Eq (α := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
    ((0 : (a : M) → SeparationQuotient M) x : SeparationQuotient M)

Tactic:
simpa [← norm_eq_zero] using h x

Premises used: norm_eq_zero
-- Module: Mathlib.Analysis.Normed.Group.Subgroup
Goal:
E : Type u_1
inst : SeminormedGroup E
s : Subgroup E
x : ↥s
⊢ ‖x‖ = ‖(↑x : E)‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Subgroup
Goal:
E : Type u_1
inst : SeminormedGroup E
s : Subgroup E
x : ↥s
⊢ ‖(↑x : E)‖ = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Subgroup
Goal:
E : Type u_1
inst : SeminormedGroup E
S : Type u_2
inst_1 : SetLike S E
inst_2 : SubgroupClass S E
s : S
x : ↥s
⊢ ‖x‖ = ‖(↑x : E)‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
s : Submodule 𝕜 E
x : ↥s
⊢ ‖x‖ = ‖(↑x : E)‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
s : Submodule 𝕜 E
x : ↥s
⊢ ‖(↑x : E)‖ = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Submodule
Goal:
R : Type u_3
R' : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
f : M →ₛₗ[σ₁₂] M'
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M'
hf : Continuous.{u_5, u_6} (X := M) (Y := M') (⇑f : (a : M) → M')
p : Submodule R M
rw : Continuous.{u_5, u_6} (X := ↥p) (Y := M') ((↑p : Set M).restrict (π := fun (a : M) ↦ M') (⇑f : (a : M) → M'))
⊢ Continuous.{u_5, u_6} (X := ↥p) (Y := M') (⇑(f.domRestrict p) : (a : ↥p) → M')

Tactic:
rw [coe_domRestrict]

Premises used: LinearMap.coe_domRestrict
-- Module: Mathlib.Analysis.Normed.Group.Submodule
Goal:
R : Type u_3
R' : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
f : M →ₛₗ[σ₁₂] M'
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M'
hf : Continuous.{u_5, u_6} (X := M) (Y := M') (⇑f : (a : M) → M')
p : Submodule R M
⊢ Continuous.{u_5, u_6} (X := ↥p) (Y := M') ((↑p : Set M).restrict (π := fun (a : M) ↦ M') (⇑f : (a : M) → M'))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
inl : IsEmpty β → Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
inr : Nonempty β → Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
rcases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : IsEmpty β
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
simpa only [tsum_empty] using tendsto_const_nhds

Premises used: tendsto_const_nhds, tsum_empty
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
inr :
  ∀ (hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) ⊥ (𝓝 (g k)))
    (h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k),
    Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) ⊥ (𝓝 (∑' (k : β), g k))
inr₁ : 𝓕.NeBot → Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
rcases 𝓕.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
h : Nonempty β
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) ⊥ (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) ⊥ (𝓝 (∑' (k : β), g k))

Tactic:
simp only [tendsto_bot]

Premises used: Filter.tendsto_bot
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
⊢ ∀ (k : β), ‖g k‖ ≤ bound k

Tactic:
have h_g_le (k : β) : ‖g k‖ ≤ bound k :=
    le_of_tendsto (tendsto_norm.comp (hab k)) <| h_bound.mono (fun n h => h k)
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
⊢ Summable (α := ℝ) fun (x : β) ↦ ‖g x‖

Tactic:
have h_sumg : Summable (‖g ·‖) :=
    h_sum.of_norm_bounded (fun k ↦ (norm_norm (g k)).symm ▸ h_g_le k)
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h : ∀ (n : α) (h : ∀ (k : β), ‖f n k‖ ≤ bound k), Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
⊢ ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖

Tactic:
filter_upwards [h_bound] with n h
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
n : α
h : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ∀ (i : β), ‖‖f n i‖‖ ≤ bound i

Tactic:
simpa only [norm_norm] using h

Premises used: norm_norm