mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x✝ : Z
⊢ x✝ ∈ e.source ↔ x✝ ∈ Subtype.val ∘ proj ⁻¹' Subtype.val '' e.baseSet

Tactic:
simp [e.source_eq]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
⊢ Continuous[a.totalSpaceTopology, inst✝²] TotalSpace.proj

Tactic:
let := a.totalSpaceTopology
  let := a.toFiberBundle
  exact FiberBundle.continuous_proj F E

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsComplete (Set.range toProdMulOpposite)

Tactic:
apply IsClosed.isComplete

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
⊢ IsClosed (Set.range toProdMulOpposite)
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case inl
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ (e.source.piecewise (↑e) (↑e') p).1 = proj p

Tactic:
piecewise_eq_of_mem,

Goal state after:
case inl
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ (↑e p).1 = proj p

case inl.hi
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ p ∈ e.source
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e : E
U : Set E
hU : U ∈ 𝓝 e
hU' : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ ∃ U ∈ 𝓝 e, ∀ (g : Additive G), ((fun x ↦ g +ᵥ x) '' U ∩ U).Nonempty → g = 0

Tactic:
exact ⟨U, hU, fun g ↦ by simpa using hU' (Additive.ofMul.symm g)⟩

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

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
⊢ IsOpen[inst✝⁵] (f '' U)

Tactic:
rw [← hf.isOpen_preimage, preim_im]
    exact isOpen_iUnion fun g ↦ open_U.preimage (continuous_const_smul g)

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left✝ : DiscreteTopology ↑(f ⁻¹' {f e})
U : Set X
heU : f e ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × ↑(f ⁻¹' {f e})
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
g : G
⊢ ((fun x ↦ g • x) '' Subtype.val '' Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2} ∩
        Subtype.val '' Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}).Nonempty →
    g = 1

Tactic:
by
      rintro ⟨_, ⟨_, ⟨x, hx, rfl⟩, rfl⟩, y, hy, eq⟩
      have := h.2.2.2.1
      apply IsCancelSMul.right_cancel _ _ x.1
      simp_rw [← eq, one_smul]
      refine congr($(H.injective <| Prod.ext (Subtype.ext ?_) <| hy.trans hx.symm))
      simp_rw [hH]
      exact h.2.2.2.2.mpr ⟨_, eq.symm⟩

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
r : ℝ
a : A
hr : 0 < r
ha : IsStrictlyPositive a
⊢ log (r • a) = (algebraMap ℝ A) (Real.log r) + log a

Tactic:
by
  grind [log_smul]

Goal state after:
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
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝¹ : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝² : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝¹ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h : IsOpen[inst✝¹] s
⊢ f ⁻¹' s ∩ V' e = (φ e).source ∩ f ⁻¹' s ∩ V ↑e

Tactic:
V'

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝¹ : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝² : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝¹ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h : IsOpen[inst✝¹] s
⊢ f ⁻¹' s ∩ (V ↑e ∩ (φ e).source) = (φ e).source ∩ f ⁻¹' s ∩ V ↑e
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : ↥(selfAdjoint A)
ha_norm : ‖a‖ ≤ 1
⊢ star ↑(unitarySelfAddISMul a ha_norm) = ↑a - I • CFC.sqrt (1 - ↑a ^ 2)

Tactic:
by
  simp [IsSelfAdjoint.star_eq, ← sub_eq_add_neg, (CFC.sqrt_nonneg (1 - a ^ 2 : A)).isSelfAdjoint]

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

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

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:
· exact ⟨![1, -1, 1, -1], 0, by simp⟩

Goal state after:
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
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✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ adjoint U.orthogonalProjectionOnto = U.subtypeL

Tactic:
by
  rw [← U.adjoint_subtypeL, adjoint_adjoint]

Goal state after:
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
hb : BddBelow (Set.range fun w ↦ ‖y - ↑w‖)
⊢ (∀ (z : E), ‖y - A x‖ ≤ ‖y - A z‖) ↔ ‖y - A x‖ = ⨅ z, ‖y - ↑z‖

Tactic:
le_antisymm_iff,

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
hb : BddBelow (Set.range fun w ↦ ‖y - ↑w‖)
⊢ (∀ (z : E), ‖y - A x‖ ≤ ‖y - A z‖) ↔ ‖y - A x‖ ≤ ⨅ z, ‖y - ↑z‖ ∧ ⨅ z, ‖y - ↑z‖ ≤ ‖y - A x‖
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✝¹ ∈ (↑T).ker
⊢ x✝¹ ∈ (↑(adjoint T ∘SL T)).ker

Tactic:
simp_all

Goal state after:
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
⊢ ⟪(adjoint T) (T x✝¹), x✝¹⟫_𝕜 = 0

Tactic:
simp_all

Goal state after:
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 ↑(affineSpan k ↑s))).direction

Tactic:
rw [coe_eq_bot_iff] at hs
    rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan]
    convert! finiteDimensional_bot k V <;> 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
ι : 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
⊢ FiniteDimensional k ↥(affineSpan k (insert p s)).direction

Tactic:
have : FiniteDimensional k (vectorSpan k s) := (direction_affineSpan k s) ▸ inferInstance

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 ↥(affineSpan k (insert p s)).direction
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 : Set P
h : finrank k V = 2
this : FiniteDimensional k V
⊢ finrank k ↥(vectorSpan k s) ≤ finrank k V

Tactic:
exact Submodule.finrank_le _

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

Tactic:
apply memℓp_infty
    simpa using hf.bddAbove

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 : (i : α) → E i
hf : Memℓp f p
⊢ Memℓp (-f) p

Tactic:
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 inr.inl
α : Type u_3
E : α → Type u_4
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
f : (i : α) → E i
hf : Memℓp f ∞
⊢ Memℓp (star f) ∞

Tactic:
apply memℓp_infty
    simpa using hf.bddAbove

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✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
⊢ Memℓp (star f) p

Tactic:
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
i : α
x : E i
⊢ ‖lp.single p i x‖ = ‖x‖

Tactic:
by
  have : Nonempty α := ⟨i⟩
  induction p with
  | top =>
    simp only [norm_eq_ciSup, lp.coeFn_single]
    refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
    · obtain rfl | hij := Decidable.eq_or_ne i j
      · rw [Pi.single_eq_same]
      · rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]
        exact norm_nonneg _
    · rw [Pi.single_eq_same]
  | coe p =>
    have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
    rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]
    · exact norm_nonneg _
    · intro j hji
      rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: case pos
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
⊢ ball c r ⊆ (univBall c r).target

Tactic:
rw [univBall_target c hr]

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)
p q r : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
i : α
x : ↥(lp E p)
⊢ ‖(evalₗ E p i) x‖ ≤ 1 * ‖x‖

Tactic:
by
    have hp : p ≠ 0 := zero_lt_one.trans_le Fact.out |>.ne'
    simpa only [evalₗ_apply, one_mul, ge_iff_le] using norm_apply_le_norm hp x i

Goal state after:
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
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
⊢ ∃ q, 0 < q ∧ q * r < ε

Tactic:
simp_rw [mul_comm]

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
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
⊢ ∃ q, 0 < q ∧ r * q < ε
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case h₁
α : 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‖)
i : ι
⊢ |g a i - g a₀ i| ≤ ↑K * dist a a₀

Tactic:
exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ ↑m fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
induction m generalizing p with
  | zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
  | succ m ihm =>
    rw [show ((m + 1 : ℕ) : WithTop ℕ∞) = m + 1 from rfl]
    refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩
    convert! ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
    exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv

Goal state after:
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: case pos
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
⊢ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
hasFDerivAt_iff_tendsto,

Goal state after:
case pos
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
⊢ Tendsto (fun x' ↦ ‖x' - x₀‖⁻¹ * ‖∫ (a : α), F x' a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x' - x₀)‖) (𝓝 x₀)
    (𝓝 0)
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:
hasFDerivAt_iff_tendsto,

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 :
  Tendsto (fun x' ↦ ‖x' - (n, x).2‖⁻¹ * ‖f (n, x).1 x' - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (x' - (n, x).2)‖)
    (𝓝 (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 <
      ε