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

Goal state before:
pp: case e_a
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
a : X
⊢ (StdSimplex.duple x y hs' ht' h').weights a = (StdSimplex.map ![x, y, y] f).weights a

Tactic:
simp [StdSimplex.duple, StdSimplex.map, Finsupp.mapDomain,
      Finsupp.sum_fintype, Fin.sum_univ_succ, f, show t' = s - s' + t by grind]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
S : F
w : StdSimplex R ↥S
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
ext; simp [Finsupp.sum]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
I : Type u_5
inst✝¹⁷ : Semiring R
inst✝¹⁶ : PartialOrder R
inst✝¹⁵ : IsStrictOrderedRing R
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R M✝
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : SetLike F M✝
inst✝⁹ : AddSubmonoidClass F M✝
inst✝⁸ : SMulMemClass F R M✝
f g : M✝ → N
inst✝⁷ : ConvexSpace R M✝
inst✝⁶ : IsModuleConvexSpace R M✝
inst✝⁵ : ConvexSpace R N
inst✝⁴ : IsModuleConvexSpace R N
x y : M✝
s t : Set M✝
a b : R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → ConvexSpace R (M i)
inst✝ : ∀ (i : ι), IsModuleConvexSpace R (M i)
w : StdSimplex R ((i : ι) → M i)
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
ext; simp [Finsupp.sum]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
ι : Type u_6
w : StdSimplex R (ι →₀ M)
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
ext; simp [Finsupp.sum]

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: 𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)

Tactic:
by
    apply subset_of_eq
    rw [AffineIndependent.convexHull_inter (R := 𝕜) (s := s ∪ t)]
    · apply indep.mono
      simp only [Finset.coe_union]
      exact Set.union_subset (Set.subset_biUnion_of_mem hs) (Set.subset_biUnion_of_mem ht)
    · exact Finset.subset_union_left
    · exact Finset.subset_union_right

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

Goal state before:
pp: V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ Disjoint G₁ G₂

Tactic:
disjoint_iff_inf_le,

Goal state after:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
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.WSameSide x y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s

Tactic:
vadd_mem_iff_mem_of_mem_direction 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.WSameSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ 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.WOppSide x y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s

Tactic:
vadd_mem_iff_mem_of_mem_direction 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.WOppSide x y ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide x y ∧ x ∉ s ∧ y ∉ s
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: case «0»
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
⊢ 0 ≤ w ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
exact mul_nonneg (mul_nonneg haz hav) hbu

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✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : y ∉ s
⊢ s.SOppSide y ((pointReflection R x) y)

Tactic:
by
  refine (sbtw_pointReflection_of_ne R fun h => hy ?_).sOppSide_of_notMem_of_mem hy hx
  rwa [← h]

Goal state after:
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.Side

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

Tactic:
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
  · rw [coe_eq_bot_iff] at h
    simp only [h, not_sSameSide_bot]
    exact isPreconnected_empty
  · 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.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.SOppSide x y}

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

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

Goal state before:
pp: case neg
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₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
⊢ SignType.sign (w₁ i) = SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0

Tactic:
exact .inl ((s.sSameSide_affineSpan_faceOpposite_iff hw₁ hw₂).1 ⟨h,
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 h0,
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.2 h0'⟩).1

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : 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)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * ∫⁻ (a : α), (Ici s).indicator (fun x ↦ 1) (f a) ∂μ =
    (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s

Tactic:
show
        (fun a => (Ici s).indicator (fun _ : ℝ => (1 : ℝ≥0∞)) (f a)) = fun a =>
          {a : α | s ≤ f a}.indicator (fun _ => 1) a
        by funext a; by_cases h : s ≤ f a <;> simp [h]

Goal state after:
α : 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)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * ∫⁻ (a : α), {a | s ≤ f a}.indicator (fun x ↦ 1) a ∂μ =
    (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) s
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
by_cases H1 : g =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᵐ[volume.restrict (Ioi 0)] 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t ↦ μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := μ (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ -r⁻¹ ≤ 0

Tactic:
by simp [hr.le]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
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
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᵐ[volume.restrict (Ioi 0)] 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have A : ∫⁻ ω, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ = 0 := by
      have : ∀ ω, ∫ t in 0..f ω, g t = ∫ t in 0..f ω, 0 := by
        intro ω
        simp_rw [intervalIntegral.integral_of_le (f_nonneg ω)]
        apply integral_congr_ae
        exact ae_restrict_of_ae_restrict_of_subset Ioc_subset_Ioi_self H1
      simp [this]
    have B : ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) = 0 := by
      have : (fun t ↦ μ {a : α | t ≤ f a} * ENNReal.ofReal (g t))
        =ᵐ[volume.restrict (Ioi (0 : ℝ))] 0 := by
          filter_upwards [H1] with t ht using by simp [ht]
      simp [lintegral_congr_ae this]
    rw [A, B]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕂 : Type u_2
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
F' : Type u_5
inst✝¹¹ : NormedAddCommGroup F'
inst✝¹⁰ : NormedSpace ℝ F'
inst✝⁹ : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
toFun : 𝓓^{n}(Ω, F) → V
T : (K : Compacts E) → ↑K ⊆ ↑Ω → 𝓓^{n}_{K}(E, F) →L[𝕜] V
toFun_eq_T :
  ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : 𝓓^{n}_{K}(E, F)), toFun (ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f
f g : 𝓓^{n}(Ω, F)
⊢ toFun (f + g) = toFun f + toFun g

Tactic:
by
    set K : Compacts E := ⟨tsupport f ∪ tsupport g, .union f.hasCompactSupport g.hasCompactSupport⟩
    have K_sub_Ω : (K : Set E) ⊆ Ω := union_subset f.tsupport_subset g.tsupport_subset
    let f_K : 𝓓^{n}_{K}(E, F) :=
      .of_support_subset f.contDiff (subset_closure.trans subset_union_left)
    let g_K : 𝓓^{n}_{K}(E, F) :=
      .of_support_subset g.contDiff (subset_closure.trans subset_union_right)
    change toFun (ofSupportedIn K_sub_Ω (f_K + g_K)) =
      toFun (ofSupportedIn K_sub_Ω f_K) + toFun (ofSupportedIn K_sub_Ω g_K)
    simp [toFun_eq_T]

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
⊢ ‖deriv^[n] (fun x ↦ x ^ r) x‖ ≤ (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k

Tactic:
Real.iter_deriv_rpow_const,

Goal state after:
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
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
⊢ μ ∈ spectrum K f ↔ (charpoly f).IsRoot μ

Tactic:
by
  rw [← hasEigenvalue_iff_mem_spectrum, hasEigenvalue_iff_isRoot_charpoly]

Goal state after:
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
this✝ : Std.Symm fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (S (f n) - S (f m) + μ • f n)
hu : μ • (f m - u) = T (f m) - T (f n)
this : u ∈ (↑S ^ (m + 1)).range
⊢ ‖μ‖ ≤ ‖f m - u‖ * ‖μ‖

Tactic:
← hf_far _ u this,

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
this✝ : Std.Symm fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
m n : ℕ
hmn : m < n
u : X := μ⁻¹ • (S (f n) - S (f m) + μ • f n)
hu : μ • (f m - u) = T (f m) - T (f n)
this : u ∈ (↑S ^ (m + 1)).range
⊢ ‖μ‖ ≤ 1 * ‖μ‖
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
⊢ ((Multiset.map (fun x ↦ RCLike.re x) ↑(List.ofFn (RCLike.ofReal ∘ hA.eigenvalues₀))).sort fun x1 x2 ↦ x1 ≥ x2) =
    List.ofFn hA.eigenvalues₀

Tactic:
Multiset.map_coe,

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
⊢ ((↑(List.map (fun x ↦ RCLike.re x) (List.ofFn (RCLike.ofReal ∘ hA.eigenvalues₀)))).sort fun x1 x2 ↦ x1 ≥ x2) =
    List.ofFn hA.eigenvalues₀
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
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
⊢ T v ∈ (eigenspace T μ)ᗮ

Tactic:
by
  intro w hw
  have : T w = (μ : 𝕜) • w := by rwa [mem_eigenspace_iff] at hw
  simp [← hT w, this, inner_smul_left, hv w hw]

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

Goal state before:
pp: 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 : IsSelfAdjoint a
⊢ ∃ φ,
    Continuous[_, instTopologicalSpaceMatrix] ⇑φ ∧
      Function.Injective ⇑φ ∧
        φ (ContinuousMap.restrict (spectrum ℝ a) (ContinuousMap.id ℝ)) = a ∧
          (∀ (f : C(↑(spectrum ℝ a), ℝ)), spectrum ℝ (φ f) = Set.range ⇑f) ∧
            ∀ (f : C(↑(spectrum ℝ a), ℝ)), IsSelfAdjoint (φ f)

Tactic:
replace ha : IsHermitian a := ha
    refine ⟨ha.cfcAux, ha.isClosedEmbedding_cfcAux.continuous,
      ha.isClosedEmbedding_cfcAux.injective, ha.cfcAux_id, fun f ↦ ?map_spec,
      fun f ↦ ?hermitian⟩
    case map_spec =>
      apply Set.eq_of_subset_of_subset
      · rw [← ContinuousMap.spectrum_eq_range f]
        apply AlgHom.spectrum_apply_subset
      · rw [cfcAux_apply, conjStarAlgAut_apply, Unitary.spectrum_star_right_conjugate]
        rintro - ⟨x, rfl⟩
        apply spectrum.of_algebraMap_mem 𝕜
        simp only [Function.comp_apply, Set.mem_range, spectrum_diagonal]
        obtain ⟨x, hx⟩ := x
        obtain ⟨i, rfl⟩ := ha.spectrum_real_eq_range_eigenvalues ▸ hx
        exact ⟨i, rfl⟩
    case hermitian =>
      simp only [isSelfAdjoint_iff, cfcAux_apply, ← map_star]
      rw [star_eq_conjTranspose, diagonal_conjTranspose]
      congr!
      simp [Pi.star_def, Function.comp_def]

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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ cfc f A = hA.cfc f

Tactic:
cfc_apply f A hA' (by rw [continuousOn_iff_continuous_domRestrict]; fun_prop),

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ (cfcHom hA') { toFun := (spectrum ℝ A).domRestrict f, continuous_toFun := ⋯ } = hA.cfc f
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
⊢ ((Multiset.map (fun x ↦ RCLike.re x) ↑(List.ofFn (RCLike.ofReal ∘ hT.eigenvalues ⋯))).sort fun x1 x2 ↦ x1 ≥ x2) =
    List.ofFn (hT.eigenvalues hn)

Tactic:
Multiset.map_coe,

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
⊢ ((↑(List.map (fun x ↦ RCLike.re x) (List.ofFn (RCLike.ofReal ∘ hT.eigenvalues ⋯)))).sort fun x1 x2 ↦ x1 ≥ x2) =
    List.ofFn (hT.eigenvalues hn)
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : 0 ≤ A
⊢ ∀ x ∈ quasispectrum ℝ A, 0 ≤ x

Tactic:
simp only [quasispectrum_eq_spectrum_union_zero ℝ A, Set.union_singleton, Set.mem_insert_iff,
      forall_eq_or_imp, le_refl, true_and]
    intro x hx
    obtain ⟨i, rfl⟩ := Set.ext_iff.mp
      hA.posSemidef.1.spectrum_real_eq_range_eigenvalues x |>.mp hx
    exact hA.posSemidef.eigenvalues_nonneg _

Goal state after: