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

Goal state before:
pp: case refine_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
⊢ affineSpan ℝ (range fun p ↦ (lineMap q ↑p) ↑(w p)) = ⊤

Tactic:
·

Goal state after:
case refine_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
⊢ affineSpan ℝ (range fun p ↦ (lineMap q ↑p) ↑(w p)) = ⊤
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

pp: case h.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
·

Goal state after:
case h.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₁
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
·

Goal state after:
case h.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ Ioi 1 ×ˢ univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))

pp: case refine_2
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x ↦ ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ Ioi 1 ×ˢ univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding fun x ↦ x * g
⊢ ∫ (y : G), f y ∂map (fun x ↦ x * g) μ = ∫ (x : G), f x ∂μ

Tactic:
map_mul_right_eq_self

Goal state after:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding fun x ↦ x * g
⊢ ∫ (y : G), f y ∂μ = ∫ (x : G), f x ∂μ
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x ↦ ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x ↦ ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h₁
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₁ ∈ line[k, p₂, p]

pp: case h₂
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₃ ∈ line[k, p₂, p]

Tactic:
·

Goal state after:
case h₁
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₁ ∈ line[k, p₂, p]
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h₂
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₃ ∈ line[k, p₂, p]

Tactic:
·

Goal state after:
case h₂
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₃ ∈ line[k, p₂, p]
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
·

Goal state after:
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : ↑s = ∅
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1

pp: case pos.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1

Tactic:
·

Goal state after:
case pos.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : ↑s = ∅
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1

Tactic:
·

Goal state after:
case pos.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ ENNReal.toReal 0
⊢ Memℓp f 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ ∞.toReal
⊢ Memℓp f ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ p.toReal
hp : 0 < p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ ENNReal.toReal 0
⊢ Memℓp f 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ ∞.toReal
⊢ Memℓp f ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ p.toReal
hp : 0 < p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ ∞.toReal
⊢ Memℓp f ∞
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case h.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ ∀ (i : α), 0 ≤ ‖f i‖ ^ p.toReal

pp: case h.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ IsLUB (Set.range fun s ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal) (⨆ s, ∑ i ∈ s, ‖f i‖ ^ p.toReal)

Tactic:
·

Goal state after:
case h.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ ∀ (i : α), 0 ≤ ‖f i‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f ∞
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
⊢ Memℓp f p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp 0 p

Tactic:
·

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp 0 p

Tactic:
·

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 ∞
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp 0 p

Tactic:
·

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp 0 p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (fun x ↦ ‖f x‖) 0 ↔ Memℓp f 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (fun x ↦ ‖f x‖) ∞ ↔ Memℓp f ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
⊢ Memℓp (fun x ↦ ‖f x‖) p ↔ Memℓp f p

Tactic:
·

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (fun x ↦ ‖f x‖) 0 ↔ Memℓp f 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (fun x ↦ ‖f x‖) ∞ ↔ Memℓp f ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
⊢ Memℓp (fun x ↦ ‖f x‖) p ↔ Memℓp f p

Tactic:
·

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (fun x ↦ ‖f x‖) ∞ ↔ Memℓp f ∞
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
⊢ Memℓp (fun x ↦ ‖f x‖) p ↔ Memℓp f p

Tactic:
·

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
⊢ Memℓp (fun x ↦ ‖f x‖) p ↔ Memℓp f p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp g 0
⊢ Memℓp f 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp g ∞
⊢ Memℓp f ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp g 0
⊢ Memℓp f 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp g ∞
⊢ Memℓp f ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp g ∞
⊢ Memℓp f ∞
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
⊢ Memℓp f p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f 0
⊢ Memℓp (-f) 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f ∞
⊢ Memℓp (-f) ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
hp : 0 < p.toReal
⊢ Memℓp (-f) p

Tactic:
·

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f 0
⊢ Memℓp (-f) 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f ∞
⊢ Memℓp (-f) ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
hp : 0 < p.toReal
⊢ Memℓp (-f) p

Tactic:
·

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f ∞
⊢ Memℓp (-f) ∞
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
hp : 0 < p.toReal
⊢ Memℓp (-f) p

Tactic:
·

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
hp : 0 < p.toReal
⊢ Memℓp (-f) p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ 0
⊢ Memℓp f 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ∞
⊢ Memℓp f ∞

pp: case inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ Memℓp f p

pp: case inr.inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f ∞
hpq : ∞ ≤ ∞
⊢ Memℓp f ∞

pp: case inr.inr.inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ∞
⊢ Memℓp f ∞

pp: case inr.inr.inr.inr.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ 0
⊢ Memℓp f 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ∞
⊢ Memℓp f ∞

pp: case inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ Memℓp f p

pp: case inr.inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f ∞
hpq : ∞ ≤ ∞
⊢ Memℓp f ∞

pp: case inr.inr.inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ∞
⊢ Memℓp f ∞

pp: case inr.inr.inr.inr.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
⊢ Memℓp f p

Tactic:
·

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ∞
⊢ Memℓp f ∞
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case pos
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ∞
C : ℝ
hC : C ∈ upperBounds ((fun i ↦ ‖f i‖) '' {i | f i ≠ 0})
i : α
hi : f i = 0
⊢ (fun i ↦ ‖f i‖) i ≤ max 0 C

pp: case neg
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ∞
C : ℝ
hC : C ∈ upperBounds ((fun i ↦ ‖f i‖) '' {i | f i ≠ 0})
i : α
hi : ¬f i = 0
⊢ (fun i ↦ ‖f i‖) i ≤ max 0 C

Tactic:
·

Goal state after:
case pos
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ∞
C : ℝ
hC : C ∈ upperBounds ((fun i ↦ ‖f i‖) '' {i | f i ≠ 0})
i : α
hi : f i = 0
⊢ (fun i ↦ ‖f i‖) i ≤ max 0 C