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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
inst✝ : CompleteSpace ↥G
hker : (↑f).ker = ⊥
⊢ (↑f).range = (↑f).range

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (∑ i, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(↑(Fintype.card ι) ^ (ENNReal.toReal 1 / p.toReal)) * edist x.ofLp y.ofLp

Tactic:
]

Goal state after:
case inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (∑ i, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(↑(Fintype.card ι) ^ (ENNReal.toReal 1 / p.toReal)) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑G
hker : (↑f).ker = ⊥
this : CompleteSpace ↥G
g : (E × ↥G) ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ↑(Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E →L[𝕜] F
G : Submodule 𝕜 F
h : IsCompl (↑f).range G
hG : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑G
hker : (↑f).ker = ⊥
this : CompleteSpace ↥G
g : (E × ↥G) ≃L[𝕜] F := f.coprodSubtypeLEquivOfIsCompl h hker
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ↑(Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥))
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
this : ↑(Fintype.card ι) = ↑↑(Fintype.card ι)
⊢ ↑↑(Fintype.card ι) ^ (1 / p.toReal) * edist x.ofLp y.ofLp = ↑↑(Fintype.card ι) ^ (1 / p.toReal) * edist x.ofLp y.ofLp

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ comap (fun x ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 ((i : ι) → β i)) = 𝓤 (WithLp p ((i : ι) → β i))

Tactic:
]

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ comap (fun x ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 ((i : ι) → β i)) = 𝓤 (WithLp p ((i : ι) → β i))
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
h : 1 ≤ 0
hp : p = ∞
⊢ False

Tactic:
]

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
h : 1 ≤ 0
hp : p = ∞
⊢ False
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ∞ β
⊢ ⨆ i, ‖f.ofLp i‖₊ = ⨆ i, ‖f.ofLp i‖₊

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑g.graph
hφ : Tendsto φ atTop (𝓝 (x, y))
this : ⇑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x
φ : ℕ → E × F
x : E
y : F
hφg : ∀ (n : ℕ), φ n ∈ ↑g.graph
hφ : Tendsto φ atTop (𝓝 (x, y))
this : ⇑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ
⊢ Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / ↑2) = √(∑ i, ‖x.ofLp i‖ ^ 2)

Tactic:
]

Goal state after:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / ↑2) = √(∑ i, ‖x.ofLp i‖ ^ 2)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / ↑2) = (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / 2)

Tactic:
]

Goal state after:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / ↑2) = (∑ i, ‖x.ofLp i‖ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (↑f).range.topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (↑f).range.topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ (↑f).range.topologicalClosure = ⊤

Tactic:
]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
σ : 𝕜 →+* 𝕜'
σ' : 𝕜' →+* 𝕜
inst✝⁷ : RingHomInvPair σ σ'
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
inst✝² : RingHomInvPair σ' σ
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomIsometric σ'
f : E →SL[σ] F
x✝ : (↑f).range.topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
hd : (↑f).range.topologicalClosure = ⊤
c : ℝ≥0
hf : AntilipschitzWith c ⇑f
⊢ (↑f).range.topologicalClosure = ⊤
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ∑ i, ‖x.ofLp i‖₊ ^ 2 = ∑ i, ‖x.ofLp i‖₊ ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
hp : Fact (1 ≤ ∞)
f : PiLp ∞ β
⊢ ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊

Tactic:
]

Goal state after:
case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
hp : Fact (1 ≤ ∞)
f : PiLp ∞ β
⊢ ‖c • f.ofLp‖₊ ≤ ‖c‖₊ * ‖f.ofLp‖₊
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal ≤ ∑ i, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal

Tactic:
]

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal ≤ ∑ i, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
hp : Fact (1 ≤ ∞)
f : PiLp ∞ β
⊢ ‖c‖₊ * ‖f.ofLp‖₊ = ‖c‖₊ * ‖f.ofLp‖₊

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal = ∑ i, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal

Tactic:
]

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal = ∑ i, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a r : ℝ
⊢ ofReal (r + r) = ofReal (r + r)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inl
a : ℝ
⊢ ∞ = ∞

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inr
a : ℝ
r : ℝ≥0
⊢ ↑r + ↑r = ↑r + ↑r

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a b : ℝ
⊢ ofReal |b - a| = ofReal |b - a|

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a : ℝ
⊢ volume (Ioi a) = ∞

Tactic:
]

Goal state after:
a : ℝ
⊢ volume (Ioi a) = ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a : ℝ
⊢ volume (Iio a) = ∞

Tactic:
]

Goal state after:
a : ℝ
⊢ volume (Iio a) = ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ volume (Icc (sInf s) (sSup s))

Tactic:
]

Goal state after:
case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ volume (Icc (sInf s) (sSup s))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ ∞

Tactic:
]

Goal state after:
case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume (Ioo l u)

Tactic:
]

