mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ IsOpen[inst✝³] (⇑g ∘ f ⁻¹' ⇑g '' U)

Tactic:
simpa [Set.preimage_comp]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
⊢ cfc exp a = exp ((cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })

Tactic:
simp_rw [← map_exp _ h, cfc_apply exp a ha]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
⊢ (cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict exp, continuous_toFun := ⋯ } =
    (cfcHom ha) (exp { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : cexp (↑t₁ * I - ↑t₂ * I) = 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1

Tactic:
← sub_mul,

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : cexp ((↑t₁ - ↑t₂) * I) = 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ Injective (⇑exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)))

Tactic:
refine (exp_injOn_Icc (a := x.val.arg) (b := angleDiff x y + x.val.arg)
    <| by simp [angleDiff_lt_two_pi]).injective_iff _ ?_ |>.mpr
    <| Path.segment_injective_of_ne <| by simp [angleDiff_pos hne |>.ne']

Goal state after:
x y : Circle
hne : x ≠ y
⊢ range ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) ⊆ Icc (↑x).arg (x.angleDiff y + (↑x).arg)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case succ
T : ℝ
x : AddCircle T
n : ℕ
ih : (n • x).toCircle = x.toCircle ^ n
⊢ ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)

Tactic:
succ_nsmul,

Goal state after:
case succ
T : ℝ
x : AddCircle T
n : ℕ
ih : (n • x).toCircle = x.toCircle ^ n
⊢ (n • x + x).toCircle = x.toCircle ^ (n + 1)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: case inr
A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type ?u.39) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type ?u.41) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
⊢ ∃ u c, x = ∑ i, c i • ↑(u i) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2

Tactic:
have := norm_smul_two_inv_smul_add_four_unitary x hx

Goal state after:
case inr
A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
this :
  have u₁ := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯;
  have u₂ := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯;
  x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))
⊢ ∃ u c, x = ∑ i, c i • ↑(u i) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 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
A : E →L[𝕜] F
y : F
x : E
⊢ y - A x ∈ (↑(adjoint A)).ker ↔ (adjoint A) (y - A x) = 0

Tactic:
LinearMap.mem_ker,

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
A : E →L[𝕜] F
y : F
x : E
⊢ ↑(adjoint A) (y - A x) = 0 ↔ (adjoint A) (y - A x) = 0
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
x✝¹ : E
x✝ : x✝¹ ∈ (↑(adjoint T ∘SL T)).ker
⊢ x✝¹ ∈ (↑T).ker

Tactic:
LinearMap.mem_ker,

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
x✝¹ : E
x✝ : x✝¹ ∈ (↑(adjoint T ∘SL T)).ker
⊢ ↑T x✝¹ = 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
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ T - star T * T = 0

Tactic:
ContinuousLinearMap.ext_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ ∀ (x : E), (T - star T * T) x = 0 x
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
p : P
⊢ FiniteDimensional k ↥(affineSpan k {p}).direction

Tactic:
direction_affineSpan

Goal state after:
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
p : P
⊢ FiniteDimensional k ↥(vectorSpan k {p})
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
p : P
⊢ FiniteDimensional k ↥(affineSpan k {p}).direction

Tactic:
rw [direction_affineSpan]
  infer_instance

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

Goal state before:
pp: 𝕜 : 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
⊢ (∀ (a : H →L[𝕜] H), a ∘SL ↑(↑g).symm = ((↑(↑g).symm ∘SL ↑↑f) ∘SL a) ∘SL ↑(↑f).symm) ↔ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
eq_comp_toContinuousLinearMap_symm,

Goal state after:
𝕜 : 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
⊢ (∀ (a : H →L[𝕜] H), (a ∘SL ↑(↑g).symm) ∘SL ↑↑f = (↑(↑g).symm ∘SL ↑↑f) ∘SL a) ↔ ∃ α, ∀ (x : H), f x = (α • g) x
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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

Tactic:
simpa [card_pos] using hst

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
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
hn : s.Nonempty
hd : (affineSpan k ↑(Finset.image p s)).direction ≤ sp.direction
⊢ (affineSpan k ↑(Finset.image p s)).direction = sp.direction

Tactic:
direction_affineSpan

Goal state after:
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
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
hn : s.Nonempty
hd : vectorSpan k ↑(Finset.image p s) ≤ sp.direction
⊢ vectorSpan k ↑(Finset.image p s) = sp.direction
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inl
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 = ⊥
⊢ FiniteDimensional k ↥(affineSpan k (insert p ∅)).direction

Tactic:
direction_affineSpan

Goal state after:
case inl
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 = ⊥
⊢ FiniteDimensional k ↥(vectorSpan k (insert p ∅))
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
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
p : P
this : FiniteDimensional k ↥(affineSpan k s).direction
⊢ FiniteDimensional k ↥(affineSpan k (insert p ↑(affineSpan k s))).direction

Tactic:
direction_affineSpan

Goal state after:
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 : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
p : P
this : FiniteDimensional k ↥(affineSpan k s).direction
⊢ FiniteDimensional k ↥(vectorSpan k (insert p ↑(affineSpan k s)))
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
s : Set P
inst✝ : FiniteDimensional k ↥(affineSpan k s).direction
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ FiniteDimensional k ↥(affineSpan k (insert p s)).direction

Tactic:
direction_affineSpan

Goal state after:
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 : Set P
inst✝ : FiniteDimensional k ↥(affineSpan k s).direction
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ FiniteDimensional k ↥(vectorSpan k (insert p s))
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
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = 0

Tactic:
simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_left_eq_self]

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✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
h : Integrable (fun t ↦ f (g / t)) μ
x✝ : G
⊢ x✝ = g / (g⁻¹ * x✝)⁻¹

Tactic:
simp_rw [div_inv_eq_mul, mul_inv_cancel_left]

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
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:
· apply Collinear.mem_affineSpan_of_mem_of_ne h (by simp) (by simp) (by simp) hne

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: 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
h : FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
| (affineSpan k ↑s).direction

Tactic:
direction_affineSpan

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
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
h : FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
| vectorSpan k ↑s
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 : (i : α) → E i
hf : Memℓp f p
⊢ Memℓp (-f) p

Tactic:
by
  rcases p.trichotomy with (rfl | rfl | hp)
  · apply memℓp_zero
    simp [hf.finite_dsupport]
  · apply memℓp_infty
    simpa using hf.bddAbove
  · apply memℓp_gen
    simpa using hf.summable hp

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
⊢ ((∀ 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:
ih

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
⊢ (∀ 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: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

Tactic:
simp [lp.norm_eq_ciSup]

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

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ ∞)
f g : ↥(lp E ∞)
h✝ : Nonempty α
i : α
⊢ (fun i ↦ ‖↑(f + g) i‖) i ≤ ‖f‖ + ‖g‖

Tactic:
refine le_trans ?_ (add_mem_upperBounds_add
            (lp.isLUB_norm f).1 (lp.isLUB_norm g).1 ⟨_, ⟨i, rfl⟩, _, ⟨i, rfl⟩, rfl⟩)

Goal state after:
case inl.inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ ∞)
f g : ↥(lp E ∞)
h✝ : Nonempty α
i : α
⊢ (fun i ↦ ‖↑(f + g) i‖) i ≤ (fun x1 x2 ↦ x1 + x2) ((fun i ↦ ‖↑f i‖) i) ((fun i ↦ ‖↑g i‖) i)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
⊢ Memℓp (star f) p

Tactic:
by
  rcases p.trichotomy with (rfl | rfl | hp)
  · apply memℓp_zero
    simp [hf.finite_dsupport]
  · apply memℓp_infty
    simpa using hf.bddAbove
  · apply memℓp_gen
    simpa using hf.summable hp

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)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
hF' : ∀ i ∈ s, F i = ‖↑f i‖ ^ p.toReal
this : HasSum F (∑ i ∈ s, F i)
⊢ HasSum (fun b ↦ ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)

Tactic:
Finset.sum_congr rfl hF'

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
hF' : ∀ i ∈ s, F i = ‖↑f i‖ ^ p.toReal
this : HasSum F (∑ x ∈ s, ‖↑f x‖ ^ p.toReal)
⊢ HasSum (fun b ↦ ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ⇑(IsometryEquiv.vaddConst c) '' (r • ball 0 1) = ball c r

Tactic:
smul_unitBall hr.ne',

Goal state after:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ⇑(IsometryEquiv.vaddConst c) '' ball 0 ‖r‖ = ball c r
Module: Mathlib.Analysis.Calculus.ContDiff.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x ↦ (f x).ofLp i) t y

Tactic:
← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffWithinAt_iff,

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ ContDiffWithinAt 𝕜 n (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) t y ↔
    ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x ↦ (f x).ofLp i) t y
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case refine_2
ι : 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this : HasFDerivAt (f (n, x).1) (f' (n, x).1 (n, x).2) (n, x).2
⊢ ∀ᶠ (y : E) in 𝓝 x,
    dist ((↑‖(n, y).2 - x‖)⁻¹ • (f (n, y).1 (n, y).2 - f (n, y).1 x - ((f' (n, y).1 x) (n, y).2 - (f' (n, y).1 x) x)))
        0 <
      ε

Tactic:
rw [hasFDerivAt_iff_tendsto, Metric.tendsto_nhds] at this

Goal state after:
case refine_2
ι : 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this :
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 (n, x).2,
      dist (‖x_1 - (n, x).2‖⁻¹ * ‖f (n, x).1 x_1 - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (x_1 - (n, x).2)‖) 0 < ε
⊢ ∀ᶠ (y : E) in 𝓝 x,
    dist ((↑‖(n, y).2 - x‖)⁻¹ • (f (n, y).1 (n, y).2 - f (n, y).1 x - ((f' (n, y).1 x) (n, y).2 - (f' (n, y).1 x) x)))
        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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
inst✝ : l.NeBot
hf' : TendstoUniformly f' g' l
hf : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x
hfg : ∀ (x : E), Tendsto (fun n ↦ f n x) l (𝓝 (g x))
x : E
⊢ HasFDerivAt g (g' x) x

Tactic:
have hf : ∀ n : ι, ∀ x : E, x ∈ Set.univ → HasFDerivAt (f n) (f' n x) x := by simp [hf]
  have hfg : ∀ x : E, x ∈ Set.univ → Tendsto (fun n => f n x) l (𝓝 (g x)) := by simp [hfg]
  have hf' : TendstoUniformlyOn f' g' l Set.univ := by rwa [tendstoUniformlyOn_univ]
  exact hasFDerivAt_of_tendstoUniformlyOn isOpen_univ hf' hf hfg (Set.mem_univ x)

Goal state after: