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

Goal state before:
pp: case const
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
⊢ Commute ((cfcHom ha) (ContinuousMap.const (↑(spectrum 𝕜 a)) r)) b

Tactic:
conv =>
      enter [1, 2]
      equals algebraMap 𝕜 _ r => rfl

Goal state after:
case const
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
r : 𝕜
⊢ Commute ((cfcHom ha) ((algebraMap 𝕜 C(↑(spectrum 𝕜 a), 𝕜)) r)) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ :
  (f, a) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f, a).2)
hs : IsCompact (quasispectrum ℝ≥0 a)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}
⊢ ContinuousOn (fun fa ↦ cfcₙ ((toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
        {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)} ∩
      Set.univ ×ˢ {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)})

Tactic:
conv in cfcₙ _ =>
    equals cfcₙ (toFun {k} (ofFun {k} (toFun {t | IsCompact t ∧ t ⊆ s} fa.1))) => rfl

Goal state after:
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ :
  (f, a) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f, a).2)
hs : IsCompact (quasispectrum ℝ≥0 a)
k : Set ℝ≥0
hks : id k ⊆ s
hka : k ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)
hk : IsCompact k
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}
⊢ ContinuousOn (fun fa ↦ cfcₙ ((toFun {k}) ((ofFun {k}) ((toFun {t | IsCompact t ∧ t ⊆ s}) fa.1))) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
        {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)} ∩
      Set.univ ×ˢ {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)})
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ cfcₙ (fun x ↦ ↑x.re) a = ↑(ℜ a)

Tactic:
conv_rhs => rw [realPart_apply_coe, ← cfcₙ_id' ℂ a, ← cfcₙ_star, ← cfcₙ_add .., ← cfcₙ_smul ..]
  refine cfcₙ_congr fun x hx ↦ ?_
  rw [Complex.re_eq_add_conj, ← smul_one_smul ℂ 2⁻¹]
  simp [div_eq_inv_mul]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
this : cfcₙ (fun z ↦ ↑z.re + I * ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ cfcₙ (fun x ↦ ↑x.im) a = ↑(ℑ a)

Tactic:
by
    rw [cfcₙ_add .., cfcₙ_const_mul .., cfcₙ_re_id a] at this
    simpa

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ star (f x)) a * cfc f a = cfc 1 a ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1

Tactic:
← cfc_mul ..,

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ star (f x) * f x) a = cfc 1 a ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
⊢ ↑a ∈ Icc 0 1 ∧ ↑b ∈ Icc 0 1

Tactic:
grind [inr_mem_Icc_iff_norm_le]

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
⊢ ‖U i j‖ ≤ 1

Tactic:
have diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1 := by
    simp only [mul_eq_one, Matrix.one_apply_eq, RCLike.one_re]

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1
⊢ ‖U i j‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i✝¹ i✝ : n
⊢ ‖U i✝¹ i✝‖ ≤ 1

Tactic:
exact entry_norm_bound_of_unitary hU _ _

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
z₀ : ↥s
hz₀ : z₀ ∈ Subtype.val ⁻¹' e.source
⊢ ↑(e.subtypeRestr hs) z₀ ∈ ↑e '' e.source

Tactic:
use z₀.val

Goal state after:
case h
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
z₀ : ↥s
hz₀ : z₀ ∈ Subtype.val ⁻¹' e.source
⊢ ↑z₀ ∈ e.source ∧ ↑e ↑z₀ = ↑(e.subtypeRestr hs) z₀
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝¹] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ f.toPartialEquiv.2 '' (f.target ∩ ↑f.symm ⁻¹' U) = f.source ∩ U

Tactic:
· apply (f.symm_image_target_inter_eq _).trans
      rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
        f.source_preimage_target, f.source_inter_preimage_inv_preimage]

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

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ ‖adjointAux A‖ ≤ ‖A‖

pp: case refine_2
𝕜 : 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
⊢ ‖A‖ ≤ ‖adjointAux A‖

Tactic:
· refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
    rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
    exact toSesqForm_apply_norm_le

Goal state after:
case refine_2
𝕜 : 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
⊢ ‖A‖ ≤ ‖adjointAux A‖
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)
⊢ ((affineCombination k {i}ᶜ s.points) fun x ↦ (↑n)⁻¹) -ᵥ s.points i = (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)

Tactic:
affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ ?_ (s.points i)

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
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ((({i}ᶜ.weightedVSubOfPoint s.points (s.points i)) fun x ↦ (↑n)⁻¹) +ᵥ s.points i) -ᵥ s.points i =
    (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)

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)
⊢ ∑ i ∈ {i}ᶜ, (↑n)⁻¹ = 1
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 * ↑((↑f).trans (↑g).symm) = ↑((↑f).trans (↑g).symm) * a) ↔ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
← Subalgebra.mem_center_iff (R := 𝕜),

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
⊢ ↑((↑f).trans (↑g).symm) ∈ Subalgebra.center 𝕜 (H →L[𝕜] H) ↔ ∃ α, ∀ (x : H), f x = (α • g) x
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.faceOppositeCentroid i -ᵥ s.centroid = (↑n)⁻¹ • (s.centroid -ᵥ s.points i)

