mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Finset E
hs : s ∈ K.faces
⊢ (convexHull 𝕜) ↑s ⊆ K.space

Tactic:
convert! subset_biUnion_of_mem hs

Goal state after:
case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide (v +ᵥ y) x ↔ s.SSameSide x y

Tactic:
sSameSide_vadd_left_iff hv,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide y x ↔ s.SSameSide x y
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ G.otherVertexOfIncident h ∈ e

Tactic:
simp [otherVertexOfIncident, Sym2.other_mem']

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

Goal state before:
pp: 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
h : Wbtw ℝ p₁ p₂ p₃
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)

Tactic:
by
  by_cases hp₁ : p₂ = p₁; · simp [hp₁]
  by_cases hp₃ : p₂ = p₃; · simp [hp₃]
  have hs : Sbtw ℝ p₁ p₂ p₃ := ⟨h, hp₁, hp₃⟩
  exact (hs.dist_lt_max_dist _).le

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

Goal state before:
pp: case inl
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y : PE
hxy : dist x y = r * dist x x
hyz : dist y x = (1 - r) * dist x x
this : y -ᵥ x ∈ [0 -[ℝ] x -ᵥ x]
⊢ y = (AffineMap.lineMap x x) r

Tactic:
obtain rfl : y = x := by simpa

Goal state after:
case inl
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
y : PE
hxy : dist y y = r * dist y y
hyz : dist y y = (1 - r) * dist y y
this : y -ᵥ y ∈ [0 -[ℝ] y -ᵥ y]
⊢ y = (AffineMap.lineMap y y) r
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: 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
⊢ ∃ j, i ≠ j ∧ w j ≠ 0

Tactic:
by
    by_contra! hij
    apply hp' i
    rw [← Finset.univ.affineCombination_piSingle ℝ s.points (Finset.mem_univ i)]
    congr 1
    ext j
    obtain rfl | hj := eq_or_ne i j
    · simp only [Pi.single_eq_same]
      rw [← hw, eq_comm]
      exact sum_eq_single i (fun k _ hk ↦ hij k hk.symm) (by simp)
    · rw [Pi.single_eq_of_ne' hj]
      exact hij j hj

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
⊢ UniformConcaveOn s 0 f ↔ ConcaveOn ℝ s f

Tactic:
by
  simp [UniformConcaveOn, ConcaveOn]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : 0 ≤ φ
⊢ ConvexOn ℝ s f

Tactic:
simpa using hf.mono hφ

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : 0 ≤ φ
⊢ ConcaveOn ℝ s f

Tactic:
simpa using hf.mono hφ

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

Goal state before:
pp: case inl
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
h : s = ⊥
⊢ IsPreconnected {y | s.SSameSide x y}

Tactic:
simp only [h, not_sSameSide_bot]

Goal state after:
case inl
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
h : s = ⊥
⊢ IsPreconnected {y | False}
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case inr
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
h : (↑s).Nonempty
⊢ IsPreconnected {y | s.SSameSide x y}

Tactic:
· by_cases hx : x ∈ s
    · simp only [hx, SSameSide, not_true, false_and, and_false]
      exact isPreconnected_empty
    · exact (isConnected_setOfPred_sSameSide hx h).isPreconnected

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

Goal state before:
pp: case inr.refine_1.refine_1
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this✝ : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 ((lineMap x (a i)) ε) ((lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)))
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j)
⊢ ∀ i_1 ∈ t.erase i, 0 ≤ w i_1 / (1 - w i)

Tactic:
intro j hj

Goal state after:
case inr.refine_1.refine_1
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this✝ : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 ((lineMap x (a i)) ε) ((lineMap x (∑ j ∈ t, w j • a j)) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)))
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j)
j : ι
hj : j ∈ t.erase i
⊢ 0 ≤ w j / (1 - w i)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

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
⊢ HasTemperateGrowth f ↔ ContDiff ℝ ∞ f ∧ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * ‖(1 + ‖x‖) ^ k‖

Tactic:
congrm ContDiff ℝ ∞ f ∧ (∀ n, ∃ k C, ∀ x, _ ≤ C * ?_)

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
n k : ℕ
C : ℝ
x : E
⊢ (1 + ‖x‖) ^ k = ‖(1 + ‖x‖) ^ k‖
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
f_bdd : f ≤ᵐ[μ] fun x ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ ∀ᵐ (a : α) ∂μ, a ∉ {a | M < f a}

Tactic:
filter_upwards [f_bdd] with a ha using not_lt.mpr ha

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
n : ℕ∞
m : MeasurableSpace E
inst✝⁷ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝⁶ : NormedAddCommGroup F₁
inst✝⁵ : NormedSpace 𝕜 F₁
inst✝⁴ : NormedSpace ℝ F₁
inst✝³ : NormedAddCommGroup F₂
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedAddCommGroup F₃
inst✝ : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω) μ
f : 𝓓^{n}(Ω, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (tsupport ⇑f) μ
x : E
hx : x ∈ support fun x ↦ (B (f x)) (φ x)
hfx : f x = 0
⊢ (fun x ↦ (B (f x)) (φ x)) x = 0

Tactic:
by simp [hfx]

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

Goal state before:
pp: case h
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
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ * ‖x ^ (r - ↑n)‖ ≤
    (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k

Tactic:
gcongr 1

Goal state after:
case h₁
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := ⋯
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
⊢ ‖Polynomial.eval r (descPochhammer ℝ n)‖ ≤ ∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖

case h₂
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := ⋯
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
⊢ ‖x ^ (r - ↑n)‖ ≤ (1 + ‖x‖) ^ k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: 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
⊢ Real.exp (Real.log 2 * (↑n - r)) ≤ Real.exp (Real.log (3 / 2) * ↑k)

Tactic:
gcongr 1

Goal state after:
case a
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := ⋯
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
⊢ Real.log 2 * (↑n - r) ≤ Real.log (3 / 2) * ↑k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h₁
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
⊢ 1 ≤ ((1 + x) / 2) ^ (-↑l)

Tactic:
apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos

Goal state after:
case h₁.hx1
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
⊢ 0 < (1 + x) / 2

case h₁.hx2
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
⊢ (1 + x) / 2 ≤ 1

case h₁.hz
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
⊢ -↑l ≤ 0
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
⊢ ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : E), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)

Tactic:
by
  rw [← integral_const_mul, ← integral_mul_const]
  apply integral_mono_of_nonneg
  · filter_upwards with v using by positivity
  · exact ((integrable_pow_neg_integrablePower μ).const_mul _).mul_const _
  filter_upwards with v
  exact (pow_mul_le_of_le_of_pow_mul_le (norm_nonneg _) (norm_nonneg _) (hf v) (h'f v)).trans
    (le_of_eq (by ring))

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : End R M
μ : R
⊢ (-1) ^ finrank R M * (f - μ • 1).charpoly.coeff 0 = 0 ↔ (charpoly f).IsRoot μ

Tactic:
simp [Polynomial.coeff_zero_eq_eval_zero, charpoly_sub_smul]

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
i : n
⊢ hA.eigenvalues i ∈ spectrum ℝ A

Tactic:
apply spectrum.of_algebraMap_mem 𝕜

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
i : n
⊢ (algebraMap ℝ 𝕜) (hA.eigenvalues i) ∈ spectrum 𝕜 A
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
x : ↑(spectrum ℝ a)
⊢ f x ∈ spectrum ℝ (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))

Tactic:
apply spectrum.of_algebraMap_mem 𝕜

Goal state after:
case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
x : ↑(spectrum ℝ a)
⊢ (algebraMap ℝ 𝕜) (f x) ∈ spectrum 𝕜 (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
H₁ : v ∈ eigenspace T μ
⊢ HasEigenvector T μ v

Tactic:
have H₂ : v ≠ 0 := by simpa using (hT.unsortedEigenvectorBasis hn).toBasis.ne_zero i

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
H₁ : v ∈ eigenspace T μ
H₂ : v ≠ 0
⊢ HasEigenvector T μ v
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)
⊢ ⇑((fderivLM 𝕜 n k) f) = if k + 1 ≤ n then fderiv ℝ ⇑f else 0

Tactic:
fderivLM

Goal state after:
𝕜 : 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)
⊢ ⇑({ toFun := fun f ↦ if hk : k + 1 ≤ n then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0, map_add' := ⋯,
          map_smul' := ⋯ }
        f) =
    if k + 1 ≤ n then fderiv ℝ ⇑f else 0
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
hT' : (↑T).IsSymmetric
S : ↥(⨆ μ, eigenspace (↑T) μ)ᗮ →L[𝕜] ↥(⨆ μ, eigenspace (↑T) μ)ᗮ := T.restrict ⋯
hS_compact : IsCompactOperator ⇑S
hS_symm : (↑S).IsSymmetric
hS : ∀ (μ : 𝕜), eigenspace (↑S) μ = ⊥
h : S = 0
⊢ (⨆ μ, eigenspace (↑T) μ)ᗮ = ⊥

Tactic:
← Submodule.subsingleton_iff_eq_bot

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
hT' : (↑T).IsSymmetric
S : ↥(⨆ μ, eigenspace (↑T) μ)ᗮ →L[𝕜] ↥(⨆ μ, eigenspace (↑T) μ)ᗮ := T.restrict ⋯
hS_compact : IsCompactOperator ⇑S
hS_symm : (↑S).IsSymmetric
hS : ∀ (μ : 𝕜), eigenspace (↑S) μ = ⊥
h : S = 0
⊢ Subsingleton ↥(⨆ μ, eigenspace (↑T) μ)ᗮ
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : ∫ (x : α), ⟪∫ (x : α), f x ∂μ, f x⟫ ∂μ = 0
⊢ ∫ (x : α), f x ∂μ = 0

Tactic:
integral_inner hf,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : ⟪∫ (x : α), f x ∂μ, ∫ (x : α), f x ∂μ⟫ = 0
⊢ ∫ (x : α), f x ∂μ = 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
⊢ abs a = cfcₙ (fun z ↦ ↑‖z‖) a

Tactic:
rw [abs, sqrt_eq_iff _ _ (hb := cfcₙ_norm_nonneg _ _), ← cfcₙ_mul ..]
  conv_rhs => rw [← cfcₙ_id' 𝕜 a, ← cfcₙ_star, ← cfcₙ_mul ..]
  simp [RCLike.conj_mul, sq]

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

Goal state before:
pp: 𝕜 : 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 : ℕ∞
K : Compacts E
inst✝ : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F' n K i) ((postcompLM T) f) ≤
    ‖T‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f

Tactic:
by
  set T' := T.restrictScalars ℝ
  change N[ℝ]_{K, n, i} (postcompLM T' f) ≤ ‖T'‖ * N[ℝ]_{K, n, i} f
  rw [ContDiffMapSupportedIn.seminorm_le_iff ℝ (by positivity)]
  intro hi x hx
  rw [postcompLM_apply]
  calc
      ‖iteratedFDeriv ℝ i (T' ∘ f) x‖
  _ = ‖T'.compContinuousMultilinearMap (iteratedFDeriv ℝ i f x)‖ := by
        rw [T'.iteratedFDeriv_comp_left f.contDiff.contDiffAt (mod_cast hi)]
  _ ≤ ‖T'‖ * ‖iteratedFDeriv ℝ i f x‖ := T'.norm_compContinuousMultilinearMap_le _
  _ ≤ ‖T'‖ * N[ℝ]_{K, n, i} f := by grw [norm_iteratedFDeriv_apply_le_seminorm ℝ hi]

Goal state after:
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (↑K) μ
x : E
hx : x ∈ support fun x ↦ (B (f x)) (φ x)
hfx : f x = 0
⊢ (fun x ↦ (B (f x)) (φ x)) x = 0

Tactic:
by simp [hfx]

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✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
x : α
⊢ ‖g x‖ = g x

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (x : AddCircle T), ‖↑↑f x‖ ^ 2 ∂haarAddCircle
⊢ HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)

Tactic:
rwa [H₂, H₃] at H₁

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i ↦ ‖fourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)

Tactic:
by
  simp_rw [← fourierBasis_repr]
  have H₁ : HasSum (fun i => ‖fourierBasis.repr f i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2) := by
    apply_mod_cast lp.hasSum_norm ?_ (fourierBasis.repr f)
    simp
  have H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp
  have H₃ := congr_arg RCLike.re (@L2.inner_def (AddCircle T) ℂ ℂ _ _ _ _ _ f f)
  rw [← integral_re] at H₃
  · simp only [← norm_sq_eq_re_inner] at H₃
    rwa [H₂, H₃] at H₁
  · exact L2.integrable_inner f f

Goal state after:
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:
inner_self_eq_norm_sq_to_K,

Goal state after:
case inl
T : ℝ
hT : Fact (0 < T)
m : ℤ
⊢ ↑‖fourierLp 2 m‖ ^ 2 = Pi.single m 1 m