mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
⊢ (f.leftMulMapPreGNS (x✝¹ + x✝)).completion = (f.leftMulMapPreGNS x✝¹).completion + (f.leftMulMapPreGNS x✝).completion

Tactic:
ext c

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
c : Completion f.PreGNS
⊢ (f.leftMulMapPreGNS (x✝¹ + x✝)).completion c =
    ((f.leftMulMapPreGNS x✝¹).completion + (f.leftMulMapPreGNS x✝).completion) c
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
⊢ (f.leftMulMapPreGNS (x✝¹ * x✝)).completion = (f.leftMulMapPreGNS x✝¹).completion * (f.leftMulMapPreGNS x✝).completion

Tactic:
ext c

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
c : Completion f.PreGNS
⊢ (f.leftMulMapPreGNS (x✝¹ * x✝)).completion c =
    ((f.leftMulMapPreGNS x✝¹).completion * (f.leftMulMapPreGNS x✝).completion) c
Module: Mathlib.Analysis.CStarAlgebra.Projection

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
⊢ [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE

Tactic:
tfae_have 1 → 2 := fun h ↦ (hq.mul_right_and_mul_left_of_nonneg_of_le hp.nonneg h).2

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p q : A
hp : IsStarProjection p
hq : IsStarProjection q
tfae_1_to_2 : p ≤ q → q * p = p
⊢ [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case refine_2
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
⊢ ‖v‖ ≤ ‖toEuclideanCLM (diagonal v)‖

Tactic:
refine (pi_norm_le_iff_of_nonneg (norm_nonneg T)).mpr fun i ↦ ?_

Goal state after:
case refine_2
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖v i‖ ≤ ‖T‖
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x x' : X
x✝ : f x = f x'
⊢ (x ≠ x' → ∃ s₁ s₂, IsOpen[inst✝] s₁ ∧ IsOpen[inst✝] s₂ ∧ x ∈ s₁ ∧ x' ∈ s₂ ∧ Disjoint s₁ s₂) ↔
    x ≠ x' → Disjoint (𝓝 x) (𝓝 x')

Tactic:
simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens x'),
    ← exists_and_left, and_assoc, and_comm, and_left_comm]

Goal state after:
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℤ
hn : IsUnit ↑n
x✝ : 𝕜
⊢ ∀ ⦃a₂ : 𝕜⦄, n • x✝ = n • a₂ → x✝ = a₂

Tactic:
zsmul_eq_mul

Goal state after:
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℤ
hn : IsUnit ↑n
x✝ : 𝕜
⊢ ∀ ⦃a₂ : 𝕜⦄, ↑n * x✝ = ↑n * a₂ → x✝ = a₂
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : z ^ n ∈ centeredArc s
hs0 : 0 < s
hn0 : n ≠ 0
⊢ 1 ≤ ↑n

Tactic:
simpa [Nat.one_le_iff_ne_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
a : ↑unitInterval
⊢ (x.path y) a = exp ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) a)

Tactic:
by
  simp [path]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ x.angleDiff y + (↑x).arg - (↑x).arg < 2 * π

Tactic:
simp [angleDiff_lt_two_pi]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hxy : x ≠ y
⊢ {x, y} ⊆ range ⇑(y.path x)

Tactic:
simp only [pair_subset_iff,
      (path y x).source_mem_range, (path y x).target_mem_range, and_self]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H
T : ℝ
y : AddCircle T
z✝ : ℝ
⊢ (↑z✝ + y).toCircle = toCircle ↑z✝ * y.toCircle

Tactic:
induction y using QuotientAddGroup.induction_on

Goal state after:
case H.H
T z✝¹ z✝ : ℝ
⊢ (↑z✝¹ + ↑z✝).toCircle = toCircle ↑z✝¹ * toCircle ↑z✝
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H.H
T z✝¹ z✝ : ℝ
⊢ (↑z✝¹ + ↑z✝).toCircle = toCircle ↑z✝¹ * toCircle ↑z✝

Tactic:
simp_rw [← coe_add, toCircle_apply_mk, mul_add, Circle.exp_add]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ∃ k, k • T = -z✝¹ + z✝

Tactic:
zsmul_eq_mul

Goal state after:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ∃ k, ↑k * T = -z✝¹ + z✝
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
y : ℝ
hy : y ∈ spectrum ℝ ↑x
⊢ (cexp (↑y * I)).arg = y

Tactic:
replace hy : ‖y‖ < π := spectrum.norm_le_norm_of_mem hy |>.trans_lt hx

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
y : ℝ
hy : ‖y‖ < π
⊢ (cexp (↑y * I)).arg = y
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : x ≠ 0
u₁ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯
⊢ x = ‖x‖ • (↑(ℜ ↑u₁) + I • ↑(ℜ ↑u₂))

Tactic:
simpa only [u₁, u₂, selfAdjoint.realPart_unitarySelfAddISMul, realPart_add_I_smul_imaginaryPart]
    using! Eq.symm <| NormedSpace.norm_smul_normalize x

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
this : -1 < Real.cos ‖↑x‖
⊢ 2 * (1 - Real.cos ‖x‖) < 2 ^ 2

Tactic:
simp only [AddSubgroupClass.coe_norm, mul_sub, mul_one, sq, gt_iff_lt]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
this : -1 < Real.cos ‖↑x‖
⊢ 2 - 2 * Real.cos ‖↑x‖ < 2 * 2
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ Function.Injective (⇑(adjoint T) ∘ ⇑T) ↔ Function.Injective ⇑T

Tactic:
← coe_comp,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ Function.Injective ⇑(adjoint T ∘SL T) ↔ Function.Injective ⇑T
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: 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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
⊢ (Finset.centroid k univ fun i ↦ s.points i -ᵥ p) = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ p)

Tactic:
centroid_def,

Goal state after:
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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
⊢ (affineCombination k univ fun i ↦ s.points i -ᵥ p) (centroidWeights k univ) = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ p)
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ Function.Injective (⇑(adjoint A) ∘ ⇑A) ↔ Function.Injective ⇑A

Tactic:
← coe_comp,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ Function.Injective ⇑(adjoint A ∘ₗ A) ↔ Function.Injective ⇑A
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case e'_3
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
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ↑fs = ⇑(fs.orderEmbOfFin h).toEmbedding '' Set.univ

Tactic:
Set.image_univ

Goal state after:
case e'_3
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
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ↑fs = Set.range ⇑(fs.orderEmbOfFin h).toEmbedding
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: 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
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face ⋯
⊢ Finset.centroid k {i}ᶜ s.points = (affineCombination k {i}ᶜ s.points) fun x ↦ (↑n)⁻¹

Tactic:
centroid_def,

Goal state after:
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
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face ⋯
⊢ (affineCombination k {i}ᶜ s.points) (centroidWeights k {i}ᶜ) = (affineCombination k {i}ᶜ s.points) fun x ↦ (↑n)⁻¹
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ im ⟪x, (adjoint T) (T x)⟫_𝕜 = 0

Tactic:
simp only [adjoint_inner_right, inner_self_eq_norm_sq_to_K]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ im (↑‖T x‖ ^ 2) = 0
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
S T : E →ₗ[𝕜] E
hS : IsStarProjection S
hT : IsStarProjection T
⊢ S = T ↔ S.range = T.range

Tactic:
have := FiniteDimensional.complete 𝕜 E
  simpa using ContinuousLinearMap.IsStarProjection.ext_iff
    (S.isStarProjection_toContinuousLinearMap_iff.mpr hS)
    (T.isStarProjection_toContinuousLinearMap_iff.mpr hT)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: 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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ↑n • (s.faceOppositeCentroid i -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i)

Tactic:
by
  simp [faceOppositeCentroid_eq_sum_vsub_vadd, smul_smul, mul_inv_cancel₀ (NeZero.ne (n : k)),
    one_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁷ : DivisionRing k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
V₂ : Type u_5
P₂ : Type u_6
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₂ P₂
s : AffineSubspace k P
inst✝ : FiniteDimensional k ↥s.direction
f : P →ᵃ[k] P₂
⊢ FiniteDimensional k ↥(map f s).direction

Tactic:
by
  rw [map_direction]
  infer_instance

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

Goal state before:
pp: case neg.inl
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : (starRingEnd 𝕜) y * y = 1
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

pp: case neg.inr
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : ↑↑g = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
· exact ⟨⟨y, by simp [Unitary.mem_iff, this, mul_comm y]⟩, fun x ↦ congr($hfg x)⟩

Goal state after:
case neg.inr
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : ↑↑g = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inr.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hs : AffineIndependent k Subtype.val
hs' : s.Nonempty
hst : affineSpan k ↑s < affineSpan k ↑∅
⊢ #s < #∅

Tactic:
simp at hst

Goal state after:
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:
· exact hfq

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 ∞

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

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 ∞

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 ∞

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
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
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:
· exact hfq

Goal state after:
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 ∞

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
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hLHS : HasSum (fun i ↦ ‖↑(c • f) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal

Tactic:
have hRHS := (lp.hasSum_norm hp f).mul_left (‖c‖ ^ p.toReal)

Goal state after:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hLHS : HasSum (fun i ↦ ‖↑(c • f) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
hRHS : HasSum (fun i ↦ ‖c‖ ^ p.toReal * ‖↑f i‖ ^ p.toReal) (‖c‖ ^ p.toReal * ‖f‖ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst✝³ : (i : I) → NonUnitalNormedRing (B i)
inst✝² : (i : I) → StarRing (B i)
inst✝¹ : ∀ (i : I), NormedStarGroup (B i)
inst✝ : ∀ (i : I), CStarRing (B i)
f : ↥(lp B ∞)
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖

Tactic:
rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _)]
    refine lp.norm_le_of_forall_le ‖star f * f‖.sqrt_nonneg fun i => ?_
    rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
    exact lp.norm_apply_le_norm ENNReal.top_ne_zero (star f * f) i

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

Goal state before:
pp: α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x ↦ g x i
a₀ : α
hga₀b : Memℓp (g a₀) ∞
a : α
⊢ Memℓp (g a) ∞

Tactic:
rcases hga₀b with ⟨M, hM⟩

Goal state after:
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x ↦ g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i ↦ ‖g a₀ i‖)
⊢ Memℓp (g a) ∞
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
rw [Metric.isOpen_iff]

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ ∀ x ∈ t, ∃ ε > 0, Metric.ball x ε ⊆ t
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case neg
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∃ p ∈ s, ∃ x, g p x ≠ 0
this : LocallyCompactSpace G
⊢ ContinuousOn (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

Tactic:
rintro ⟨q₀, x₀⟩ ⟨hq₀, -⟩

Goal state after:
case neg
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∃ p ∈ s, ∃ x, g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
⊢ ContinuousWithinAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)