mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case e'_3
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ∞
⊢ ∫ (t : ℝ) in Ioi 0, μ.real {a | t < f a} = (∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}).toReal

Tactic:
· have aux := @integral_eq_lintegral_of_nonneg_ae _ _ ((volume : Measure ℝ).restrict (Set.Ioi 0))
      (fun t ↦ μ.real {a : α | t < f a}) ?_ ?_
    · rw [aux]
      congr 1
      apply setLIntegral_congr_fun measurableSet_Ioi
      exact fun t t_pos ↦ ENNReal.ofReal_toReal (rhs_integrand_finite t t_pos).ne
    · exact Eventually.of_forall (fun x ↦ by positivity)
    · apply Measurable.aestronglyMeasurable
      refine Measurable.ennreal_toReal ?_
      exact Antitone.measurable (fun _ _ hst ↦ measure_mono (fun _ h ↦ lt_of_le_of_lt hst h))

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

Goal state before:
pp: case zero
R : Type u_3
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedRing R
inst✝ : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth (f ^ 0)

Tactic:
simpa only [pow_zero] using! HasTemperateGrowth.const 1

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
x : E
hx : ¬x = 0
this : T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - c ^ 2 / (2 * t)
⊢ T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t))

Tactic:
this,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
x : E
hx : ¬x = 0
this : T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - c ^ 2 / (2 * t)
⊢ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - c ^ 2 / (2 * t) ≤
    (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t))
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case neg
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 : r - ↑n < 0
⊢ |x| ^ (r - ↑n) ≤ (1 + |x|) ^ k

Tactic:
have h : 0 < n - r := by grind

Goal state after:
case neg
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✝ : r - ↑n < 0
h : 0 < ↑n - r
⊢ |x| ^ (r - ↑n) ≤ (1 + |x|) ^ k
Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
f : End K V
μ : K
⊢ f.HasEigenvalue μ ↔ (charpoly f).IsRoot μ

Tactic:
hasEigenvalue_iff_isRoot_charpoly

Goal state after:
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
f : End K V
μ : K
⊢ (charpoly f).IsRoot μ ↔ (charpoly f).IsRoot μ
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
hK : ∀ K > 0, ∃ x, ‖(T - μ • 1) x‖ < K * ‖x‖
⊢ HasEigenvalue (↑T) μ

Tactic:
replace hK : ∃ c > 0, ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε := by
    obtain ⟨C, hC⟩ := NormedField.exists_one_lt_norm 𝕜
    refine ⟨‖C‖⁻¹, by positivity, fun ε hε ↦ ?_⟩
    obtain ⟨x, hx⟩ := hK ε (by positivity)
    have : x ≠ 0 := by aesop
    obtain ⟨η, hη, h₁, h₂, h₃⟩ := rescale_to_shell hC (ε := 1) (by simp) this
    refine ⟨η • x, h₁.le, by simpa using h₂, ?_⟩
    grw [map_smul, norm_smul, hx, mul_left_comm, ← norm_smul]
    linear_combination ε * h₁

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
hK : ∃ c > 0, ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
⊢ HasEigenvalue (↑T) μ
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K✝ : NNReal
hK✝ : AntilipschitzWith K✝ ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 (‖c‖ + 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : CauchySeq ((fun n ↦ ↑T (f n)) ∘ ψ)
⊢ False

Tactic:
Metric.cauchySeq_iff'

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K✝ : NNReal
hK✝ : AntilipschitzWith K✝ ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 (‖c‖ + 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (((fun n ↦ ↑T (f n)) ∘ ψ) n) (((fun n ↦ ↑T (f n)) ∘ ψ) N) < ε
⊢ False
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
⊢ A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues₀) Finset.univ.val

Tactic:
rw [hA.roots_charpoly_eq_eigenvalues]

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
⊢ Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) Finset.univ.val =
    Multiset.map (RCLike.ofReal ∘ hA.eigenvalues₀) Finset.univ.val
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this : (∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
hi : ↑i ≤ n
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
simp [hi, forall_const, ContDiffMapSupportedIn.seminorm_apply, structureMapCLM_apply,
      BoundedContinuousFunction.norm_le hC, this]

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsSelfAdjoint A
⊢ Isometry ⇑(cfcHom hA)

Tactic:
← isHermitian_iff_isSelfAdjoint

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
⊢ Isometry ⇑(cfcHom hA✝)
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') ?m.157 μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
⊢ eLpNorm (f - g') p μ ≤ ENNReal.ofReal ε

Tactic:
this,

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
g : E → F
hg₁ : HasCompactSupport g
hg₂ : eLpNorm (f - g) p μ ≤ ENNReal.ofReal (ε / 2)
hg₃ : Continuous g
hg₄ : MemLp g p μ
g' : E → F
hg'₁ : HasCompactSupport g'
hg'₂ : ContDiff ℝ ∞ g'
hg'₃ : eLpNorm (g - g') ?m.157 μ ≤ ENNReal.ofReal (ε / 2)
this : f - g' = f - g - (g' - g)
⊢ eLpNorm (f - g - (g' - g)) p μ ≤ ENNReal.ofReal ε
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
b : SchauderBasis 𝕜 X
⊢ b.proj 0 = 0

Tactic:
rw [proj, Finset.range_zero, GeneralSchauderBasis.proj_empty]

Goal state after:
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✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g,
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ

Tactic:
suffices H :
      ∃ g : α → E, eLpNorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MemLp g p μ ∧ HasCompactSupport g by
    rcases H with ⟨g, hg, g_cont, g_mem, g_support⟩
    exact ⟨g, g_support, hg, g_cont, g_mem⟩
  -- It suffices to check that the set of functions we consider approximates characteristic
  -- functions, is stable under addition and consists of ae strongly measurable functions.
  -- First check the latter easy facts.
  apply hf.induction_dense hp _ _ _ _ hε
  rotate_left
  -- stability under addition
  · rintro f g ⟨f_cont, f_mem, hf⟩ ⟨g_cont, g_mem, hg⟩
    exact ⟨f_cont.add g_cont, f_mem.add g_mem, hf.add hg⟩
  -- ae strong measurability
  · rintro f ⟨_f_cont, f_mem, _hf⟩
    exact f_mem.aestronglyMeasurable
  -- We are left with approximating characteristic functions.
  -- This follows from `exists_continuous_eLpNorm_sub_le_of_closed`.
  intro c t ht htμ ε hε
  rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩
  obtain ⟨η, ηpos, hη⟩ :
      ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → eLpNorm (s.indicator fun _x => c) p μ ≤ δ :=
    exists_eLpNorm_indicator_le hp c δpos.ne'
  have hη_pos' : (0 : ℝ≥0∞) < η := ENNReal.coe_pos.2 ηpos
  obtain ⟨s, st, s_compact, s_closed, μs⟩ :
      ∃ s, s ⊆ t ∧ IsCompact s ∧ IsClosed s ∧ μ (t \ s) < η :=
    ht.exists_isCompact_isClosed_sdiff_lt htμ.ne hη_pos'.ne'
  have hsμ : μ s < ∞ := (measure_mono st).trans_lt htμ
  have I1 : eLpNorm ((s.indicator fun _y => c) - t.indicator fun _y => c) p μ ≤ δ := by
    rw [← eLpNorm_neg, neg_sub, ← indicator_sdiff st]
    exact hη _ μs.le
  obtain ⟨k, k_compact, sk⟩ : ∃ k : Set α, IsCompact k ∧ s ⊆ interior k :=
    exists_compact_superset s_compact
  rcases exists_continuous_eLpNorm_sub_le_of_closed hp s_closed isOpen_interior sk hsμ.ne c δpos.ne'
    with ⟨f, f_cont, I2, _f_bound, f_support, f_mem⟩
  have I3 : eLpNorm (f - t.indicator fun _y => c) p μ ≤ ε := by
    convert!
      (hδ _ _
          (f_mem.aestronglyMeasurable.sub
            (aestronglyMeasurable_const.indicator s_closed.measurableSet))
          ((aestronglyMeasurable_const.indicator s_closed.measurableSet).sub
            (aestronglyMeasurable_const.indicator ht))
          I2 I1).le using 2
    simp only [sub_add_sub_cancel]
  refine ⟨f, I3, f_cont, f_mem, HasCompactSupport.intro k_compact fun x hx => ?_⟩
  rw [← Function.notMem_support]
  contrapose hx
  exact interior_subset (f_support hx)

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

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := ⋯
V : Submodule 𝕜 X := ⋯
W : Submodule 𝕜 X := ⋯
hV : V ≤ W
hUW : U ≤ W
⊢ W ≤ U ⊔ V

Tactic:
rintro x ⟨y, hy⟩

Goal state after:
case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
x y : X
hy : ↑(P (n + 1)) y = x
⊢ x ∈ U ⊔ V
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: case hf
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ i ∈ Finset.univ,
    Integrable (fun x ↦ (L ((∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} f)) x)) (g x)) μ

pp: case hf
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ i ∈ Finset.univ,
    Integrable (fun x ↦ (L (f x)) ((∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} g)) x)) μ

Tactic:
· exact fun _ _ ↦ (pairing L (∂_{_} <| ∂_{_} f) g).integrable

Goal state after:
case hf
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ i ∈ Finset.univ,
    Integrable (fun x ↦ (L (f x)) ((∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} g)) x)) μ
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case inl
T : ℝ
hT : Fact (0 < T)
m : ℤ
⊢ inner ℂ (fourierLp 2 m) (fourierLp 2 m) = Pi.single m 1 m

Tactic:
rw [inner_self_eq_norm_sq_to_K, (orthonormal_fourier (hT := hT)).1 m]

Goal state after:
case inl
T : ℝ
hT : Fact (0 < T)
m : ℤ
⊢ ↑1 ^ 2 = Pi.single m 1 m
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
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
by
  rw [← mul_add]
  gcongr _ * ?_
  rw [iteratedFDeriv_add_apply (f.smooth _).contDiffAt (g.smooth _).contDiffAt]
  exact norm_add_le _ _

Goal state after:
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)
⊢ Function.HasTemperateGrowth ⇑f

Tactic:
by
  refine ⟨smooth f ⊤, fun n => ?_⟩
  rcases f.decay 0 n with ⟨C, Cpos, hC⟩
  exact ⟨0, C, by simpa using hC⟩

Goal state after:
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 μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact 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₀ ∈ closure[inst✝⁷] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
⊢ Tendsto (fun n ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
apply
    tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos hs _ hc
      h'c hnc hnc₀ this hmg hcg

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 μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact 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₀ ∈ closure[inst✝⁷] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
⊢ ∀ (u : Set α), IsOpen[inst✝⁷] u → x₀ ∈ u → 0 < μ (u ∩ s)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case right
ι : 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
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' : ∀ (N : ℕ), 1 ≤ N → N ≤ n → ‖iteratedFDeriv ℝ N g x‖ ≤ ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this : ‖iteratedFDeriv ℝ n (⇑f ∘ g) x‖ ≤ ↑n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (⇑f ∘ g) x‖ ≤
    (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * ↑n ! * 2 ^ k') * ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
have hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k :=
    pow_le_pow_left₀ (norm_nonneg _) (by simp only [zero_le_one, le_add_iff_nonneg_left]) _

Goal state after:
case right
ι : 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
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' : ∀ (N : ℕ), 1 ≤ N → N ≤ n → ‖iteratedFDeriv ℝ N g x‖ ≤ ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this : ‖iteratedFDeriv ℝ n (⇑f ∘ g) x‖ ≤ ↑n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (⇑f ∘ g) x‖ ≤
    (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * ↑n ! * 2 ^ k') * ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x ↦ -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂volume = ∫ (x : ℝ) in (fun x ↦ -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ici (-c), f x

Tactic:
this,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x ↦ -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂volume = ∫ (x : ℝ) in (fun x ↦ -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in (fun x ↦ -x) ⁻¹' Ici (-c), f (-x)
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < 0
c : ℝ
this : Tendsto (fun x ↦ Complex.exp (a * ↑x)) atTop (𝓝 0)
⊢ Tendsto (fun i ↦ (Complex.exp (a * ↑i) - Complex.exp (a * ↑c)) / a) atTop (𝓝 (-Complex.exp (a * ↑c) / a))

Tactic:
simpa using this.sub_const _ |>.div_const _

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

Goal state before:
pp: s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
⊢ False

Tactic:
have : IntegrableOn (fun x ↦ x⁻¹) (Ioi (max 1 t)) := by
    apply H'.mono' measurable_inv.aestronglyMeasurable
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
    have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le
    simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]
    rw [← Real.rpow_neg_one x]
    exact Real.rpow_le_rpow_of_exponent_le x_one h

Goal state after:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
this : IntegrableOn (fun x ↦ x⁻¹) (Ioi (max 1 t)) volume
⊢ False