awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
y : F
rw :
  Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
    a⁻¹ * a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)
rw₁ :
  Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) = 1 * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)
⊢ Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
    a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E))
have rw₂ : Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) = Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)
Tactic: rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
y : F
⊢ a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)) =
    a⁻¹ * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F)
have rw : a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)) =
  a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E))
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
y : F
⊢ Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) = a⁻¹ * ‖y‖
have rw : Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
  a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E))
Tactic: calc
    ‖f.symm y‖ = a⁻¹ * (a * ‖f.symm y‖) := by
      rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]
    _ = a⁻¹ * ‖f (f.symm y)‖ := by rw [hf]
    _ = a⁻¹ * ‖y‖ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
y : F
rw :
  Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
    a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E))
⊢ Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) = a⁻¹ * ‖y‖
have rw₁ : a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)) =
  a⁻¹ * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F)
Tactic: calc
    ‖f.symm y‖ = a⁻¹ * (a * ‖f.symm y‖) := by
      rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]
    _ = a⁻¹ * ‖f (f.symm y)‖ := by rw [hf]
    _ = a⁻¹ * ‖y‖ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousLinearMap (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : Ring 𝕜₂
inst_2 : SeminormedAddCommGroup E
inst_3 : SeminormedAddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst_6 : RingHomInvPair σ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), Norm.norm.{u_4} (E := F) ((f : (a : E) → F) x : F) = a * ‖x‖
y : F
rw :
  Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) =
    a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E))
rw₁ :
  a⁻¹ * (a * Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E)) =
    a⁻¹ * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F)
⊢ Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) = a⁻¹ * ‖y‖
have rw₂ : a⁻¹ * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F) = a⁻¹ * ‖y‖
Tactic: calc
    ‖f.symm y‖ = a⁻¹ * (a * ‖f.symm y‖) := by
      rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]
    _ = a⁻¹ * ‖f (f.symm y)‖ := by rw [hf]
    _ = a⁻¹ * ‖y‖ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h :
  DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ) ∧
    IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
cont : Continuous.{u_4, u_5} (Y := F) (⋯.extend (⇑f : (a : E) → F))
eq : ∀ (b : E), Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) b) : F) ((f : (a : E) → F) b : F)
⊢ ∀ (x y : Eₗ),
    ⋯.extend (⇑f : (a : E) → F) (x + y) =
      HAdd.hAdd (α := F) (⋯.extend (⇑f : (a : E) → F) x) (⋯.extend (⇑f : (a : E) → F) y)
have refine_1 : IsClosed.{u_4} (X := Eₗ × Eₗ)
  {q : Eₗ × Eₗ |
    sorry.extend (⇑f : (a : E) → F) (q.1 + q.2) =
      HAdd.hAdd (α := F) (sorry.extend (⇑f : (a : E) → F) q.1) (sorry.extend (⇑f : (a : E) → F) q.2)}
Tactic: refine h.1.induction_on₂ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h :
  DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ) ∧
    IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
cont : Continuous.{u_4, u_5} (Y := F) (⋯.extend (⇑f : (a : E) → F))
eq : ∀ (b : E), Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) b) : F) ((f : (a : E) → F) b : F)
refine_1 :
  IsClosed.{u_4} (X := Eₗ × Eₗ)
    {q : Eₗ × Eₗ |
      ⋯.extend (⇑f : (a : E) → F) (q.1 + q.2) =
        HAdd.hAdd (α := F) (⋯.extend (⇑f : (a : E) → F) q.1) (⋯.extend (⇑f : (a : E) → F) q.2)}
⊢ ∀ (x y : Eₗ),
    ⋯.extend (⇑f : (a : E) → F) (x + y) =
      HAdd.hAdd (α := F) (⋯.extend (⇑f : (a : E) → F) x) (⋯.extend (⇑f : (a : E) → F) y)
have refine_2 : ∀ (a₁ a₂ : E),
  sorry.extend (⇑f : (a : E) → F)
      (HAdd.hAdd (α := Eₗ) (β := Eₗ) ((e : (a : E) → Eₗ) a₁ : Eₗ) ((e : (a : E) → Eₗ) a₂ : Eₗ)) =
    HAdd.hAdd (α := F) (sorry.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) a₁))
      (sorry.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) a₂))
Tactic: refine h.1.induction_on₂ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h :
  DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ) ∧
    IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
cont : Continuous.{u_4, u_5} (Y := F) (⋯.extend (⇑f : (a : E) → F))
eq : ∀ (b : E), Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) b) : F) ((f : (a : E) → F) b : F)
x y : E
⊢ ⋯.extend (⇑f : (a : E) → F) (HAdd.hAdd (α := Eₗ) (β := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ) ((e : (a : E) → Eₗ) y : Eₗ)) =
    HAdd.hAdd (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) x))
      (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) y))
have refine_2 : (f : (a : E) → F) (x + y) = HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)
Tactic: simp only [eq, ← e.map_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h :
  DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ) ∧
    IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
cont : Continuous.{u_4, u_5} (Y := F) (⋯.extend (⇑f : (a : E) → F))
eq : ∀ (b : E), Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) b) : F) ((f : (a : E) → F) b : F)
k : 𝕜
⊢ ∀ (x : Eₗ),
    ⋯.extend (⇑f : (a : E) → F) (k • x) =
      HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) (⋯.extend (⇑f : (a : E) → F) x)
have refine_1 : ∀ (b : Eₗ),
  IsClosed.{u_4} (X := Eₗ)
    {b : Eₗ |
      sorry.extend (⇑f : (a : E) → F) (k • b) =
        HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) (sorry.extend (⇑f : (a : E) → F) b)}
Tactic: refine fun b => h.1.induction_on b ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h :
  DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ) ∧
    IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
cont : Continuous.{u_4, u_5} (Y := F) (⋯.extend (⇑f : (a : E) → F))
eq : ∀ (b : E), Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) b) : F) ((f : (a : E) → F) b : F)
k : 𝕜
refine_1 :
  ∀ (b : Eₗ),
    IsClosed.{u_4} (X := Eₗ)
      {b : Eₗ |
        ⋯.extend (⇑f : (a : E) → F) (k • b) =
          HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) (⋯.extend (⇑f : (a : E) → F) b)}
⊢ ∀ (x : Eₗ),
    ⋯.extend (⇑f : (a : E) → F) (k • x) =
      HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) (⋯.extend (⇑f : (a : E) → F) x)
have refine_2 : ∀ (b : Eₗ) (a : E),
  sorry.extend (⇑f : (a : E) → F) (HSMul.hSMul (β := Eₗ) k ((e : (a : E) → Eₗ) a : Eₗ)) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂)
      (sorry.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) a))
Tactic: refine fun b => h.1.induction_on b ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h :
  DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ) ∧
    IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
cont : Continuous.{u_4, u_5} (Y := F) (⋯.extend (⇑f : (a : E) → F))
eq : ∀ (b : E), Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) b) : F) ((f : (a : E) → F) b : F)
k : 𝕜
b : Eₗ
x : E
⊢ ⋯.extend (⇑f : (a : E) → F) (HSMul.hSMul (β := Eₗ) k ((e : (a : E) → Eₗ) x : Eₗ)) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂)
      (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) x))
have refine_2 : sorry.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) (k • x)) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂)
    (sorry.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) x))
Tactic: rw [← map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h :
  DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ) ∧
    IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
cont : Continuous.{u_4, u_5} (Y := F) (⋯.extend (⇑f : (a : E) → F))
eq : ∀ (b : E), Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) b) : F) ((f : (a : E) → F) b : F)
k : 𝕜
b : Eₗ
x : E
⊢ ⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) (k • x)) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂)
      (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) x))
