awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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⁻¹ * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F) = a⁻¹ * ‖y‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
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)
rw₂ : a⁻¹ * Norm.norm.{u_4} (E := F) ((f : (a : E) → F) ((f.symm : (a : F) → E) y : E) : F) = a⁻¹ * ‖y‖
⊢ Norm.norm.{u_3} (E := E) ((f.symm : (a : F) → E) y : E) = 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

Premises used: Norm.norm, LinearEquiv.symm, HMul.hMul, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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)

Tactic:
h.1.induction_on₂ ?_ ?_

Premises used: And.left, DenseRange.induction_on₂
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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)}
refine_2 :
  ∀ (a₁ a₂ : E),
    ⋯.extend (⇑f : (a : E) → F)
        (HAdd.hAdd (α := Eₗ) (β := Eₗ) ((e : (a : E) → Eₗ) a₁ : Eₗ) ((e : (a : E) → Eₗ) a₂ : Eₗ)) =
      HAdd.hAdd (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) a₁))
        (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) a₂))
⊢ ∀ (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)

Tactic:
refine h.1.induction_on₂ ?_ ?_
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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)
⊢ 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)}

Tactic:
isClosed_eq (cont.comp continuous_add)
          ((cont.comp continuous_fst).add (cont.comp continuous_snd))

Premises used: Continuous.comp, continuous_snd, continuous_fst, isClosed_eq, continuous_add, Continuous.add
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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)
⊢ 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)}

Tactic:
exact isClosed_eq (cont.comp continuous_add)
          ((cont.comp continuous_fst).add (cont.comp continuous_snd))

Premises used: Continuous.comp, continuous_snd, continuous_fst, isClosed_eq, continuous_add, Continuous.add
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
refine_2 : (f : (a : E) → F) (x + y) = HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)
⊢ ⋯.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))

Tactic:
simp only [eq, ← e.map_add]

Premises used: ContinuousLinearMap.map_add
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ (f : (a : E) → F) (x + y) = HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)

Tactic:
f.map_add _ _

Premises used: ContinuousLinearMap.map_add
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ (f : (a : E) → F) (x + y) = HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)

Tactic:
exact f.map_add _ _

Premises used: ContinuousLinearMap.map_add
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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)

Tactic:
fun b => h.1.induction_on b ?_ ?_

Premises used: And.left, DenseRange.induction_on
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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)}
refine_2 :
  ∀ (b : Eₗ) (a : E),
    ⋯.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 : 𝕜₂)
        (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) a))
⊢ ∀ (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)

Tactic:
refine fun b => h.1.induction_on b ?_ ?_
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
⊢ 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)}

Tactic:
isClosed_eq (cont.comp (continuous_const_smul _))
          ((continuous_const_smul _).comp cont)

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, isClosed_eq
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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ₗ
⊢ 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)}

Tactic:
exact isClosed_eq (cont.comp (continuous_const_smul _))
          ((continuous_const_smul _).comp cont)

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, isClosed_eq
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
refine_2 :
  ⋯.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))
⊢ ⋯.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))

Tactic:
rw [← map_smul]

Premises used: map_smul
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
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)
⊢ ⋯.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))

Tactic:
simp only [eq]
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ (f : (a : E) → F) (k • x) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) ((f : (a : E) → F) x : F)

Tactic:
map_smulₛₗ _ _ _

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
⊢ (f : (a : E) → F) (k • x) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜₂) (β := F) ((σ₁₂ : (a : 𝕜) → 𝕜₂) k : 𝕜₂) ((f : (a : E) → F) x : F)

Tactic:
exact map_smulₛₗ _ _ _

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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
simp : Eq.{u_5 + 1} (α := F) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) x) : F) ((f : (a : E) → F) x : F)
⊢ Eq.{u_5 + 1} (α := F) ((f.extend e : (a : Eₗ) → F) ((e : (a : E) → Eₗ) x : Eₗ) : 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]

Premises used: LinearMap.coe_mk, and_self, reduceDIte, ContinuousLinearMap.extend, AddHom.coe_mk, ContinuousLinearMap.coe_mk'
-- Module: Mathlib.Analysis.Normed.Operator.Extend
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) (⋯.extend (⇑f : (a : E) → F) ((e : (a : E) → Eₗ) x) : F) ((f : (a : E) → F) x : F)

Tactic:
IsDenseInducing.extend_eq (h_e.isDenseInducing h_dense) f.cont _

Premises used: IsUniformInducing.isDenseInducing, ContinuousLinearMap.cont, IsDenseInducing.extend_eq