mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ ∑ x ∈ (Finsupp.mapDomain convexCombination f.weights).support,
      (Finsupp.mapDomain convexCombination f.weights) x • (x -ᵥ b) =
    ∑ x ∈ (f.weights.sum fun d r ↦ r • d.weights).support, (f.weights.sum fun d r ↦ r • d.weights) x • (x -ᵥ b)

Tactic:
change (Finsupp.mapDomain convexCombination f.weights).sum (fun x w => w • (x -ᵥ b)) = _

Goal state after:
case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ ((Finsupp.mapDomain convexCombination f.weights).sum fun x w ↦ w • (x -ᵥ b)) =
    ∑ x ∈ (f.weights.sum fun d r ↦ r • d.weights).support, (f.weights.sum fun d r ↦ r • d.weights) x • (x -ᵥ b)
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
this : f =ᵐ[μ] 0
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
simp only [average_congr this, Pi.zero_apply, average_zero]

Goal state after:
case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
this : f =ᵐ[μ] 0
⊢ f =ᵐ[μ] const α 0 ∨ ‖0‖ < C
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ ∑ d ∈ f.weights.support, f.weights d • ∑ x ∈ d.weights.support, d.weights x • (x -ᵥ b) =
    ∑ x ∈ (∑ x ∈ f.weights.support, f.weights x • x.weights).support,
      (∑ x ∈ f.weights.support, f.weights x • x.weights) x • (x -ᵥ b)

Tactic:
simp_rw [Finset.smul_sum, smul_smul]

Goal state after:
case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ ∑ x ∈ f.weights.support, ∑ x_1 ∈ x.weights.support, (f.weights x * x.weights x_1) • (x_1 -ᵥ b) =
    ∑ x ∈ (∑ x ∈ f.weights.support, f.weights x • x.weights).support,
      (∑ x ∈ f.weights.support, f.weights x • x.weights) x • (x -ᵥ b)
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
⊢ x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ (convexHull 𝕜) ↑s

Tactic:
by
  simp [space]

Goal state after:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
⊢ (map f s).SSameSide (f x) (f y) ↔ s.SSameSide x y

Tactic:
by
  simp_rw [SSameSide, hf.wSameSide_map_iff, mem_map_iff_mem_of_injective hf]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V) ⦃a : V⦄, G.Adj v a → ¬H.Adj v a) ↔ ∀ ⦃a : Sym2 V⦄, a ∈ G.edgeSet → a ∉ H.edgeSet

Tactic:
Sym2.forall,

Goal state after:
V : Type u
G H : SimpleGraph V
⊢ (∀ (v : V) ⦃a : V⦄, G.Adj v a → ¬H.Adj v a) ↔ ∀ (x y : V), s(x, y) ∈ G.edgeSet → s(x, y) ∉ H.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)
⊢ #{v}.toFinsetᶜ = Fintype.card V - 1

Tactic:
Finset.card_compl,

Goal state after:
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)
⊢ Fintype.card V - #{v}.toFinset = Fintype.card V - 1
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
v : V
⊢ ⊥.neighborSet v = ∅

Tactic:
by
  grind [mem_neighborSet, bot_adj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G H : SimpleGraph V
⊢ (∀ (u v : V) ⦃a : V⦄, G.Adj u a ∧ G.Adj v a → ¬(H.Adj u a ∧ H.Adj v a)) ↔
    ∀ ⦃a : Sym2 V⦄, a ∈ G.edgeSet → a ∉ H.edgeSet

Tactic:
Sym2.forall,

Goal state after:
V : Type u
G H : SimpleGraph V
⊢ (∀ (u v : V) ⦃a : V⦄, G.Adj u a ∧ G.Adj v a → ¬(H.Adj u a ∧ H.Adj v a)) ↔
    ∀ (x y : V), s(x, y) ∈ G.edgeSet → s(x, y) ∉ H.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G = ⊤ ↔ ∀ (v : V), G.IsUniversal v

Tactic:
by
  simp [eq_top_iff_forall_ne_adj, IsUniversal]

Goal state after:
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
rw [openSegment_eq_image, Set.mem_image] at h

Goal state after:
case inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : ∃ x ∈ Set.Ioo 0 1, (1 - x) • (p₁ -ᵥ p) + x • (p₃ -ᵥ p) = p₂ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ s.WSameSide x y → x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rintro ⟨p₁', hp₁', p₂', hp₂', h0 | h0 | ⟨r₁, r₂, hr₁, hr₂, hr⟩⟩

Goal state after:
case mp.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

case mp.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : y -ᵥ p₂' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

case mp.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (y -ᵥ p₂')
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ s.WOppSide x y → x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
rintro ⟨p₁', hp₁', p₂', hp₂', h0 | h0 | ⟨r₁, r₂, hr₁, hr₂, hr⟩⟩

Goal state after:
case mp.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

case mp.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : p₂' -ᵥ y = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

case mp.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
hr : r₁ • (x -ᵥ p₁') = r₂ • (p₂' -ᵥ y)
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
t : R
ht : t ≤ 0
p' : P
hp' : p' ∈ ↑s
⊢ s.WOppSide x (t • (x -ᵥ p) +ᵥ p')

Tactic:
exact wOppSide_smul_vsub_vadd_right x hp hp' ht

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
hf' : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
⊢ ↑n ! * (C₃ * (1 + ‖x‖) ^ (k₁ * k₂)) * ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ n =
    ↑n ! * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)

Tactic:
rw [mul_pow, ← pow_mul, pow_add]; ring

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case pos
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
⊢ |x| ^ (r - ↑n) ≤ (1 + |x|) ^ k

Tactic:
have : r - n ≤ k := by simpa using hk₁.trans (by simp)

Goal state after:
case pos
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this✝ : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
this : r - ↑n ≤ ↑k
⊢ |x| ^ (r - ↑n) ≤ (1 + |x|) ^ k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case inl
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)

pp: case inr
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)