have refine_2 : (f : (a : E) → F) (k • x) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) ((f : (a : E) → F) x : F)
Tactic: simp only [eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
x : E
⊢ Eq.{u_5 + 1} (α := F) ((f.extend e : (a : Eₗ) → F) ((e : (a : E) → Eₗ) x : Eₗ) : F) ((f : (a : E) → F) x : F)
have simp : Eq.{u_5 + 1} (α := F) (sorry.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) x) : F) ((f : (a : E) → F) x : F)
Tactic: simp only [extend, h_dense, h_e, and_self, ↓reduceDIte, coe_mk', LinearMap.coe_mk, AddHom.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : AddCommGroup E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : AddCommGroup F
inst_4 : UniformSpace F
inst_5 : IsUniformAddGroup F
inst_6 : T0Space F
inst_7 : AddCommMonoid Eₗ
inst_8 : UniformSpace Eₗ
inst_9 : ContinuousAdd Eₗ
inst_10 : Semiring 𝕜
inst_11 : Semiring 𝕜₂
inst_12 : Module 𝕜 E
inst_13 : Module 𝕜₂ F
inst_14 : Module 𝕜 Eₗ
inst_15 : ContinuousConstSMul 𝕜 Eₗ
inst_16 : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst_17 : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : IsUniformInducing.{u_3, u_4} (α := E) (β := Eₗ) (⇑e : (a : E) → Eₗ)
g : Eₗ →SL[σ₁₂] F
H : g ∘SL e = f
⊢ f.extend e = g
have simp : { toFun := sorry.extend (⇑f : (a : E) → F), map_add' := sorry, map_smul' := sorry, cont := sorry } = g
Tactic: simp only [extend, h_dense, h_e, and_self, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
⊢ ‖f.extend e‖ ≤ (↑N : ℝ) * ‖f‖
have refine_1 : 0 ≤ (↑N : ℝ) * ‖f‖
Tactic: refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ (by fun_prop)) fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
refine_1 : 0 ≤ (↑N : ℝ) * ‖f‖
⊢ ‖f.extend e‖ ≤ (↑N : ℝ) * ‖f‖
have refine_2 : Continuous (Y := ℝ) fun (x : Eₗ) ↦ norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) x : F)
Tactic: refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ (by fun_prop)) fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
refine_1 : 0 ≤ (↑N : ℝ) * ‖f‖
refine_2 : Continuous (Y := ℝ) fun (x : Eₗ) ↦ norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) x : F)
⊢ ‖f.extend e‖ ≤ (↑N : ℝ) * ‖f‖
have refine_3 : ∀ (x : E),
  norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) ((e : (a : E) → Eₗ) x : Eₗ) : F) ≤
    (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
Tactic: refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ (by fun_prop)) fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
hN : N ≤ 0
⊢ 0 ≤ (↑N : ℝ) * ‖f‖
have refine_1 : ∀ (this : Unique E), 0 ≤ (↑N : ℝ) * ‖f‖
Tactic: have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
        (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
hN : N ≤ 0
this : Unique E
⊢ 0 ≤ (↑N : ℝ) * ‖f‖
have refine_1 : 0 ≤ (↑N : ℝ) * norm (E := E →SL[σ₁₂] F) 0
Tactic: obtain rfl : f = 0 := Subsingleton.elim ..
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
⊢ 0 ≤ (↑N : ℝ) * ‖f‖
have x : 0 ≤ N ∨ N ≤ 0
Tactic: cases le_total 0 N with
    | inl hN => exact mul_nonneg hN (norm_nonneg _)
    | inr hN =>
      have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
        (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
      obtain rfl : f = 0 := Subsingleton.elim ..
      simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Extend (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup Eₗ
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 Eₗ
inst_7 : NormedSpace 𝕜₂ F
inst_8 : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst_9 : RingHomIsometric σ₁₂
h_dense : DenseRange.{u_4, u_3} (X := Eₗ) (α := E) (⇑e : (a : E) → Eₗ)
h_e : ∀ (x : E), ‖x‖ ≤ (↑N : ℝ) * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
x : E
⊢ norm.{u_5} (E := F) ((f.extend e : (a : Eₗ) → F) ((e : (a : E) → Eₗ) x : Eₗ) : F) ≤
    (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
have refine_3 : norm.{u_5} (E := F) ((f : (a : E) → F) x : F) ≤ (↑N : ℝ) * ‖f‖ * norm.{u_4} (E := Eₗ) ((e : (a : E) → Eₗ) x : Eₗ)
Tactic: rw [extend_eq _ h_dense (isUniformEmbedding_of_bound _ h_e).isUniformInducing]