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

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i
⊢ iConvexComb w f = iConvexComb w g

Tactic:
refine congr(sConvexComb $(?_))
  ext i
  simp only [weights_map]
  -- TODO: This should just be `congr! 2 with i hi`.
  congr 1
  refine Finsupp.mapDomain_congr fun i hi ↦ ?_
  exact hfg i (by simpa using hi)

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

Goal state before:
pp: case pos
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∈ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y

pp: case neg
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y

Tactic:
· rw [← huw, Finset.mem_image] at hy
    obtain ⟨x, hx, rfl⟩ := hy
    convert mapDomain_apply' _ _ support_onFinset_subset hfu hx
    exact (if_pos hx).symm

Goal state after:
case neg
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
w : StdSimplex K X
t : Finset X := w.weights.support
hw : ↑t ⊆ s
hsw : t = w.weights.support
⊢ sConvexComb w ∈ s

Tactic:
have ht : t.Nonempty := w.support_weights_nonempty

Goal state after:
K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
w : StdSimplex K X
t : Finset X := w.weights.support
hw : ↑t ⊆ s
hsw : t = w.weights.support
ht : t.Nonempty
⊢ sConvexComb w ∈ s
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : ι → Set E
s : Finset ι
h_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_ss : I ⊆ s
hI_card : #I ≤ finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty

Tactic:
obtain ⟨J, hI_ss_J, hJ_ss, hJ_card⟩ := exists_subsuperset_card_eq hI_ss hI_card h_card

Goal state after:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : ι → Set E
s : Finset ι
h_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_ss : I ⊆ s
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset ι
hI_ss_J : I ⊆ J
hJ_ss : J ⊆ s
hJ_card : #J = finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
a b : V
s : Set (SimpleGraph V)
hs : s.Nonempty
⊢ (∀ G ∈ s, G.Adj a b) → a ≠ b

Tactic:
by
      obtain ⟨G, hG⟩ := hs
      exact fun h => (h _ hG).ne

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

Goal state before:
pp: ι : Sort u_1
V : Type u
a b : V
inst✝ : Nonempty ι
f : ι → SimpleGraph V
⊢ (∀ G ∈ Set.range fun i ↦ f i, G.Adj a b) ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
Set.forall_mem_range

Goal state after:
ι : Sort u_1
V : Type u
a b : V
inst✝ : Nonempty ι
f : ι → SimpleGraph V
⊢ (∀ (i : ι), (f i).Adj a b) ↔ ∀ (i : ι), (f i).Adj a b
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ s.WSameSide x y

Tactic:
refine
      ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩

Goal state after:
case mp
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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (y -ᵥ p₂)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ s.WOppSide x y

Tactic:
refine
      ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩

Goal state after:
case mp
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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
h : SameRay R ((v +ᵥ x) -ᵥ p₁) (p₂ -ᵥ y)
⊢ SameRay R (x -ᵥ (-v +ᵥ p₁)) (p₂ -ᵥ y)
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.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
constructor
  · rintro ⟨p₁', hp₁', p₂', hp₂', h0 | h0 | ⟨r₁, r₂, hr₁, hr₂, hr⟩⟩
    · rw [vsub_eq_zero_iff_eq] at h0
      rw [h0]
      exact Or.inl hp₁'
    · refine Or.inr ⟨p₂', hp₂', ?_⟩
      rw [h0]
      exact SameRay.zero_right _
    · refine Or.inr ⟨(-r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂',
        Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, ?_⟩)⟩
      rw [vadd_vsub_assoc, ← vsub_sub_vsub_cancel_right x p₁ p₁']
      linear_combination (norm := match_scalars <;> field) hr
  · rintro (h' | ⟨h₁, h₂, h₃⟩)
    · exact wOppSide_of_left_mem y h'
    · exact ⟨p₁, h, h₁, h₂, h₃⟩

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

Goal state before:
pp: case inr
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 z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne : dist x z ≠ 0
a b : ℝ
left✝¹ : 0 ≤ a
hb : 0 ≤ b
left✝ : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b = r
⊢ y = (AffineMap.lineMap x z) r

Tactic:
AffineMap.lineMap_apply,

Goal state after:
case inr
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 z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne : dist x z ≠ 0
a b : ℝ
left✝¹ : 0 ≤ a
hb : 0 ≤ b
left✝ : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b = r
⊢ y = r • (z -ᵥ x) +ᵥ x
Module: Mathlib.Analysis.Convex.Strong

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y - a * b * φ ‖x - y‖ ≤ a • f x + b • f y - a * b * ψ ‖x - y‖

Tactic:
by gcongr; apply 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 → ℝ
hψφ : ψ ≤ φ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + a * b * ψ ‖x - y‖ ≤ a • f x + b • f y + a * b * φ ‖x - y‖

Tactic:
by gcongr; apply hψφ

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 p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : t < 0
⊢ s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
by
  refine ⟨wOppSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩
  rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne,
    vsub_right_mem_direction_iff_mem hp₁] at h

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

Goal state before:
pp: case inr.refine_2
𝕜 : 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
⊢ (w i)⁻¹ < (1 - ε) / ε + (w i)⁻¹

Tactic:
exact lt_add_of_pos_left _ <| by positivity

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
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
y : V
hy : y ∈ (convexHull ℝ) s
z : V
hz : z ∈ (convexHull ℝ) s
hxzy : Wbtw ℝ x z y
hxz : IsVisible ℝ ((convexHull ℝ) s) x z
⊢ y ∈ ↑(affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

Tactic:
exact AffineSubspace.right_mem_of_wbtw hxzy (subset_affineSpan _ _ <| subset_union_left rfl)
    (affineSpan_mono _ subset_union_right <| convexHull_subset_affineSpan _ <|
      hxz.mem_convexHull_isVisible hx hz) (ne_of_mem_of_not_mem hz hx).symm

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
x : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] ((convexHull ℝ) s)
hx : x ∉ (convexHull ℝ) s
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    Module.rank ℝ ↥(span ℝ ↑(-x +ᵥ affineSpan ℝ ({x} ∪ {y | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y})))

Tactic:
push_cast
      refine Submodule.rank_mono ?_
      gcongr
      exact (subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isVisible hx

Goal state after:
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g₁ g₂ : ↥(Lp E q μ)
⊢ MemLp.toLp (↑↑f • ↑↑(g₁ + g₂)) ⋯ = MemLp.toLp (↑↑f • ↑↑g₁ + ↑↑f • ↑↑g₂) ⋯

Tactic:
apply MemLp.toLp_congr _ _ ?_

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g₁ g₂ : ↥(Lp E q μ)
⊢ ↑↑f • ↑↑(g₁ + g₂) =ᵐ[μ] ↑↑f • ↑↑g₁ + ↑↑f • ↑↑g₂
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: case e'_2
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
⊢ f • 0 = MemLp.toLp 0 ⋯

Tactic:
apply MemLp.toLp_congr _ _ ?_

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
⊢ ↑↑f • ↑↑0 =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: case e'_2
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
⊢ 0 • f = MemLp.toLp 0 ⋯

Tactic:
apply MemLp.toLp_congr _ _ ?_

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
⊢ ↑↑0 • ↑↑f =ᵐ[μ] 0
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
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have g_intble' : ∀ t : ℝ, 0 ≤ t → IntervalIntegrable g volume 0 t := by
    intro t ht
    rcases eq_or_lt_of_le ht with h | h
    · simp [← h]
    · exact g_intble t 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
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
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 ∂μ =
    ∫⁻ (a : ℝ), (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) a

Tactic:
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.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✝¹ : 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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h : w₂ i < 0
h' : 0 < w₁ i
⊢ (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:
exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₁ hw₂ h' h).wOppSide

Goal state after:
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
μ : Measure E
H : LocallyIntegrableOn (fun x ↦ 1) (↑Ω) μ
f : 𝓓^{n}(Ω, F)
⊢ Integrable (⇑f) μ

Tactic:
← integrableOn_iff_integrable_of_support_subset (subset_tsupport f)

Goal state after:
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
μ : Measure E
H : LocallyIntegrableOn (fun x ↦ 1) (↑Ω) μ
f : 𝓓^{n}(Ω, F)
⊢ IntegrableOn (⇑f) (tsupport ⇑f) μ
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
⊢ |x| ^ (r - ↑n) = x ^ (-(↑n - r))

Tactic:
neg_sub

Goal state after:
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
⊢ |x| ^ (r - ↑n) = x ^ (r - ↑n)
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.PosDef
i : n
a✝ : i ∈ Finset.univ
⊢ 0 < ↑(⋯.eigenvalues i)

Tactic:
simpa using hA.eigenvalues_pos i

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

Goal state before:
pp: case neg
𝕜 : 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
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = 0

Tactic:
Finset.card_filter_eq_zero_iff

Goal state after:
case neg
𝕜 : 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
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ ∀ x ∈ Finset.univ, ¬↑(hT.unsortedEigenvalues hn x) = μ
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
⊢ HasEigenvector T (↑(hT.unsortedEigenvalues hn i)) ((hT.unsortedEigenvectorBasis hn) i)

Tactic:
let μ : 𝕜 :=
    (hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i
      hT.orthogonalFamily_eigenspaces').val

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 ⋯)
⊢ HasEigenvector T (↑(hT.unsortedEigenvalues hn i)) ((hT.unsortedEigenvectorBasis hn) 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 ⋯)
⊢ HasEigenvector T (↑(RCLike.re μ)) v

Tactic:
have key : HasEigenvector T μ v := by
    have H₁ : v ∈ eigenspace T μ := by
      simp_rw [v, unsortedEigenvectorBasis]
      exact
        hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i
          hT.orthogonalFamily_eigenspaces'
    have H₂ : v ≠ 0 := by simpa using (hT.unsortedEigenvectorBasis hn).toBasis.ne_zero i
    exact ⟨H₁, H₂⟩

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 ⋯)
key : HasEigenvector T μ v
⊢ HasEigenvector T (↑(RCLike.re μ)) v
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 | ↑(hT.eigenvalues hn i) = μ}.card = finrank 𝕜 ↥(eigenspace T μ)

Tactic:
rw [← hT.card_filter_unsortedEigenvalues_eq hn, eigenvalues_def]

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 | ↑((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)) ∘ ⇑Fin.revPerm) i) = μ}.card =
    {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card