mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst✝²⁴ : NormedField 𝕜
inst✝²³ : SeminormedAddCommGroup V
inst✝²² : NormedSpace 𝕜 V
inst✝²¹ : PseudoMetricSpace P
inst✝²⁰ : NormedAddTorsor V P
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : NormedSpace 𝕜 V₁
inst✝¹⁷ : PseudoMetricSpace P₁
inst✝¹⁶ : NormedAddTorsor V₁ P₁
inst✝¹⁵ : SeminormedAddCommGroup V₁'
inst✝¹⁴ : NormedSpace 𝕜 V₁'
inst✝¹³ : MetricSpace P₁'
inst✝¹² : NormedAddTorsor V₁' P₁'
inst✝¹¹ : SeminormedAddCommGroup V₂
inst✝¹⁰ : NormedSpace 𝕜 V₂
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : NormedAddTorsor V₂ P₂
inst✝⁷ : SeminormedAddCommGroup V₃
inst✝⁶ : NormedSpace 𝕜 V₃
inst✝⁵ : PseudoMetricSpace P₃
inst✝⁴ : NormedAddTorsor V₃ P₃
inst✝³ : SeminormedAddCommGroup V₄
inst✝² : NormedSpace 𝕜 V₄
inst✝¹ : PseudoMetricSpace P₄
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝¹ : P ≃ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖toAffineEquiv✝¹.linear x‖ = ‖x‖
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖toAffineEquiv✝.linear x‖ = ‖x‖
h :
  { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ }.toFun =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }.toFun
x✝ :
  { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ }.invFun =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }.invFun
⊢ toAffineEquiv✝¹ = toAffineEquiv✝

Tactic:
simpa using

Goal state after:
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₁' : Type u_4
V₂ : Type u_5
V₃ : Type u_6
V₄ : Type u_7
P₁ : Type u_8
P₁' : Type u_9
P : Type u_10
P₂ : Type u_11
P₃ : Type u_12
P₄ : Type u_13
inst✝²⁴ : NormedField 𝕜
inst✝²³ : SeminormedAddCommGroup V
inst✝²² : NormedSpace 𝕜 V
inst✝²¹ : PseudoMetricSpace P
inst✝²⁰ : NormedAddTorsor V P
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : NormedSpace 𝕜 V₁
inst✝¹⁷ : PseudoMetricSpace P₁
inst✝¹⁶ : NormedAddTorsor V₁ P₁
inst✝¹⁵ : SeminormedAddCommGroup V₁'
inst✝¹⁴ : NormedSpace 𝕜 V₁'
inst✝¹³ : MetricSpace P₁'
inst✝¹² : NormedAddTorsor V₁' P₁'
inst✝¹¹ : SeminormedAddCommGroup V₂
inst✝¹⁰ : NormedSpace 𝕜 V₂
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : NormedAddTorsor V₂ P₂
inst✝⁷ : SeminormedAddCommGroup V₃
inst✝⁶ : NormedSpace 𝕜 V₃
inst✝⁵ : PseudoMetricSpace P₃
inst✝⁴ : NormedAddTorsor V₃ P₃
inst✝³ : SeminormedAddCommGroup V₄
inst✝² : NormedSpace 𝕜 V₄
inst✝¹ : PseudoMetricSpace P₄
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝¹ : P ≃ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖toAffineEquiv✝¹.linear x‖ = ‖x‖
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖toAffineEquiv✝.linear x‖ = ‖x‖
h :
  { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ }.toFun =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }.toFun
x✝ :
  { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ }.invFun =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }.invFun
⊢ toAffineEquiv✝¹ = toAffineEquiv✝
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝² : Countable ι
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
inst✝ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
hc : ∀ (i : ι), c i ≠ ∞
h : Summable fun i ↦ (c i).toReal * ‖f (x i)‖
⊢ Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂c i • Measure.dirac (x i)

Tactic:
simpa using

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝² : Countable ι
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
inst✝ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
hc : ∀ (i : ι), c i ≠ ∞
h : Summable fun i ↦ (c i).toReal * ‖f (x i)‖
⊢ Summable fun i ↦ (c i).toReal * ‖f (x i)‖
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
inst✝ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
hf : Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ Summable fun i ↦ (c i).toReal * ‖f (x i)‖

Tactic:
simpa using

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
inst✝ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
hf : Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ Summable fun i ↦ (c i).toReal * ‖f (x i)‖
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : CompleteSpace E
hc : ∀ (i : ι), c i ≠ ∞
hf : Summable fun i ↦ (c i).toReal * ‖f (x i)‖
⊢ HasSum (fun i ↦ (c i).toReal • f (x i)) (∫ (x : X), f x ∂Measure.sum fun i ↦ c i • Measure.dirac (x i))

Tactic:
simpa using

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : CompleteSpace E
hc : ∀ (i : ι), c i ≠ ∞
hf : Summable fun i ↦ (c i).toReal * ‖f (x i)‖
⊢ HasSum (fun i ↦ (c i).toReal • f (x i)) (∫ (x : X), f x ∂Measure.sum fun i ↦ c i • Measure.dirac (x i))
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x ↦ x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ x ∈ (fun x ↦ x ^ n) '' s * s

Tactic:
rw [← ypow_eq_x, pow_succ y n]

Goal state after:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x ↦ x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ y ^ n * y ∈ (fun x ↦ x ^ n) '' s * s
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith C fun p ↦ p.1 * p.2
p a b : R
a_in_s : a ∈ s
b_in_t : b ∈ t
eq_p : a * b = p
⊢ p ∈ s * t

Tactic:
simpa using

Goal state after:
case mpr
R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith C fun p ↦ p.1 * p.2
p a b : R
a_in_s : a ∈ s
b_in_t : b ∈ t
eq_p : a * b = p
⊢ a * b ∈ s * t
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
⊢ Tendsto (fun x_1 ↦ x_1 - x) (cobounded R) (cobounded R)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
⊢ Tendsto (fun x_1 ↦ x_1 + -x) (cobounded R) (cobounded R)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
⊢ setToFun μ (-T) ⋯ f = -setToFun μ T hT f

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
⊢ setToFun μ (-T) ⋯ f = -setToFun μ T hT f
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (closedBall 0 Af ×ˢ closedBall 0 Ag)
a✝ x : ℝ≥0
x_in_s : x ∈ s
y : ℝ≥0
y_in_t : y ∈ t
xy_eq : (fun x1 x2 ↦ x1 * x2) x y = a✝
⊢ (x, y) ∈ closedBall 0 Af ×ˢ closedBall 0 Ag ∧ (fun p ↦ p.1 * p.2) (x, y) = a✝

Tactic:
simpa using

Goal state after:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (closedBall 0 Af ×ˢ closedBall 0 Ag)
a✝ x : ℝ≥0
x_in_s : x ∈ s
y : ℝ≥0
y_in_t : y ∈ t
xy_eq : (fun x1 x2 ↦ x1 * x2) x y = a✝
⊢ (x ∈ closedBall 0 Af ∧ y ∈ closedBall 0 Ag) ∧ x * y = a✝
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬∃ s, Nonempty (Basis (↥s) 𝕜 E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦
    (if H : ∃ s, Nonempty (Basis (↥s) 𝕜 E) then LinearMap.detAux (Trunc.mk ⋯.some) else 1) ↑f

Tactic:
simpa using

Goal state after:
case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬∃ s, Nonempty (Basis (↥s) 𝕜 E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ 1
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᵐ[μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
have hgi : ¬Integrable g μ := by rw [integrable_congr h] at hfi; exact hfi
    rw [setToFun_undef hT hfi, setToFun_undef hT hgi]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} = ∞
⊢ ε * μ.real {x | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} = ∞
⊢ 0 ≤ ∫ (x : α), f x ∂μ
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : IsEmpty α
⊢ dist f g = ⨆ x, dist (f x) (g x)

Tactic:
iSup_of_empty',

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : IsEmpty α
⊢ dist f g = sSup ∅
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ↑(nndist f g) = ⨆ x, ↑(nndist (f x) (g x))

Tactic:
nndist_eq_iSup

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ↑(⨆ x, nndist (f x) (g x)) = ⨆ x, ↑(nndist (f x) (g x))
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hf_int : Integrable f μ
ε : ℝ
⊢ ε * μ.real {x | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ

Tactic:
rcases eq_top_or_lt_top (μ {x | ε ≤ f x}) with hμ | hμ
  · simpa [measureReal_def, hμ] using integral_nonneg_of_ae hf_nonneg
  · have := Fact.mk hμ
    calc
      ε * μ.real { x | ε ≤ f x } = ∫ _ in {x | ε ≤ f x}, ε ∂μ := by simp [mul_comm]
      _ ≤ ∫ x in {x | ε ≤ f x}, f x ∂μ :=
        integral_mono_ae (integrable_const _) (hf_int.mono_measure μ.restrict_le_self) <|
          ae_restrict_mem₀ <| hf_int.aemeasurable.nullMeasurable measurableSet_Ici
      _ ≤ _ := integral_mono_measure μ.restrict_le_self hf_nonneg hf_int

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
x : α
⊢ ENNReal.ofReal (‖f x‖ ^ p) = ENNReal.ofReal ‖f x‖ ^ p

Tactic:
ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.nonneg

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
x : α
⊢ ENNReal.ofReal (‖f x‖ ^ p) = ENNReal.ofReal (‖f x‖ ^ p)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
⊢ Integrable f μ

Tactic:
obtain ⟨i, hi, h'i⟩ : ∃ i, ∫⁻ x, ‖fs i x - f x‖ₑ ∂μ < 1 ∧ Integrable (fs i) μ :=
      (((tendsto_order.1 hfs).2 _ zero_lt_one).and hfsi).exists

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
⊢ Integrable f μ
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
⊢ LipschitzWith (LipschitzAdd.C β) fun p ↦ p.1 + p.2

Tactic:
rw [lipschitzWith_iff_dist_le_mul]

Goal state after:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
C_nonneg : 0 ≤ ↑(LipschitzAdd.C β)
⊢ ∀ (x y : (α →ᵇ β) × (α →ᵇ β)), dist (x.1 + x.2) (y.1 + y.2) ≤ ↑(LipschitzAdd.C β) * dist x y
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
n : ℤ
f : α →ᵇ β
⊢ ∃ C, ∀ (x y : α), dist ((n • f.toContinuousMap).toFun x) ((n • f.toContinuousMap).toFun y) ≤ C

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
n : ℤ
f : α →ᵇ β
⊢ ∃ C, ∀ (x y : α), dist (n • f x) (n • f y) ≤ C
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
this : ∃ x, x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖-(y - x)‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
this : ∃ x, x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖x - y‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
x✝ : α →ᵇ β
⊢ ‖{ toFun := fun f ↦ f.compContinuous g, map_add' := ⋯, map_smul' := ⋯ } x✝‖ ≤ 1 * ‖x✝‖

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
x✝ : α →ᵇ β
⊢ ‖x✝.compContinuous g‖ ≤ ‖x✝‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 β
inst✝ : SeminormedAddCommGroup γ
g : C(γ, α)
x : α →ᵇ β
⊢ ‖(compContinuousCLM β 𝕜 g) x‖ ≤ 1 * ‖x‖

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 β
inst✝ : SeminormedAddCommGroup γ
g : C(γ, α)
x : α →ᵇ β
⊢ ‖x.compContinuous g‖ ≤ ‖x‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
⊢ ∀ (x : α), f x = 0 ∨ g x = 0

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
⊢ ∀ (x : α), f x = 0 ∨ g x = 0
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : ContinuousSMul 𝕜 V
r : ℝ
rpos : 0 < r
c : V
h : IsCompact (closedBall c r)
⊢ IsCompact (closedBall 0 r)

Tactic:
simpa using

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : ContinuousSMul 𝕜 V
r : ℝ
rpos : 0 < r
c : V
h : IsCompact (closedBall c r)
⊢ IsCompact (closedBall 0 r)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
⊢ ProperSpace E

Tactic:
rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  have hC : ∀ n, IsCompact (closedBall (0 : E) (‖c‖ ^ n * r)) := fun n ↦ by
    have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
    simpa [_root_.smul_closedBall' this] using hr.smul (c ^ n)
  have hTop : Tendsto (fun n ↦ ‖c‖ ^ n * r) atTop atTop :=
    Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
  exact .of_seq_closedBall hTop (Eventually.of_forall hC)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
⊢ ‖f - g‖ = max ‖f‖ ‖g‖

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
⊢ ‖f + -g‖ = max ‖f‖ ‖g‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
h : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
this : f j * ∑ i ∈ s, f i = 0
⊢ ‖∑ i ∈ insert j s, f i‖₊ = (insert j s).sup fun x ↦ ‖f x‖₊

Tactic:
simpa using

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
h : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
this : f j * ∑ i ∈ s, f i = 0
⊢ ‖f j + ∑ i ∈ s, f i‖₊ = max ‖f j‖₊ ‖∑ i ∈ s, f i‖₊
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: case insert
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
h : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
⊢ f j * ∑ i ∈ s, f i = 0

Tactic:
simpa using

Goal state after:
case insert
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
ι : Type u_2
f : ι → α →ᵇ R
h : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
⊢ ∑ i ∈ s, f j * f i = 0
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ∃ C, ∀ (x y : α), dist ((f.toContinuousMap ^ n).toFun x) ((f.toContinuousMap ^ n).toFun y) ≤ C

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ∃ C, ∀ (x y : α), dist (f x ^ n) (f y ^ n) ≤ C
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
h₁ : f ≤ g
h : α →ᵇ β
t : α
⊢ (fun f ↦ f.toFun) (f + h) t ≤ (fun f ↦ f.toFun) (g + h) t

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
h₁ : f ≤ g
h : α →ᵇ β
t : α
⊢ f t ≤ g t