mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
rw [Nat.add_one] at hn

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
this : Function.Injective ⇑↑f
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
apply this.sbtw_map_iff

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✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R w x z
h₂ : Sbtw R x y z
⊢ Sbtw R w y z

Tactic:
by
  rw [wbtw_comm] at *
  rw [sbtw_comm] at *
  exact h₁.trans_sbtw_left h₂

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case inr
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
hs : s.Nonempty
j : J
ji : j ⟶ i
⊢ ∃ x, ∀ (i_1 : j ⟶ i), (ConcreteCategory.hom (F.map i_1)) x ∈ s

Tactic:
obtain ⟨y, ys⟩ := hs

Goal state after:
case inr
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
j : J
ji : j ⟶ i
y : F.obj i
ys : y ∈ s
⊢ ∃ x, ∀ (i_1 : j ⟶ i), (ConcreteCategory.hom (F.map i_1)) x ∈ s
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
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
⊢ ∑ y ∈ t.erase ↑⟨i₀, hi₀⟩, k y = 1

Tactic:
by convert! ksum

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
⊢ 0 < ‖x - y‖

Tactic:
norm_sub_pos_iff

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hxy : x ≠ y
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
⊢ x ≠ y
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p i ∈ (convexHull 𝕜) (p '' {j})

Tactic:
rw [hij, Set.image_singleton, convexHull_singleton]

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p j ∈ {p j}
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
x✝ : ℝ
⊢ x✝ ∈ (-f) '' ball x₀ r ↔ x✝ ∈ -f '' ball x₀ r

Tactic:
simp [neg_eq_iff_eq_neg]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
by
  replace hf' : IsBounded ((-f) '' ball x₀ r) := by convert! hf'.neg; ext; simp [neg_eq_iff_eq_neg]
  simpa using hf.neg.exists_lipschitzOnWith_of_isBounded hr hf'

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
h : ContinuousAt (fun δ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0
⊢ C ∈ 𝓝 ((fun δ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0)

Tactic:
simpa using! hC.mem_nhds hx

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

Goal state before:
pp: case refine_4
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ (p * a₁ + q * a₂) • x + (p * b₁ + q * b₂) • y = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)

Tactic:
hx,

Goal state after:
case refine_4
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
x₁ : E
hx₁ : x₁ ∈ s
y₁ : E
hy₁ : y₁ ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
x₂ : E
hx₂ : x₂ ∈ s
y₂ : E
hy₂ : y₂ ∈ t
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
x : E
hxs : x ∈ s
hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂
y : E
hyt : y ∈ t
hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂
⊢ (p * a₁) • x₁ + (q * a₂) • x₂ + (p * b₁ + q * b₂) • y = p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂)
Module: Mathlib.Analysis.Convex.KreinMilman

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x ↦ x ∈ S) t
⊢ (extremePoints ℝ s).Nonempty

Tactic:
obtain ⟨⟨x, hxt⟩, htclos, hst⟩ := ht.prop

Goal state after:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
ht : Minimal (fun x ↦ x ∈ S) t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
⊢ (extremePoints ℝ s).Nonempty
Module: Mathlib.Analysis.Convex.KreinMilman

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a ↦ f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ y = x

Tactic:
mem_extremePoints

Goal state after:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ ⇑f '' s ∧ ∀ x₁ ∈ ⇑f '' s, ∀ x₂ ∈ ⇑f '' s, f x ∈ openSegment ℝ x₁ x₂ → x₁ = f x ∧ x₂ = f x
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a ↦ f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ y = x
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
⊢ intrinsicInterior 𝕜 (f '' s) = f '' intrinsicInterior 𝕜 s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs
  · simp
  · have : Nonempty s := hs.to_subtype
    rw [intrinsicInterior, ← image_interior_preimage_comp e he_homeo,
      (funext he : (↑) ∘ e = f ∘ (↑)),
      preimage_image_eq_of_homeomorph_affineSpan e he_homeo he, image_comp]; rfl

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

Goal state before:
pp: R : Type u_1
I : Type u_6
inst✝² : PartialOrder R
inst✝¹ : Semiring R
inst✝ : IsStrictOrderedRing R
w w' : StdSimplex R I
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
hst : s + t = 1
⊢ (convexCombPair s t hs ht hst w w').weights = s • w.weights + t • w'.weights

Tactic:
simp [convexCombPair, sum_add_index, add_smul]

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

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

Tactic:
simp only [coe_mem, card_erase_of_mem]

Goal state after:
case hn
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
i : ↥s
⊢ #s - 1 = k
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ≥0 univ fun x ↦ x ^ p

Tactic:
exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ p

Tactic:
exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn

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

Tactic:
vadd_vsub

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
p₁ p₂ x : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 ≤ t
⊢ SameRay R (t • (x -ᵥ p₁)) (x -ᵥ 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
⊢ ((x ∉ s ∧ y ∉ s) ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
and_assoc

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 y p₂ : P
h : p₂ ∈ s
⊢ (x ∉ s ∧ y ∉ s ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
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 = r • (z -ᵥ x) +ᵥ x

Tactic:
← H',

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 = b • (z -ᵥ x) +ᵥ x
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
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
⊢ a i = ∑ i ∈ t, w i • a i

Tactic:
← one_smul 𝕜 (a i),

Goal state after:
𝕜 : 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
⊢ 1 • a i = ∑ i ∈ t, w i • a i
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ ENNReal.ofReal (g s) * ((Ioi 0).indicator (fun x ↦ 1) s * μ {a | s ≤ f a}) =
    (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a}) s * ENNReal.ofReal (g s)

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

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
aux₁ :
  (fun x ↦ (Ioc 0 (f x)).indicator (fun t ↦ ENNReal.ofReal (g t)) s) = fun x ↦
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f x)
⊢ ENNReal.ofReal (g s) * (Ioi 0).indicator (fun _x ↦ 1 * μ {a | s ≤ f a}) s =
    (Ioi 0).indicator (fun t ↦ μ {a | t ≤ f a}) s * ENNReal.ofReal (g s)
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f g : 𝓓^{n}(Ω, F)
⊢ (toBoundedContinuousFunctionCLM 𝕜) f = (toBoundedContinuousFunctionCLM 𝕜) g → f = g

Tactic:
by simp [toBoundedContinuousFunctionCLM]

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

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

Tactic:
intro x
    rw [norm_pow, norm_norm, one_mul, add_pow_two]
    exact le_add_of_nonneg_left (by positivity)

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
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ M * (2 * (‖x‖ ^ 2 + ‖y‖ ^ 2)) / 4 ≤ M

Tactic:
hx,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ M * (2 * (1 ^ 2 + ‖y‖ ^ 2)) / 4 ≤ M
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: M₁ : Type u_2
M₂ : Type u_3
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ IsCompactOperator f ↔ ∃ V ∈ 𝓝 0, IsCompact (closure[inst✝¹] (f '' V))

Tactic:
by
  rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]
  exact
    ⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, hK.closure_of_subset hKV⟩,
      fun ⟨V, hV, hVc⟩ => ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩

Goal state after:
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
⊢ Real.exp (Real.log 2 * (↑n - r)) ≤ Real.exp (Real.log (3 / 2) * ↑k)

Tactic:
by
      gcongr 1
      apply le_trans _ hk₂
      gcongr

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
T : E →L[𝕜] E
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε

Tactic:
by
  by_cases hT0 : T = 0
  · simp [hT0, spectrum.mem_resolventSet_iff] at hT'
  obtain ⟨ε, hε0, hε⟩ := T.rayleighQuotient_le_of_mem_resolventSet ‖T‖ (by positivity) hT'
  refine ⟨ε, hε0, fun x ↦ ?_⟩
  grw [hε]
  field_simp
  grind

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
hK : ∀ K > 0, ∃ x, ‖(T - μ • 1) x‖ < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : ‖(T - μ • 1) x‖ < ε * ‖x‖
this : x ≠ 0
η : 𝕜
hη : η ≠ 0
h₁ : ‖η • x‖ < 1
h₂ : 1 / ‖C‖ ≤ ‖η • x‖
h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖
⊢ ‖η‖ * ‖(T - μ • 1) x‖ < ε

Tactic:
hx,

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
hK : ∀ K > 0, ∃ x, ‖(T - μ • 1) x‖ < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : ‖(T - μ • 1) x‖ < ε * ‖x‖
this : x ≠ 0
η : 𝕜
hη : η ≠ 0
h₁ : ‖η • x‖ < 1
h₂ : 1 / ‖C‖ ≤ ‖η • x‖
h₃ : ‖η‖⁻¹ ≤ 1⁻¹ * ‖C‖ * ‖x‖
⊢ ‖η‖ * (ε * ‖x‖) ≤ ε
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x✝² x✝¹ : n → 𝕜
x✝ : 𝕜
⊢ M *ᵥ x✝¹ ⬝ᵥ star (x✝ • x✝²) = (starRingEnd 𝕜) x✝ * M *ᵥ x✝¹ ⬝ᵥ star x✝²

Tactic:
← smul_eq_mul,

Goal state after:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x✝² x✝¹ : n → 𝕜
x✝ : 𝕜
⊢ M *ᵥ x✝¹ ⬝ᵥ star (x✝ • x✝²) = (starRingEnd 𝕜) x✝ • (M *ᵥ x✝¹ ⬝ᵥ star x✝²)