mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e_6.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin c.length
⊢ ∀ (i : ℕ) (him : i < update c.partSize j (c.partSize j + 1) j) (hin : i < c.partSize j + 1),
    (cons e v ∘ (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨i, him⟩ = cons e (v ∘ c.emb j) ⟨i, hin⟩

Tactic:
intro a ha h'a

Goal state after:
case e_6.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
m : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : OrderedFinpartition m
e : E
v : Fin m → E
j : Fin c.length
a : ℕ
ha : a < update c.partSize j (c.partSize j + 1) j
h'a : a < c.partSize j + 1
⊢ (cons e v ∘ (fun i ↦ cases 0 (succ ∘ c.emb j) i) ∘ Fin.cast ⋯) ⟨a, ha⟩ = cons e (v ∘ c.emb j) ⟨a, h'a⟩
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ posTangentConeAt univ a

pp: case hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ posTangentConeAt univ a

Tactic:
<;>

Goal state after:
case hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ posTangentConeAt univ a

case hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ posTangentConeAt univ a
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ univ

pp: case hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ univ

Tactic:
<;>

Goal state after:
case hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ univ

case hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ univ
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case zero.zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin 0 (fun x ↦ x ^ 0) s x = ↑(Nat.descFactorial 0 0) * x ^ (0 - 0)

pp: case zero.succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n✝ : ℕ
⊢ iteratedDerivWithin (n✝ + 1) (fun x ↦ x ^ 0) s x = ↑(Nat.descFactorial 0 (n✝ + 1)) * x ^ (0 - (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero.zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin 0 (fun x ↦ x ^ 0) s x = ↑(Nat.descFactorial 0 0) * x ^ (0 - 0)

case zero.succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n✝ : ℕ
⊢ iteratedDerivWithin (n✝ + 1) (fun x ↦ x ^ 0) s x = ↑(Nat.descFactorial 0 (n✝ + 1)) * x ^ (0 - (n✝ + 1))
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
h✝ : k ≤ i
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)

pp: case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
h✝ : i < k
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)

Tactic:
<;>

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
h✝ : k ≤ i
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)

case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
h✝ : i < k
⊢ (i + 1) * i.descFactorial k = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ.succ.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      ↑((k + 1).choose i_1) * iteratedDerivWithin i_1 (fun x ↦ x ^ i) s x *
        iteratedDerivWithin (k + 1 - i_1) (fun x ↦ x) s x =
    ↑((i + 1).descFactorial (k + 1)) * x ^ (i + 1 - (k + 1))

pp: case succ.succ.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      ↑((k + 1).choose i_1) * iteratedDerivWithin i_1 (fun x ↦ x ^ i) s x *
        iteratedDerivWithin (k + 1 - i_1) (fun x ↦ x) s x =
    ↑((i + 1).descFactorial (k + 1)) * x ^ (i + 1 - (k + 1))

Tactic:
<;>

Goal state after:
case succ.succ.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : i ≤ k
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      ↑((k + 1).choose i_1) * iteratedDerivWithin i_1 (fun x ↦ x ^ i) s x *
        iteratedDerivWithin (k + 1 - i_1) (fun x ↦ x) s x =
    ↑((i + 1).descFactorial (k + 1)) * x ^ (i + 1 - (k + 1))

case succ.succ.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
this : (i + 1).descFactorial (k + 1) = (k + 1) * i.descFactorial k + i.descFactorial (k + 1)
hik : k < i
⊢ ∑ i_1 ∈ Finset.range (k + 1 + 1),
      ↑((k + 1).choose i_1) * iteratedDerivWithin i_1 (fun x ↦ x ^ i) s x *
        iteratedDerivWithin (k + 1 - i_1) (fun x ↦ x) s x =
    ↑((i + 1).descFactorial (k + 1)) * x ^ (i + 1 - (k + 1))
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case neg.hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ ∀ x ∈ Icc a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
· intro x x_in
    rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
    · exact ⟨la, ha.mono_left <| nhdsWithin_mono _ Ioo_subset_Ioi_self⟩
    · exact ⟨lb, hb.mono_left <| nhdsWithin_mono _ Ioo_subset_Iio_self⟩
    · exact ⟨f x, hf x h⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ iteratedDeriv 0 id x = if 0 = 0 then x else if 0 = 1 then 1 else 0

pp: case succ.zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ iteratedDeriv (0 + 1) id x = if 0 + 1 = 0 then x else if 0 + 1 = 1 then 1 else 0

pp: case succ.succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ iteratedDeriv (n + 1 + 1) id x = if n + 1 + 1 = 0 then x else if n + 1 + 1 = 1 then 1 else 0

Tactic:
<;>

Goal state after:
case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ iteratedDeriv 0 id x = if 0 = 0 then x else if 0 = 1 then 1 else 0

case succ.zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ iteratedDeriv (0 + 1) id x = if 0 + 1 = 0 then x else if 0 + 1 = 1 then 1 else 0

case succ.succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ iteratedDeriv (n + 1 + 1) id x = if n + 1 + 1 = 0 then x else if n + 1 + 1 = 1 then 1 else 0
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : n < m
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)

