awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q f g : NonarchAddGroupNorm E
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ) ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun) f)
    ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : E → ℝ) (map_zero' : toFun 0 = 0)
  (add_le_max' :
    ∀ (r s : E),
      { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (r + s) ≤
        max ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
          ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun s))
  (neg' :
    ∀ (r : E),
      { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (-r) =
        { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
  (eq_zero_of_map_eq_zero' :
    ∀ (x : E),
      { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' :
                NonarchAddGroupSeminorm E }.toFun
            x =
          0 →
        x = 0)
  (h :
    Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
      ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
        { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
          eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
      ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun) g)),
  { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : NonarchAddGroupNorm E } =
    g
Tactic: obtain ⟨⟨⟨_, _⟩, _, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : AddGroup E
p q g : NonarchAddGroupNorm E
toFun : E → ℝ
map_zero' : toFun 0 = 0
add_le_max' :
  ∀ (r s : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (r + s) ≤
      max ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
        ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun s)
neg' :
  ∀ (r : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (-r) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r
eq_zero_of_map_eq_zero' :
  ∀ (x : E),
    { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' :
              NonarchAddGroupSeminorm E }.toFun
          x =
        0 →
      x = 0
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun) g)
⊢ { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : NonarchAddGroupNorm E } =
    g
have mk : ∀ (toNonarchAddGroupSeminorm : NonarchAddGroupSeminorm E)
  (eq_zero_of_map_eq_zero'_1 : ∀ (x : E), toNonarchAddGroupSeminorm.toFun x = 0 → x = 0)
  (h :
    Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
      ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
        { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
          eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
      ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
        { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm,
          eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })),
  { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : NonarchAddGroupNorm E } =
    { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x y : M
h : Inseparable x y
⊢ HSub.hSub (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) = 0
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x - y) : N) (0 : N)
Tactic: rw [← map_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x y : M
h : Inseparable x y
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x - y) : N) (0 : N)
have h₁ : ‖x - y‖ = 0
Tactic: rw [Metric.inseparable_iff, dist_eq_norm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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)
⊢ ∃ (C : ℝ),
    ∀ (v : SeparationQuotient M),
      norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) v : N) ≤
        C * ‖v‖
have refine : ∀ (v : SeparationQuotient M),
  norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) sorry : (a : SeparationQuotient M) → N) v : N) ≤ ‖f‖ * ‖v‖
Tactic: refine ⟨‖f‖, fun v ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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)
v : SeparationQuotient M
⊢ norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) v : N) ≤ ‖f‖ * ‖v‖
have obtain : ∀ (v : M),
  norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) sorry : (a : SeparationQuotient M) → N) (mk v) : N) ≤
    ‖f‖ * norm (E := SeparationQuotient M) (mk v)
Tactic: obtain ⟨v, rfl⟩ := surjective_mk v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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
⊢ norm.{u_2} (E := N) ((liftNormedAddGroupHom f hf : (a : SeparationQuotient M) → N) x : N) ≤ ‖f‖ * ‖x‖
have 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)
Tactic: obtain ⟨x, rfl⟩ := surjective_mk x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (hypothesis)
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.{u_3 + 1} (α := N) ((g.comp normedMk : (a : M) → N) x : N) (0 : N)
have hx₁ : Eq (α := SeparationQuotient M) (mk x) 0
Tactic: rw [← norm_mk, norm_eq_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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
⊢ (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
have 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) sorry)
            ((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) sorry :
                  { 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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
⊢ 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)
have 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) sorry)
            ((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) sorry :
                  { 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: obtain ⟨x, rfl⟩ := surjective_mk x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (hypothesis)
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
⊢ norm.{u_3} (E := N) ((liftNormedAddGroupHom f hf : (a : SeparationQuotient M) → N) x : N) ≤ ‖x‖
have fb' : ‖f‖ ≤ 1
Tactic: have fb' : ‖f‖ ≤ 1 := NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.mp fb
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
inst_1 : NontrivialTopology M
⊢ norm.{u_1} (E := NormedAddGroupHom M (SeparationQuotient M)) normedMk = 1
have h_above : ∀ (x : M),
  norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤ 1 * ‖x‖
Tactic: apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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‖
⊢ norm.{u_1} (E := NormedAddGroupHom M (SeparationQuotient M)) normedMk = 1
have h_below : ∀ N ≥ 0,
  (∀ (x : M),
      norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M) ≤
        N * ‖x‖) →
    1 ≤ N
Tactic: apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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‖
⊢ 1 ≤ N
have h_below : ∀ (x : M), ‖x‖ ≠ 0 → 1 ≤ N
Tactic: obtain ⟨x, _⟩ := exists_norm_ne_zero M
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
⊢ Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0 ↔ ∀ (x : M), ‖x‖ = 0
have mp : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0 → ∀ (x : M), ‖x‖ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
mp : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0 → ∀ (x : M), ‖x‖ = 0
⊢ Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0 ↔ ∀ (x : M), ‖x‖ = 0
have mpr : (∀ (x : M), ‖x‖ = 0) → Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
x : M
⊢ ‖x‖ = 0
have mp : Eq (α := SeparationQuotient M) (mk x) 0
Tactic: rw [SeparationQuotient.mk_eq_zero_iff.mp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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)
have rw : Eq (α := SeparationQuotient M) ((0 : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
  (0 : SeparationQuotient M)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (hypothesis)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
x : M
⊢ Eq (α := SeparationQuotient M) (mk x) 0
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
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) 0
have mp : Eq (α := SeparationQuotient M) (mk x) ((normedMk : (a : M) → SeparationQuotient M) x)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.SeparationQuotient (goal)
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
h : ∀ (x : M), ‖x‖ = 0
⊢ Eq.{u_1 + 1} (α := NormedAddGroupHom M (SeparationQuotient M)) normedMk 0
have mpr : ∀ (x : M),
  Eq (α := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
    ((0 : (a : M) → SeparationQuotient M) x : SeparationQuotient M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Submodule (goal)
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') (⇑(f.domRestrict p) : (a : ↥p) → M')
have rw : Continuous.{u_5, u_6} (X := ↥p) (Y := M') ((↑p : Set M).restrict (π := fun (a : M) ↦ M') (⇑f : (a : M) → M'))
Tactic: rw [coe_domRestrict]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
have inl : IsEmpty β → Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
Tactic: rcases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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))
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
have inr : Nonempty β → Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
Tactic: rcases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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 β
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
have 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))
Tactic: rcases 𝓕.eq_or_neBot with rfl | _
Cleared hypotheses: 𝓕, hab, h_bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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))
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
have inr₁ : 𝓕.NeBot → Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
Tactic: rcases 𝓕.eq_or_neBot with rfl | _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (hypothesis)
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
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
have h_g_le : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (hypothesis)
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
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
have h_sumg : 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
⊢ ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
have h : ∀ (n : α) (h : ∀ (k : β), ‖f n k‖ ≤ bound k), Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
Tactic: filter_upwards [h_bound] with n h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (hypothesis)
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
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
have h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
Tactic: have h_suma : ∀ᶠ n in 𝓕, Summable (‖f n ·‖) := by
    filter_upwards [h_bound] with n h
    exact h_sum.of_norm_bounded <| by simpa only [norm_norm] using h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
have inr : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
Tactic: rw [Metric.tendsto_nhds]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
have inr : ∀ (S : ℝ) (hS : HasSum bound S), ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
Tactic: let ⟨S, hS⟩ := h_sum