mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
⊢ DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
by
  refine ⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩
  have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
    iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x H
  rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] at this

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

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
iso : E ≃L[𝕜] F
f : G → E
⊢ DifferentiableOn 𝕜 (⇑iso ∘ f) univ ↔ Differentiable 𝕜 f

Tactic:
← differentiableOn_univ

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
⊢ DifferentiableOn 𝕜 (⇑iso ∘ f) univ ↔ DifferentiableOn 𝕜 f univ
Module: Mathlib.Analysis.Calculus.FDeriv.Add

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
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L
⊢ HasFDerivAtFilter (fun y ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L

Tactic:
simp only [hasFDerivAtFilter_iff_isLittleO] at *

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
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun p ↦ A i p.1 - A i p.2 - (A' i) (p.1 - p.2)) =o[L] fun p ↦ p.1 - p.2
⊢ (fun p ↦ ∑ i ∈ u, A i p.1 - ∑ i ∈ u, A i p.2 - (∑ i ∈ u, A' i) (p.1 - p.2)) =o[L] fun p ↦ p.1 - p.2
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ fderiv 𝕜 (⇑iso ∘ f) x = ↑iso ∘SL fderiv 𝕜 f x

Tactic:
by
  rw [← fderivWithin_univ, ← fderivWithin_univ]
  exact iso.comp_fderivWithin uniqueDiffWithinAt_univ

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

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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
⊢ f' = (f' ∘SL ↑iso) ∘SL ↑iso.symm

Tactic:
ContinuousLinearMap.comp_assoc,

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
⊢ f' = f' ∘SL ↑iso ∘SL ↑iso.symm
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
B : f' = (f' ∘SL ↑iso) ∘SL ↑iso.symm
⊢ HasFDerivWithinAt f f' s (iso x)

Tactic:
A,

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
B : f' = (f' ∘SL ↑iso) ∘SL ↑iso.symm
⊢ HasFDerivWithinAt ((f ∘ ⇑iso) ∘ ⇑iso.symm) f' s (iso x)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : E →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ ⇑iso) ((f' ∘SL ↑iso.symm) ∘SL ↑iso) (⇑iso ⁻¹' s) x

Tactic:
ContinuousLinearMap.comp_assoc,

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : E →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso.symm ∘SL ↑iso) (⇑iso ⁻¹' s) x
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
⊢ ‖{ toFun := fun x ↦ x.fderivCompContinuousLinearMap g, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤
    ↑(Fintype.card ι) * ‖g‖ ^ (Fintype.card ι - 1) * ‖f‖

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ (by positivity) fun dg ↦ ?_

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
⊢ ‖({ toFun := fun x ↦ x.fderivCompContinuousLinearMap g, map_add' := ⋯, map_smul' := ⋯ } f) dg‖ ≤
    ↑(Fintype.card ι) * ‖g‖ ^ (Fintype.card ι - 1) * ‖f‖ * ‖dg‖
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: case hbc
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤ ‖g‖ ^ #{i}ᶜ * ∏ i ∈ {i}ᶜ, ‖v i‖

Tactic:
← Finset.prod_const,

Goal state after:
case hbc
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤ (∏ _x ∈ {i}ᶜ, ‖g‖) * ∏ i ∈ {i}ᶜ, ‖v i‖
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
ι' : Type u_1
inst✝ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
⊢ ‖f.mkContinuousAlternating C H‖ ≤ max C 0

Tactic:
by
  dsimp only [mkContinuousAlternating]
  exact mkContinuous_norm_le _ (le_max_right _ _) _

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
a : α
⊢ dist ↑a ↑a = 0

Tactic:
rw [Completion.dist_eq, dist_self]

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

Goal state before:
pp: case pos
𝕜 : Type u
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
m : ℕ
hm : ↑m ≤ ↑n + 1
h' : m ≤ n
⊢ ContinuousOn (fun x ↦ p x m) s

Tactic:
apply h.1.cont m (mod_cast h')

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
x : E
f g : E → F
y : E
hsx : UniqueDiffWithinAt 𝕜 s x
hyt : UniqueDiffWithinAt 𝕜 t y
⊢ dist (iteratedFDerivWithin 𝕜 1 f s x) (iteratedFDerivWithin 𝕜 1 g t y) =
    dist (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)

Tactic:
simp only [iteratedFDerivWithin_succ_eq_comp_left, comp_apply,
    LinearIsometryEquiv.dist_map, iteratedFDerivWithin_zero_eq_comp,
    LinearIsometryEquiv.comp_fderivWithin, hsx, hyt]
  apply (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearIsometry.postcomp.dist_map

Goal state after:
Module: Mathlib.Analysis.Analytic.Uniqueness

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
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
p : E [×0]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (0 + 1)‖
⊢ ‖p fun x ↦ y‖ = 0

Tactic:
by
      simpa only [fin0_apply_norm, norm_eq_zero, norm_zero, zero_add, pow_one,
        mul_zero, norm_le_zero_iff] using! ht 0 (δε (Metric.mem_ball_self δ_pos))

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a) • slope f a b +ᵥ f a = f b

Tactic:
sub_smul_slope,

Goal state after:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (f b -ᵥ f a) +ᵥ f a = f b
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: case refine_2.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ ContinuousWithinAt f (s ∩ t) x

Tactic:
apply H'.continuousWithinAt.mono inter_subset_left

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
z : 𝕜
k : ℕ
hk : k < p.order
⊢ p.coeff (0 + k) = 0

Tactic:
zero_add,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
z : 𝕜
k : ℕ
hk : k < p.order
⊢ p.coeff k = 0
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
⊢ ∃ c, f =ᶠ[𝓝 x] fun x ↦ c

Tactic:
use f x

Goal state after:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
⊢ f =ᶠ[𝓝 x] fun x_1 ↦ f x
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv (fun x ↦ x⁻¹) x = -1 / x

Tactic:
simpa using logDeriv_zpow x (-1)

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

Goal state before:
pp: 𝕜 : Type u
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
inst✝ : CompleteSpace F
⊢ ContDiffWithinAt 𝕜 ω f s x ↔ AnalyticWithinAt 𝕜 f s x

Tactic:
refine ⟨fun h ↦ h.analyticWithinAt, fun h ↦ ?_⟩

Goal state after:
𝕜 : Type u
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
inst✝ : CompleteSpace F
h : AnalyticWithinAt 𝕜 f s x
⊢ ContDiffWithinAt 𝕜 ω f s x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
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✝ c : OrderedFinpartition n
⊢ StrictMono (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) 0)

Tactic:
exact @Subsingleton.strictMono _ _ _ _ (by simp; infer_instance) _

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

Goal state before:
pp: 𝕜 : Type u
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
n : ℕ∞ω
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
⊢ ContDiffOn 𝕜 n f s

Tactic:
intro x xs

Goal state after:
𝕜 : Type u
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
n : ℕ∞ω
h : ∀ x ∈ s, ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f s x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedDerivWithin (n + 1) f s = derivWithin (iteratedDerivWithin n f s) s

Tactic:
ext x
  by_cases hxs : AccPt x (𝓟 s)
  · rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
      iteratedFDerivWithin_eq_equiv_comp,
      LinearIsometryEquiv.comp_fderivWithin _ hxs.uniqueDiffWithinAt, derivWithin]
    change ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜
      (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun _ : Fin n => 1) =
      (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
    simp
  · simp [derivWithin_zero_of_not_accPt hxs, iteratedDerivWithin, iteratedFDerivWithin,
      fderivWithin_zero_of_not_accPt hxs]

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

Goal state before:
pp: case 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✝ c : OrderedFinpartition n
m : Fin c.length
a : Fin (c.partSize m + 1) := ⟨c.partSize m, ⋯⟩
b : Fin (c.partSize m) := ⟨c.partSize m - 1, ⋯⟩
⊢ cases 0 (succ ∘ c.emb m) a = (c.emb m b).succ

Tactic:
have : a = succ b := by
        simpa [a, b, succ] using (Nat.sub_eq_iff_eq_add (c.partSize_pos m)).mp rfl

Goal state after:
case 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✝ c : OrderedFinpartition n
m : Fin c.length
a : Fin (c.partSize m + 1) := ⟨c.partSize m, ⋯⟩
b : Fin (c.partSize m) := ⟨c.partSize m - 1, ⋯⟩
this : a = b.succ
⊢ cases 0 (succ ∘ c.emb m) a = (c.emb m b).succ
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✝ c : OrderedFinpartition n
k : Fin c.length
⊢ ∀ (x : Fin (n + 1)),
    ∃ m,
      x ∈
        range
          (if h : m = k then
            have this := ⋯;
            (fun i ↦ cases 0 (succ ∘ c.emb k) i) ∘ Fin.cast this
          else
            have this := ⋯;
            succ ∘ c.emb m ∘ Fin.cast this)

Tactic:
refine Fin.cases ?_ (fun i ↦ ?_)
    · simp only [mem_range]
      exact ⟨k, ⟨0, by simp⟩, by simp⟩
    · simp only [mem_range]
      rcases eq_or_ne (c.index i) k with rfl | hi
      · have A : update c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) =
          c.partSize (c.index i) + 1 := by simp
        exact ⟨c.index i, (succ (c.invEmbedding i)).cast A.symm, by simp⟩
      · have A : update c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i) := by
          simp [hi]
        exact ⟨c.index i, (c.invEmbedding i).cast A.symm, by simp [hi]⟩

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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
v : Fin n → E
q : E [×c.partSize m]→L[𝕜] F
d : Fin c.length
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d

Tactic:
by_cases h : d = m

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
m : Fin c.length
v : Fin n → E
q : E [×c.partSize m]→L[𝕜] F
d : Fin c.length
h : d = m
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d

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

Goal state before:
pp: β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ (map (↑f) atTop).NeBot

Tactic:
by infer_instance

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
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * (exp (0 + a✝) - 1 - (ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp x * exp a✝ - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) a✝

Tactic:
zero_add,

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
a✝ : 𝔸
hh : a✝ ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * (exp a✝ - 1 - (ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp x * exp a✝ - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) a✝
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 ((0 + h) • x) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h) =
    exp (t • x) * exp (h • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h

Tactic:
zero_add,

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) - exp (0 • x) - (ContinuousLinearMap.smulRight 1 x) h) =
    exp (t • x) * exp (h • x) - exp (t • x) - (exp (t • x) • ContinuousLinearMap.smulRight 1 x) h