mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹⁸ : Ring R
inst✝¹⁷ : AddCommGroup V
inst✝¹⁶ : Module R V
inst✝¹⁵ : TopologicalSpace P
inst✝¹⁴ : AddTorsor V P
inst✝¹³ : AddCommGroup W
inst✝¹² : Module R W
inst✝¹¹ : TopologicalSpace Q
inst✝¹⁰ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝⁹ : AddCommGroup W₂
inst✝⁸ : Module R W₂
inst✝⁷ : TopologicalSpace Q₂
inst✝⁶ : AddTorsor W₂ Q₂
inst✝⁵ : TopologicalSpace V
inst✝⁴ : IsTopologicalAddTorsor P
inst✝³ : TopologicalSpace W
inst✝² : IsTopologicalAddTorsor Q
inst✝¹ : TopologicalSpace W₂
inst✝ : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous ⇑(↑f).linear

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
⊢ Injective toAffineEquiv

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
⊢ Injective toContinuousAffineMap

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
s : Set P₂
⊢ ⇑e.symm '' s = ⇑e ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous ((↑e₁).prodCongr ↑e₂).toFun

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous ((↑e₁).prodCongr ↑e₂).invFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous (AffineEquiv.prodAssoc k P₁ P₂ P₃).toFun

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this✝ : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
this : Tendsto (fun n ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous (AffineEquiv.prodAssoc k P₁ P₂ P₃).invFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
⊢ f.contLinear = 0 ↔ (↑f).linear = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s t : AffineSubspace R P
inst✝¹ : Nonempty ↥s
inst✝ : Nonempty ↥t
h : s = t
⊢ Continuous (AffineEquiv.ofEq s t h).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace P
inst✝² : AddTorsor V P
s t : AffineSubspace R P
inst✝¹ : Nonempty ↥s
inst✝ : Nonempty ↥t
h : s = t
⊢ Continuous (AffineEquiv.ofEq s t h).invFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module R V
inst✝⁶ : TopologicalSpace P
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace Q
inst✝¹ : AddTorsor W Q
e : P ≃ᴬ[R] Q
s : AffineSubspace R P
inst✝ : Nonempty ↥s
⊢ Continuous ((↑e).affineSubspaceMap s).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module R V
inst✝⁶ : TopologicalSpace P
inst✝⁵ : AddTorsor V P
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace Q
inst✝¹ : AddTorsor W Q
e : P ≃ᴬ[R] Q
s : AffineSubspace R P
inst✝ : Nonempty ↥s
⊢ Continuous ((↑e).affineSubspaceMap s).invFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
s : AffineSubspace R P
inst✝ : Nonempty ↥s
⊢ Continuous fun p ↦ p.1 +ᵥ p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
s : AffineSubspace R P
inst✝ : Nonempty ↥s
⊢ Continuous fun x ↦ x.1 -ᵥ x.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.AffineSubspace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module R V
inst✝⁴ : TopologicalSpace P
inst✝³ : AddTorsor V P
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddTorsor P
inst✝ : T1Space V
s : AffineSubspace R P
⊢ IsClosed ↑s.direction ↔ IsClosed ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
⊢ ∀ (q : Q), f = const R P q ↔ ↑f = AffineMap.const R P q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
⊢ f.contLinear = 0 ↔ ∃ q, f = const R P q

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace P
inst✝⁹ : AddTorsor V P
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace Q
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace W
inst✝³ : IsTopologicalAddGroup W
inst✝² : IsTopologicalAddTorsor Q
inst✝¹ : ContinuousConstSMul R W
inst✝ : SMulCommClass R R W
f g : P →ᴬ[R] Q
c : R
p : P
⊢ ((AffineMap.lineMap f g) c) p = (AffineMap.lineMap (f p) (g p)) c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝²⁹ : Ring R
inst✝²⁸ : AddCommGroup V
inst✝²⁷ : Module R V
inst✝²⁶ : TopologicalSpace P
inst✝²⁵ : AddTorsor V P
inst✝²⁴ : AddCommGroup W
inst✝²³ : Module R W
inst✝²² : TopologicalSpace Q
inst✝²¹ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Continuous ((↑f).prod ↑g).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝²⁹ : Ring R
inst✝²⁸ : AddCommGroup V
inst✝²⁷ : Module R V
inst✝²⁶ : TopologicalSpace P
inst✝²⁵ : AddTorsor V P
inst✝²⁴ : AddCommGroup W
inst✝²³ : Module R W
inst✝²² : TopologicalSpace Q
inst✝²¹ : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₃ →ᴬ[k] P₄
⊢ Continuous ((↑f).prodMap ↑g).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : TopologicalSpace W
f : V →L[R] W
⊢ ∀ (p v : V), f (v +ᵥ p) = ↑f v +ᵥ f p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : TopologicalSpace W
f : V →L[R] W
⊢ f.toContinuousAffineMap 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup V
inst✝ : IsTopologicalAddGroup W
f : V →ᴬ[R] W
⊢ ⇑f = ⇑f.contLinear + Function.const V (f 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
⊢ (fun p ↦ p.2.toContinuousAffineMap +ᵥ const R V p.1) ((fun f ↦ (f 0, f.contLinear)) f) = f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
⊢ Function.RightInverse (fun p ↦ p.2.toContinuousAffineMap +ᵥ const R V p.1) fun f ↦ (f 0, f.contLinear)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module R W
inst✝³ : TopologicalSpace W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
⊢ ((decompEquiv R V Q).symm p).contLinear = p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Ring S
inst✝¹¹ : Ring R
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : AddCommGroup W
inst✝⁵ : Module R W
inst✝⁴ : TopologicalSpace W
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : IsTopologicalAddGroup W
p : W × (V →L[R] W)
⊢ ((decompLinearEquiv R S V W).symm p).contLinear = p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁵ : Ring S
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup V
inst✝¹² : Module R V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : IsTopologicalAddGroup V
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module R W
inst✝⁷ : TopologicalSpace W
inst✝⁶ : Module S W
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : ContinuousConstSMul S W
inst✝³ : AddTorsor W Q
inst✝² : TopologicalSpace Q
inst✝¹ : IsTopologicalAddGroup W
inst✝ : IsTopologicalAddTorsor Q
p : Q × (V →L[R] W)
⊢ ((decompAffineEquiv R S V Q).symm p).contLinear = p.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
E : Type u_2
inst✝ : NormedAddCommGroup E
z : E
⊢ ‖↑‖z‖‖ = ‖z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ‖↑‖x‖ • coord 𝕜 x h‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
⊢ ‖f z₁‖ ≤ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
⊢ ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ f z = ↑‖z‖ / ↑r * f z₁

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
⊢ ‖f‖ = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖

Tactic:
by

Goal state after:
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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hμ : μ ≪ μ'
f : ↥(α →₁ₛ[μ] E)
f' : ↥(α →₁ₛ[μ'] E)
h : ↑↑↑f =ᵐ[μ] ↑↑↑f'
⊢ setToL1S T f = setToL1S T f'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
⊢ ‖f z‖ ≤ c / r * ‖z‖

Tactic:
by

Goal state after:
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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : ↥(α →₁ₛ[μ] E)
⊢ setToL1S T (f + g) = setToL1S T f + setToL1S T g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ 0 ∈ closedBall 0 r

Tactic:
by

Goal state after:
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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(α →₁ₛ[μ] E)
⊢ setToL1S T (-f) = -setToL1S T f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ z ∈ closedBall 0 r, ‖f z‖ ≤ c
⊢ ‖f‖ ≤ c / r

Tactic:
by

Goal state after: