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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖d‖ * ‖x - y'‖ = ‖d • x - y‖

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 α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT') f = c • (setToL1 hT) f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖

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
𝕜 : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) (c • f) = c • (setToL1 hT) f

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
x : E
⊢ (setToL1 hT) ↑(indicatorConst 1 hs ⋯ x) = (T s) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ x₀ ≠ 0

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
⊢ (setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
⊢ ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ : ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
h₁ : r * ‖x₀‖ ≤ ‖x₀ - ↑‖x₀‖ • y‖
⊢ 0 < ‖x₀‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁵ : NormedAddCommGroup G''
inst✝⁴ : PartialOrder G''
inst✝³ : IsOrderedAddMonoid G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : CompleteSpace G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) f ≤ (setToL1 hT') f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
⊢ ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: α : Type u_2
m : Type u_4
n : Type u_5
R : Type u_8
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace α
f : α → m → n → R
⊢ (Continuous fun x ↦ of (f x)) ↔ Continuous f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Fintype n
inst✝³ : Mul R
inst✝² : AddCommMonoid R
inst✝¹ : ContinuousAdd R
inst✝ : ContinuousMul R
A B : X → n → R
hA : Continuous A
hB : Continuous B
⊢ Continuous fun x ↦ A x ⬝ᵥ B x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x ↦ (A x).det

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
⊢ ∀ (i : n ⊕ p) (j : l ⊕ m), Continuous fun a ↦ fromBlocks (A a) (B a) (C a) (D a) i j

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
⊢ Continuous fun a ↦ blockDiagonal' (A a) ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: m : Type u_4
R : Type u_8
inst✝³ : TopologicalSpace R
α : Type u_11
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Zero R
inst✝ : T2Space R
⊢ IsClosed {M | M.BlockTriangular b}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : CompleteSpace G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : ↥(Lp G' 1 μ)
hf : 0 ≤ f
⊢ 0 ≤ (setToL1 hT) f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
f : P →ᵃⁱ[𝕜] P₂
⊢ f.linear = f.linearIsometry.toLinearMap

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁹ : NormedAddCommGroup G''
inst✝⁸ : PartialOrder G''
inst✝⁷ : IsOrderedAddMonoid G''
inst✝⁶ : NormedSpace ℝ G''
inst✝⁵ : CompleteSpace G''
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : PartialOrder G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : ClosedIciTopology G''
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(Lp G' 1 μ)
hfg : f ≤ g
⊢ (setToL1 hT) f ≤ (setToL1 hT) g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : 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₄
f✝ f g : P →ᵃⁱ[𝕜] P₂
⊢ (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g → f = g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : 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₄
f✝ f g : P →ᵃⁱ[𝕜] P₂
⊢ (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g → f = g

Tactic:
by cases f; cases g; simp

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)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
⊢ (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
f : P →ᵃⁱ[𝕜] P₂
⊢ ⇑f.toAffineMap = ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
⊢ Injective toAffineMap

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
f : V →ₗᵢ[𝕜] V₂
⊢ f.toAffineIsometry.linearIsometry = f

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ ‖setToL1 hT‖ ≤ ↑1 * ‖setToL1SCLM α E μ hT‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ dist (f x) (f y) = dist x y

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ ↑1 * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ nndist (f x) (f y) = nndist x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ edist (f x) (f y) = edist x y

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
C : ℝ
f : α → E
hF : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
⊢ setToFun μ T hT f = (L1.setToL1 hT) (Integrable.toL1 f hf)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ e.linear = e.linearIsometryEquiv.toLinearEquiv

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
C : ℝ
inst✝ : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ setToFun μ T hT ↑↑f = (setToL1 hT) f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : 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 f g : P ≃ᵃⁱ[𝕜] P₂
h : f.toFun = g.toFun
x✝ : f.invFun = g.invFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V₁ : Type u_3
V₂ : Type u_5
P₁ : Type u_8
P₂ : Type u_11
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₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p
⊢ (mk' e e' p h).linearIsometryEquiv = e'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
e : V ≃ₗᵢ[𝕜] V₂
⊢ ⇑e.toAffineIsometryEquiv = ⇑e

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
e : V ≃ₗᵢ[𝕜] V₂
⊢ e.toAffineIsometryEquiv.linearIsometryEquiv = e

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
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ range ⇑e = univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p : P
⊢ (constVSub 𝕜 p).symm = (LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (vaddConst 𝕜 p)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
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₂
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ Isometry g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) x = dist y 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) y = ‖2 • (x -ᵥ y)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) y = ‖2‖ * dist x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: V : Type u_2
P : Type u_10
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedSpace ℝ V
x y : P
⊢ dist ((pointReflection ℝ x) y) y = 2 * dist x y

Tactic:
by

Goal state after: