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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x ↦ x * m) l (𝓝 m)
m : A
⊢ (star ∘ fun x ↦ x * star m) =ᶠ[l] fun x ↦ m * x

Tactic:
filter_upwards [hl] with x hx

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x ↦ x * m) l (𝓝 m)
m x : A
hx : IsSelfAdjoint x
⊢ (star ∘ fun x ↦ x * star m) x = m * x
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖fun i j ↦ A i j‖ = ↑(Finset.univ.sup fun i ↦ Finset.univ.sup fun j ↦ ‖A i j‖₊)

Tactic:
Pi.norm_def,

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ↑(Finset.univ.sup fun b ↦ ‖fun j ↦ A b j‖₊) = ↑(Finset.univ.sup fun i ↦ Finset.univ.sup fun j ↦ ‖A i j‖₊)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case mul
𝕜 : 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
f g : C(↑(spectrum 𝕜 a), 𝕜)
hf : Commute ((cfcHom ha) f) b
hg : Commute ((cfcHom ha) g) b
⊢ Commute ((cfcHom ha) (f * g)) b

Tactic:
map_mul

Goal state after:
case mul
𝕜 : 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
f g : C(↑(spectrum 𝕜 a), 𝕜)
hf : Commute ((cfcHom ha) f) b
hg : Commute ((cfcHom ha) g) b
⊢ Commute ((cfcHom ha) f * (cfcHom ha) g) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case mul
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Commute ((cfcₙHom ha) f) b
hg : Commute ((cfcₙHom ha) g) b
⊢ Commute ((cfcₙHom ha) (f * g)) b

Tactic:
map_mul

Goal state after:
case mul
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Commute ((cfcₙHom ha) f) b
hg : Commute ((cfcₙHom ha) g) b
⊢ Commute ((cfcₙHom ha) f * (cfcₙHom ha) g) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
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
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : ↑t → Set ℝ≥0
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
classical
  refine ha_cont.cfcₙ_nnreal (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
    (by simpa +contextual using hS₁) ?_ ha' ?_
  all_goals simp +contextual only [↓reduceDIte]
  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ ‖(toCLM M) ((equiv A (m → A)).symm (Pi.single i (star (M i j))))‖ ≤ ‖M‖ * ‖M i j‖

Tactic:
apply (toCLM M).le_opNorm _ |>.trans

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ ‖toCLM M‖ * ‖(equiv A (m → A)).symm (Pi.single i (star (M i j)))‖ ≤ ‖M‖ * ‖M i j‖
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ AntilipschitzWith (↑(Fintype.card n) * ↑(Fintype.card m)) ⇑ofMatrixₗ.symm

Tactic:
refine AddMonoidHomClass.antilipschitz_of_bound _ fun M => ?_

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ‖M‖ ≤ ↑(↑(Fintype.card n) * ↑(Fintype.card m)) * ‖ofMatrixₗ.symm M‖
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
h₁ : ‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ ‖M * star M‖ * ‖v‖ ^ 2
h₂ : ‖v‖ = √(‖v‖ ^ 2)
⊢ √‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ √‖M * star M‖ * ‖v‖

Tactic:
rw [h₂, ← Real.sqrt_mul]

Goal state after:
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
h₁ : ‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ ‖M * star M‖ * ‖v‖ ^ 2
h₂ : ‖v‖ = √(‖v‖ ^ 2)
⊢ √‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ √(‖M * star M‖ * ‖v‖ ^ 2)

case hx
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
h₁ : ‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ ‖M * star M‖ * ‖v‖ ^ 2
h₂ : ‖v‖ = √(‖v‖ ^ 2)
⊢ 0 ≤ ‖M * star M‖
Module: Mathlib.Analysis.Normed.Group.NullSubmodule

Goal state before:
pp: M : Type u_1
inst✝⁴ : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
⊢ ‖c‖ * 0 = 0

Tactic:
mul_zero

Goal state after:
M : Type u_1
inst✝⁴ : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
⊢ 0 = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
⊢ cfcₙ (fun r ↦ ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ

Tactic:
have : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a) := .of_forall fun x ↦
    hf.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨Set.mem_univ _, hz⟩
  refine cfcₙ_integral' _ _ this f_zero ⟨?_, ?_⟩ ha
  · exact aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf f_zero
  · exact hasFiniteIntegral_mkD_restrict_of_bound f _ this f_zero bound bound_int bound_ge

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ ↑ℓ (ℓ z • x - ℓ x • z) = 0

Tactic:
map_sub,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ ↑ℓ (ℓ z • x) - ↑ℓ (ℓ x • z) = 0
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_2
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h : ∀ (x_1 : ι), ∀ x₁ ∈ s x_1, ∀ x₂ ∈ s x_1, x x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = x x_1
⊢ ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x

Tactic:
rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
case refine_2
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
x₁ : (i : ι) → M i
hx₁ : ∀ (i : ι), x₁ i ∈ s i
x₂ : (i : ι) → M i
hx₂ : ∀ (i : ι), x₂ i ∈ s i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : ∀ (i : ι), (a • x₁ + b • x₂) i ∈ s i
h : ∀ (x : ι), ∀ x₁_1 ∈ s x, ∀ x₂_1 ∈ s x, (a • x₁ + b • x₂) x ∈ openSegment 𝕜 x₁_1 x₂_1 → x₁_1 = (a • x₁ + b • x₂) x
⊢ x₁ = a • x₁ + b • x₂
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: ⊢ ∃ a, 𝐞 a ≠ 1 a

Tactic:
use 2⁻¹

Goal state after:
case h
⊢ 𝐞 2⁻¹ ≠ 1 2⁻¹
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = ↑e '' e.source ∩ ↑e '' s

Tactic:
refine image_inter_on ?_

Goal state after:
case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ ∀ x ∈ s, ∀ y ∈ e.source, ↑e x = ↑e y → x = y
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = comap (TotalSpace.mk b) (𝓝 { proj := b, snd := x })

Tactic:
(Z.localTrivAt b).nhds_eq_comap_inf_principal (mk_mem_localTrivAt_source _ _ _),

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x =
    comap (TotalSpace.mk b)
      (comap (↑(Z.localTrivAt b).toOpenPartialHomeomorph)
          (𝓝 (↑(Z.localTrivAt b).toOpenPartialHomeomorph { proj := b, snd := x })) ⊓
        𝓟 (Z.localTrivAt b).source)
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ l ≤ comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ ↑e) (𝓝 (↑e z).2)

Tactic:
rw [le_inf_iff, ← tendsto_iff_comap, ← tendsto_iff_comap]

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ ↑e) l (𝓝 (↑e z).2)
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsLocalHomeomorph f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)

Tactic:
by
  simp_rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ,
    isLocalHomeomorphOn_iff_isOpenEmbedding_restrict, imp_iff_right (Set.mem_univ _)]

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

Goal state before:
pp: x y : ℝ
⊢ exp x = exp y ↔ ∃ m, x = y + ↑m * (2 * π)

Tactic:
Subtype.ext_iff,

Goal state after:
x y : ℝ
⊢ ↑(exp x) = ↑(exp y) ↔ ∃ m, x = y + ↑m * (2 * π)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ range ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) ⊆ Icc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
Path.range_segment,

Goal state after:
x y : Circle
hne : x ≠ y
⊢ 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: x y : Circle
⊢ ⇑exp '' range ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) = ⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
Path.range_segment,

Goal state after:
x y : Circle
⊢ ⇑exp '' segment ℝ (↑x).arg (x.angleDiff y + (↑x).arg) = ⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg)
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)
h : ∀ (i : Fin (n + 1)), ∑ j ∈ {i}ᶜ, (↑n)⁻¹ • (s.points j -ᵥ s.points i) = ∑ j, (↑n)⁻¹ • (s.points j -ᵥ s.points i)
⊢ ∑ i_1 ∈ {i}ᶜ, (↑n)⁻¹ • (s.points i_1 -ᵥ s.points i) = (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)

Tactic:
h 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)
h : ∀ (i : Fin (n + 1)), ∑ j ∈ {i}ᶜ, (↑n)⁻¹ • (s.points j -ᵥ s.points i) = ∑ j, (↑n)⁻¹ • (s.points j -ᵥ s.points i)
⊢ ∑ j, (↑n)⁻¹ • (s.points j -ᵥ s.points i) = (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)
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 = ↑n • (s.centroid -ᵥ s.faceOppositeCentroid i)

Tactic:
by
  symm
  rw [← vsub_sub_vsub_cancel_right _ _ (s.points i),
    faceOppositeCentroid_vsub_point_eq_smul_sum_vsub,
    centroid_vsub_eq, ← neg_vsub_eq_vsub_rev,
    centroid_vsub_eq, ← sub_smul, smul_smul, ← neg_smul]
  congr
  simp_rw [mul_sub, sub_eq_iff_eq_add, neg_add_eq_sub]
  symm
  rw [sub_eq_iff_eq_add, mul_inv_cancel₀ (NeZero.ne (n : k))]
  have : (↑n + (1 : k))⁻¹ = 1 * (↑n + (1 : k))⁻¹ := by simp
  nth_rw 2 [this]
  rw [← add_mul, mul_inv_cancel₀ (by norm_cast)]

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.centroid = ↑n • (s.faceOppositeCentroid i -ᵥ 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.centroid = (s.centroid -ᵥ s.points i) +ᵥ s.points i
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
⊢ p -ᵥ s.centroid = 0

Tactic:
set i₀ : Fin (n + 1) := 0

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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
⊢ p -ᵥ s.centroid = 0
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
h : ¬Collinear k {p₁, p₁, p₃}
⊢ False

Tactic:
simp [collinear_pair] at h

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

Tactic:
simp [collinear_pair] at h

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

Tactic:
simp [collinear_pair] at h

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 ∞
⊢ BddAbove (Set.range fun i ↦ ‖(-f) i‖)

Tactic:
simpa using hf.bddAbove

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 ∞
⊢ BddAbove (Set.range fun i ↦ ‖star f i‖)

Tactic:
simpa using hf.bddAbove

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)
I : Type u_5
B : I → Type u_6
inst✝³ : (i : I) → NonUnitalNormedRing (B i)
inst✝² : (i : I) → StarRing (B i)
inst✝¹ : ∀ (i : I), NormedStarGroup (B i)
inst✝ : ∀ (i : I), CStarRing (B i)
f : ↥(lp B ∞)
i : I
⊢ ‖↑f i‖ ≤ √‖star f * f‖

Tactic:
Real.le_sqrt (norm_nonneg _) (norm_nonneg _),

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst✝³ : (i : I) → NonUnitalNormedRing (B i)
inst✝² : (i : I) → StarRing (B i)
inst✝¹ : ∀ (i : I), NormedStarGroup (B i)
inst✝ : ∀ (i : I), CStarRing (B i)
f : ↥(lp B ∞)
i : I
⊢ ‖↑f i‖ ^ 2 ≤ ‖star f * f‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ∞
⊢ ‖f‖ ≤ C

Tactic:
have : 0 < p := zero_lt_one.trans_le _i.elim
    have hp' : 0 < p.toReal := ENNReal.toReal_pos this.ne' hp.ne
    apply norm_le_of_forall_sum_le hp' hC
    exact sum_rpow_le_of_tendsto hp.ne hCF hf

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

Goal state before:
pp: α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
⊢ LipschitzOnWith K f s ↔ ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s

Tactic:
by
  simp_rw [lipschitzOnWith_iff_dist_le_mul]
  constructor
  · intro hfl i x hx y hy
    calc
      dist (f x i) (f y i) ≤ dist (f x) (f y) := by
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm top_ne_zero (f x - f y) i
      _ ≤ K * dist x y := hfl x hx y hy
  · intro hgl x hx y hy
    rw [dist_eq_norm]
    apply lp.norm_le_of_forall_le
    · positivity
    intro i
    apply hgl i x hx y hy

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

Goal state before:
pp: case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) (Polynomial.eval x⁻¹ (X ^ 2 * (p - derivative p)) * 0) x

Tactic:
mul_zero

Goal state after:
case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ Polynomial.eval y⁻¹ p * 0 = 0

Tactic:
mul_zero

Goal state after:
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

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

Tactic:
by
  apply contDiff_all_iff_nat.2 (fun m => ?_) n
  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: