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

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
hp : Fact (1 ≤ ∞)
__spread✝⁻⁰ : WithLp ∞ (α × β) ≃ α := (WithLp.equiv ∞ (α × β)).trans (Equiv.prodUnique α β)
x y : WithLp ∞ (α × β)
⊢ edist x.fst y.fst = edist x y

pp: case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = edist x y

Tactic:
·

Goal state after:
case inr.inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
hp : Fact (1 ≤ ∞)
__spread✝⁻⁰ : WithLp ∞ (α × β) ≃ α := (WithLp.equiv ∞ (α × β)).trans (Equiv.prodUnique α β)
x y : WithLp ∞ (α × β)
⊢ edist x.fst y.fst = edist x y
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = edist x y

Tactic:
·

Goal state after:
case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = edist x y
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✝ : (i : ι) → SeminormedAddCommGroup (β i)
hp : Fact (1 ≤ ∞)
x y : PiLp ∞ β
⊢ dist x y = ‖-x + y‖

pp: case inr
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 ≤ p.toReal
⊢ dist x y = ‖-x + y‖

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
hp : Fact (1 ≤ ∞)
x y : PiLp ∞ β
⊢ dist x y = ‖-x + y‖
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✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
h : 1 ≤ p.toReal
⊢ dist x y = ‖-x + y‖

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✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp p β
h : 1 ≤ p.toReal
⊢ dist x y = ‖-x + y‖
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‖₊ ≤ ‖c‖₊ * ‖f‖₊

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
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

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‖₊ ≤ ‖c‖₊ * ‖f‖₊
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
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

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
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
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‖₊ = ‖c‖₊ * ‖f‖₊

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
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

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 : ι), NormSMulClass 𝕜 (β i)
c : 𝕜
hp : Fact (1 ≤ ∞)
f : PiLp ∞ β
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
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
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

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
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inl
a : ℝ
⊢ volume (eball a ∞) = 2 * ∞

pp: case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (eball a r) = 2 * r

Tactic:
·

Goal state after:
case inl
a : ℝ
⊢ volume (eball a ∞) = 2 * ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (eball a r) = 2 * r

Tactic:
·

Goal state after:
case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (eball a r) = 2 * r
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inl
a : ℝ
⊢ volume (closedEBall a ∞) = 2 * ∞

pp: case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (closedEBall a r) = 2 * r

Tactic:
·

Goal state after:
case inl
a : ℝ
⊢ volume (closedEBall a ∞) = 2 * ∞
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (closedEBall a r) = 2 * r

Tactic:
·

Goal state after:
case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (closedEBall a r) = 2 * r
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✝⁷ : Semiring 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → Module 𝕜 (α i)
inst✝³ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
hp : Fact (1 ≤ ∞)
__LinearEquiv✝ : (PiLp ∞ fun x ↦ E) ≃ₗ[𝕜] PiLp ∞ fun x ↦ E :=
  WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
    (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv ∞ 𝕜 (ι' → E)).symm)
x' : PiLp ∞ fun x ↦ E
⊢ ‖(WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv ∞ 𝕜 (ι' → E)).symm))
        x'‖ =
    ‖x'‖

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 : 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x ↦ E
h : 1 ≤ p.toReal
⊢ ‖(WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv p 𝕜 (ι' → E)).symm))
        x'‖ =
    ‖x'‖

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → Module 𝕜 (α i)
inst✝³ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
hp : Fact (1 ≤ ∞)
__LinearEquiv✝ : (PiLp ∞ fun x ↦ E) ≃ₗ[𝕜] PiLp ∞ fun x ↦ E :=
  WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
    (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv ∞ 𝕜 (ι' → E)).symm)
x' : PiLp ∞ fun x ↦ E
⊢ ‖(WithLp.linearEquiv ∞ 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv ∞ 𝕜 (ι' → E)).symm))
        x'‖ =
    ‖x'‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ ediam s

pp: case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ ediam s

Tactic:
·

Goal state after:
case pos
s : Set ℝ
hs : Bornology.IsBounded s
⊢ volume s ≤ ediam 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 : 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x ↦ E
h : 1 ≤ p.toReal
⊢ ‖(WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv p 𝕜 (ι' → E)).symm))
        x'‖ =
    ‖x'‖

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✝⁷ : Semiring 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → Module 𝕜 (α i)
inst✝³ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
ι' : Type u_5
inst✝² : Fintype ι'
E : Type u_6
inst✝¹ : SeminormedAddCommGroup E
inst✝ : Module 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x ↦ E
h : 1 ≤ p.toReal
⊢ ‖(WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x ↦ E) e ≪≫ₗ (WithLp.linearEquiv p 𝕜 (ι' → E)).symm))
        x'‖ =
    ‖x'‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

Tactic:
·

Goal state after:
case neg
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ volume s ≤ ediam s
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case refine_1
ι : 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
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ 0 ≤ x i

pp: case refine_2
ι : 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
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ x i ≤ 1

Tactic:
·

Goal state after:
case refine_1
ι : 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
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ 0 ≤ x i
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case refine_2
ι : 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
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ x i ≤ 1

Tactic:
·

Goal state after:
case refine_2
ι : 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
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (e.symm i)) ∧ ∀ (i : ι), x (e.symm i) ≤ 1
i : ι'
⊢ x i ≤ 1
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✝⁴ : 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 : Fact (1 ≤ ∞)
__LinearEquiv✝ : PiLp ∞ α ≃ₗ[𝕜] PiLp ∞ β :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → α i) ≪≫ₗ LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) ≪≫ₗ
    (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → β i)).symm
⊢ ‖toLp ∞ ((LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) x)‖ = ‖toLp ∞ x‖

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:
·

Goal state after:
case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
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 : Fact (1 ≤ ∞)
__LinearEquiv✝ : PiLp ∞ α ≃ₗ[𝕜] PiLp ∞ β :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → α i) ≪≫ₗ LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) ≪≫ₗ
    (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → β i)).symm
⊢ ‖toLp ∞ ((LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) x)‖ = ‖toLp ∞ x‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inl
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : a < 0
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x ↦ a * x) volume) (Ioo ↑p ↑q)

pp: case inr
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : 0 < a
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x ↦ a * x) volume) (Ioo ↑p ↑q)

Tactic:
·

Goal state after:
case inl
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : a < 0
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x ↦ a * x) volume) (Ioo ↑p ↑q)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inr
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : 0 < a
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x ↦ a * x) volume) (Ioo ↑p ↑q)

Tactic:
·

Goal state after:
case inr
a : ℝ
h✝ : a ≠ 0
p q : ℚ
h : 0 < a
⊢ volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x ↦ a * x) volume) (Ioo ↑p ↑q)
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
⊢ Icc 0 1 ⊆ F '' Icc 0 1

pp: case h₂
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
⊢ F '' Icc 0 1 ⊆ Icc 0 1

Tactic:
·

Goal state after:
case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
⊢ Icc 0 1 ⊆ F '' Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h₂
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
⊢ F '' Icc 0 1 ⊆ Icc 0 1

Tactic:
·

Goal state after:
case h₂
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := ⋯
⊢ F '' Icc 0 1 ⊆ Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ 1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

pp: case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
·

Goal state after:
case inl
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ 1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
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:
·

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✝⁴ : 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‖
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
·

Goal state after:
case inr
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x ↦ -1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case mp
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i, t i • v i) →
    ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a ↦ a • v i) '' Icc 0 1), ∑ i, g i = x✝

pp: case mpr
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a ↦ a • v i) '' Icc 0 1), ∑ i, g i = x✝) →
    ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i, t i • v i

Tactic:
·

Goal state after:
case mp
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i, t i • v i) →
    ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a ↦ a • v i) '' Icc 0 1), ∑ i, g i = x✝
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)
⊢ Measurable ⇑(toLin' (Matrix.diagonal D))

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)

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)
⊢ Measurable ⇑(toLin' (Matrix.diagonal D))
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 : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
hp : p ≠ ∞
⊢ ‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
        ((WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x)‖₊ =
    ‖(WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x‖₊

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✝⁹ : Semiring 𝕜
inst✝⁸ : (i : ι✝) → SeminormedAddCommGroup (α✝ i)
inst✝⁷ : (i : ι✝) → SeminormedAddCommGroup (β i)
inst✝⁶ : (i : ι✝) → Module 𝕜 (α✝ i)
inst✝⁵ : (i : ι✝) → Module 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : Fintype ι
inst✝² : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst✝¹ : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst✝ : (i : ι) → (k : κ i) → Module 𝕜 (α i k)
x : (i : Sigma κ) → (fun i ↦ α i.fst i.snd) i
hp : p ≠ ∞
⊢ ‖((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α i.fst i.snd) ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
            LinearEquiv.piCongrRight fun x ↦ (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j)).symm) ≪≫ₗ
          (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))).symm)
        ((WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x)‖₊ =
    ‖(WithLp.addEquiv p ((i : Sigma κ) → α i.fst i.snd)).invFun x‖₊