awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
σ₂₁ : 𝕜₂ →+* 𝕜
inst_17 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
m : 𝕜
c : StrongDual 𝕜 E
⊢ smulRightₗ (m • c) =
    HSMul.hSMul (α := 𝕜) (β := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜) (smulRightₗ c)
have h : ∀ (x : Fₗ) (x_1 : E),
  Eq.{u_7 + 1} (α := Fₗ) ((((smulRightₗ (m • c) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) : (a : E) → Fₗ) x_1 : Fₗ)
    ((((HSMul.hSMul (α := 𝕜) (β := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜) (smulRightₗ c) :
                (a : Fₗ) → E →L[𝕜] Fₗ)
              x :
            E →L[𝕜] Fₗ) :
          (a : E) → Fₗ)
        x_1 :
      Fₗ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
σ₂₁ : 𝕜₂ →+* 𝕜
inst_17 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
m : 𝕜
c : StrongDual 𝕜 E
x : Fₗ
x_1 : E
⊢ Eq.{u_7 + 1} (α := Fₗ) ((((smulRightₗ (m • c) : (a : Fₗ) → E →L[𝕜] Fₗ) x : E →L[𝕜] Fₗ) : (a : E) → Fₗ) x_1 : Fₗ)
    ((((HSMul.hSMul (α := 𝕜) (β := Fₗ →ₗ[𝕜] E →L[𝕜] Fₗ) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜) (smulRightₗ c) :
                (a : Fₗ) → E →L[𝕜] Fₗ)
              x :
            E →L[𝕜] Fₗ) :
          (a : E) → Fₗ)
        x_1 :
      Fₗ)
have h : HMul.hMul (β := 𝕜) m ((c : (a : E) → 𝕜) x_1 : 𝕜) • x =
  m • HSMul.hSMul.{u_1, u_7, u_7} (α := 𝕜) ((c : (a : E) → 𝕜) x_1 : 𝕜) x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Bilinear (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst : SeminormedAddCommGroup E
inst_1 : SeminormedAddCommGroup Eₗ
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup Fₗ
inst_4 : SeminormedAddCommGroup G
inst_5 : SeminormedAddCommGroup Gₗ
inst_6 : NontriviallyNormedField 𝕜
inst_7 : NontriviallyNormedField 𝕜₂
inst_8 : NontriviallyNormedField 𝕜₃
inst_9 : NormedSpace 𝕜 E
inst_10 : NormedSpace 𝕜 Eₗ
inst_11 : NormedSpace 𝕜₂ F
inst_12 : NormedSpace 𝕜 Fₗ
inst_13 : NormedSpace 𝕜₃ G
inst_14 : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : FunLike 𝓕 E F
σ₂₁ : 𝕜₂ →+* 𝕜
inst_17 : RingHomInvPair σ₁₂ σ₂₁
inst_18 : RingHomInvPair σ₂₁ σ₁₂
E' : Type u_11
F' : Type u_12
inst_19 : SeminormedAddCommGroup E'
inst_20 : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst_21 : NontriviallyNormedField 𝕜₁'
inst_22 : NontriviallyNormedField 𝕜₂'
inst_23 : NormedSpace 𝕜₁' E'
inst_24 : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst_25 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst_26 : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst_27 : RingHomIsometric σ₂₃
inst_28 : RingHomIsometric σ₁₃'
inst_29 : RingHomIsometric σ₂₃'
inst_30 : RingHomIsometric σ₁₃
inst_31 : RingHomIsometric σ₁'
inst_32 : RingHomIsometric σ₂'
m : 𝕜
c : StrongDual 𝕜 E
x : Fₗ
x_1 : E
⊢ HMul.hMul (β := 𝕜) m ((c : (a : E) → 𝕜) x_1 : 𝕜) • x =
    m • HSMul.hSMul.{u_1, u_7, u_7} (α := 𝕜) ((c : (a : E) → 𝕜) x_1 : 𝕜) x
have h : HMul.hMul (β := 𝕜) m ((c : (a : E) → 𝕜) x_1 : 𝕜) • x = HMul.hMul (β := 𝕜) m ((c : (a : E) → 𝕜) x_1 : 𝕜) • x
Tactic: rw [smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
⊢ IsBoundedLinearMap 𝕜 (F := E) fun (x : E × F) ↦ x.1
have refine : ∀ (x : E × F), norm.{u_2} (E := E) ((LinearMap.fst 𝕜 E F : (a : E × F) → E) x : E) ≤ 1 * ‖x‖
Tactic: refine (LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
x : E × F
⊢ norm.{u_2} (E := E) ((LinearMap.fst 𝕜 E F : (a : E × F) → E) x : E) ≤ 1 * ‖x‖
have rw : norm.{u_2} (E := E) ((LinearMap.fst 𝕜 E F : (a : E × F) → E) x : E) ≤ ‖x‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
⊢ IsBoundedLinearMap 𝕜 (F := F) fun (x : E × F) ↦ x.2
have refine : ∀ (x : E × F), norm.{u_3} (E := F) ((LinearMap.snd 𝕜 E F : (a : E × F) → F) x : F) ≤ 1 * ‖x‖
Tactic: refine (LinearMap.snd 𝕜 E F).isLinear.with_bound 1 fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
x : E × F
⊢ norm.{u_3} (E := F) ((LinearMap.snd 𝕜 E F : (a : E × F) → F) x : F) ≤ 1 * ‖x‖
have rw : norm.{u_3} (E := F) ((LinearMap.snd 𝕜 E F : (a : E × F) → F) x : F) ≤ ‖x‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
𝕜' : Type u_5
c : 𝕜'
inst_5 : SeminormedRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : IsBoundedSMul 𝕜' F
inst_8 : SMulCommClass 𝕜 𝕜' F
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
M : ℝ
left : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
x : E
⊢ ‖c‖ * ‖f x‖ ≤ ‖c‖ * (M * ‖x‖)
have h₁ : 0 ≤ ‖c‖
Tactic: grw [hM]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f : E → F
𝕜' : Type u_5
c : 𝕜'
inst_5 : SeminormedRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : IsBoundedSMul 𝕜' F
inst_8 : SMulCommClass 𝕜 𝕜' F
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
M : ℝ
left : 0 < M
hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
x : E
h₁ : 0 ≤ ‖c‖
⊢ ‖c‖ * ‖f x‖ ≤ ‖c‖ * (M * ‖x‖)
have grw : ‖c‖ * (M * ‖x‖) ≤ ‖c‖ * (M * ‖x‖)
Tactic: grw [hM]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left_1 : 0 < Mg
hMg : ∀ (x : E), ‖g x‖ ≤ Mg * ‖x‖
x : E
⊢ Mf * ‖x‖ + Mg * ‖x‖ ≤ (Mf + Mg) * ‖x‖
have rw : Mf * ‖x‖ + Mg * ‖x‖ ≤ Mf * ‖x‖ + Mg * ‖x‖
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E → F
g : F → G
hg : IsBoundedLinearMap 𝕜 g
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left_1 : 0 < Mg
hMg : ∀ (x : F), ‖g x‖ ≤ Mg * ‖x‖
x : E
⊢ ‖g (f x)‖ ≤ Mg * Mf * ‖x‖
have grw : Mg * ‖f x‖ ≤ Mg * Mf * ‖x‖
Tactic: grw [hMg, hMf, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E → F
g : F → G
hg : IsBoundedLinearMap 𝕜 g
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left_1 : 0 < Mg
hMg : ∀ (x : F), ‖g x‖ ≤ Mg * ‖x‖
x : E
grw : Mg * ‖f x‖ ≤ Mg * Mf * ‖x‖
⊢ ‖g (f x)‖ ≤ Mg * Mf * ‖x‖
have grw₁ : Mg * (Mf * ‖x‖) ≤ Mg * Mf * ‖x‖
Tactic: grw [hMg, hMf, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E → F
g : F → G
hg : IsBoundedLinearMap 𝕜 g
hf : IsBoundedLinearMap 𝕜 f
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left_1 : 0 < Mg
hMg : ∀ (x : F), ‖g x‖ ≤ Mg * ‖x‖
x : E
grw : Mg * ‖f x‖ ≤ Mg * Mf * ‖x‖
grw₁ : Mg * (Mf * ‖x‖) ≤ Mg * Mf * ‖x‖
⊢ ‖g (f x)‖ ≤ Mg * Mf * ‖x‖
have grw₂ : Mg * (Mf * ‖x‖) ≤ Mg * (Mf * ‖x‖)
Tactic: grw [hMg, hMf, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
⊢ ∃ C > 0, ∀ (x : F) (y : E), ‖f ((x, y).2, (x, y).1)‖ ≤ C * ‖x‖ * ‖y‖
have obtain : ∀ (C : ℝ) (hC_pos : C > 0) (hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖),
  ∃ C > 0, ∀ (x : F) (y : E), ‖f ((x, y).2, (x, y).1)‖ ≤ C * ‖x‖ * ‖y‖
Tactic: obtain ⟨C, hC_pos, hC⟩ := h.bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
⊢ ∃ (M : ℝ), 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖
have let : ∀ (C : ℝ) (hC_pos : C > 0) (hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖),
  ∃ (M : ℝ), 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖
Tactic: let ⟨C, hC_pos, hC⟩ := h.bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∃ (M : ℝ), 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖
have refine : ∀ (y : F), C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
Tactic: refine ⟨C * max ‖x‖ 1, by positivity, fun y ↦ (hC x y).trans ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
have inl : ∀ (hx : max ‖x‖ 1 = ‖x‖ ∧ 1 ≤ ‖x‖), C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
Tactic: rcases max_cases ‖x‖ 1 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
inl : ∀ (hx : max ‖x‖ 1 = ‖x‖ ∧ 1 ≤ ‖x‖), C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
have inr : ∀ (hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1), C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
Tactic: rcases max_cases ‖x‖ 1 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = ‖x‖ ∧ 1 ≤ ‖x‖
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
have inl : C * ‖x‖ * ‖y‖ ≤ C * ‖x‖ * ‖y‖
Tactic: grw [hx.1]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
have inr : C * ‖x‖ * ‖y‖ ≤ C * 1 * ‖y‖
Tactic: grw [hx.1, hx.2.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1
inr : C * ‖x‖ * ‖y‖ ≤ C * 1 * ‖y‖
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
have inr₁ : C * 1 * ‖y‖ ≤ C * 1 * ‖y‖
Tactic: grw [hx.1, hx.2.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
have refine : ∀ (x : E × F), Tendsto (β := G) (fun (x_1 : E × F) ↦ f x_1 - f x) (𝓝 x) (𝓝 0)
Tactic: refine continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (β := G) (fun (x_1 : E × F) ↦ f x_1 - f x) (𝓝 x) (𝓝 0)
have suffices : Tendsto (fun (y : E × F) ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (HAdd.hAdd (α := G) 0 0))
Tactic: suffices Tendsto (fun y : E × F ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0)) by
    simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun (y : E × F) ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (HAdd.hAdd (α := G) 0 0))
have hf : Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) (𝓝 x) (𝓝 0)
Tactic: apply Tendsto.add
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hf : Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) (𝓝 x) (𝓝 0)
⊢ Tendsto (fun (y : E × F) ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (HAdd.hAdd (α := G) 0 0))
have hg : Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) (𝓝 x) (𝓝 0)
Tactic: apply Tendsto.add
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) (𝓝 x) (𝓝 0)
have hf : IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) fun (_x : E × F) ↦ HMul.hMul (α := ℝ) 1 1
Tactic: rw [← isLittleO_one_iff ℝ, ← one_mul 1]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x_1.1 - x.1, x_1.2)) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1
have hf : IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.1 - x.1‖ * ‖x_1.2‖) fun (_x : E × F) ↦
  HMul.hMul (α := ℝ) 1 1
Tactic: refine h.isBigO_comp.trans_isLittleO ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.1 - x.1‖ * ‖x_1.2‖) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1
have hf : IsLittleO (E := E) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ x_1.1 - x.1) fun (_x : E × F) ↦ 1
Tactic: refine (IsLittleO.norm_left ?_).mul_isBigO (IsBigO.norm_left ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
hf : IsLittleO (E := E) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ x_1.1 - x.1) fun (_x : E × F) ↦ 1
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.1 - x.1‖ * ‖x_1.2‖) fun (_x : E × F) ↦
    HMul.hMul (α := ℝ) 1 1
have hf₁ : IsBigO (F := ℝ) (𝓝 x) Prod.snd fun (_x : E × F) ↦ 1
Tactic: refine (IsLittleO.norm_left ?_).mul_isBigO (IsBigO.norm_left ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (β := G) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) (𝓝 x) (𝓝 0)
have hg : IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) fun (_x : E × F) ↦ 1
Tactic: rw [← isLittleO_one_iff ℝ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := G) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ f (x.1, x_1.2 - x.2)) fun (_x : E × F) ↦ 1
have hg : IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x.1‖ * ‖x_1.2 - x.2‖) fun (_x : E × F) ↦ 1
Tactic: refine h.isBigO_comp.trans_isLittleO ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x.1‖ * ‖x_1.2 - x.2‖) fun (_x : E × F) ↦ 1
have hg : IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.2 - x.2‖) fun (_x : E × F) ↦ 1
Tactic: apply IsLittleO.const_mul_left
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : Semiring 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 x) (fun (x_1 : E × F) ↦ ‖x_1.2 - x.2‖) fun (_x : E × F) ↦ 1
have hg : Tendsto (fun (x_1 : E × F) ↦ x_1.2 - x.2) (𝓝 x) (𝓝 (x.2 - x.2))
Tactic: rw [isLittleO_norm_left, isLittleO_one_iff, ← sub_self x.2]