mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
x✝ : H
⊢ (↑↑e * ↑↑e.symm) x✝ = 1 x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
x✝ : H
⊢ (↑↑e.symm * ↑↑e) x✝ = 1 x✝

Tactic:
simp

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)
⊢ -(s.points i -ᵥ s.centroid) = -1 • (s.points i -ᵥ s.centroid)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
m : Type u_5
n : Type u_6
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : FiniteDimensional 𝕜 E
v₁ : OrthonormalBasis n 𝕜 E
e : n ≃ m
f : E →ₗ[𝕜] E
i j : m
⊢ ((v₁.reindex e).repr (f ((v₁.reindex e) j))).ofLp i = (v₁.repr (f (v₁ (e.symm j)))).ofLp (e.symm i)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
have : range b = univ :=
      AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
    simp [this]

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

Goal state before:
pp: case e'_2
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
s : AffineSubspace k P
inst✝ : FiniteDimensional k ↥s.direction
p : P
hs : s = ⊥
x✝ : V
⊢ vectorSpan k (insert p ∅) = ⊥

Tactic:
simp

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

Goal state before:
pp: case e'_4
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
s : AffineSubspace k P
inst✝ : FiniteDimensional k ↥s.direction
p : P
hs : s = ⊥
e_2✝ : ↥(vectorSpan k (insert p ∅)) = ↥⊥
⊢ vectorSpan k (insert p ∅) = ⊥

Tactic:
simp

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

Goal state before:
pp: case e'_5.e'_6
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
s : AffineSubspace k P
inst✝ : FiniteDimensional k ↥s.direction
p : P
hs : s = ⊥
e_2✝ : ↥(vectorSpan k (insert p ∅)) = ↥⊥
e_4✝ : (vectorSpan k (insert p ∅)).addCommGroup ≍ ⊥.addCommGroup
e_3✝ : inst✝⁴.toSemiring = DivisionRing.toDivisionSemiring.toSemiring
e_5✝ : inst✝² ≍ inst✝²
⊢ vectorSpan k (insert p ∅) = ⊥

Tactic:
simp

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

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
⊢ Module.rank k ↥⊥ ≤ 1

Tactic:
simp

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

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
p : P
⊢ Module.rank k ↥⊥ ≤ 1

Tactic:
simp

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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint {i} {j}
⊢ Disjoint (k ∙ u i) (k ∙ u j)

Tactic:
simp_rw [← Set.image_singleton, hi.disjoint_span_image h_ij]

Goal state after:
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
s : Set P
p₀ : P
h : p₀ ∈ s
v₀ : V
hv : ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v
p : P
hp : p ∈ s
r : k
hr : r • v₀ = p -ᵥ p₀
⊢ p -ᵥ p₀ = r • v₀

Tactic:
exact hr.symm

Goal state after:
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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
⊢ w ∈ vectorSpan k s → ∃ r, r • v = w

Tactic:
hw

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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
⊢ ∃ r, r • v = w
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
⊢ s.medial.points 0 ∈ Set.range s.medial.points

Tactic:
simp

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
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
⊢ Set.range (s.faceOpposite 0).points ⊆ Set.range s.points

Tactic:
simp

Goal state after:
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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
r : k
hp : r • v +ᵥ p₀ ∈ s
⊢ r • v = (r • v +ᵥ p₀) -ᵥ p₀

Tactic:
simp

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

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
p₁ p₂ : P
⊢ Collinear k {p₁, p₂}

Tactic:
collinear_iff_exists_forall_eq_smul_vadd

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
p₁ p₂ : P
⊢ ∃ p₀ v, ∀ p ∈ {p₁, p₂}, ∃ r, p = r • v +ᵥ p₀
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}

Tactic:
affineIndependent_iff_not_collinear,

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
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ ¬Collinear k (Set.range p) ↔ ¬Collinear k {p i₁, p i₂, p i₃}
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
f : ContDiffBump 0
x : E
⊢ ↑f (-x) = ↑f x

Tactic:
simp_rw [← zero_sub, f.sub, zero_add]

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁴ : MeasurableSpace G
inst✝³ : NormedAddCommGroup F
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
⊢ s⁻¹ = ⇑(MeasurableEquiv.inv G) ⁻¹' s

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁴ : MeasurableSpace G
inst✝³ : NormedAddCommGroup F
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) s⁻¹ μ

Tactic:
apply (integrable_map_equiv (MeasurableEquiv.inv G) f).mp
  have : s⁻¹ = MeasurableEquiv.inv G ⁻¹' s := by simp
  rw [this, ← MeasurableEquiv.restrict_map]
  simpa using! hf

Goal state after:
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
⊢ ∫ (x : G), f (x / g) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
by
  simp_rw [div_eq_mul_inv, integral_mul_right_eq_self f g⁻¹]

Goal state after:
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₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₄} ⊆ {p₄, p₅}

Tactic:
simp

Goal state after:
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₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₃} ⊆ {p₃, p₄}

Tactic:
simp

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

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
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₂ ∈ {p₁, p₂, p}

Tactic:
simp

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

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
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 ∈ {p₁, p₂, p}

Tactic:
simp

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

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
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₁ ∈ {p₁, p₂, p}

Tactic:
simp

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

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
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₂ ∈ {p₂, p₃, p}

Tactic:
simp

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

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
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 ∈ {p₂, p₃, p}

Tactic:
simp

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

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
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₃ ∈ {p₂, p₃, p}

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_2
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 = ⊥
x✝ : V
⊢ ⊥ = vectorSpan k (insert p ∅)

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_4.e'_6
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 = ⊥
e_2✝ : ↥⊥ = ↥(vectorSpan k (insert p ∅))
e_3✝ : DivisionRing.toDivisionSemiring.toSemiring = inst✝³.toSemiring
e_5✝ : inst✝¹ ≍ inst✝¹
⊢ ⊥ = vectorSpan k (insert p ∅)

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_5.e'_6
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 = ⊥
e_2✝ : ↥⊥ = ↥(vectorSpan k (insert p ∅))
e_4✝ : ⊥.addCommMonoid ≍ (vectorSpan k (insert p ∅)).addCommMonoid
e_3✝ : DivisionRing.toDivisionSemiring.toSemiring = inst✝³.toSemiring
e_5✝ : inst✝¹ ≍ inst✝¹
⊢ ⊥ = vectorSpan k (insert p ∅)

Tactic:
simp

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

Goal state before:
pp: α : 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
H : Summable fun x ↦ 1
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ ∞.toReal
H : Summable fun x ↦ 1
⊢ 0 < 1

Tactic:
simp

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)
⊢ {i | 0 i ≠ 0}.Finite

Tactic:
simp

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

Goal state before:
pp: α : 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
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a ↦ ∑ i ∈ s, f i a) p
⊢ (∀ i_1 ∈ insert i s, Memℓp (f i_1) p) → Memℓp (fun a ↦ ∑ i ∈ insert i s, f i a) p

Tactic:
hf

Goal state after:
case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a ↦ ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (f i_1) p
⊢ Memℓp (fun a ↦ ∑ i ∈ insert i s, f i a) p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ 1 = ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ f = 0 → ‖f‖ = 0

Tactic:
by rintro rfl; exact norm_zero

Goal state after:
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 : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0

Tactic:
hasSum_zero_iff_of_nonneg this

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i ↦ ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0
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
x✝ : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x✝, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x✝) l)
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x✝)
this✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝ :
  TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) 0 (l ×ˢ l) (𝓝 x✝) ∧
    TendstoUniformlyOnFilter (fun n x ↦ f n.1 x✝ - f n.2 x✝) 0 (l ×ˢ l) (𝓝 x✝)
this :
  TendstoUniformlyOnFilter ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) 0
    (l ×ˢ l) (𝓝 x✝)
x : (ι × ι) × E
⊢ ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) x.1 x.2 =
    -f x.1.1 x.2 + f x.1.2 x.2

Tactic:
simp

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
x✝ : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x✝, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x✝) l)
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x✝)
this✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝ :
  TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) 0 (l ×ˢ l) (𝓝 x✝) ∧
    TendstoUniformlyOnFilter (fun n x ↦ f n.1 x✝ - f n.2 x✝) 0 (l ×ˢ l) (𝓝 x✝)
this :
  TendstoUniformlyOnFilter ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) 0
    (l ×ˢ l) (𝓝 x✝)
x : (ι × ι) × E
⊢ f x.1.1 x✝ - f x.1.2 x✝ - (f x.1.1 x.2 - f x.1.2 x.2) + (f x.1.2 x✝ - f x.1.1 x✝) = -f x.1.1 x.2 + f x.1.2 x.2
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: case zero
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
hk : ↑0 ≤ N
x : E
⊢ iteratedFDeriv 𝕜 0 (fun y ↦ ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 0 (f n) x

Tactic:
simp_rw [iteratedFDeriv_zero_eq_comp]

Goal state after:
case zero
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
hk : ↑0 ≤ N
x : E
⊢ (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ fun y ↦ ∑' (n : α), f n y) x =
    ∑' (n : α), (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f n) x
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖‖↑f a‖‖

Tactic:
by simpa using f.2.summable

Goal state after:
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)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
f g : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖↑f a‖

Tactic:
by simpa using f.2.summable

Goal state after:
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)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖↑f a‖

Tactic:
by simpa using f.2.summable

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

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp : p ≠ 0
f : ↥(lp E p)
⊢ ‖0 • f‖ = ‖0‖ * ‖f‖

Tactic:
simp

Goal state after:
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)
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ {i_1 | Pi.single i a i_1 ≠ 0} ⊆ {i}

Tactic:
intro j

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p✝ q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
j : α
⊢ j ∈ {i_1 | Pi.single i a i_1 ≠ 0} → j ∈ {i}
Module: Mathlib.Analysis.SpecialFunctions.Sqrt

Goal state before:
pp: case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x ↦ √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x ↦ √x) x

Tactic:
rw [sqrt_eq_zero_of_nonpos hx.le, mul_zero, div_zero]

Goal state after:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x ↦ √x) 0 x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x ↦ √x) x
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ∀ (b' : α), b' ≠ i → ‖↑(lp.single (↑p) i x) b'‖ ^ (↑p).toReal = 0

Tactic:
intro j

Goal state after:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
j : α
⊢ j ≠ i → ‖↑(lp.single (↑p) i x) j‖ ^ (↑p).toReal = 0