Goal state after:
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x | p x}
⊢ 0 < volume (Ioo l u)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ∏ i, volume (Icc (a i) (b i)) = ∏ i, ofReal (b i - a i)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ∏ i, volume (Icc (a i) (b i)) = ∏ i, ofReal (b i - a i)
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
⊢ ⇑K ⁻¹' Icc 0 1 = Icc 0 1

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
⊢ ⇑K ⁻¹' Icc 0 1 = Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
this : Icc 0 1 = ⇑K '' Icc 0 1
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) ∘ ⇑K '' Icc 0 1

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a ↦ ℝ) e
this : Icc 0 1 = ⇑K '' Icc 0 1
⊢ (fun t ↦ ∑ i, t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t ↦ ∑ i, t i • v i) ∘ ⇑K '' Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * volume s

Tactic:
]

Goal state after:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * volume s
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring 𝕜
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (α i)
inst✝ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
e : (i : ι) → α i ≃ₗᵢ[𝕜] β i
x : (i : ι) → α i
hp : 1 ≤ p.toReal
⊢ ‖toLp p ((LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) x)‖ = ‖toLp p x‖

Tactic:
· have : 0 < p.toReal := zero_lt_one.trans_le <| by norm_cast
      simp only [PiLp.norm_eq_sum this, LinearEquiv.piCongrRight_apply,
        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.norm_map, one_div]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal |∏ i, D i| * volume (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi s) = ∏ x, volume (s x)

pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable ⇑(toLin' (Matrix.diagonal D))

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal |∏ i, D i| * volume (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi s) = ∏ x, volume (s x)

ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Measurable ⇑(toLin' (Matrix.diagonal D))
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ Convex ℝ (∑ i, segment ℝ 0 (v i))

Tactic:
]

Goal state after:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ Convex ℝ (∑ i, segment ℝ 0 (v i))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
i : ι
A : D i ≠ 0
⊢ ofReal (|D i| * |(D i)⁻¹|) * volume (s i) = volume (s i)

Tactic:
← abs_mul,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
i : ι
A : D i ≠ 0
⊢ ofReal |D i * (D i)⁻¹| * volume (s i) = volume (s i)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
i : ι
A : D i ≠ 0
⊢ volume (s i) = volume (s i)

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ ∏ x, ofReal |D x| * volume ((fun x_1 ↦ D x * x_1) ⁻¹' s x) = ∏ x, volume (s x)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ ∏ x, ofReal |D x| * volume ((fun x_1 ↦ D x * x_1) ⁻¹' s x) = ∏ x, volume (s x)
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mp.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : a i ≤ 0
⊢ a i ≤ t i * a i ∧ t i * a i ≤ 0

Tactic:
]

Goal state after:
case mp.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : a i ≤ 0
⊢ a i ≤ t i * a i ∧ t i * a i ≤ 0
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mp.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : 0 ≤ a i
⊢ 0 ≤ t i * a i ∧ t i * a i ≤ a i

Tactic:
]

Goal state after:
case mp.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : 0 ≤ a i
⊢ 0 ≤ t i * a i ∧ t i * a i ≤ a i
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂Measure.pi fun x ↦ volume) =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i ↦ volume

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂Measure.pi fun x ↦ volume) =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i ↦ volume
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_1.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : a i ≤ x i ∧ x i ≤ 0
hai : a i ≤ 0
⊢ 0 ≤ (fun i ↦ x i / a i) i ∧ (fun i ↦ x i / a i) i ≤ 1

Tactic:
]

Goal state after:
case mpr.refine_1.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : a i ≤ x i ∧ x i ≤ 0
hai : a i ≤ 0
⊢ 0 ≤ (fun i ↦ x i / a i) i ∧ (fun i ↦ x i / a i) i ≤ 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_1.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ≤ x i ∧ x i ≤ a i
hai : 0 ≤ a i
⊢ 0 ≤ (fun i ↦ x i / a i) i ∧ (fun i ↦ x i / a i) i ≤ 1

Tactic:
]

Goal state after:
case mpr.refine_1.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ≤ x i ∧ x i ≤ a i
hai : 0 ≤ a i
⊢ 0 ≤ (fun i ↦ x i / a i) i ∧ (fun i ↦ x i / a i) i ≤ 1
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case top.refine_1.inl
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ∞)
⊢ ‖b‖₊ ≤ ‖b‖₊

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_2.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 = x i
hai : a i = 0
⊢ x i = x i / a i * a i

Tactic:
]

Goal state after:
case mpr.refine_2.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 = x i
hai : a i = 0
⊢ x i = x i / a i * a i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_2.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 = x i
hai : a i = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case top.refine_2
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ∞)
n : ℝ≥0
hn : n < ‖b‖₊
⊢ ‖b‖₊ = ‖b‖₊

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mpr.refine_2.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i ≠ 0
⊢ x i = x i

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
⊢ (univ.pi fun i ↦ interior (Icc (0 i) (1 i))).Nonempty

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
⊢ (univ.pi fun i ↦ interior (Icc (0 i) (1 i))).Nonempty