mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ #A ≤ #(A.biUnion f)

Tactic:
suffices #A * s ≤ #(A.biUnion f) * s by exact_mod_cast le_of_mul_le_mul_right this hs

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ↑(#A) * s ≤ ↑(#(A.biUnion f)) * s
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
⊢ 0 ∈ K

Tactic:
obtain ⟨x, hx⟩ := K.nonempty

Goal state after:
V : Type u_1
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
K : ConvexBody V
h_symm : ∀ x ∈ K, -x ∈ K
x : V
hx : x ∈ ↑K
⊢ 0 ∈ K
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : μ t = 0
⊢ 0 = (μ t).toReal • ⨍ (x : α), f x ∂μ

Tactic:
h₀,

Goal state after:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
h₀ : μ t = 0
⊢ 0 = ENNReal.toReal 0 • ⨍ (x : α), f x ∂μ
Module: Mathlib.Analysis.Convex.LinearIsometry

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃ₗᵢ[𝕜] F
⊢ StrictConvexSpace 𝕜 E ↔ StrictConvexSpace 𝕜 F

Tactic:
simp only [strictConvexSpace_iff, ← map_zero e, ← e.image_closedBall, e.strictConvex_image]

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

Goal state before:
pp: case pos.inr
α : 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 : 0 < C
hfi : Integrable f μ
hμt : μ univ < ∞
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
have : IsFiniteMeasure μ := ⟨hμt⟩

Goal state after:
case pos.inr
α : 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 : 0 < C
hfi : Integrable f μ
hμt : μ univ < ∞
this : IsFiniteMeasure μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ iConvexComb (iConvexComb f fun i ↦ map (fun x ↦ (i, x)) g) (Function.uncurry e) =
    iConvexComb (iConvexComb g fun i ↦ map (fun x ↦ (i, x)) f) (Function.uncurry fun j i ↦ e i j)

Tactic:
iConvexComb_reindex _ (.prodComm ..)

Goal state after:
R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ iConvexComb (map (⇑(Equiv.prodComm I J)) (iConvexComb f fun i ↦ map (fun x ↦ (i, x)) g))
      (Function.uncurry e ∘ ⇑(Equiv.prodComm I J).symm) =
    iConvexComb (iConvexComb g fun i ↦ map (fun x ↦ (i, x)) f) (Function.uncurry fun j i ↦ e i j)
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case h_inter
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
i : ↥s
J : Finset ι
hJ_ss : J ⊆ s.erase ↑i
hJ_card : #J ≤ finrank 𝕜 E + 1
⊢ (⋂ i ∈ J, F i).Nonempty

Tactic:
exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
⊢ finrank 𝕜 ↥(vectorSpan 𝕜 (Set.range a)) ≤ k - 1

Tactic:
exact (Submodule.finrank_le (vectorSpan 𝕜 (range a))).trans (Nat.le_pred_of_lt h_card)

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
h : s.WSameSide x y
f : P →ᵃ[R] P'
⊢ (AffineSubspace.map f s).WSameSide (f x) (f y)

Tactic:
by
  rcases h with ⟨p₁, hp₁, p₂, hp₂, h⟩
  refine ⟨f p₁, mem_map_of_mem f hp₁, f p₂, mem_map_of_mem f hp₂, ?_⟩
  simp_rw [← linearMap_vsub]
  exact h.map f.linear

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
h : s.WOppSide x y
f : P →ᵃ[R] P'
⊢ (AffineSubspace.map f s).WOppSide (f x) (f y)

Tactic:
by
  rcases h with ⟨p₁, hp₁, p₂, hp₂, h⟩
  refine ⟨f p₁, mem_map_of_mem f hp₁, f p₂, mem_map_of_mem f hp₂, ?_⟩
  simp_rw [← linearMap_vsub]
  exact h.map f.linear

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, G.Adj a b → a ≠ b
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ w ∈ {v}ᶜ

Tactic:
simp_rw [Set.mem_union, mem_neighborSet, compl_adj, Set.mem_compl_iff, Set.mem_singleton_iff]

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V}, G.Adj a b → a ≠ b
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
ι : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi✝ : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
hi : w i = 0
⊢ (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ interior s

Tactic:
simp only [hi, zero_add, zero_div, zero_smul, ne_eq, hsum_t, not_false_eq_true, div_self,
        one_smul]
      grind

Goal state after:
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
y : P
⊢ (∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y) → s.SOppSide x y

Tactic:
rintro ⟨t, ht, p', hp', rfl⟩
    exact sOppSide_smul_vsub_vadd_right hx hp hp' ht

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

Goal state before:
pp: 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✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide
      ((Finset.affineCombination R Finset.univ s.points) (Pi.single i 1))
      ((Finset.affineCombination R Finset.univ s.points) w) ↔
    0 < w i

Tactic:
s.sSameSide_affineSpan_faceOpposite_iff (Fintype.sum_pi_single' _ _) hw,

Goal state after:
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✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : ∑ j, w j = 1
i : Fin (n + 1)
⊢ SignType.sign (Pi.single i 1 i) = SignType.sign (w i) ∧ Pi.single i 1 i ≠ 0 ↔ 0 < w i
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case succ
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h'f : HasTemperateGrowth (fderiv ℝ f)
hf : Differentiable ℝ f
k : ℕ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k
m : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ (m + 1) f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
rcases h'f.2 m with ⟨k', C', h'⟩
    refine ⟨k', C', ?_⟩
    simpa [iteratedFDeriv_succ_eq_comp_right] using h'

Goal state after:
Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty

Goal state before:
pp: E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Tactic:
have h := zero_at_infty f
  rw [tendsto_zero_iff_norm_tendsto_zero, tendsto_def] at h
  specialize h (Metric.ball 0 ε) (Metric.ball_mem_nhds 0 hε)
  rcases Metric.closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩
  use r
  intro x hr'
  suffices x ∈ (fun x ↦ ‖f x‖) ⁻¹' Metric.ball 0 ε by simp_all
  apply hr
  simp_all

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε

Tactic:
obtain ⟨ε, hε0, hε⟩ := T.rayleighQuotient_le_of_mem_resolventSet ‖T‖ (by positivity) hT'

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ (‖T‖ ^ 2 + ‖T‖ ^ 2) / (2 * ‖T‖) - ε
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ↑i ≤ n
⊢ Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ) ↔ ↑i ≤ n → Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)

Tactic:
simp only [hin, true_imp_iff, false_imp_iff, iff_true]

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

Goal state before:
pp: case neg
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ¬↑i ≤ n
⊢ Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ) ↔ ↑i ≤ n → Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)

Tactic:
simp only [hin, true_imp_iff, false_imp_iff, iff_true]

Goal state after:
case neg
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
X : Type u_5
inst✝ : TopologicalSpace X
φ : X → 𝓓^{n}_{K}(E, F)
i : ℕ
hin : ¬↑i ≤ n
⊢ Continuous[inst✝, _] (⇑(structureMapCLM ℝ n i) ∘ φ)
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinLM B μ φ) f = ∫ (x : E) in ↑K, (B (f x)) (φ x) ∂μ

Tactic:
rw [integralAgainstBilinLM_eq_integral hφ, setIntegral_eq_integral_of_forall_compl_eq_zero]
  intro x hx
  rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, zero_apply]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case e_s
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A B : Finset β
x : X
a✝ : β
⊢ a✝ ∈ B ∩ A ↔ a✝ ∈ A ∩ B

Tactic:
simp [and_comm]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
⊢ MemLp f p AddCircle.haarAddCircle ↔ MemLp f p volume

Tactic:
AddCircle.volume_eq_smul_haarAddCircle

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : AddCircle T → ℂ
p : ℝ≥0∞
⊢ MemLp f p AddCircle.haarAddCircle ↔ MemLp f p (ENNReal.ofReal T • AddCircle.haarAddCircle)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k : ℕ
d : ℝ
left✝ : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d
⊢ ∃ c, ∀ᶠ (x : E) in cocompact E, ‖f x‖ ≤ c * ‖‖x‖ ^ (-↑k)‖

Tactic:
refine ⟨d, Filter.Eventually.filter_mono Filter.cocompact_le_cofinite ?_⟩

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k : ℕ
d : ℝ
left✝ : 0 < d
hd' : ∀ (x : E), ‖x‖ ^ k * ‖f x‖ ≤ d
⊢ ∀ᶠ (x : E) in cofinite, ‖f x‖ ≤ d * ‖‖x‖ ^ (-↑k)‖
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case hf
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 f, DifferentiableAt ℝ g x

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 _ _ ↦ (differentiable_fourierChar_neg_bilinear_left _ _).differentiableAt

Goal state after:
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
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
n : ℕ
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀_u : x₀ ∈ u
hu : u ∩ s ⊆ c ⁻¹' Ioi 0
⊢ 0 < μ ((Function.support fun x ↦ c x ^ n) ∩ s)

Tactic:
apply (hμ u u_open x₀_u).trans_le

Goal state after:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := ⋯
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
n : ℕ
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀_u : x₀ ∈ u
hu : u ∩ s ⊆ c ⁻¹' Ioi 0
⊢ μ (u ∩ s) ≤ μ ((Function.support fun x ↦ c x ^ n) ∩ s)
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ x ∈ uᶜ, dist (0 x) (n ^ finrank ℝ F * φ (n • x)) < ε

Tactic:
filter_upwards [Ioi_mem_atTop (M / δ)] with c (hc : M / δ < c) x hx

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
⊢ dist (0 x) (c ^ finrank ℝ F * φ (c • x)) < ε
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: 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
⊢ fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)) w n =
    (fun w ↦
        fourierPowSMulRight (-L.flip)
          (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) fun v ↦ fourierPowSMulRight L f v k) w n)
      w

pp: 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 ≤ N → Integrable (iteratedFDeriv ℝ n fun v ↦ fourierPowSMulRight L f v k) μ

Tactic:
· congr
    rw [iteratedFDeriv_fourierIntegral (N := K) _ _ hf.continuous.aestronglyMeasurable hk]
    intro k hk
    simpa only [norm_iteratedFDeriv_zero] using h'f k 0 hk bot_le

Goal state after:
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 ≤ N → Integrable (iteratedFDeriv ℝ n fun v ↦ fourierPowSMulRight L f v k) μ