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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ M ∈ doublyStochastic R n ↔ M ∈ rowStochastic R n ∧ M ∈ colStochastic R n

Tactic:
doublyStochastic_eq_rowStochastic_inf_colStochastic,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ M ∈ rowStochastic R n ⊓ colStochastic R n ↔ M ∈ rowStochastic R n ∧ M ∈ colStochastic R n
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:

Tactic:
_ ≤ 0 := by
          apply mul_nonpos_of_nonneg_of_nonpos
          · apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)
          · simpa only [s, mem_filter, het, true_and, not_lt] using hes
        _ ≤ f e := fpos e het

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

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✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
by
  rcases le_total r₁ r₂ with (h | h)
  · exact Or.inl (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₁ h)
  · exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₂ h)

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ Set.Ioo (min (x₁ i j) (x₂ i j)) (max (x₁ i j) (x₂ i j)) ⊆ Set.Ioo 0 1

Tactic:
apply Set.Ioo_subset_Ioo <;>
    simp_all [nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic]

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

Goal state before:
pp: case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ico y z
hyx : y < x
h : ContinuousWithinAt f (Ioo y z) x
⊢ ContinuousWithinAt f (Ico y z) x

Tactic:
continuousWithinAt_iff_continuousAt (Ioo_mem_nhds hyx hx.2)

Goal state after:
case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ico y z
hyx : y < x
h : ContinuousAt f x
⊢ ContinuousWithinAt f (Ico y z) x
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
w : StdSimplex K X
p : X → Prop
inst✝ : DecidablePred p
hp : ∃ a, p a ∧ w.weights a ≠ 0
⊢ filter p w.weights ≠ 0

Tactic:
by simpa [ne_iff, filter_apply]

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
J : Type u_7
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s : StdSimplex R I
f : I → J
g : J → M
⊢ iConvexComb (map f s) g = iConvexComb s fun i ↦ g (f i)

Tactic:
by
  simp only [iConvexComb, map_map]

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:
simp_rw [SSameSide, hf.wSameSide_map_iff, mem_map_iff_mem_of_injective hf]

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ↑a + ↑b = 1

Tactic:
by simp; norm_cast

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

Goal state before:
pp: V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, ‖p i -ᵥ p₀‖ ≤ r
⊢ ‖∑ i ∈ t, w i • (p i -ᵥ p₀)‖ < r

Tactic:
exact norm_sum_lt_of_strictConvexSpace h0 h1 hi hj (by simpa using hij) hi0 hj0 hp

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

Goal state before:
pp: case e_6.inl
V : Type u_2
P : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)), i ≠ j → w j = 0
⊢ w i = Pi.single i 1 i

Tactic:
simp only [Pi.single_eq_same]

Goal state after:
case e_6.inl
V : Type u_2
P : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points) w ≠ s.points i
i : Fin (n + 1)
hi : w i ≠ 0
hij : ∀ (j : Fin (n + 1)), i ≠ j → w j = 0
⊢ w i = 1
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case pos
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty ↥s
hx : x ∈ s
⊢ IsConnected {y | s.WOppSide x y}

pp: case neg
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty ↥s
hx : x ∉ s
⊢ IsConnected {y | s.WOppSide x y}

Tactic:
· simp only [wOppSide_of_left_mem, hx]
    have := AddTorsor.connectedSpace V P
    exact isConnected_univ

Goal state after:
case neg
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty ↥s
hx : x ∉ s
⊢ IsConnected {y | s.WOppSide x y}
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ↑‖holder r B f g‖₊ ≤ ↑(‖B‖₊ * ‖f‖₊ * ‖g‖₊)

Tactic:
ENNReal.coe_mul,

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ ↑‖holder r B f g‖₊ ≤ ↑‖B‖₊ * ↑‖f‖₊ * ↑‖g‖₊
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∉ Ioc 0 (f p_fst)
⊢ (Ioc 0 (f p_fst)).indicator (fun t ↦ ENNReal.ofReal (g t)) p_snd =
    {p | p.2 ∈ Ioc 0 (f p.1)}.indicator (fun p ↦ ENNReal.ofReal (g p.2)) (p_fst, p_snd)

Tactic:
have h' : (p_fst, p_snd) ∉ {p : α × ℝ | p.snd ∈ Ioc 0 (f p.fst)} := h
      rw [Set.indicator_of_notMem h', Set.indicator_of_notMem h]

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
i : ℕ
hi : i ≤ n
⊢ C₂ * (‖f x‖ + 1) ^ k₂ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * ↑(k₂.choose i))

Tactic:
add_pow,

Goal state after:
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
i : ℕ
hi : i ≤ n
⊢ C₂ * ∑ m ∈ Finset.range (k₂ + 1), ‖f x‖ ^ m * 1 ^ (k₂ - m) * ↑(k₂.choose m) =
    ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * ↑(k₂.choose i))
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
hk : k + 1 ≤ n
⊢ ⇑((fderivCLM 𝕜 n k) f) = fderiv ℝ ⇑f

Tactic:
by
  simp [hk]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
⊢ ((lineDerivCLM 𝕜 v) f) x = lineDeriv ℝ (⇑f) x v

Tactic:
by
  simp [hk]

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
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
hT'' : -(algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε
ε' : ℝ
hε'0 : ε' > 0
hε' : ∀ (x : E), (-T).rayleighQuotient x ≤ ‖-T‖ - ε'
x : E
⊢ |T.rayleighQuotient x| ≤ ‖T‖ - min ε ε'

Tactic:
grind [rayleighQuotient_neg_apply, norm_neg]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
R : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : BorelSpace E
μ : Measure E
h : μ.IsAddHaarMeasure
⊢ Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑(finrank ℝ E + 1))) μ

Tactic:
apply integrable_one_add_norm

Goal state after:
ι : Type u_1
𝕜 : Type u_2
R : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : BorelSpace E
μ : Measure E
h : μ.IsAddHaarMeasure
⊢ ↑(finrank ℝ E) < ↑(finrank ℝ E + 1)
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case e'_12
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
e_8✝ : Real.instAddCommGroup = Real.instRCLike.toDivisionRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ toInnerProductSpaceReal.toModule
y : F
⊢ 2 • ((innerSL ℝ) (T x₀)) y =
    ⟪(T x₀, id x₀).1, (T y, (ContinuousLinearMap.id ℝ F) y).2⟫_ℝ +
      ⟪(T y, (ContinuousLinearMap.id ℝ F) y).1, (T x₀, id x₀).2⟫_ℝ

Tactic:
innerSL_apply_apply,

Goal state after:
case e'_12
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
T : F →L[ℝ] F
hT : (↑T).IsSymmetric
x₀ : F
e_8✝ : Real.instAddCommGroup = Real.instRCLike.toDivisionRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ toInnerProductSpaceReal.toModule
y : F
⊢ 2 • ⟪T x₀, y⟫_ℝ =
    ⟪(T x₀, id x₀).1, (T y, (ContinuousLinearMap.id ℝ F) y).2⟫_ℝ +
      ⟪(T y, (ContinuousLinearMap.id ℝ F) y).1, (T x₀, id x₀).2⟫_ℝ
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case coe.inr
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
⊢ ∃ k, eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ∞

Tactic:
| inr hp =>

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst✝ : RCLike 𝕜
h : A.IsHermitian
i : n
⊢ ↑(re (A i i)) = A i i

Tactic:
← conj_eq_iff_re,

Goal state after:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst✝ : RCLike 𝕜
h : A.IsHermitian
i : n
⊢ (starRingEnd 𝕜) (A i i) = A i i
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
j : n
⊢ A *ᵥ (hA.eigenvectorBasis j).ofLp = hA.eigenvalues j • (hA.eigenvectorBasis j).ofLp

Tactic:
simpa only [eigenvectorBasis, OrthonormalBasis.reindex_apply, toLpLin_apply,
    RCLike.real_smul_eq_coe_smul (K := 𝕜)] using!
      congr(⇑$((isSymmetric_toEuclideanLin_iff.mpr hA).apply_eigenvectorBasis
        finrank_euclideanSpace ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm j)))

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

Goal state before:
pp: 𝕜 : 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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ ⇑((fderivLM 𝕜 n k) f) = fderiv ℝ ⇑f

Tactic:
by
  simp [hk]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : k + ↑i ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : ¬k + ↑i ≤ n
⊢ 0 = 0 + 0

Tactic:
· have hi' : (i : ℕ∞ω) ≤ n := mod_cast (le_of_add_le_right hi)
      ext
      simp [iteratedFDeriv_add (f.contDiff.of_le hi') (g.contDiff.of_le hi'), FunLike.coe_add]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
i : ℕ
f g : 𝓓^{n}_{K}(E, F)
hi : ¬k + ↑i ≤ n
⊢ 0 = 0 + 0
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace ℝ F
inst✝¹⁶ : NormedSpace 𝕜 F
inst✝¹⁵ : SMulCommClass ℝ 𝕜 F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ 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₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ∫ (x : E), (B ((c • f) x)) (φ x) ∂μ = (RingHom.id 𝕜) c • ∫ (x : E), (B (f x)) (φ x) ∂μ

pp: case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace ℝ F
inst✝¹⁶ : NormedSpace 𝕜 F
inst✝¹⁵ : SMulCommClass ℝ 𝕜 F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ 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₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : ¬IntegrableOn φ (↑K) μ
⊢ 0 = (RingHom.id 𝕜) c • 0

Tactic:
· simp_rw [smul_apply, map_smul, smul_apply, integral_smul c, RingHom.id_apply]

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : NormedSpace ℝ F
inst✝¹⁶ : NormedSpace 𝕜 F
inst✝¹⁵ : SMulCommClass ℝ 𝕜 F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ 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₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : ¬IntegrableOn φ (↑K) μ
⊢ 0 = (RingHom.id 𝕜) c • 0
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ (fourier n) ↑x = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
rw [fourier_apply, ← QuotientAddGroup.mk_zsmul, toCircle, Function.Periodic.lift_coe,
    Circle.coe_exp, Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_mul, zsmul_eq_mul,
    Complex.ofReal_mul, Complex.ofReal_intCast]

Goal state after:
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (↑2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ hV.linearIsometry.range = (⨆ i, (V i).range).topologicalClosure

Tactic:
refine le_antisymm ?_ ?_
  · rintro x ⟨f, rfl⟩
    refine mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (Eventually.of_forall ?_)
    intro s
    rw [SetLike.mem_coe]
    refine sum_mem ?_
    intro i _
    refine mem_iSup_of_mem i ?_
    exact LinearMap.mem_range_self _ (f i)
  · apply topologicalClosure_minimal
    · refine iSup_le ?_
      rintro i x ⟨x, rfl⟩
      use lp.single 2 i x
      exact hV.linearIsometry_apply_single x
    exact hV.linearIsometry.isometry.isUniformInducing.isComplete_range.isClosed

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

Goal state before:
pp: case e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ ⟪x, b i⟫ * ⟪b i, y⟫ = ((innerSL 𝕜) x) (↑(b.repr y) i • b i)

Tactic:
innerSL_apply_apply,

Goal state after:
case e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, ↑(b.repr y) i • b i⟫
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
⊢ fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Tactic:
have := Fact.mk (by linarith : 0 < b - a)
  rw [fourierCoeffOn, fourierCoeff_eq_intervalIntegral _ _ a, add_sub, add_sub_cancel_left]
  congr 1
  simp_rw [intervalIntegral.integral_of_le hab.le]
  refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_
  rw [liftIoc_coe_apply]
  rwa [add_sub, add_sub_cancel_left]

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

Goal state before:
pp: case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ uIoc a (a + T)
⊢ x ∈ Ioc a (a + T)

Tactic:
rwa [uIoc_of_le (lt_add_of_pos_right a hT.out).le] at hx

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ inner ℂ (fourierBasis i) f = ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle

Tactic:
MeasureTheory.L2.inner_def,

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (a : AddCircle T), inner ℂ (↑↑(fourierBasis i) a) (↑↑f a) ∂haarAddCircle =
    ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle