awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
𝕜_2 : Type u_6
E_2 : Type u_7
inst : NormedField 𝕜_2
inst_1 : AddCommGroup E_2
inst_2 : Module 𝕜_2 E_2
inst_3 : Norm E_2
𝕜 : Type u_8
E : Type u_9
inst_4 : NormedField 𝕜
inst_5 : SeminormedAddCommGroup E
inst_6 : Module 𝕜 E
core : Core 𝕜 E
r : 𝕜
x : E
rw rw₁ : ‖r‖ * ‖x‖ ≤ ‖r‖ * ‖x‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
rw [core.norm_smul r x]

Premises used: SeminormedSpace.Core.norm_smul, NormedSpace.Core.toCore
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
obtain :
  ∀ (δ : ℝ) (hδ : δ > 0) (hUε : ball 0 δ ⊆ s),
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (⇑f : (a : G) → H)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)

Tactic:
obtain ⟨δ, hδ, hUε⟩ := Metric.mem_nhds_iff.mp hs

Premises used: Metric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
obtain :
  ∀ (C : ℝ) (hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)),
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (⇑f : (a : G) → H)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)

Tactic:
obtain ⟨C, hC⟩ := (isBounded_iff_subset_ball 0).1 (hbounded.subset <| image_mono hUε)

Premises used: Metric.isBounded_iff_subset_ball, Set.image_mono, Bornology.IsBounded.subset, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)

Tactic:
continuous_of_continuousAt_zero _ (continuousAt_iff.2 fun ε (hε : _ < _) => ?_)

Premises used: Iff.mpr, continuous_of_continuousAt_zero, Metric.continuousAt_iff
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)
refine :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∃ δ > 0, ∀ ⦃x : G⦄, dist x 0 < δ → dist.{u_7} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) 0 : H) < ε
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : G) → H)

Tactic:
refine continuous_of_continuousAt_zero _ (continuousAt_iff.2 fun ε (hε : _ < _) => ?_)

Premises used: Iff.mpr, continuous_of_continuousAt_zero, Metric.continuousAt_iff
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)
ε : ℝ
hε : 0 < ε
simp : ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, dist x 0 < δ → dist.{u_7} (α := H) ((f : (a : G) → H) x : H) ((f : (a : G) → H) 0 : H) < ε

Tactic:
simp only [dist_zero_right, map_zero]

Premises used: map_zero, dist_zero_right
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C : ℝ
hC : Subset.{u_7} (α := Set H) (image.{u_6, u_7} (α := G) (⇑f : (a : G) → H) (ball 0 δ)) (ball 0 C)
ε : ℝ
hε : 0 < ε
⊢ ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C

Tactic:
simp only [subset_def, mem_image, mem_ball, dist_zero_right, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at hC

Premises used: Set.subset_def, and_imp, Set.mem_image, forall_exists_index, Metric.mem_ball, dist_zero_right, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
⊢ norm.{u_6} (E := G) 0 < δ

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
⊢ 0 < C

Tactic:
have hC₀ : 0 < C := (norm_nonneg _).trans_lt <| hC 0 (by simpa)
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
obtain :
  ∀ (n : ℕ) (hn : C / ε < (↑n : ℝ)), ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt (C / ε)

Premises used: HDiv.hDiv, exists_nat_gt
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have hnpos : 0 < (n : ℝ) := (div_pos hC₀ hε).trans hn
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
hn : C / ε < (↑0 : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑0 : ℝ)
⊢ False

Tactic:
simp at hnpos
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ n ≠ 0

Tactic:
have hn₀ : n ≠ 0 := by rintro rfl; simp at hnpos
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε

Tactic:
⟨δ / n, div_pos hδ hnpos, fun {x} hxδ => ?_⟩

Premises used: HDiv.hDiv, Nat.cast, And.intro, Exists.intro, div_pos
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
refine : ∀ {x : G} (hxδ : ‖x‖ < δ / (↑n : ℝ)), norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε
⊢ ∃ δ > 0, ∀ ⦃x : G⦄, ‖x‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε

Tactic:
refine ⟨δ / n, div_pos hδ hnpos, fun {x} hxδ => ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) x : H) =
    ‖HSMul.hSMul (α := ℝ) (β := H) (↑n : ℝ)⁻¹ ((f : (a : G) → H) (n • x) : H)‖

Tactic:
simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]

Premises used: Real, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ ‖HSMul.hSMul (α := ℝ) (β := H) (↑n : ℝ)⁻¹ ((f : (a : G) → H) (n • x) : H)‖ ≤
    norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H)

Tactic:
norm_smul_le ..

Premises used: norm_smul_le
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
ha : 0 < norm (E := ℝ) (↑n : ℝ)⁻¹
hbc : norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < C
⊢ norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < norm (E := ℝ) (↑n : ℝ)⁻¹ * C

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ 0 < norm (E := ℝ) (↑n : ℝ)⁻¹

Tactic:
simpa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < C

Tactic:
hC _ <| norm_nsmul_le.trans_lt ?_

Premises used: norm_nsmul_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
hbc : (↑n : ℝ) * ‖x‖ < δ
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < C

Tactic:
refine hC _ <| norm_nsmul_le.trans_lt ?_

Premises used: norm_nsmul_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ (↑n : ℝ) * ‖x‖ < δ

Tactic:
simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ

Premises used: lt_div_iff₀, Real.norm_natCast, norm_mul, mul_comm
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ norm (E := ℝ) (↑n : ℝ)⁻¹ * C = (↑n : ℝ)⁻¹ * C

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
ha : 0 < C
hbc : 0 < C / ε
⊢ (↑n : ℝ)⁻¹ * C < (C / ε)⁻¹ * C

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
⊢ (C / ε)⁻¹ * C = ε

Tactic:
simp [hC₀.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
G : Type u_6
H : Type u_7
inst : SeminormedAddCommGroup G
inst_1 : SeminormedAddCommGroup H
inst_2 : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : Membership.mem (γ := Filter G) (𝓝 0) s
hbounded : Bornology.IsBounded.{u_7} (α := H) ((⇑f : (a : G) → H) '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → norm.{u_7} (E := H) ((f : (a : G) → H) a : H) < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < (↑n : ℝ)
hnpos : LT.lt (α := ℝ) 0 (↑n : ℝ)
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / (↑n : ℝ)
_ :
  norm.{u_7} (E := H) ((f : (a : G) → H) x : H) =
    ‖HSMul.hSMul (α := ℝ) (β := H) (↑n : ℝ)⁻¹ ((f : (a : G) → H) (n • x) : H)‖
_₁ : norm (E := ℝ) (↑n : ℝ)⁻¹ * norm.{u_7} (E := H) ((f : (a : G) → H) (n • x) : H) < norm (E := ℝ) (↑n : ℝ)⁻¹ * C
_₂ : norm (E := ℝ) (↑n : ℝ)⁻¹ * C = (↑n : ℝ)⁻¹ * C
_₃ : (↑n : ℝ)⁻¹ * C < (C / ε)⁻¹ * C
_₄ : (C / ε)⁻¹ * C = ε
⊢ norm.{u_7} (E := H) ((f : (a : G) → H) x : H) < ε

Tactic:
calc
    ‖f x‖
    _ = ‖(n : ℝ)⁻¹ • f (n • x)‖ := by simp [← Nat.cast_smul_eq_nsmul ℝ, hn₀]
    _ ≤ ‖(n : ℝ)⁻¹‖ * ‖f (n • x)‖ := norm_smul_le ..
    _ < ‖(n : ℝ)⁻¹‖ * C := by
      gcongr
      · simpa [pos_iff_ne_zero]
      · refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ
    _ = (n : ℝ)⁻¹ * C := by simp
    _ < (C / ε : ℝ)⁻¹ * C := by gcongr
    _ = ε := by simp [hC₀.ne']

Premises used: norm_smul_le, HDiv.hDiv, Nat.cast, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
inst_8 : CompleteSpace (F × G)
f : E →L[𝕜] F
g : E →L[𝕜] G
hf : (↑f : E →ₗ[𝕜] F).range = ⊤
hg : (↑g : E →ₗ[𝕜] G).range = ⊤
hfg : IsCompl (↑f : E →ₗ[𝕜] F).ker (↑g : E →ₗ[𝕜] G).ker
⊢ (↑(↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) : E ≃ₗ[𝕜] F × G) : E →ₗ[𝕜] F × G) = (↑(f.prod g) : E →ₗ[𝕜] F × G)

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
inst_8 : CompleteSpace (F × G)
f : E →L[𝕜] F
g : E →L[𝕜] G
hf : (↑f : E →ₗ[𝕜] F).range = ⊤
hg : (↑g : E →ₗ[𝕜] G).range = ⊤
hfg : IsCompl (↑f : E →ₗ[𝕜] F).ker (↑g : E →ₗ[𝕜] G).ker
⊢ (↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) : E ≃ₗ[𝕜] F × G) =
    (↑f : E →ₗ[𝕜] F).equivProdOfSurjectiveOfIsCompl (↑g : E →ₗ[𝕜] G) hf hg hfg

Tactic:
rfl

Premises used: LinearMap.equivProdOfSurjectiveOfIsCompl, LinearEquiv.trans, rfl, LinearEquiv.ofBijective
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
inst_8 : CompleteSpace (F × G)
f : E →L[𝕜] F
g : E →L[𝕜] G
hf : (↑f : E →ₗ[𝕜] F).range = ⊤
hg : (↑g : E →ₗ[𝕜] G).range = ⊤
hfg : IsCompl (↑f : E →ₗ[𝕜] F).ker (↑g : E →ₗ[𝕜] G).ker
x : E
⊢ Eq (α := F × G) ((f.equivProdOfSurjectiveOfIsCompl g hf hg hfg : (a : E) → F × G) x : F × G)
    (((f : (a : E) → F) x, (g : (a : E) → G) x) : F × G)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
⊢ CompleteSpace.{u_2} (↑(↑p : Set E) : Type u_2)

Tactic:
haveI := hp.completeSpace_coe
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
this : CompleteSpace.{u_2} (↑(↑p : Set E) : Type u_2)
⊢ CompleteSpace.{u_2} (↑(↑q : Set E) : Type u_2)

Tactic:
haveI := hq.completeSpace_coe
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
this_1 : CompleteSpace.{u_2} (↑(↑p : Set E) : Type u_2)
this : CompleteSpace.{u_2} (↑(↑q : Set E) : Type u_2)
refine : Continuous (X := ↥p × ↥q) (Y := E) (⇑(prodEquivOfIsCompl p q h) : (a : ↥p × ↥q) → E)
⊢ (↥p × ↥q) ≃L[𝕜] E

Tactic:
refine (p.prodEquivOfIsCompl q h).toContinuousLinearEquivOfContinuous ?_

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.toContinuousLinearEquivOfContinuous
-- Module: Mathlib.Analysis.Normed.Module.Complemented
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed (↑p : Set E)
hq : IsClosed (↑q : Set E)
this_1 : CompleteSpace.{u_2} (↑(↑p : Set E) : Type u_2)
this : CompleteSpace.{u_2} (↑(↑q : Set E) : Type u_2)
⊢ Continuous (X := ↥p × ↥q) (Y := E) (⇑(prodEquivOfIsCompl p q h) : (a : ↥p × ↥q) → E)

Tactic:
(p.subtypeL.coprod q.subtypeL).continuous

Premises used: Submodule.subtypeL, Set.Mem, setOf, ContinuousLinearMap.continuous, ContinuousLinearMap.coprod