mathlib-initiative/mathlib-tactics huggingface dataset:
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_cases hp₁ : p₂ = p₁

Goal state after:
case pos
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₃
hp₁ : p₂ = p₁
⊢ dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)

case neg
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₃
hp₁ : ¬p₂ = p₁
⊢ dist p₂ p ≤ max (dist p₁ p) (dist 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 z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
ht : t ≠ 1
hy' : (t - 1) • (z -ᵥ x) ∈ s.direction
⊢ x ∈ s

Tactic:
s.direction.smul_mem_iff (sub_ne_zero_of_ne ht)

Goal state after:
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 z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
ht : t ≠ 1
hy' : z -ᵥ x ∈ s.direction
⊢ x ∈ s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

pp: case mp.inr.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

pp: case mp.inr.inr
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
· rw [vsub_eq_zero_iff_eq] at h
      exact False.elim (hx (h.symm ▸ hp))

Goal state after:
case mp.inr.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

case mp.inr.inr
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

pp: case mp.inr.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

pp: case mp.inr.inr
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
· rw [vsub_eq_zero_iff_eq] at h
      exact False.elim (hx (h.symm ▸ hp))

Goal state after:
case mp.inr.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : y -ᵥ p₂ = 0
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

case mp.inr.inr
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (y -ᵥ p₂)
⊢ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: 𝕜 : 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
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hw₁ : ∀ i_1 ∈ t.erase i, w i_1 = 0
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i = 1
j : ι
hj : j ∈ t
hji : j ≠ i
⊢ w j • a j = 0

Tactic:
rw [hw₁ _ <| mem_erase.2 ⟨hji, hj⟩, zero_smul]

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

Goal state before:
pp: case mp.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

pp: case mp.inr.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

pp: case mp.inr.inr
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
· rw [vsub_eq_zero_iff_eq] at h
      exact False.elim (hx (h.symm ▸ hp))

Goal state after:
case mp.inr.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

case mp.inr.inr
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 p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ ∃ a ≤ 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

pp: case mp.inr.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

pp: case mp.inr.inr
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
· rw [vsub_eq_zero_iff_eq] at h
      exact False.elim (hx (h.symm ▸ hp))

Goal state after:
case mp.inr.inl
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
h : p₂ -ᵥ y = 0
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

case mp.inr.inr
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 p : P
hx : x ∉ s
hp : p ∈ s
y : P
hy : y ∉ s
p₂ : P
hp₂ : p₂ ∈ s
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (x -ᵥ p) = r₂ • (p₂ -ᵥ y)
⊢ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂✝ : Type u_2
𝕜₃✝ : Type u_3
inst✝³⁹ : NormedField 𝕜₁
inst✝³⁸ : NormedField 𝕜₂✝
inst✝³⁷ : NormedField 𝕜₃✝
σ : 𝕜₁ →+* 𝕜₂✝
τ : 𝕜₂✝ →+* 𝕜₃✝
ρ : 𝕜₁ →+* 𝕜₃✝
inst✝³⁶ : RingHomCompTriple σ τ ρ
E✝ : Type u_4
F✝ : Type u_5
G✝ : Type u_6
inst✝³⁵ : AddCommGroup E✝
inst✝³⁴ : Module 𝕜₁ E✝
inst✝³³ : AddCommGroup F✝
inst✝³² : Module 𝕜₂✝ F✝
inst✝³¹ : AddCommGroup G✝
inst✝³⁰ : Module 𝕜₃✝ G✝
𝕜 : Type u_7
𝕜₂ : Type u_8
𝕜₃ : Type u_9
𝕜₄ : Type u_10
E : Type u_11
F : Type u_12
G : Type u_13
H : Type u_14
inst✝²⁹ : AddCommGroup E
inst✝²⁸ : AddCommGroup F
inst✝²⁷ : AddCommGroup G
inst✝²⁶ : AddCommGroup H
inst✝²⁵ : NormedField 𝕜
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
inst✝²² : NormedField 𝕜₄
inst✝²¹ : Module 𝕜 E
inst✝²⁰ : Module 𝕜₂ F
inst✝¹⁹ : Module 𝕜₃ G
inst✝¹⁸ : Module 𝕜₄ H
inst✝¹⁷ : TopologicalSpace E
inst✝¹⁶ : TopologicalSpace F
inst✝¹⁵ : TopologicalSpace G
inst✝¹⁴ : TopologicalSpace H
inst✝¹³ : IsTopologicalAddGroup G
inst✝¹² : IsTopologicalAddGroup H
inst✝¹¹ : ContinuousConstSMul 𝕜₃ G
inst✝¹⁰ : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁷ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁶ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁵ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁴ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
s : Set F
⊢ s ∈ {S | IsCompact S} ↔ ⇑e₁₂ ⁻¹' s ∈ {S | IsCompact S}

Tactic:
by
    simp [← e₁₂.toHomeomorph.isCompact_preimage]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := ⋯
⊢ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}} ⊆ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}

Tactic:
intro t

Goal state after:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t ↦ μ {a | t ≤ g a}
t : R
⊢ t ∈ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}} → t ∈ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ 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
⊢ ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t

Tactic:
intro t

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
t : ℝ
⊢ 0 ≤ t → IntervalIntegrable g volume 0 t
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
⊢ SignType.sign (w₁ i) = SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0

Tactic:
by_cases h0' : w₂ i = 0

Goal state after:
case pos
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

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
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)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
by_cases h0' : w₂ i = 0

Goal state after:
case pos
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
h0' : w₂ i = 0
⊢ (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₂)

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
h0' : ¬w₂ i = 0
⊢ (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₂)
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)).WOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : ¬w₁ i = 0
⊢ SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0

Tactic:
by_cases h0' : w₂ i = 0

Goal state after:
case pos
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)).WOppSide ((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

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)).WOppSide ((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
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

Goal state after:
case pos
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
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₂)

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
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₂)
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 ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
a : α
ha : a ∈ {a | s < f a}
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ≤ ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t)

Tactic:
apply ENNReal.ofReal_le_ofReal

Goal state after:
α : 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
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
a : α
ha : a ∈ {a | s < f a}
⊢ ∫ (t : ℝ) in 0..s, g t ≤ ∫ (t : ℝ) in 0..f a, g t
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h'f
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ HasTemperateGrowth (fderiv ℝ fun x ↦ ‖x‖ ^ 2)

pp: case hf
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ Differentiable ℝ fun x ↦ ‖x‖ ^ 2

pp: case h
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ ∀ (x : H), ‖‖x‖ ^ 2‖ ≤ 1 * (1 + ‖x‖) ^ 2

Tactic:
· rw [fderiv_norm_sq]
    convert! (2 • innerSL ℝ).hasTemperateGrowth

Goal state after:
case hf
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ Differentiable ℝ fun x ↦ ‖x‖ ^ 2

case h
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ ∀ (x : H), ‖‖x‖ ^ 2‖ ≤ 1 * (1 + ‖x‖) ^ 2
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
f : 𝓓^{n}(Ω, F)
⊢ StronglyMeasurable ⇑f

Tactic:
exact f.continuous.stronglyMeasurable_of_hasCompactSupport f.hasCompactSupport

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
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
⊢ HasEigenvalue T ↑(⨆ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)

Tactic:
have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀'

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ HasEigenvalue T ↑(⨆ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)