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

Goal state before:
pp: case inl
A : Type u_1
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module ℝ A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : SMulCommClass ℝ A A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : IsTopologicalRing A
inst✝⁷ : T2Space A
inst✝⁶ : PartialOrder A
inst✝⁵ : NonnegSpectrumClass ℝ A
inst✝⁴ : StarOrderedRing A
inst✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ f a
h₁ : ContinuousOn f (quasispectrum ℝ a)
h₂ : f 0 = 0
h₃ : IsSelfAdjoint a
⊢ ∃ x, (∀ x_1 ∈ quasispectrum ℝ a, 0 ≤ x x_1) ∧ cfcₙ x a = cfcₙ f a

Tactic:
refine ⟨f, ?_, rfl⟩
    rwa [cfcₙ_nonneg_iff f a] at hf

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

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) Aᴴ‖ = ‖A‖

Tactic:
toEuclideanLin_eq_toLin_orthonormal,

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖(toLin (EuclideanSpace.basisFun m 𝕜).toBasis (EuclideanSpace.basisFun n 𝕜).toBasis ≪≫ₗ toContinuousLinearMap) Aᴴ‖ =
    ‖A‖
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (Aᴴ * A)‖ = ‖A‖ * ‖A‖

Tactic:
toEuclideanLin_eq_toLin_orthonormal,

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖(toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun n 𝕜).toBasis ≪≫ₗ toContinuousLinearMap)
        (Aᴴ * A)‖ =
    ‖A‖ * ‖A‖
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
obtain ⟨⟨x, y⟩, -⟩ := id h

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen[inst✝¹] ↑s
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    f.symm.restr (f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s))

Tactic:
set_identity,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen[inst✝¹] ↑s
⊢ (f.symm.trans (s.openPartialHomeomorphSubtypeCoe hs).symm).trans (s.openPartialHomeomorphSubtypeCoe hs) ≈
    f.symm.restr (f.symm.source ∩ ↑f.symm ⁻¹' ↑s)
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:
by
    rw [(Z.localTrivAt b).nhds_eq_comap_inf_principal (mk_mem_localTrivAt_source _ _ _), comap_inf,
      comap_principal, comap_comap]
    simp only [Function.comp_def, localTrivAt_apply_mk, Trivialization.coe_coe,
      ← (isEmbedding_prodMkRight b).nhds_eq_comap]
    convert_to 𝓝 x = 𝓝 x ⊓ 𝓟 univ
    · congr
      exact eq_univ_of_forall (mk_mem_localTrivAt_source Z _)
    · rw [principal_univ, inf_top_eq]

Goal state after:
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 ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ ↑e) l (𝓝 (↑e z).2)

Tactic:
exact e.tendsto_nhds_iff hz

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

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : ∀ (x : B), Nonempty (E x)
e : Trivialization F TotalSpace.proj
⊢ ContinuousOn (fun z ↦ TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)

Tactic:
have : ∀ z ∈ e.baseSet ×ˢ (univ : Set F),
      TotalSpace.mk z.1 (e.symm z.1 z.2) = e.toOpenPartialHomeomorph.symm z := by
    rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩
    rw [e.mk_symm hx]
  refine ContinuousOn.congr ?_ this
  rw [← e.target_eq]
  exact e.toOpenPartialHomeomorph.continuousOn_symm

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
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)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun m ↦ m • e) g' ∈ U
hfe : f ((fun m ↦ m • e) g') = f e
⊢ g • (g⁻¹ * g') • e = g' • e

Tactic:
mul_smul,

Goal state after:
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)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun m ↦ m • e) g' ∈ U
hfe : f ((fun m ↦ m • e) g') = f e
⊢ g • g⁻¹ • g' • e = g' • e
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_5
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)
g₁ g₂ : G
hne : g₁ ≠ g₂
e : E
x✝ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁ ⊓ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
h₁ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁
h₂ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
⊢ (g₁ * g₂⁻¹) • g₂ • e = g₁ • e

Tactic:
mul_smul,

Goal state after:
case refine_5
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)
g₁ g₂ : G
hne : g₁ ≠ g₂
e : E
x✝ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁ ⊓ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
h₁ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₁
h₂ : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g₂
⊢ g₁ • g₂⁻¹ • g₂ • e = g₁ • e
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
⊢ t₁ ∈ s → ∀ ⦃x₂ : ℝ⦄, x₂ ∈ s → exp t₁ = exp x₂ → t₁ = x₂

Tactic:
ht₁

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
⊢ ∀ ⦃x₂ : ℝ⦄, x₂ ∈ s → exp t₁ = exp x₂ → t₁ = x₂
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case h
x y : Circle
hne : x ≠ y
⊢ (y.path x) ⟨2⁻¹, ⋯⟩ ∈ ⇑(y.path x) '' Ioo 0 1

Tactic:
refine mem_image_of_mem _ ⟨by simp [← unitInterval.coe_pos], unitInterval.coe_lt_one.mp ?_⟩

Goal state after:
case h
x y : Circle
hne : x ≠ y
⊢ ↑⟨2⁻¹, ⋯⟩ < 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: θ : Angle
⊢ ↑(↑θ.toCircle).arg = θ

Tactic:
by
  induction θ using Angle.induction_on
  rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]

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
A : E →L[𝕜] F
x : E
y : F
⊢ ⟪x, (adjointAux A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Tactic:
← inner_conj_symm,

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
A : E →L[𝕜] F
x : E
y : F
⊢ (starRingEnd 𝕜) ⟪(adjointAux A) y, x⟫_𝕜 = ⟪A x, y⟫_𝕜
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
A : E →L[𝕜] E
hA : (↑A).IsSymmetric
⊢ IsSelfAdjoint A

Tactic:
rwa [← ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric] at hA

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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
⊢ (s.reindex e).faceOppositeCentroid i = (s.faceOppositeCentroid ∘ ⇑e.symm) i

Tactic:
faceOppositeCentroid

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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
⊢ ((s.reindex e).faceOpposite i).centroid = (s.faceOppositeCentroid ∘ ⇑e.symm) 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
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i ∈ s.median i

Tactic:
simp [median, left_mem_affineSpan_pair]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
⊢ p -ᵥ s.centroid = 0

Tactic:
have hi : LinearIndependent k u := by
    set p : Fin (n + 1) → P := fun x => if x = i₀ then s.centroid else s.points x
    have hindep : AffineIndependent k p := by
      have := affineIndependent_points_update_centroid s i₀
      unfold Function.update at this
      grind
    have h1 := (affineIndependent_iff_linearIndependent_vsub k p i₀).mp hindep
    simp_rw [ne_eq, p] at h1
    set f : {x // x ∈ ({i₀}ᶜ : Finset (Fin (n + 1)))} → {x // x ≠ i₀} :=
      have h (x : {x // x ∈ ({i₀}ᶜ : Finset (Fin (n + 1)))}) : x.val ≠ i₀ := by
        grind [mem_compl, Finset.notMem_singleton]
      fun x => ⟨x.val, h x⟩
    have f_inj : Function.Injective f := by intro x y hxy; grind
    have h2 := h1.comp f f_inj
    convert! h2 using 1
    grind only [mem_compl, Finset.notMem_singleton]

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

Tactic:
by
  rw [collinear_iff_rank_le_one, vectorSpan_singleton]
  simp

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

Goal state before:
pp: case h.inr
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
hp : p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
use 1

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
hp : p = p₂
⊢ p = 1 • (p₂ -ᵥ p₁) +ᵥ p₁
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✝⁴ : PartialOrder G
inst✝³ : CommGroup G
inst✝² : IsOrderedMonoid G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Ici c⁻¹) μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) (Set.Iic c) μ

Tactic:
by
  simpa using hf.comp_inv

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✝⁴ : PartialOrder G
inst✝³ : CommGroup G
inst✝² : IsOrderedMonoid G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Iic c⁻¹) μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) (Set.Ici c) μ

Tactic:
by
  simpa using hf.comp_inv

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✝⁴ : PartialOrder G
inst✝³ : CommGroup G
inst✝² : IsOrderedMonoid G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Ioi c⁻¹) μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) (Set.Iio c) μ

Tactic:
by
  simpa using hf.comp_inv

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✝⁴ : PartialOrder G
inst✝³ : CommGroup G
inst✝² : IsOrderedMonoid G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Iio c⁻¹) μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) (Set.Ioi c) μ

Tactic:
by
  simpa using hf.comp_inv

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ 0
⊢ Memℓp f 0

Tactic:
exact hfq

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

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f ∞
hpq : ∞ ≤ ∞
⊢ Memℓp f ∞

Tactic:
exact hfq

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ {i | (f + g) i ≠ 0}.Finite

Tactic:
refine (hf.finite_dsupport.union hg.finite_dsupport).subset fun i => ?_

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ i ∈ {i | (f + g) i ≠ 0} → i ∈ {i | f i ≠ 0} ∪ {i | g i ≠ 0}
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl.inl
𝕜 : 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✝ : IsEmpty α
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

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 α
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
· simp only [lp.eq_zero' f, zero_add, norm_zero, le_refl]

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 α
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
Module: Mathlib.Analysis.Calculus.SmoothSeries

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

Tactic:
have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
by
  cases isEmpty_or_nonempty α
  · simpa [eq_zero' f] using hC
  · exact norm_le_of_forall_le' C hCf

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)) * expNegInvGlue x) x

Tactic:
rw [zero_of_nonpos hx.le, 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.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)
  · exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩
  have : IsCompact s :=
    (isCompact_closedBall x r).of_isClosed_subset hs (h.trans ball_subset_closedBall)
  obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) :=
    this.exists_isMaxOn (β := α) (α := ℝ) hne (by fun_prop)
  have hyr : dist y x < r := h hys
  rcases exists_between hyr with ⟨r', hyr', hrr'⟩
  exact ⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
⊢ ProperSpace α ↔ ∀ (x : α), IsProperMap (dist x)

Tactic:
by
  refine ⟨fun _ ↦ isProperMap_dist, fun H ↦ ⟨fun x r ↦ ?_⟩⟩
  convert! (H x).isCompact_preimage (isCompact_closedBall 0 r)
  ext
  simp [dist_comm, Real.dist_eq]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : NormedSpace 𝕜 E'
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup P
inst✝² : NormedSpace 𝕜 P
μ : Measure G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
L : E' →L[𝕜] E →L[𝕜] F
s : Set P
n : ℕ∞
v : P → G
hv : ContDiffOn 𝕜 (↑n) v s
f : G → E
g : P → G → E'
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
⊢ ContDiffOn 𝕜 (↑n) (fun x ↦ (g x ⋆[L, μ] f) (v x)) s

Tactic:
by
  apply (contDiffOn_convolution_left_with_param L hs hk hgs hf hg).comp (contDiffOn_id.prodMk hv)
  intro x hx
  simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]

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

Goal state before:
pp: G : Type uG
E' : Type uE'
inst✝⁶ : NormedAddCommGroup E'
g : G → E'
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace E'
φ : ContDiffBump 0
inst✝ : HasContDiffBump G
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ (↑φ ⋆[lsmul ℝ ℝ, μ] g) x₀ = integral μ ↑φ • g x₀

Tactic:
convolution_eq_right' _ φ.support_eq.subset hg,

Goal state after:
G : Type uG
E' : Type uE'
inst✝⁶ : NormedAddCommGroup E'
g : G → E'
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : NormedSpace ℝ E'
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace E'
φ : ContDiffBump 0
inst✝ : HasContDiffBump G
x₀ : G
hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀
⊢ ∫ (t : G), ((lsmul ℝ ℝ) (↑φ t)) (g x₀) ∂μ = integral μ ↑φ • g x₀