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

Goal state before:
pp: 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ c.applyOrderedFinpartition p (update v j z) (c.index j) =
    update (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j)) (update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z)) (c.index j)

Tactic:
simp only [applyOrderedFinpartition, update_self]

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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ (p (c.index j)) (update v j z ∘ c.emb (c.index j)) =
    (p (c.index j)) (update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z)
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: case right
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s

Tactic:
rintro ⟨a, b⟩ ⟨⟨a', ⟨ha'1, ha'2⟩⟩, ⟨b', ⟨hb'1, hb'2⟩⟩⟩
    dsimp at ha'1 ha'2 hb'1 hb'2
    rw [← ha'2, ← hb'2]
    apply hεs
    rw [dist_eq_norm]
    apply hN <;> assumption

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun h ↦ exp x * (exp (0 + h) - exp 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h ↦
    exp (x + h) - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) h

Tactic:
have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
    Metric.eball_mem_nhds _ hx.pos

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ (fun h ↦ exp x * (exp (0 + h) - exp 0 - (ContinuousLinearMap.id 𝕂 𝔸) h)) =ᶠ[𝓝 0] fun h ↦
    exp (x + h) - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) h
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
this✝¹ : Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 0)
this✝ : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
h : 𝕊
hh : h • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : Commute (t • x) (h • x)
⊢ exp (t • x) * (exp (h • x) - 1 - h • x) = exp (t • x) * exp (h • x) - exp (t • x) - exp (t • x) • h • x

Tactic:
smul_eq_mul,

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)
this✝ : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
h : 𝕊
hh : h • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : Commute (t • x) (h • x)
⊢ exp (t • x) * (exp (h • x) - 1 - h • x) = exp (t • x) * exp (h • x) - exp (t • x) - exp (t • x) * h • x
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
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt exp w✝ (t • x)
⊢ HasStrictFDerivAt (fun u ↦ exp (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (exp (t • x))) t

Tactic:
convert! hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1

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
w✝ : FormalMultilinearSeries 𝕂 𝔸 𝔸
h✝ : HasFPowerSeriesAt exp w✝ (t • x)
⊢ (ContinuousLinearMap.smulRight 1 x).smulRight (exp (t • x)) = exp (t • x) • ContinuousLinearMap.smulRight 1 x
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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ (fderivWithin ℝ f s a) y ≤ 0

Tactic:
fderivWithin_zero_of_not_differentiableWithinAt hf

Goal state after:
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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y ≤ 0
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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
fderivWithin_zero_of_not_differentiableWithinAt hf

Goal state after:
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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0
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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ (fderivWithin ℝ f s a) y

Tactic:
fderivWithin_zero_of_not_differentiableWithinAt hf

Goal state after:
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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ 0 y
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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
fderivWithin_zero_of_not_differentiableWithinAt hf

Goal state after:
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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun x ↦ a + d x) l (𝓝 a)
n : ι
hcdn : 0 < c n • d n
hdn : a + d n ∈ s
⊢ a + d n ∈ Ioi a ∩ s

Tactic:
refine ⟨?_, hdn⟩

Goal state after:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun x ↦ a + d x) l (𝓝 a)
n : ι
hcdn : 0 < c n • d n
hdn : a + d n ∈ s
⊢ a + d n ∈ Ioi a
Module: Mathlib.Topology.ExtendFrom

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst✝²] A
hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
this : ∀ V' ∈ 𝓝 (φ x), IsClosed[inst✝¹] V' → φ ⁻¹' V' ∈ 𝓝[B] x
⊢ ContinuousWithinAt φ B x

Tactic:
by
    simpa [ContinuousWithinAt, (closed_nhds_basis (φ x)).tendsto_right_iff]

Goal state after:
Module: Mathlib.Topology.Order.Rolle

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 l)
hb : Tendsto f (𝓝[<] b) (𝓝 l)
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c

Tactic:
have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b) := extendFrom_extends hfc
  obtain ⟨c, hc, hfc⟩ : ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c :=
    exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hfc ha hb)
      ((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)
  exact ⟨c, hc, (hfc.on_subset Ioo_subset_Icc_self).congr h (h hc)⟩

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

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c

Tactic:
rcases exists_hasDerivAt_eq_zero' hab hha hhb hhh' with ⟨c, cmem, hc⟩

Goal state after:
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c ∈ Ioo a b, (lgb - lga) * f' c = (lfb - lfa) * g' c
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✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid O
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
c : R
hc : 0 < c
x : M
hx : x ∈ ⇑f ⁻¹' ↑C
⊢ c • f x ∈ ↑C

Tactic:
exact C.smul_mem hc hx

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : C₁.IsGenerating
⊢ C₂.IsGenerating

Tactic:
rw [IsGenerating, ← top_le_iff] at hgen ⊢

Goal state after:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : ⊤ ≤ Submodule.span R ↑C₁
⊢ ⊤ ≤ Submodule.span R ↑C₂
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
⊢ ‖f (x + y) - f x - L₂ (x + y - x)‖ + ‖f (x + y) - f x - L₁ (x + y - x)‖ ≤ ε * r + ε * r

Tactic:
by
      apply add_le_add
      · apply le_of_mem_A h₂
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
      · apply le_of_mem_A h₁
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]

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
⊢ |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - x ^ 2)

Tactic:
have A : ∀ y ∈ Ioo (-1 : ℝ) 1, 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 : |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
⊢ |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - x ^ 2)
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)
e p q e' p' q' : ℕ
hp : n e ≤ p
hq : n e ≤ q
hp' : n e' ≤ p'
hq' : n e' ≤ q'
he' : e ≤ e'
r : ℕ := max (n e) (n e')
I : (1 / 2) ^ e' ≤ (1 / 2) ^ e
J1 : ‖L e p q - L e p r‖ ≤ 4 * ‖c‖ * (1 / 2) ^ e
I1 : x ∈ A f (L e p r) ((1 / 2) ^ r) ((1 / 2) ^ e)
I2 : x ∈ A f (L e' p' r) ((1 / 2) ^ r) ((1 / 2) ^ e')
⊢ ‖L e p r - L e' p' r‖ ≤ 4 * ‖c‖ * (1 / 2) ^ e

Tactic:
exact norm_sub_le_of_mem_A hc P P I1 (A_mono _ _ I I2)

Goal state after:
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 * c ≤ r * r⁻¹ • ↑f ⟨x, hx⟩
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩

Tactic:
smul_eq_mul,

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 : r * c ≤ r * (r⁻¹ * ↑f ⟨x, hx⟩)
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2.inr.inr
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 : 0 < r
this : r * c ≤ r * r⁻¹ • ↑f ⟨x, hx⟩
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩

Tactic:
smul_eq_mul,

Goal state after:
case refine_2.inr.inr
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 : 0 < r
this : r * c ≤ r * (r⁻¹ * ↑f ⟨x, hx⟩)
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.mp
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : MulActionWithZero α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
⊢ a⁻¹ • a • y ∈ s

Tactic:
inv_smul_smul₀ ha'.ne'

Goal state after:
case inr.mp
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : MulActionWithZero α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
⊢ y ∈ s
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst✝¹] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : ε⁻¹ • gauge s x < 1
⊢ gauge s x < ε

Tactic:
smul_eq_mul,

Goal state after:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst✝¹] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : ε⁻¹ * gauge s x < 1
⊢ gauge s x < ε
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_1.inr
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 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
h : 0 < y
⊢ (RingHom.id ℝ) y ≤ y • gauge s x₀

Tactic:
smul_eq_mul,

Goal state after:
case refine_1.inr
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 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
h : 0 < y
⊢ (RingHom.id ℝ) y ≤ y * gauge s x₀
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
hs₀ : Balanced 𝕜 s
hs₁ : Convex ℝ s
hs₂ : Absorbent ℝ s
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : IsOpen[inst✝¹] s
⊢ (gaugeSeminorm hs₀ hs₁ hs₂).ball 0 1 = s

Tactic:
by
  rw [Seminorm.ball_zero_eq]
  exact setOfPred_gauge_lt_one_eq_self_of_isOpen hs₁ hs₂.zero_mem hs

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ |r|⁻¹ • ‖x‖ = ‖x‖ / r

pp: case inr.symmetric
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ x ∈ ball 0 1, -x ∈ ball 0 1

Tactic:
smul_eq_mul,

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ |r|⁻¹ * ‖x‖ = ‖x‖ / r

case inr.symmetric
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ x ∈ ball 0 1, -x ∈ ball 0 1
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
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ A, A x = y

Tactic:
obtain ⟨G, Gx, Gy⟩ : ∃ G : StrongDual R V, G x = 1 ∧ G y ≠ 0 :=
    exists_eq_one_ne_zero_of_ne_zero_pair hx hy
  let A : V ≃L[R] V :=
  { toFun := fun z ↦ z + G z • (y - x)
    invFun := fun z ↦ z + ((G y)⁻¹ * G z) • (x - y)
    map_add' := fun a b ↦ by simp [add_smul]; abel
    map_smul' := by simp [smul_smul]
    left_inv := fun z ↦ by
      simp only [RingHom.id_apply, smul_eq_mul,
        -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `map_smulₛₗ` into `map_smulₛₗ _`
        map_add, map_smulₛₗ _, map_sub, Gx, mul_sub, mul_one, add_sub_cancel]
      rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel₀ Gy]
      simp only [smul_sub, one_mul]
      abel
    right_inv := fun z ↦ by
        -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `map_smulₛₗ` into `map_smulₛₗ _`
      simp only [map_add, map_smulₛₗ _, map_mul, map_inv₀, RingHom.id_apply, map_sub, Gx,
        smul_eq_mul, mul_sub, mul_one]
      rw [mul_comm _ (G y), ← mul_assoc, mul_inv_cancel₀ Gy]
      simp only [smul_sub, one_mul, add_sub_cancel]
      abel }
  exact ⟨A, show x + G x • (y - x) = y by simp [Gx]⟩

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
⊢ B f K r s ε ∈ 𝓝[>] x

Tactic:
obtain ⟨L, LK, hL₁, hL₂⟩ : ∃ L : F, L ∈ K ∧ x ∈ A f L r ε ∧ x ∈ A f L s ε := by
    simpa only [B, mem_iUnion, mem_inter_iff, exists_prop] using hx

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
⊢ B f K r s ε ∈ 𝓝[>] x
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case e_f
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
x : X
⊢ ↑(re (f x)) + I • ↑(im (f x)) = f x

Tactic:
smul_eq_mul,

Goal state after:
case e_f
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
x : X
⊢ ↑(re (f x)) + I * ↑(im (f x)) = f x