pp: case inr.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : n = m
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)

pp: case inr.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : m < n
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)

Tactic:
<;>

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : n < m
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)

case inr.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : n = m
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)

case inr.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : ℕ
h : m < n
⊢ iteratedDeriv n (fun x ↦ x ^ m) 0 = ↑(if n = m then m.factorial else 0)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : c = 0
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : ¬c = 0
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < f' x

Tactic:
exact hf' _

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ f' x

Tactic:
exact hf' _

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ f' x < 0

Tactic:
exact hf' _

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ f' x ≤ 0

Tactic:
exact hf' _

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : ConvexCone R M
h : ↑C - ↑C = univ
x : M
⊢ x ∈ Submodule.span R ↑C

Tactic:
Set.eq_univ_iff_forall

Goal state after:
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : ConvexCone R M
h : ∀ (x : M), x ∈ ↑C - ↑C
x : M
⊢ x ∈ Submodule.span R ↑C
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
⊢ ↑C - ↑C = univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
⊢ ∀ (x : M), x ∈ ↑C - ↑C
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ p) ((1 / 2) ^ e)

pp: case refine_2
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ q) ((1 / 2) ^ e)

Tactic:
<;>

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ p) ((1 / 2) ^ e)

case refine_2
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ q) ((1 / 2) ^ e)
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case smul_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → c • x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s

pp: case add_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → ∀ ⦃y : M⦄, y ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → x + y ∈ ⋃ c, ⋃ (_ : 0 < c), c • s

Tactic:
<;>

Goal state after:
case smul_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → c • x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s

case add_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → ∀ ⦃y : M⦄, y ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → x + y ∈ ⋃ c, ⋃ (_ : 0 < c), c • s
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case const
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : c = 0
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
⊢ ∃ g,
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0)) x) ∧
      UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * ((-x) ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) =
    2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Tactic:
Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x

Goal state after:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : -(r⁻¹ • x) - y ∈ s
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩

Tactic:
replace := le_c (r⁻¹ • ⟨x, hx⟩) this

Goal state after:
case refine_2.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : ↑f (r⁻¹ • ⟨x, hx⟩) ≤ c
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
x✝² : { c // 0 ≤ c }
x✝¹ : E × ℝ
x✝ : x✝¹ ∈ {p | N p.1 ≤ p.2}
val✝ : ℝ
hc : 0 ≤ val✝
h✝ : val✝ = 0
⊢ ⟨val✝, hc⟩ • x✝¹ ∈ {p | N p.1 ≤ p.2}

pp: case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
x✝² : { c // 0 ≤ c }
x✝¹ : E × ℝ
x✝ : x✝¹ ∈ {p | N p.1 ≤ p.2}
val✝ : ℝ
hc : 0 ≤ val✝
h✝ : 0 < val✝
⊢ ⟨val✝, hc⟩ • x✝¹ ∈ {p | N p.1 ≤ p.2}

Tactic:
<;>

Goal state after:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
x✝² : { c // 0 ≤ c }
x✝¹ : E × ℝ
x✝ : x✝¹ ∈ {p | N p.1 ≤ p.2}
val✝ : ℝ
hc : 0 ≤ val✝
h✝ : val✝ = 0
⊢ ⟨val✝, hc⟩ • x✝¹ ∈ {p | N p.1 ≤ p.2}

case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
x✝² : { c // 0 ≤ c }
x✝¹ : E × ℝ
x✝ : x✝¹ ∈ {p | N p.1 ≤ p.2}
val✝ : ℝ
hc : 0 ≤ val✝
h✝ : 0 < val✝
⊢ ⟨val✝, hc⟩ • x✝¹ ∈ {p | N p.1 ≤ p.2}
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
s : PointedCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x

Tactic:
set f' := (-f).coprod (LinearMap.id.toPMap ⊤)

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
s : PointedCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)
⊢ ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x