mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
c✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
⊢ (fun c ↦ c.fst.extend c.snd)
      ((fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩) c) =
    c

Tactic:
by_cases h : range (c.emb 0) = {0}

Goal state after:
case pos
𝕜 : 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 + 1)
h : range (c.emb 0) = {0}
⊢ (fun c ↦ c.fst.extend c.snd)
      ((fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩) c) =
    c

case neg
𝕜 : 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 + 1)
h : ¬range (c.emb 0) = {0}
⊢ (fun c ↦ c.fst.extend c.snd)
      ((fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩) c) =
    c
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ exp 0 = 1

Tactic:
exp

Goal state after:
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ (if h : Nonempty (Algebra ℚ 𝔸) then (expSeries ℚ 𝔸).sum 0 else 1) = 1
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕂
inst✝⁷ : NormedRing 𝔸
inst✝⁶ : NormedRing 𝔹
inst✝⁵ : NormedAlgebra 𝕂 𝔸
inst✝⁴ : CompleteSpace 𝔸
inst✝³ : Algebra 𝕂 𝔹
inst✝² : CharZero 𝕂
F : Type u_4
inst✝¹ : FunLike F 𝔸 𝔹
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ ∑' (b : ℕ), (↑b !)⁻¹ • f (x ^ b) = ∑' (n : ℕ), (↑n !)⁻¹ • f x ^ n

Tactic:
map_pow

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

Goal state before:
pp: 𝔸 : Type u_1
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra ℚ 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp x ∈ unitary 𝔸

Tactic:
rw [Unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
    exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
    neg_add_cancel, add_neg_cancel, exp_zero, and_self_iff]

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
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
⊢ 0 ≤ ‖f‖ * ∏ i, ‖p i‖

Tactic:
by positivity

Goal state after:
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: case ha
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ f j ∈ t

Tactic:
solve_by_elim [le_refl]

Goal state after:
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: case hb
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ f N ∈ t

Tactic:
solve_by_elim [le_refl]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun h ↦ exp (t • x) * (exp ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h ↦
    exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h

Tactic:
have : Tendsto (fun h : 𝕊 => h • x) (𝓝 0) (𝓝 0) := by
    rw [← zero_smul 𝕊 x]
    exact tendsto_id.smul_const x

Goal state after:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 0)
⊢ (fun h ↦ exp (t • x) * (exp ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h ↦
    exp ((t + h) • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
classical
  exact if hf : DifferentiableWithinAt ℝ f s a then
    h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
  else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
classical
  exact if hf : DifferentiableWithinAt ℝ f s a then
    h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
  else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

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

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

Tactic:
by
  obtain h | h | h := lt_trichotomy n m <;>
    simp_all [Nat.descFactorial_self, Nat.descFactorial_eq_zero_iff_lt.mpr, ne_of_lt, ne_of_gt]

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 g : E → 𝕜
n : ℕ∞ω
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
h0 : ∀ (x : E), g x ≠ 0
⊢ ContDiff 𝕜 n (f / g)

Tactic:
simp only [contDiff_iff_contDiffAt] at *
  exact fun x => (hf x).div (hg x) (h0 x)

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

Goal state before:
pp: case add
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {ε : ℝ≥0∞},
    ε ≠ 0 → ∃ g, (∀ (x : α), f₁ x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞},
    ε ≠ 0 → ∃ g, (∀ (x : α), f₂ x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f₂ x) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), f₁ x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(g₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε / 2
⊢ ∃ g,
    (∀ (x : α), (f₁ + f₂) x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ + ε

Tactic:
rcases h₂ (ENNReal.half_pos ε0).ne' with ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩

Goal state after:
case add
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {ε : ℝ≥0∞},
    ε ≠ 0 → ∃ g, (∀ (x : α), f₁ x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞},
    ε ≠ 0 → ∃ g, (∀ (x : α), f₂ x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f₂ x) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), f₁ x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(g₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), f₂ x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(g₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(f₂ x) ∂μ + ε / 2
⊢ ∃ g,
    (∀ (x : α), (f₁ + f₂) x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ + ε
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv f x ∈ Iic (-1)
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg

Tactic:
rw [(nhdsLT_basis a).eventually_iff] at hf

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → deriv f x ∈ Iic (-1)
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
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:
rw [add_assoc, ENNReal.add_halves]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
⊢ 0 < δ

Tactic:
by positivity

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

Goal state before:
pp: R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
⊢ ¬C.Pointed → ¬C.Flat

Tactic:
exact mt Flat.pointed

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ 0 ≤ 4 * ‖c‖ * ε

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r / (2 * ‖c‖) ≤ ‖y‖
ylt : ‖y‖ < r / 2
⊢ 0 < 2 * ‖c‖

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
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
⊢ 0 < (1 / 2) ^ p

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
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
⊢ 0 < (1 / 2) ^ q

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
⊢ D f K ⊆ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Goal state after:
𝕜 : 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)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
⊢ D f K ⊆ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: 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)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : y ^ 2 ≤ x ^ 2
⊢ (x ^ 2) ^ n / (1 - x ^ 2) ≤ |x| ^ (2 * n) / (1 - x ^ 2)

Tactic:
by simp [pow_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: 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)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - x ^ 2)
⊢ x ∈ Set.Icc (-|x|) |x|

Tactic:
by simp [le_abs_self, neg_le, neg_le_abs x]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
i : ℕ
⊢ 0 ≤ |x| ^ i

Tactic:
by positivity

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
⊢ 0 < ε / (12 * ‖c‖)

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : δ⁻¹ • x ∈ s
⊢ 0 ≤ r⁻¹ * δ

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
absorbs : Absorbent ℝ s
ε : ℝ
hε : 0 < ε
a : ℝ
ha : 0 < a
x : E
hx : x ∈ s
ha' : a < gauge s ((fun x ↦ a • x) x) + ε / 2
b : ℝ
hb : 0 < b
y : E
hy : y ∈ s
hb' : b < gauge s ((fun x ↦ b • x) y) + ε / 2
⊢ 0 ≤ a + b

Tactic:
by positivity

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

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun x ↦ b • x) x}
hx : (fun x ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x ↦ b • x) x} ⊆ c • s
hba : b < a
ha : 0 < a
⊢ 0 ≤ a⁻¹ * b

Tactic:
by positivity

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
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:
rw [add_assoc, ENNReal.add_halves]

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

Goal state before:

Tactic:
-g (x, 0) = g (0, N x) - g (x, N x) := by simp [← map_sub, ← map_neg]
      _ = N x - g (x, N x) := by simpa using g_eq 0 (N x)
      _ ≤ N x := by simpa using g_nonneg ⟨x, N x⟩ (le_refl (N x))

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

Goal state before:
pp: case inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
⊢ r ≤ p x + ε

Tactic:
have hpε : 0 < p x + ε := by positivity

Goal state after:
case inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ r ≤ p x + ε
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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ ∫ (x : α), (↑(gp x)).toReal - (↑↑(gm x)).toReal ∂μ = ∫ (x : α), (↑(gp x)).toReal ∂μ - ∫ (x : α), ↑(gm x) ∂μ

Tactic:
simp only [EReal.toReal_coe_ennreal, ENNReal.coe_toReal]

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ ∫ (x : α), (gp x).toReal - ↑(gm x) ∂μ = ∫ (x : α), (gp x).toReal ∂μ - ∫ (x : α), ↑(gm x) ∂μ
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 0
⊢ sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x

Tactic:
convert! csInf_Ioi (a := (0 : ℝ))
    exact Set.ext fun r ↦ and_iff_left (.inr hx)

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

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hr : 0 ≤ 0
⊢ gauge (closedBall 0 0) x = ‖x‖ / 0

Tactic:
rw [div_zero, closedBall_zero', singleton_zero, gauge_closure_zero]; rfl

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

Goal state before:
pp: case inl
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace ℝ E
L : E ≃L[𝕜] F
φ : X → E
this : CompleteSpace E ↔ CompleteSpace F
left✝ : CompleteSpace E
right✝ : CompleteSpace F
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

Tactic:
exact L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _

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

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ ¬Integrable f μ

Tactic:
hf,

Goal state after:
case neg
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
hc : ¬c = 0
⊢ ¬False
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : ¬Integrable g (μ.withDensity fun x ↦ ↑(f x))
⊢ (∫ (x : X), g x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • g x ∂μ

Tactic:
rw [integral_undef hg, integral_undef]
    rwa [← integrable_withDensity_iff_integrable_smul f_meas]

Goal state after: