mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
n : ℕ
a✝ : True
⊢ ‖c ^ n‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
⊢ (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
⊢ μH[↑(finrank ℝ E)] U ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ⊢ μH[1] = volume

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ⊢ μH[2] = volume

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ E →ₗ[ℝ] E →ₗ[ℝ] ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) y = o.volumeForm ![x, y]

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ (o.areaForm x) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
this : μH[1] ((fun x ↦ ‖v‖ • x) '' ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s
⊢ μH[1] ((fun r ↦ r • v) '' s) = ‖v‖₊ • μH[1] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
⊢ Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
⊢ Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) y = -(o.areaForm y) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ (-o).areaForm = -o.areaForm

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ |(o.areaForm x) y| ≤ ‖x‖ * ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
⊢ μH[1] ((fun r ↦ r • v) '' s) = ‖v‖₊ • μH[1] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
⊢ ‖σ c‖ < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) y ≤ ‖x‖ * ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this :
  μH[d] (⇑(IsometryEquiv.vaddConst x) '' (fun x ↦ c • x) '' ⇑(IsometryEquiv.vaddConst x).symm '' s) = ‖c‖₊ ^ d • μH[d] s
⊢ μH[d] (⇑(AffineMap.homothety x c) '' s) = ‖c‖₊ ^ d • μH[d] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
this✝ : Tendsto (fun n ↦ σ c ^ n) atTop (𝓝 0)
this : Tendsto ((fun n ↦ σ c ^ n) • fun n ↦ (σ c ^ n)⁻¹ • f (u n)) atTop (𝓝 0)
n : ℕ
⊢ ((fun n ↦ σ c ^ n) • fun n ↦ (σ c ^ n)⁻¹ • f (u n)) n = (⇑f ∘ u) n

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑(AffineMap.homothety x c) '' s) = ‖c‖₊ ^ d • μH[d] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
⊢ Tendsto (⇑f ∘ u) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ μH[d] (⇑(AffineMap.homothety x c) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μH[d] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
⊢ ContinuousAt (⇑f) 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
⊢ Measure.map ⇑(AffineMap.homothety x c) μH[d] = ‖c‖₊⁻¹ ^ d • μH[d]

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Montel

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
⊢ Continuous[topologicalSpace, UniformConvergenceCLM.instTopologicalSpace σ F {S | IsCompact S}]
    (↑(LinearEquiv.toCompactConvergenceCLM σ E F)).toFun

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
s : Set ℝ
this : μH[1] (⇑(IsometryEquiv.vaddConst x) '' (fun x_1 ↦ x_1 • (y -ᵥ x)) '' s) = nndist x y • μH[1] s
⊢ μH[1] (⇑(AffineMap.lineMap x y) '' s) = nndist x y • μH[1] s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
s : Set ℝ
⊢ μH[1] (⇑(AffineMap.lineMap x y) '' s) = nndist x y • μH[1] s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
⊢ μH[1] (affineSegment ℝ x y) = edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
⊢ |(o.areaForm x) y| = ‖x‖ * ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
x y : E
⊢ μH[1] (segment ℝ x y) = edist x y

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
d : ℝ
s : Set E
hs : 0 ≤ d
⊢ μH[d] (⇑K.orthogonalProjectionOnto '' s) ≤ μH[d] s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ⇑φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y]

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Montel

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
⊢ Continuous[UniformConvergenceCLM.instTopologicalSpace σ F {S | IsCompact S}, topologicalSpace]
    (LinearEquiv.toCompactConvergenceCLM σ E F).invFun

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.StrongTopology

Goal state before:
pp: R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : IsTopologicalAddGroup F
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
⊢ LocallyConvexSpace R (E →SLᵤ[σ, 𝔖] F)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence

Goal state before:
pp: α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜₁ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜₂ F
x : E
⊢ ‖0 x‖ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence

Goal state before:
pp: α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜₁ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜₂ F
x : E
A B : E →SLₚₜ[σ] F
⊢ ‖(A + B) x‖ ≤ ‖A x‖ + ‖B x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence

Goal state before:
pp: α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜₁ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜₂ F
x : E
A : E →SLₚₜ[σ] F
⊢ ‖(-A) x‖ = ‖A x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence

Goal state before:
pp: α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜₁ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜₂ F
x : E
r : 𝕜₂
A : E →SLₚₜ[σ] F
⊢ ‖(r • A) x‖ = ‖r‖ * ‖A x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ (o.areaForm (φ x)) (φ y) = (o.areaForm x) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪o.rightAngleRotationAux₁ x, y⟫ = (o.areaForm x) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪x, o.rightAngleRotationAux₁ y⟫ = -(o.areaForm x) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.PointwiseConvergence

Goal state before:
pp: α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
inst✝¹⁰ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜₁ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : AddCommGroup D
inst✝³ : TopologicalSpace D
inst✝² : Module 𝕜₃ D
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜₂ G
A : (E →SL[σ] F) →ₗ[𝕜₂] D →SL[τ] G
hbound : ∀ (f : D), ∃ s C, ∀ (B : E →SL[σ] F), ∃ g, ∃ (_ : g ∈ s), ‖(A B) f‖ ≤ C • ‖B g‖
⊢ Continuous
    (↑(toUniformConvergenceCLM τ G {s | Finite ↑s}) ∘ₗ A ∘ₗ ↑(toUniformConvergenceCLM σ F {s | Finite ↑s}).symm).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
⊢ finrank ℝ ↥K ≤ {x}.card

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
⊢ Nontrivial ↥Kᗮ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, ↑w⟫ = 0
hw : ↑w ≠ 0
⊢ 0 < ‖↑w‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ‖o.rightAngleRotationAux₁ x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ o.rightAngleRotationAux₂.toLinearMap ∘ₗ (-o.rightAngleRotationAux₁) = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ (-o.rightAngleRotationAux₁) ∘ₗ o.rightAngleRotationAux₂.toLinearMap = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪o.rightAngleRotation x, y⟫ = (o.areaForm x) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪x, o.rightAngleRotation y⟫ = -(o.areaForm x) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ o.rightAngleRotation (o.rightAngleRotation x) = -x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ o.rightAngleRotation.symm = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)

Tactic:
by

Goal state after: