mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : 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✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
⊢ ∀ (a : E), ⋯.extend (⇑f) (k • e a) = σ₁₂ k • ⋯.extend (⇑f) (e a)

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
⊢ ∀ (a : E), ⋯.extend (⇑f) (k • e a) = σ₁₂ k • ⋯.extend (⇑f) (e a)
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ 0 ≤ ↑N * ‖f‖

pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ Continuous fun x ↦ ‖(f.extend e) x‖

pp: case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖(f.extend e) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ 0 ≤ ↑N * ‖f‖
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ Continuous fun x ↦ ‖(f.extend e) x‖

pp: case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖(f.extend e) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ Continuous fun x ↦ ‖(f.extend e) x‖
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case hbc
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ C ≤ max C C'

pp: case hbc
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ C' ≤ max C C'

Tactic:
·

Goal state after:
case hbc
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ C ≤ max C C'
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖(f.extend e) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖

Tactic:
·

Goal state after:
case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖(f.extend e) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case hbc
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ C' ≤ max C C'

Tactic:
·

Goal state after:
case hbc
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ C' ≤ max C C'
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = 0
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T f = 0

Tactic:
simp_rw [setToSimpleFunc]

Goal state after:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = 0
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x = 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = 0
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
x✝ : x ∈ f.range
hx0 : x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0

pp: case neg
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = 0
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
x✝ : x ∈ f.range
hx0 : ¬x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = 0
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
x✝ : x ∈ f.range
hx0 : x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case h_dense
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ DenseRange ⇑e.range.subtypeL

pp: case h_e
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ IsUniformInducing ⇑e.range.subtypeL

pp: case H
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ g ∘SL e.range.subtypeL = f.compLeftInverse e

Tactic:
·

Goal state after:
case h_dense
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ DenseRange ⇑e.range.subtypeL
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case h_e
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ IsUniformInducing ⇑e.range.subtypeL

pp: case H
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ g ∘SL e.range.subtypeL = f.compLeftInverse e

Tactic:
·

Goal state after:
case h_e
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ IsUniformInducing ⇑e.range.subtypeL
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ ∀ x ∈ Set.range ⇑e₁, ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) ((↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun x) = x

pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ IsClosed {x | ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) ((↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun x) = x}

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ ∀ x ∈ Set.range ⇑e₁, ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) ((↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun x) = x
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ IsClosed {x | ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) ((↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun x) = x}

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ IsClosed {x | ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) ((↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun x) = x}
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ ∀ x ∈ Set.range ⇑e₂, (↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun (((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x) = x

pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ IsClosed {x | (↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun (((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x) = x}

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ ∀ x ∈ Set.range ⇑e₂, (↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun (((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x) = x
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ IsClosed {x | (↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun (((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x) = x}

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ IsClosed {x | (↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun (((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x) = x}