mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ s + t * s' + t * t' = 1

Tactic:
add_assoc,

Goal state after:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ s + (t * s' + t * t') = 1
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
i : T
⊢ 0 ≤ 1 - f i

Tactic:
by simpa using hf1 _

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

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ 0 ≤ 1 - f j

Tactic:
by simpa using hf1 _

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

Goal state before:
pp: case neg.inr
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
⊢ ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (x t) r

Tactic:
filter_upwards [hx.continuousAt ((hf.isOpen_preimage _ isClosed_singleton.isOpen_compl).mem_nhds
      (x := t) (by simp [*])) (Metric.ball_mem_nhds _ (show 0 < r / 3 by simpa)),
      hf.tendsto' _ _ ht (Metric.ball_mem_nhds _ (show 0 < r / D / 3 by simp [*]))] with j hj hj'

Goal state after:
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : j ∈ x ⁻¹' Metric.ball (x t) (r / 3)
hj' : j ∈ f ⁻¹' Metric.ball 1 (r / D / 3)
⊢ convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j) ∈ Metric.ball (x t) r
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ 0 ≤ 1 - f j

Tactic:
by simpa using hf1 _

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

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝⁴ : ConvexSpace ℝ X
inst✝³ : MetricSpace X
inst✝² : IsConvexDist X
inst✝¹ : BoundedSpace X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
i : T
⊢ 0 ≤ 1 - f i

Tactic:
by simpa using hf1 _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ (∀ x ∈ G.edgeSet, x ∈ s ∧ ¬x.IsDiag) ↔ ∀ x ∈ G.edgeSet, x ∈ s

Tactic:
grind [not_isDiag_of_mem_edgeSet]

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✝⁵ : 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
⊢ s.WSameSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ y ∉ s ∧ x ∉ s

Tactic:
and_comm (b := x ∉ s)

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
⊢ s.WSameSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WSameSide y x ∧ x ∉ s ∧ y ∉ s
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : Nontrivial E
S : Set E
x : E
x✝ : x ∈ interior S ∩ extremePoints ℝ S
x_int : x ∈ interior S
x_ext : x ∈ extremePoints ℝ S
⊢ x ∈ ∅

Tactic:
rw [mem_interior_iff_mem_nhds] at x_int

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : Nontrivial E
S : Set E
x : E
x✝ : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
⊢ x ∈ ∅
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
⊢ s.WOppSide y x ∧ x ∉ s ∧ y ∉ s ↔ s.WOppSide y x ∧ y ∉ s ∧ x ∉ s

Tactic:
and_comm (b := x ∉ s)

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

Goal state before:
pp: case inr.inr
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
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ dist p₂ p < max (dist p₁ p) (dist p₃ p)

Tactic:
simp_rw [@dist_eq_norm_vsub V, ← hr]

Goal state after:
case inr.inr
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
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ ‖(1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p)‖ < max ‖p₁ -ᵥ p‖ ‖p₃ -ᵥ p‖
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₂ : P
h : p₂ ∈ s
⊢ s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
rw [SOppSide, and_comm, wOppSide_iff_exists_right h, and_assoc, and_congr_right_iff,
    and_congr_right_iff]
  rintro _ hy
  rw [or_iff_right hy]

Goal state after:
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
⊢ dist ((affineCombination ℝ univ s.points) w) p₀ < r

Tactic:
obtain ⟨j, hij, hj⟩ : ∃ j, i ≠ j ∧ w j ≠ 0 := 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:
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 : Fin (n + 1)
hij : i ≠ j
hj : w j ≠ 0
⊢ dist ((affineCombination ℝ univ s.points) w) p₀ < r
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:
rw [coe_eq_bot_iff] at h
    simp only [h, not_sSameSide_bot]
    exact isPreconnected_empty

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

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
have ht₁ : 1 ∈ t := by simpa [t]

Goal state after:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z
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)
⊢ ∫⁻ (a : α), ∫⁻ (a_1 : ℝ), (Ioc 0 (f a)).indicator (fun t ↦ ENNReal.ofReal (g t)) a_1 ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
rw [← lintegral_indicator measurableSet_Ioi, lintegral_lintegral_swap]

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)
⊢ ∫⁻ (y : ℝ), ∫⁻ (x : α), (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) y ∂μ =
    ∫⁻ (a : ℝ), (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a

case hf
α : 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)
⊢ AEMeasurable (Function.uncurry fun a ↦ (Ioc 0 (f a)).indicator fun t ↦ ENNReal.ofReal (g t)) (μ.prod volume)
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 : SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0
h0 : ¬w₁ i = 0
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
by_cases h0' : w₂ i = 0
      · exact wOppSide_of_right_mem _
          ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).2 h0')
      simp only [h0, h0', or_self, or_false] at h
      rcases Ne.lt_or_gt h0 with h' | h'
      · rw [sign_neg h', neg_inj, eq_comm, sign_eq_one_iff] at h
        exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₂ hw₁ h h').symm.wOppSide
      · rw [sign_pos h', eq_comm, neg_eq_iff_eq_neg, sign_eq_neg_one_iff] at h
        exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₁ hw₂ h' h).wOppSide

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ = 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)

Tactic:
by rw [rpow_neg]; positivity

Goal state after:
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
hf_temperate : HasTemperateGrowth f
N : ℕ
⊢ ∃ k, ∀ n ≤ N, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k

Tactic:
choose k hk using hf_temperate.isBigO
  use (Finset.range (N + 1)).sup k
  intro n hn
  refine (hk n).trans (isBigO_of_le _ fun x ↦ ?_)
  rw [Real.norm_of_nonneg (by positivity), Real.norm_of_nonneg (by positivity)]
  gcongr
  · simp
  · exact Finset.le_sup (by simpa using hn)

Goal state after:
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✝
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
F : E → (N : Fin (n + 1)) → E [×↑N]→L[ℝ] F✝ := fun x N ↦ iteratedFDeriv ℝ (↑N) f x
this : F =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
C : ℝ
C_nonneg : C ≥ 0
hC : IsBigOWith C ⊤ F fun x ↦ (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
simp (discharger := positivity) only [isBigOWith_top, Real.norm_of_nonneg,
    pi_norm_le_iff_of_nonneg, Fin.forall_iff, Nat.lt_succ_iff] at hC

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✝
hf_temperate : HasTemperateGrowth f
n k : ℕ
hk : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
F : E → (N : Fin (n + 1)) → E [×↑N]→L[ℝ] F✝ := fun x N ↦ iteratedFDeriv ℝ (↑N) f x
this : F =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
C : ℝ
C_nonneg : C ≥ 0
hC : ∀ (x : E) (i : ℕ) (h : i ≤ n), ‖F x ⟨i, ⋯⟩‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k
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
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ (1 + C₁) * (1 + ‖x‖) ^ k₁ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i

Tactic:
by
        apply le_self_pow₀ (one_le_mul_of_one_le_of_one_le (by simp [hC₁]) (by simp [one_le_pow₀]))
        grind

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

Goal state before:
pp: case e_f
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun x ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}
ω : α
⊢ ENNReal.ofReal (f ω) = ENNReal.ofReal (∫ (x : ℝ) in 0..f ω, 1)

Tactic:
simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, mul_one]

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

Goal state before:
pp: case hg₁
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
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ ContDiff ℝ ∞ g

Tactic:
exact hg.1

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

Goal state before:
pp: case left
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
⊢ ContDiff ℝ ∞ fun x ↦ (B (f x)) (g x)

Tactic:
apply (B.bilinearRestrictScalars ℝ).isBoundedBilinearMap.contDiff.comp (hf.1.prodMk hg.1)

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
⊢ σ = sort f

Tactic:
have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)

Goal state after:
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f))) h ⋯
⊢ σ = sort f
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
⊢ ((↑(List.ofFn fun x ↦ RCLike.re ↑(hA.eigenvalues₀ x))).sort fun x1 x2 ↦ x1 ≥ x2) = List.ofFn hA.eigenvalues₀

Tactic:
RCLike.ofReal_re,

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.ofFn fun x ↦ hA.eigenvalues₀ x)).sort fun x1 x2 ↦ x1 ≥ x2) = List.ofFn hA.eigenvalues₀
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 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ ∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
classical
  have : hA.eigenvalues ≠ 0 := by
    contrapose h_ne
    have := hA.spectral_theorem
    rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this
  obtain ⟨i, hi⟩ := Function.ne_iff.mp this
  exact ⟨_, _, hi, (ofLp_eq_zero 2).ne.2 <| hA.eigenvectorBasis.orthonormal.ne_zero i,
    hA.mulVec_eigenvectorBasis i⟩

Goal state after:
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
⊢ ((↑(List.ofFn fun x ↦ RCLike.re ↑(hT.eigenvalues ⋯ x))).sort fun x1 x2 ↦ x1 ≥ x2) = List.ofFn (hT.eigenvalues hn)

Tactic:
RCLike.ofReal_re,

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.ofFn fun x ↦ hT.eigenvalues ⋯ x)).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
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (cfc (⇑NNReal.sqrt) A).det = RCLike.sqrt A.det

Tactic:
cfc_nnreal_eq_real _ A,

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (cfc (fun x ↦ ↑(NNReal.sqrt x.toNNReal)) A).det = RCLike.sqrt A.det
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
x y : Matrix n n 𝕜
hy : IsUnit y
hM : (star y * y).PosDef
__spread✝⁻⁰ : PreInnerProductSpace.Core 𝕜 (Matrix n n 𝕜) := ⋯.matrixPreInnerProductSpace
hx : (x * star y * y * xᴴ).trace = 0
⊢ x = 0

Tactic:
← conjTranspose_conjTranspose x,

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
x y : Matrix n n 𝕜
hy : IsUnit y
hM : (star y * y).PosDef
__spread✝⁻⁰ : PreInnerProductSpace.Core 𝕜 (Matrix n n 𝕜) := ⋯.matrixPreInnerProductSpace
hx : (xᴴᴴ * star y * y * xᴴᴴᴴ).trace = 0
⊢ x = 0