Tactic:
· gcongr
    · apply (pow_le_one₀ hx h'x).trans
      apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos
      · positivity
      · linarith
      · simp
    · linarith

Goal state after:
case inr
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : ¬x₀ = 0
hb : ¬b = 0
⊢ T x₀ = (-b⁻¹ * a) • x₀

Tactic:
linear_combination (norm := match_scalars <;> field) b⁻¹ • h₂

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
| (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).rank

Tactic:
← coe_star

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
| (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * ↑(star hA.eigenvectorUnitary)).rank
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
⊢ (succSub P i) ((succSub P j) x) = if i = j then (succSub P j) x else 0

Tactic:
simp only [succSub, _root_.sub_apply, map_sub, hcomp,
    Nat.add_min_add_right]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
⊢ (P (min i j + 1)) x - (P (min i (j + 1))) x - ((P (min (i + 1) j)) x - (P (min i j)) x) =
    if i = j then (P (j + 1)) x - (P j) x else 0
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝¹² : TopologicalSpace α
inst✝¹¹ : NormalSpace α
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : BorelSpace α
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝⁷ : SecondCountableTopologyEither α E
_i : Fact (1 ≤ p)
𝕜 : Type u_3
inst✝⁶ : NormedRing 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsBoundedSMul 𝕜 E
inst✝³ : NormedSpace ℝ E
inst✝² : CompactSpace α
inst✝¹ : μ.WeaklyRegular
inst✝ : IsFiniteMeasure μ
hp : p ≠ ∞
f : α →ᵇ E
⊢ (BoundedContinuousFunction.toLp p μ 𝕜) f ∈ range ⇑(toLp p μ 𝕜)

Tactic:
exact ⟨f.toContinuousMap, rfl⟩

Goal state after:
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᵐ[volume.restrict (Ioc a b)] g
⊢ fourierCoeffOn hab f = fourierCoeffOn hab g

Tactic:
ext n
  rw [fourierCoeffOn_eq_integral, fourierCoeffOn_eq_integral]
  congr! 1
  apply intervalIntegral.integral_congr_ae_restrict
  simp only [uIoc_of_le hab.le]
  filter_upwards [h] with x hx
  rw [hx]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + -⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
← decay_neg_aux k n g x

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + -⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (-⇑g) x‖
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case hg
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) μ
w : W
y : V
g : V → ℂ := fun v ↦ ↑(𝐞 (-(L v) w))
A : ∀ (x : V), (fderiv ℝ g x) y = -2 * ↑π * I * ↑((L y) w) * g x
⊢ ∀ x ∈ tsupport g, DifferentiableAt ℝ f x

Tactic:
· exact fun _ _ ↦ h'f.differentiableAt

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case pos
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : Integrable f μ
⊢ ContDiff ℝ (↑N) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)

Tactic:
exact (hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f.1).contDiff

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ ↑K * (‖g x‖ + ‖g 0‖) ≤ ↑K * (‖g x‖ + max 1 ‖g 0‖)

Tactic:
gcongr
    exact le_max_right _ _

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case e_f
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
⊢ iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) fun v ↦ fourierPowSMulRight L f v k

Tactic:
iteratedFDeriv_fourierIntegral (N := K) _ _ hf.continuous.aestronglyMeasurable hk

Goal state after:
case e_f
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) fun v ↦ fourierPowSMulRight L f v k) =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) fun v ↦ fourierPowSMulRight L f v k

E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
⊢ ∀ (n : ℕ), ↑n ≤ K → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + (k + 1)) s = Gamma s

Tactic:
← hk,

Goal state after:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + (k + 1)) s = GammaAux (⌊1 - s.re⌋₊ + k) s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ ⌊1 - s.re⌋₊ ≤ n

Tactic:
by_cases h : 0 ≤ 1 - s.re

Goal state after:
case pos
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : 0 ≤ 1 - s.re
⊢ ⌊1 - s.re⌋₊ ≤ n

case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ ⌊1 - s.re⌋₊ ≤ n