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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕'.Nonempty
f : ℕ → ↑s → ℝ
hf : 𝓕' = range f
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hlc : ∀ (i : ℕ), f i = s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i)
⊢ sSup 𝓕' = s.domRestrict φ

Tactic:
h𝓕'.2.1

Goal state after:
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕'.Nonempty
f : ℕ → ↑s → ℝ
hf : 𝓕' = range f
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hlc : ∀ (i : ℕ), f i = s.domRestrict (⇑re ∘ ⇑(l i)) + const (↑s) (c i)
⊢ s.domRestrict φ = s.domRestrict φ
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), #s ≤ #(s.biUnion t)

Tactic:
rintro ⟨f, hf₁, hf₂⟩ s

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #s ≤ #(s.biUnion t)
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case h
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := ⋯
down : J' ⥤ J := ⋯
F' : J' ⥤ Type (max u v w) := ⋯
this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
⊢ (fun j ↦ (u { down := j }).down) ∈ F.sections

Tactic:
intro j j' f

Goal state after:
case h
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)
this✝ : ∀ (i : J'), Finite (F'.obj i)
h✝ : Nonempty J
this : IsCofiltered J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map f)) ((fun j ↦ (u { down := j }).down) j) = (fun j ↦ (u { down := j }).down) j'
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : Sbtw R (w₁ i) (r * (w₂ i - w₁ i) + w₁ i) (w₂ i)
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)

Tactic:
sbtw_mul_sub_add_iff

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∃ f, Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), #s ≤ #(s.biUnion t)

Tactic:
rintro ⟨f, hf₁, hf₂⟩ s

Goal state after:
case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #s ≤ #(s.biUnion t)
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b i j : α
⊢ (if i = a then some b else none) = some j ↔ some i = some j

Tactic:
rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p : P
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
hp : p ∈ affineSpan R (Set.range t.points)
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, (lineMap (t.points i₂) (t.points i₃)) r₁]
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
h₂' : p ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
⊢ Sbtw R (t.points i₁) p ((lineMap (t.points i₂) (t.points i₃)) r₁)

Tactic:
rcases eq_affineCombination_of_mem_affineSpan_of_fintype hp with ⟨w, hw, rfl⟩

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₁, (lineMap (t.points i₂) (t.points i₃)) r₁]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
⊢ Sbtw R (t.points i₁) ((Finset.affineCombination R Finset.univ t.points) w) ((lineMap (t.points i₂) (t.points i₃)) r₁)
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: case isTrue
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝¹ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
i' j : n
h✝ : σ i' = j
⊢ M i (σ i) ≤ M i' j

pp: case isFalse
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝¹ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
i' j : n
h✝ : ¬σ i' = j
⊢ 0 ≤ M i' j

Tactic:
case isTrue h => exact (hi' i' (by simp)).trans_eq (by rw [h])

Goal state after:
case isFalse
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝¹ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
i' j : n
h✝ : ¬σ i' = j
⊢ 0 ≤ M i' j
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ (convexHull 𝕜) ↑i
⊢ ∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x

Tactic:
obtain ⟨t, ht₁, ht₂, ht₃⟩ := hx

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
ht₃ : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : IsEmpty n
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
exact ⟨fun _ => 1, by simp, by simp, Subsingleton.elim _ _⟩

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

Goal state before:
pp: case inl.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
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
rw [wbtw_comm (z := x)]
      rw [← or_assoc]
      exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonpos _ _ hy0.le hz0.le)

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
⊢ ∃ b, 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s

Tactic:
set ε' : ℝ := ε / 2 / (cnorm + 1)

Goal state after:
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
⊢ ∃ b, 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
⊢ ∃ u, s ⊆ interior ((convexHull ℝ) ↑u) ∧ (convexHull ℝ) ↑u ⊆ t

Tactic:
rcases compact_open_separated_add_left hs₂ hU₁ hU₂ with ⟨V, hV₁, hV₂⟩

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
⊢ ∃ u, s ⊆ interior ((convexHull ℝ) ↑u) ∧ (convexHull ℝ) ↑u ⊆ t
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
⊢ i ∈ s

Tactic:
by_contra H
    refine h i s ?_
    rw [Set.sdiff_singleton_eq_self H]
    exact hi

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})) → ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t

Tactic:
rintro hs t ht x ⟨hxs, hxt⟩

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ (convexHull 𝕜) t
⊢ x ∈ t
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
hne : (interior s).Nonempty
hb : Bornology.IsBounded s
⊢ ∃ h,
    ⇑h '' interior s = ball 0 1 ∧
      ⇑h '' closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s = closedBall 0 1 ∧
        ⇑h '' frontier s = sphere 0 1

Tactic:
by
  simpa [isOpen_ball.interior_eq, closure_ball, frontier_ball]
    using exists_homeomorph_image_eq hc hne (NormedSpace.isVonNBounded_of_isBounded _ hb)
    (convex_ball 0 1) (by simp [isOpen_ball.interior_eq]) (NormedSpace.isVonNBounded_ball _ _ _)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
h : s(u, v) = s(w, x)
⊢ G.Adj u v ↔ G.Adj w x

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h

Goal state after:
V : Type u
G : SimpleGraph V
u v w x : V
h : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ G.Adj u v ↔ G.Adj w x
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
ι : Type u_4
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall 0 r
⊢ ∑ k ∈ t, w k • z k ∈ ball 0 r

Tactic:
exact sum_mem_ball_of_strictConvexSpace h0 h1 hi hj hij hi0 hj0 hz

Goal state after:
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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
⊢ 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}

Tactic:
simpa using! trivial

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
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : E → ℝ := fun x ↦ ‖iteratedFDeriv ℝ n f x‖
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
have hg : Continuous g := (h₂.continuous_iteratedFDeriv <| mod_cast le_top).norm

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
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
n : ℕ
g : E → ℝ := fun x ↦ ‖iteratedFDeriv ℝ n f x‖
hg : Continuous g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᵐ[μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
ω : α
⊢ f ω = F ω → ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)

Tactic:
fω_nn

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᵐ[μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
ω : α
fω_nn : f ω = F ω
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᵐ[μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
ω : α
fω_nn : f ω = F ω
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)

Tactic:
fω_nn

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᵐ[μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
ω : α
fω_nn : f ω = F ω
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, g t) = ENNReal.ofReal (∫ (t : ℝ) in 0..F ω, G t)
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ⇑f}
huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}
T : Set M₂
hT : T.Finite
hTv✝ : closure[inst✝⁴.toTopologicalSpace] (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V
hTv : closedBall 0 1 ⊆ ⇑v ⁻¹' ⋃ y ∈ T, y +ᵥ V
⊢ closedBall 0 1 ⊆ ⇑u ⁻¹' ⋃ y ∈ T, y +ᵥ U

Tactic:
preimage_iUnion₂

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ⇑f}
huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}
T : Set M₂
hT : T.Finite
hTv✝ : closure[inst✝⁴.toTopologicalSpace] (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V
hTv : closedBall 0 1 ⊆ ⋃ i ∈ T, ⇑v ⁻¹' (i +ᵥ V)
⊢ closedBall 0 1 ⊆ ⋃ i ∈ T, ⇑u ⁻¹' (i +ᵥ U)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ (-↑l) * (x ^ (k + l) * f) ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)

Tactic:
apply mul_le_mul _ _ (by positivity) (by positivity)

Goal state after:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ (-↑l) ≤ ((1 + x) / 2) ^ (-↑l)

C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ (k + l) * f ≤ C₁ + C₂