Tactic:
centroid_vsub_point_eq_smul_vsub,

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
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i -ᵥ s.centroid = (↑n)⁻¹ • ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid)
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.faceOppositeCentroid i = (↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid

Tactic:
centroid_vsub_point_eq_smul_vsub,

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
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i = (↑n)⁻¹ • ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid
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.centroid -ᵥ s.points i = (↑n * (1 / (↑n + 1))) • (s.faceOppositeCentroid i -ᵥ s.points i)

Tactic:
centroid_vsub_point_eq_smul_vsub,

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
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid) = (↑n * (1 / (↑n + 1))) • (s.faceOppositeCentroid i -ᵥ s.points i)
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

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

Tactic:
use ⟨p, ht₁ hp⟩

Goal state after:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := ⋯
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := ⋯
p : P
hp : p ∈ s
⊢ (fun p ↦ (lineMap q ↑p) ↑(w p)) ⟨p, ⋯⟩ = 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)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
this : Summable fun a ↦ ‖c‖₊ ^ p.toReal * ‖f a‖₊ ^ p.toReal
⊢ Summable fun a ↦ ‖c • f a‖₊ ^ p.toReal

Tactic:
← NNReal.mul_rpow

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)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
this : Summable fun a ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
⊢ Summable fun a ↦ ‖c • f a‖₊ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ∞
hg : Memℓp g ∞
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i ↦ ‖g i‖)
i : I
⊢ (fun i ↦ ‖(f * g) i‖) i ≤ Cf * Cg

Tactic:
calc
    ‖(f * g) i‖ ≤ ‖f i‖ * ‖g i‖ := norm_mul_le (f i) (g i)
    _ ≤ Cf * Cg :=
      mul_le_mul (hCf ⟨i, rfl⟩) (hCg ⟨i, rfl⟩) (norm_nonneg _)
        ((norm_nonneg _).trans (hCf ⟨i, rfl⟩))

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

Goal state before:
pp: case inr.left
ι : 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 𝕜 := ⋯
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝ : NormedSpace ℝ E := ⋯
this : l.NeBot
hr : 0 < r
⊢ TendstoUniformlyOn (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (Metric.ball x r)

Tactic:
Metric.tendstoUniformlyOn_iff

Goal state after:
case inr.left
ι : 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
⊢ ∀ ε > 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 - (f n.1 x - f n.2 x)) < ε
Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
A : ContinuousAt (fun p ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0)
B : ∀ᶠ (p : ℝ × E) in 𝓝 (R, 0), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1)
⊢ ContDiffAt ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, 0)

Tactic:
refine (contDiffAt_const (c := 1)).congr_of_eventuallyEq <| B.mono fun _ ↦
        smoothTransition.one_of_one_le

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
⊢ ContDiffAt ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, 0)

Tactic:
have A : ContinuousAt (fun p : ℝ × E ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0) := by
        fun_prop (disch := positivity)
      have B : ∀ᶠ p in 𝓝 (R, (0 : E)), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1) :=
        A.eventually <| le_mem_nhds <| (one_lt_div hR).2 <| sub_lt_sub_left (by simp) _
      refine (contDiffAt_const (c := 1)).congr_of_eventuallyEq <| B.mono fun _ ↦
        smoothTransition.one_of_one_le

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_1
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t✝ : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
x✝ : t ∈ u
⊢ ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * C

Tactic:
apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
⊢ ‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t ↦ ‖L‖ * ‖f t‖ * C) t

Tactic:
by
  -- Porting note: had to add `f := _`
  refine le_indicator (f := fun t ↦ ‖L (f t) (g (x - t))‖) (fun t _ => ?_) (fun t ht => ?_) t
  · apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]
  · have : x - t ∉ support g := by
      refine mt (fun hxt => hu ?_) ht
      refine ⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, ?_⟩
      simp only [neg_sub, sub_add_cancel]
    simp only [notMem_support.mp this, (L _).map_zero, norm_zero, le_rfl]

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

Goal state before:
pp: α : 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₀‖
x : H
x_in : x ∈ ball x₀ ε
this : ∀ᵐ (a : α) ∂μ, ‖F x₀ a - F x a‖ ≤ ε * b a
⊢ Integrable (F x) μ

Tactic:
exact integrable_of_norm_sub_le (hF_meas x (hε x_in)) hF_int
      (bound_integrable.norm.const_mul ε) this

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_1
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : 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✝² : AddGroup G
inst✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun t ↦ -t + x₀) ⁻¹' s
hbg : BddAbove ((fun i ↦ ‖g i‖) '' s')
t : G
ht : t ∈ s
⊢ ‖(L (f t)) (g (x₀ - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g ↑i‖

Tactic:
apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]

Goal state after:
case refine_1.hy
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : 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✝² : AddGroup G
inst✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
s' : Set G := ⋯
hbg : BddAbove ((fun i ↦ ‖g i‖) '' s')
t : G
ht : t ∈ s
⊢ ‖g (x₀ - t)‖ ≤ ⨆ i, ‖g ↑i‖