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

Goal state before:
pp: case inr
𝕜 : 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
x✝¹ : i ∈ univ
j : Fin c.length
x✝ : j ∈ univ
hij : i ≠ j
h : i ≠ c.index 0
hj : j ≠ c.index 0
⊢ (Disjoint on fun m ↦
      range fun j ↦ if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j

Tactic:
· simp only [onFun, h, ↓reduceDIte, hj]
      apply Set.disjoint_iff_forall_ne.2
      simp only [mem_range, ne_eq, forall_exists_index, forall_apply_eq_imp_iff, pred_inj]
      intro a b
      exact c.emb_ne_emb_of_ne hij

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case emb
𝕜 : 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i a : Fin c.length
⊢ c.emb a ≍ fun j ↦
    if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle i).emb a (Fin.cast ⋯ j)).pred ⋯

Tactic:
rcases eq_or_ne a i with rfl | hij

Goal state after:
case emb.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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
a : Fin c.length
⊢ c.emb a ≍ fun j ↦
    if h : a = a then ((c.extendMiddle a).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle a).emb a (Fin.cast ⋯ j)).pred ⋯

case emb.inr
𝕜 : 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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ c.emb a ≍ fun j ↦
    if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ j.succ)).pred ⋯
    else ((c.extendMiddle i).emb a (Fin.cast ⋯ j)).pred ⋯
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x)

Tactic:
exact norm_expSeries_summable_of_mem_ball x hx

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable (norm ∘ fun n ↦ (expSeries 𝕂 𝔸 n) fun x_1 ↦ x)

Tactic:
exact norm_expSeries_summable_of_mem_ball x hx

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDerivWithin n (fun z ↦ c + f z) s x = iteratedDerivWithin n f s x

Tactic:
obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'
  rw [iteratedDerivWithin_succ', iteratedDerivWithin_succ']
  congr 1 with y
  exact derivWithin_const_add _

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : 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
α : Type u_5
H : Type u_6
inst✝ : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖p₁ x k‖
hpf : ∀ k ≤ n, (fun a ↦ p₁ a k - p₂ a k) =O[l] f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₂ x k‖
hqf : ∀ k ≤ n, (fun a ↦ q₁ a k - q₂ a k) =O[l] f
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
⊢ (fun x ↦
      ‖p₁ x c.length‖ * ↑c.length * max ‖fun m ↦ q₁ x (c.partSize m)‖ ‖fun m ↦ q₂ x (c.partSize m)‖ ^ (c.length - 1) *
          ‖(fun m ↦ q₁ x (c.partSize m)) - fun m ↦ q₂ x (c.partSize m)‖ +
        ‖p₁ x c.length - p₂ x c.length‖ * ∏ i, ‖q₂ x (c.partSize i)‖) =O[l]
    f

Tactic:
refine .add ?_ ?_

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
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Type u_5
H : Type u_6
inst✝ : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖p₁ x k‖
hpf : ∀ k ≤ n, (fun a ↦ p₁ a k - p₂ a k) =O[l] f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₂ x k‖
hqf : ∀ k ≤ n, (fun a ↦ q₁ a k - q₂ a k) =O[l] f
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
⊢ (fun x ↦
      ‖p₁ x c.length‖ * ↑c.length * max ‖fun m ↦ q₁ x (c.partSize m)‖ ‖fun m ↦ q₂ x (c.partSize m)‖ ^ (c.length - 1) *
        ‖(fun m ↦ q₁ x (c.partSize m)) - fun m ↦ q₂ x (c.partSize m)‖) =O[l]
    f

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
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Type u_5
H : Type u_6
inst✝ : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖p₁ x k‖
hpf : ∀ k ≤ n, (fun a ↦ p₁ a k - p₂ a k) =O[l] f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₂ x k‖
hqf : ∀ k ≤ n, (fun a ↦ q₁ a k - q₂ a k) =O[l] f
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
⊢ (fun x ↦ ‖p₁ x c.length - p₂ x c.length‖ * ∏ i, ‖q₂ x (c.partSize i)‖) =O[l] f
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
⊢ iteratedDerivWithin (n + 1) (f • g) s x =
    ∑ i ∈ Finset.range (n + 1 + 1),
      (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x

Tactic:
obtain ⟨U, hU, H⟩ := ((hf.eventually (by simp)).and (hg.eventually (by simp))).exists_mem

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
n✝ : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
𝔸 : Type u_5
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕜 𝔸
inst✝² : Module 𝔸 F
inst✝¹ : IsBoundedSMul 𝔸 F
inst✝ : IsScalarTower 𝕜 𝔸 F
n : ℕ
IH :
  ∀ {f : 𝕜 → 𝔸} {g : 𝕜 → F},
    ContDiffWithinAt 𝕜 (↑n) f s x →
      ContDiffWithinAt 𝕜 (↑n) g s x →
        iteratedDerivWithin n (f • g) s x =
          ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x
f : 𝕜 → 𝔸
g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
hg : ContDiffWithinAt 𝕜 (↑(n + 1)) g s x
U : Set 𝕜
hU : U ∈ 𝓝[insert x s] x
H : ∀ y ∈ U, ContDiffWithinAt 𝕜 (↑(n + 1)) f s y ∧ ContDiffWithinAt 𝕜 (↑(n + 1)) g s y
⊢ iteratedDerivWithin (n + 1) (f • g) s x =
    ∑ i ∈ Finset.range (n + 1 + 1),
      (n + 1).choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n + 1 - i) g s x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_7
inst✝² : NontriviallyNormedField 𝕜
F : Type u_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₁ f₂ : 𝕜 → F
x : 𝕜
h : f₁ =ᶠ[𝓝 x] f₂
n : ℕ
⊢ iteratedDeriv n f₁ =ᶠ[𝓝 x] iteratedDeriv n f₂

Tactic:
by
  simp_all [← nhdsWithin_univ, ← iteratedDerivWithin_univ, EventuallyEq.iteratedDerivWithin]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ y
⊢ ContDiffWithinAt 𝕜 n (Prod.map f g) univ (x, y)

Tactic:
simpa only [univ_prod_univ] using hf.prodMap hg

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n✝ : ℕ∞ω
𝕜' : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
n : ℕ∞
h : ContDiffWithinAt 𝕜' (↑n) f s x
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Tactic:
rcases h m hm with ⟨u, u_mem, p', hp'⟩

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n✝ : ℕ∞ω
𝕜' : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
n : ℕ∞
h : ContDiffWithinAt 𝕜' (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn (↑m) f p' u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: case neg
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
z : ℝ
hz : z ∈ Icc a b
hz' : ¬z = a
⊢ ContinuousWithinAt f (Icc a b) z

Tactic:
· exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
f' : α → ℝ≥0∞ := fun x ↦ ↑(f x + w x)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(f x) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), ↑(f x) ∂μ + ε

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
f' : α → ℝ≥0∞ := fun x ↦ ↑(f x + w x)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(f x) ∂μ + (ε / 2 + ε / 2) = ∫⁻ (x : α), ↑(f x) ∂μ + ε
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C✝ C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
⊢ False

Tactic:
have h' : b - a ≠ 0 := fun h'' => h (eq_of_sub_eq_zero h'').symm

Goal state after:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C✝ C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
⊢ False
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : x ∈ hull 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ {y | ∃ r, 0 < r ∧ y ∈ r • s} → c • x ∈ {y | ∃ r, 0 < r ∧ y ∈ r • s}

Tactic:
by
                intro r₁ hr₁ y ⟨r₂, hr₂, hy⟩
                refine ⟨r₁ * r₂, mul_pos hr₁ hr₂, ?_⟩
                rw [mul_smul]
                exact smul_mem_smul_set hy

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2
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
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑xp + y + (-↑xn - y) ∈ s
⊢ ↑f xn ≤ ↑f xp

Tactic:
add_assoc,

Goal state after:
case refine_2
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
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
this : ↑xp + (y + (-↑xn - y)) ∈ s
⊢ ↑f xn ≤ ↑f xp
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
⊢ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) ≤ 1 / 2 * log ((1 + x) / (1 - x))

Tactic:
have A : ∀ y ∈ Icc 0 x, HasDerivAt F (F' y) y := by
    intro y hy
    exact hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range _ (by grind) (by grind)

Goal state after:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
⊢ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) ≤ 1 / 2 * log ((1 + x) / (1 - x))
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ 0} = 0 0

pp: case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x

Tactic:
· simp only [csInf_Ioi, mem_zero, Pi.zero_apply, sep_true, smul_zero]

Goal state after:
case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x : E
hx : x ≠ 0
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ 0} = 0 x
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), fs x ≤ f x
int_fs : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(fs x) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), ↑(fs x) ∂μ ≠ ∞
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ fs x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(fs x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(g x) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), ↑(g x) ∂μ + ε

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), fs x ≤ f x
int_fs : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(fs x) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), ↑(fs x) ∂μ ≠ ∞
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ fs x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(fs x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑(g x) ∂μ + (ε / 2 + ε / 2) = ∫⁻ (x : α), ↑(g x) ∂μ + ε
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), φ ↑x = ↑f x
hφ₂ : ∀ (x : E), φ x ≤ gauge s x
hφ₃ : φ x₀ = 1
hφ₄ : ∀ x ∈ s, φ x < 1
⊢ ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1

Tactic:
refine ⟨⟨φ, ?_⟩, hφ₃, hφ₄⟩

Goal state after:
case refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), φ ↑x = ↑f x
hφ₂ : ∀ (x : E), φ x ≤ gauge s x
hφ₃ : φ x₀ = 1
hφ₄ : ∀ x ∈ s, φ x < 1
⊢ Continuous φ.toFun
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
⊢ ∃ f u, (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
by_cases htne : t.Nonempty
  · obtain ⟨f, u, -, hs', ht'⟩ :=
      geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne
    exact ⟨f, u, hs', ht'⟩
  · exact ⟨0, 0, by simp⟩

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝¹² : Field R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : Module R V
inst✝⁶ : SeparatingDual R V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : TopologicalSpace W
inst✝³ : Module R W
inst✝² : Nontrivial W
inst✝¹ : ContinuousSMul R W
inst✝ : Nontrivial V
v : V
hv : v ≠ 0
⊢ Nontrivial (V →L[R] W)

Tactic:
obtain ⟨w, hw⟩ := exists_ne (0 : W)

Goal state after:
R : Type u_1
V : Type u_2
inst✝¹² : Field R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : Module R V
inst✝⁶ : SeparatingDual R V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : TopologicalSpace W
inst✝³ : Module R W
inst✝² : Nontrivial W
inst✝¹ : ContinuousSMul R W
inst✝ : Nontrivial V
v : V
hv : v ≠ 0
w : W
hw : w ≠ 0
⊢ Nontrivial (V →L[R] W)
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s : Set E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c // ∀ y ∈ s, re (l y) ≤ c }
l : ι → StrongDual 𝕜 E := fun lc ↦ lc.fst
c : ι → ℝ := fun lc ↦ ↑lc.snd
hc : ∀ (i : ι), ∀ y ∈ s, re ((l i) y) ≤ c i := fun lc ↦ Subtype.prop lc.snd
⊢ ∃ l c, ⋂ n, {x | re ((l n) x) ≤ c n} = s

Tactic:
have : Nonempty ι := ⟨0, 0, fun _ _ ↦ by simp⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s : Set E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c // ∀ y ∈ s, re (l y) ≤ c }
l : ι → StrongDual 𝕜 E := fun lc ↦ lc.fst
c : ι → ℝ := fun lc ↦ ↑lc.snd
hc : ∀ (i : ι), ∀ y ∈ s, re ((l i) y) ≤ c i := fun lc ↦ Subtype.prop lc.snd
this : Nonempty ι
⊢ ∃ l c, ⋂ n, {x | re ((l n) x) ≤ c n} = s
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
hf : ¬Continuous[instTopologicalSpaceSubtype, inst✝¹] (s.domRestrict f)
⊢ mkD (s.domRestrict f) g = g

Tactic:
exact mkD_of_not_continuous hf

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

Goal state before:
pp: α : Type u_1
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → G
f : α → G
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ bound n a
bound_integrable : Integrable (fun a ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ F n a) (f a)
⊢ HasSum (fun n ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)

Tactic:
simp only [integral_eq_setToFun]
  exact hasSum_setToFun_of_dominated_convergence _ bound hF_meas h_bound bound_summable
    bound_integrable h_lim

Goal state after: