mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊
b : A
⊢ ‖a.toProd.2 b‖₊ ^ 2 = ‖a.toProd.2 b * star (a.toProd.2 b)‖₊

Tactic:
simpa only [← sq] using CStarRing.nnnorm_self_mul_star.symm

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
I : Type u_3
inst✝¹ : TopologicalSpace I
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : ↑t.baseSet × I
⊢ (fun e ↦ (⟨f ↑e, ⋯⟩, (↑t ↑e).2)) ((fun xi ↦ ⟨t.invFun (↑xi.1, xi.2), ⋯⟩) xi) = xi

Tactic:
by simp [t.proj_symm_apply', t.apply_symm_apply']

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
x : { x // x ∈ f ⁻¹' U }
hx : x ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
y : { x // x ∈ f ⁻¹' U }
hy : y ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
eq : ↑y = (fun x ↦ g • x) ↑x
this : IsCancelSMul G E
⊢ ↑(H y).1 = ↑(H x).1

Tactic:
simp_rw [hH]

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
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
x : { x // x ∈ f ⁻¹' U }
hx : x ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
y : { x // x ∈ f ⁻¹' U }
hy : y ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
eq : ↑y = (fun x ↦ g • x) ↑x
this : IsCancelSMul G E
⊢ f ↑y = f ↑x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n ↦ (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f
⊢ (∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
simp_rw [← ContinuousMap.tsum_apply h_sum a, NormedSpace.expSeries_apply_eq]

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n ↦ (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f
⊢ ∑' (i : ℕ), ((↑i.factorial)⁻¹ • f ^ i) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } a
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : 2 ^ 2 ≤ 2 * (1 - z.re)
⊢ -1 ∈ spectrum ℂ u

Tactic:
replace key : z.re ≤ -1 := by linarith

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
⊢ -1 ∈ spectrum ℂ u
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✝²] (f ⁻¹' s ∩ V' e)
⊢ f '' V' e ⊆ f '' (φ e).source

Tactic:
exact image_mono inter_subset_right

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

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
w✝ : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f w✝ s
right✝ : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (w✝ x n) fun x ↦ 1
⊢ ContDiffOn ℝ ∞ f s

Tactic:
exact hp.contDiffOn

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

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
hf : ContDiff ℝ ∞ f
h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x
⊢ AbsolutelyMonotoneOn f s

Tactic:
by
  refine ⟨ftaylorSeries ℝ f, (hf.ftaylorSeries).hasFTaylorSeriesUpToOn s, fun n x hx => ?_⟩
  exact iteratedDeriv_eq_iteratedFDeriv (𝕜 := ℝ) (f := f) ▸ h n x hx

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
⊢ ‖adjoint A‖ * ‖A‖ = ‖A‖ * ‖A‖

Tactic:
by rw [LinearIsometryEquiv.norm_map]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
f : E →L[𝕜] E
hf : (↑f).IsSymmetric
⊢ (innerSL 𝕜) x ∘SL f = (innerSL 𝕜) (f x)

Tactic:
by
  ext; simp [hf]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
w : E
⊢ ⟪w, (adjoint (A ∘ₗ B)) v⟫_𝕜 = ⟪w, (adjoint B ∘ₗ adjoint A) v⟫_𝕜

Tactic:
simp only [adjoint_inner_right, LinearMap.coe_comp, Function.comp_apply]

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✝ : CharZero k
s : Simplex k P n
p : P
⊢ s.centroid -ᵥ p = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ p)

Tactic:
rw [centroid_vsub_const _ _ (by simp), centroid_def, affineCombination_eq_linear_combination
    (hw := sum_centroidWeights_eq_one_of_nonempty _ _ (by simp))]

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✝ : CharZero k
s : Simplex k P n
p : P
⊢ ∑ i, centroidWeights k univ i • (s.points i -ᵥ p) = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ p)
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
x✝¹ : ∃ α, ∀ (x : H), f x = (α • g) x
y : ↥(unitary 𝕜)
h : ∀ (x : H), f x = (y • g) x
x✝ : H
⊢ (↑y • 1) x✝ = (↑(↑g).symm ∘SL ↑↑f) x✝

Tactic:
simp [h]

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

Goal state before:
pp: case mp
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
p₀ : P
h : p₀ ∈ s
⊢ (∃ v₀, ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v) → ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
rintro ⟨v₀, hv⟩
    use v₀
    intro p hp
    obtain ⟨r, hr⟩ := hv (p -ᵥ p₀) (vsub_mem_vectorSpan k hp h)
    use r
    rw [eq_vadd_iff_vsub_eq]
    exact hr.symm

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
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ Collinear k s ↔ ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
simp_rw [collinear_iff_rank_le_one, rank_submodule_le_one_iff', Submodule.le_span_singleton_iff]
  constructor
  · rintro ⟨v₀, hv⟩
    use v₀
    intro p hp
    obtain ⟨r, hr⟩ := hv (p -ᵥ p₀) (vsub_mem_vectorSpan k hp h)
    use r
    rw [eq_vadd_iff_vsub_eq]
    exact hr.symm
  · rintro ⟨v, hp₀v⟩
    use v
    intro w hw
    have hs : vectorSpan k s ≤ k ∙ v := by
      rw [vectorSpan_eq_span_vsub_set_right k h, Submodule.span_le, Set.subset_def]
      intro x hx
      rw [SetLike.mem_coe, Submodule.mem_span_singleton]
      rw [Set.mem_image] at hx
      rcases hx with ⟨p, hp, rfl⟩
      rcases hp₀v p hp with ⟨r, rfl⟩
      use r
      simp
    have hw' := SetLike.le_def.1 hs hw
    rwa [Submodule.mem_span_singleton] at hw'

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

Goal state before:
pp: case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p : P
hp : p ∈ {p₁, p₂}
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp

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 = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
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
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points)
⊢ Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points) =
    Submodule.span k (Set.range s.points -ᵥ Set.range s.points)

Tactic:
suffices Set.range s.medial.points -ᵥ Set.range s.medial.points
    = (-n : k)⁻¹ • (Set.range s.points -ᵥ Set.range s.points) by
    rw [this, Submodule.span_smul_eq_of_isUnit]
    simpa using NeZero.ne n

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
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points)
⊢ Set.range s.medial.points -ᵥ Set.range s.medial.points = (-↑n)⁻¹ • (Set.range s.points -ᵥ Set.range s.points)
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ support ↑f = ball c f.rOut

Tactic:
simp only [toFun, support_comp_eq_preimage, ContDiffBumpBase.support _ _ f.one_lt_rOut_div_rIn]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ (fun x ↦ f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) = ball c f.rOut
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁴ : MeasurableSpace G
inst✝³ : NormedAddCommGroup F
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) s⁻¹ μ

Tactic:
by
  apply (integrable_map_equiv (MeasurableEquiv.inv G) f).mp
  have : s⁻¹ = MeasurableEquiv.inv G ⁻¹' s := by simp
  rw [this, ← MeasurableEquiv.restrict_map]
  simpa using! hf

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
⊢ ∫ (x : G), f x ∂μ = 0

Tactic:
have : IsAddTorsionFree E := .of_isTorsionFree ℝ E

Goal state after:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = 0
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
⊢ ∫ (x : G), f x ∂μ = 0

Tactic:
have : IsAddTorsionFree E := .of_isTorsionFree ℝ E

Goal state after:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = 0
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
swap

Goal state after:
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: ⊢ Monotone expNegInvGlue

Tactic:
intro x y hxy
  rcases le_or_gt x 0 with hx | hx
  · simp [zero_of_nonpos hx, nonneg]
  simp [expNegInvGlue, not_le.2 hx, not_le.2 (hx.trans_le hxy),
    inv_le_inv₀ (hx.trans_le hxy) hx, hxy]

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' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F x a - F x₀ a‖ ≤ bound a * ‖x - x₀‖
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₀‖⁻¹
⊢ Integrable F' μ ∧ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
set b : α → ℝ := fun a ↦ |bound a|

Goal state after:
α : 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' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F x a - F x₀ a‖ ≤ bound a * ‖x - x₀‖
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|
⊢ Integrable F' μ ∧ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
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 :
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 (n, x).2,
      dist (‖x_1 - (n, x).2‖⁻¹ * ‖f (n, x).1 x_1 - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (x_1 - (n, x).2)‖) 0 < ε
y : E
hy : dist (‖y - (n, x).2‖⁻¹ * ‖f (n, x).1 y - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (y - (n, x).2)‖) 0 < ε
⊢ dist ((↑‖(n, y).2 - x‖)⁻¹ • (f (n, y).1 (n, y).2 - f (n, y).1 x - ((f' (n, y).1 x) (n, y).2 - (f' (n, y).1 x) x))) 0 <
    ε

Tactic:
rw [dist_eq_norm] at hy ⊢

Goal state after:
case refine_2
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this :
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 (n, x).2,
      dist (‖x_1 - (n, x).2‖⁻¹ * ‖f (n, x).1 x_1 - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (x_1 - (n, x).2)‖) 0 < ε
y : E
hy : ‖‖y - (n, x).2‖⁻¹ * ‖f (n, x).1 y - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (y - (n, x).2)‖ - 0‖ < ε
⊢ ‖(↑‖(n, y).2 - x‖)⁻¹ • (f (n, y).1 (n, y).2 - f (n, y).1 x - ((f' (n, y).1 x) (n, y).2 - (f' (n, y).1 x) x)) - 0‖ < ε
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : SFinite μ
inst✝ : μ.IsNegInvariant
hcf : HasCompactSupport f₀
hf : ContDiff 𝕜 1 f₀
hg : LocallyIntegrable g₀ μ
x₀ : 𝕜
⊢ HasDerivAt (g₀ ⋆[L.flip, μ] f₀) ((g₀ ⋆[L.flip, μ] deriv f₀) x₀) x₀

Tactic:
exact hcf.hasDerivAt_convolution_right L.flip hg hf x₀

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✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
⊢ BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ x₀ - t) ⁻¹' ball 0 R)

pp: case refine_2
𝕜 : 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✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
⊢ (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ support f

Tactic:
swap

Goal state after:
case refine_2
𝕜 : 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✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
⊢ (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ support f

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✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
⊢ BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ x₀ - t) ⁻¹' ball 0 R)