mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
s : Set X
heq : EqOn (↑e) (↑e') (e'.source ∩ interior s)
hsub : e'.source ∩ interior s ⊆ e.source
⊢ (e.restr (e'.source ∩ interior s)).source = (e'.restr s).source

Tactic:
rw [e'.restr_source s, e.restr_source' _ (e'.open_source.inter isOpen_interior),
    inter_eq_right.mpr hsub]

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

Goal state before:
pp: n : ℕ
c : OrderedFinpartition n
inst✝ : NeZero n
⊢ c.emb (c.index 0) 0 ≤ 0

Tactic:
conv_rhs => rw [← c.emb_invEmbedding 0]

Goal state after:
n : ℕ
c : OrderedFinpartition n
inst✝ : NeZero n
⊢ c.emb (c.index 0) 0 ≤ c.emb (c.index 0) (c.invEmbedding 0)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case zero
𝕜 : 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
i : Fin (c.length + 1)
hij : i < 0
⊢ (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      i <
    (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      0

Tactic:
simp at hij

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

Goal state before:
pp: case mp
𝕜 : 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
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 0 f s x → ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)

Tactic:
intro h
    obtain ⟨u, H, p, hp⟩ := h 0 le_rfl
    refine ⟨u, ?_, ?_⟩
    · simpa [hx] using H
    · simp only [Nat.cast_zero, hasFTaylorSeriesUpToOn_zero_iff] at hp
      exact hp.1.mono inter_subset_right

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 : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s

Tactic:
by
  constructor
  · intro x _
    simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
      iteratedFDerivWithin_zero_apply]
  · intro m hm x hx
    have : (m + 1 : ℕ) ≤ n := ENat.add_one_natCast_le_withTop_of_lt hm
    rcases (h x hx).of_le this _ le_rfl with ⟨u, hu, p, Hp⟩
    rw [insert_eq_of_mem hx] at hu
    rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
    rw [inter_comm] at ho
    have : p x m.succ = ftaylorSeriesWithin 𝕜 f s x m.succ := by
      change p x m.succ = iteratedFDerivWithin 𝕜 m.succ f s x
      rw [← iteratedFDerivWithin_inter_open o_open xo]
      exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩
    rw [← this, ← hasFDerivWithinAt_inter (IsOpen.mem_nhds o_open xo)]
    have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m := by
      rintro y ⟨hy, yo⟩
      change p y m = iteratedFDerivWithin 𝕜 m f s y
      rw [← iteratedFDerivWithin_inter_open o_open yo]
      exact
        (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m)
          (hs.inter o_open) ⟨hy, yo⟩
    exact
      ((Hp.mono ho).fderivWithin m (mod_cast lt_add_one m) x ⟨hx, xo⟩).congr
        (fun y hy => (A y hy).symm) (A x ⟨hx, xo⟩).symm
  · intro m hm
    apply continuousOn_of_locally_continuousOn
    intro x hx
    rcases (h x hx).of_le hm _ le_rfl with ⟨u, hu, p, Hp⟩
    rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
    rw [insert_eq_of_mem hx] at ho
    rw [inter_comm] at ho
    refine ⟨o, o_open, xo, ?_⟩
    have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m := by
      rintro y ⟨hy, yo⟩
      change p y m = iteratedFDerivWithin 𝕜 m f s y
      rw [← iteratedFDerivWithin_inter_open o_open yo]
      exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩
    exact ((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm

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

Goal state before:
pp: case neg.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
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
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ c.emb i (Fin.cast ⋯ j) ≠ 0

Tactic:
conv_rhs => rw [← c.emb_invEmbedding 0]

Goal state after:
case neg.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
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
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ c.emb i (Fin.cast ⋯ j) ≠ c.emb (c.index 0) (c.invEmbedding 0)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 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 ⋯

Tactic:
refine (Fin.heq_fun_iff ?_).mpr ?_

Goal state after:
case emb.inl.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✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
a : Fin c.length
⊢ c.partSize a =
    update (c.extendMiddle a).partSize ((c.extendMiddle a).index 0)
      ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a

case emb.inl.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
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
⊢ ∀ (i : Fin (c.partSize a)),
    c.emb a i =
      if h : a = a then ((c.extendMiddle a).emb a (Fin.cast ⋯ ⟨↑i, ⋯⟩.succ)).pred ⋯
      else ((c.extendMiddle a).emb a (Fin.cast ⋯ ⟨↑i, ⋯⟩)).pred ⋯
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 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 ⋯

Tactic:
refine (Fin.heq_fun_iff ?_).mpr ?_

Goal state after:
case emb.inr.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✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition n
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ c.partSize a =
    update (c.extendMiddle i).partSize ((c.extendMiddle i).index 0)
      ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a

case emb.inr.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
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
⊢ ∀ (i_1 : Fin (c.partSize a)),
    c.emb a i_1 =
      if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ ⟨↑i_1, ⋯⟩.succ)).pred ⋯
      else ((c.extendMiddle i).emb a (Fin.cast ⋯ ⟨↑i_1, ⋯⟩)).pred ⋯
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.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 + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
⊢ cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
      (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i ≍
    c.emb (Fin.cast A i)

Tactic:
refine (Fin.heq_fun_iff ?_).mpr ?_

Goal state after:
case pos.emb.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✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
⊢ cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i = c.partSize (Fin.cast A i)

case pos.emb.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
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}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
⊢ ∀ (i_1 : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i)),
    cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
        (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i i_1 =
      c.emb (Fin.cast A i) ⟨↑i_1, ⋯⟩
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.emb.refine_2.zero
𝕜 : 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}
A : c.length - 1 + 1 = c.length
h' : 0 ≍ Fin.cast A 0
j : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)
⊢ cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
      (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) 0 j =
    c.emb (Fin.cast A 0) ⟨↑j, ⋯⟩

Tactic:
simp only [cases_zero, cast_zero, val_eq_zero]

Goal state after:
case pos.emb.refine_2.zero
𝕜 : 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}
A : c.length - 1 + 1 = c.length
h' : 0 ≍ Fin.cast A 0
j : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) 0)
⊢ 0 = c.emb 0 ⟨0, ⋯⟩
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✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp (-x) * exp x = 1

Tactic:
have hnx : -x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := by
      rw [Metric.mem_eball, ← neg_zero, edist_neg_neg]
      exact hx
    rw [← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx,
      neg_add_cancel, exp_zero]

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
⊢ c.applyOrderedFinpartition (update p m q) v = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m))

Tactic:
by
  ext d
  by_cases h : d = m
  · rw [h]
    simp [applyOrderedFinpartition]
  · simp [h, applyOrderedFinpartition]

Goal state after:
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‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ ‖↑f a' - ↑f b'‖ < ε

Tactic:
apply hN <;> assumption

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
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
H₁ : (fun a ↦ p₁ a c.length - p₂ a c.length) =O[l] f
⊢ (fun x ↦ ‖p₁ x c.length - p₂ x c.length‖ * ∏ i, ‖q₂ x (c.partSize i)‖) =O[l] f

Tactic:
have H₂ : ∀ i, (q₂ · (c.partSize i)) =O[l] (1 : α → ℝ) := fun i ↦
      (hq₂_bdd _ <| c.partSize_le i).isBigO_one ℝ

Goal state after:
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
H₁ : (fun a ↦ p₁ a c.length - p₂ a c.length) =O[l] f
H₂ : ∀ (i : Fin c.length), (fun x ↦ q₂ x (c.partSize i)) =O[l] 1
⊢ (fun x ↦ ‖p₁ x c.length - p₂ x c.length‖ * ∏ i, ‖q₂ x (c.partSize i)‖) =O[l] f
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 : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ∀ x ∈ univ, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)

Tactic:
simpa using hf

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 : ℕ∞ω
A : Type u_4
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : Module A F
inst✝¹ : IsScalarTower 𝕜 A F
inst✝ : IsBoundedSMul A F
f : E → A
x : E
hf : ContDiffWithinAt 𝕜 n f univ x
v : F
⊢ ContDiffWithinAt 𝕜 n (fun y ↦ f y • v) univ x

Tactic:
exact hf.smul_const v

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

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : ∀ t ∈ atTop, ∃ i, a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
⊢ ∃ i, a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1

Tactic:
obtain ⟨b, hab, hb⟩ := hf (Ioi (max (derivWithin f (Ioi a) a + 1) 0)) (Ioi_mem_atTop _)

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : ∀ t ∈ atTop, ∃ i, a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
hb : MapsTo (derivWithin f (Ioi a)) (Ioo a b) (Ioi (max (derivWithin f (Ioi a) a + 1) 0))
⊢ ∃ i, a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ < y
x : ℝ
hx : x ∈ interior D
⊢ -C < deriv (fun y ↦ -f y) x

Tactic:
rw [deriv.fun_neg, neg_lt_neg_iff]

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ < y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x < C
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ f y ≤ f x

Tactic:
by
  simpa only [zero_mul, sub_nonpos] using
    hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos x hx y hy hxy

Goal state after:
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
y₁ : M
r₁ : 𝕜
hr₁ : 0 < r₁
hy₁ : y₁ ∈ r₁ • s
y₂ : M
r₂ : 𝕜
hr₂ : 0 < r₂
hy₂ : y₂ ∈ r₂ • s
⊢ y₁ + y₂ ∈ r₁ • s + r₂ • s

Tactic:
exact add_mem_add hy₁ hy₂

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

Goal state before:
pp: case e_a.e_f
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
i : ℕ
⊢ y ^ i = ↑(i + 1) * y ^ i / (↑i + 1)

Tactic:
Nat.cast_succ,

Goal state after:
case e_a.e_f
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
i : ℕ
⊢ y ^ i = (↑i + 1) * y ^ i / (↑i + 1)
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
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, hz⟩ ∈ s
⊢ 0 ≤ ↑(f.supSpanSingleton y (-c) hy) ⟨x + r • y, hz⟩

Tactic:
simp only at hzs

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
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
⊢ 0 ≤ ↑(f.supSpanSingleton y (-c) hy) ⟨x + r • y, hz⟩
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)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ interior (Set.Icc 0 x)
⊢ 0 ≤ F' y

Tactic:
simp only [interior_Icc, Set.mem_Ioo] at hy

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
y : ℝ
hy : 0 < y ∧ y < x
⊢ 0 ≤ F' y