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
o : Option (Fin c.length)
⊢ (fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩)
      ((fun c ↦ c.fst.extend c.snd) ⟨c, none⟩) =
    ⟨c, none⟩

Tactic:
simp only [extend, range_extendLeft_zero, ↓reduceDIte, Sigma.mk.inj_iff, heq_eq_eq,
        and_true]

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
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)
⊢ c.extendLeft.eraseLeft ⋯ = c
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
o : Option (Fin c.length)
⊢ (fun c ↦ if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩)
      ((fun c ↦ c.fst.extend c.snd) ⟨c, none⟩) =
    ⟨c, none⟩

Tactic:
simp only [extend, range_extendLeft_zero, ↓reduceDIte, Sigma.mk.inj_iff, heq_eq_eq,
        and_true]
      rfl

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
⊢ (expSeries ℚ 𝔸).sum x = (expSeries 𝕂 𝔸).sum x

Tactic:
← @expSeries_sum_eq_rat (𝕂 := 𝕂)

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
⊢ (expSeries 𝕂 𝔸).sum x = (expSeries 𝕂 𝔸).sum x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case neg.emb.refine_2.inl.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 + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ c.emb (c.index 0) 0 = cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) (Fin.cast ⋯ ⟨↑0, ⋯⟩)

pp: case neg.emb.refine_2.inl.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 + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
⊢ c.emb (c.index 0) j = cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) (Fin.cast ⋯ ⟨↑j, ⋯⟩)

Tactic:
· simpa using c.emb_zero

Goal state after:
case neg.emb.refine_2.inl.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 + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
⊢ c.emb (c.index 0) j = cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) (Fin.cast ⋯ ⟨↑j, ⋯⟩)
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
α : Type u_5
H : Type u_6
inst✝ : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖p₁ x k‖
hpf : ∀ k ≤ n, (fun a ↦ p₁ a k - p₂ a k) =O[l] f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₂ x k‖
hqf : ∀ k ≤ n, (fun a ↦ q₁ a k - q₂ a k) =O[l] f
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
⊢ (fun x ↦
      ‖p₁ x c.length‖ * ↑c.length * max ‖fun m ↦ q₁ x (c.partSize m)‖ ‖fun m ↦ q₂ x (c.partSize m)‖ ^ (c.length - 1) *
        ‖(fun m ↦ q₁ x (c.partSize m)) - fun m ↦ q₂ x (c.partSize m)‖) =O[l]
    f

Tactic:
have H₁ : (p₁ · c.length) =O[l] (1 : α → ℝ) := (hp_bdd _ c.length_le).isBigO_one ℝ

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

Goal state before:
pp: β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, dist (u n) (CauSeq.lim ⟨u, C⟩) < ε

Tactic:
obtain ⟨N, hN⟩ := (CauSeq.equiv_lim ⟨u, C⟩) _ εpos

Goal state after:
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN : ∀ j ≥ N, ‖↑(⟨u, C⟩ - CauSeq.const norm (CauSeq.lim ⟨u, C⟩)) j‖ < ε
⊢ ∃ N, ∀ n ≥ N, dist (u n) (CauSeq.lim ⟨u, C⟩) < ε
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun x ↦ Φ x i) (p i) (u i)
h'p : ∀ (i : ι) (i_1 : ℕ), AnalyticOn 𝕜 (fun x ↦ p i x i_1) (u i)
m : ℕ
L : ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i := ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
⊢ AnalyticOn 𝕜 (fun x ↦ L fun i ↦ p i x m) (⋂ i, u i)

Tactic:
apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun x ↦ Φ x i) (p i) (u i)
h'p : ∀ (i : ι) (i_1 : ℕ), AnalyticOn 𝕜 (fun x ↦ p i x i_1) (u i)
m : ℕ
L : ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i := ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
⊢ AnalyticOn 𝕜 (fun x i ↦ p i x m) (⋂ i, u i)
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
⊢ HasStrictFDerivAt (fun u ↦ exp (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (exp (t • x))) t

Tactic:
by
  let ⟨_, _⟩ := analyticAt_exp_of_mem_ball (t • x) htx
  convert! hasStrictFDerivAt_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1
  ext t'
  change Commute (t' • x) (exp (t • x))
  exact (((Commute.refl x).smul_left t').smul_right t).exp_right

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

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

Tactic:
filter_upwards [hf.eventually (by simp), hg.eventually (by simp)] with y hfy hgy
      rw [derivWithin_smul (hfy.differentiableWithinAt _) (hgy.differentiableWithinAt _)]
      all_goals simp

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

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

Tactic:
induction n generalizing f g with

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ -((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h) = -(iteratedFDerivWithin 𝕜 (i + 1) f s x) h

Tactic:
iteratedFDerivWithin_succ_apply_left

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hu : UniqueDiffOn 𝕜 s
i : ℕ
hi : ∀ {x : E}, x ∈ s → iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
x : E
hx : x ∈ s
h : Fin (i + 1) → E
⊢ -((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h) =
    -((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (h 0)) (tail h)
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
⊢ ∀ V' ∈ 𝓝 (φ x), IsClosed[inst✝¹] V' → φ ⁻¹' V' ∈ 𝓝[B] x

Tactic:
intro V' V'_in V'_closed

Goal state after:
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
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst✝¹] V'
⊢ φ ⁻¹' V' ∈ 𝓝[B] x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_5
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
n : ℕ
f : 𝕜 → 𝔸
c : 𝔸
hf : ContDiffAt 𝕜 (↑n) f x
⊢ iteratedDeriv n (fun x ↦ c * f x) x = c * iteratedDeriv n f x

Tactic:
simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_const_mul (Set.mem_univ x) uniqueDiffOn_univ c hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ extendFrom (Ioo a b) f a = la

Tactic:
apply extendFrom_eq
  · rw [closure_Ioo hab.ne]
    simp only [le_of_lt hab, left_mem_Icc]
  · simpa [hab]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
⊢ iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0

Tactic:
by
  obtain (_ | _ | n) := n <;>
    simp [iteratedDeriv_succ', iteratedDeriv_const]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
hfg : f =ᶠ[𝓝 x] g
⊢ iteratedDeriv n f x = iteratedDeriv n g x

Tactic:
by
  simp only [← iteratedDerivWithin_univ, iteratedDerivWithin_eq_iteratedFDerivWithin]
  rw [(hfg.filter_mono nhdsWithin_le_nhds).iteratedFDerivWithin_eq hfg.eq_of_nhds n]

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

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)

Tactic:
refine not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi f' <| Tendsto.congr' hderiv.symm ?_

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
⊢ Tendsto (-deriv f ∘ Neg.neg) (𝓝[>] (-a)) atTop
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t ↦ (AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : (f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)

Tactic:
rw [segment_eq_image_lineMap, exists_mem_image]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t ↦ (AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : (f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ x_1 ∈ Icc 0 1, f y - f x = (f' ((AffineMap.lineMap x y) x_1)) (y - x)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∉ s
⊢ ↑(f x) < (fun x ↦ g0 x + g1 x) x

Tactic:
· have : f x = fmeas.mk f x := by rw [Set.compl_subset_comm] at hs; exact hs h
      rw [this]
      exact (f_lt_g0 x).trans_le le_self_add

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
hs : Convex 𝕜 s
x : M
⊢ x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ c • x ∈ s

Tactic:
by
  refine hs.mem_toCone.trans ⟨?_, ?_⟩
  · rintro ⟨c, hc, y, hy, rfl⟩
    exact ⟨c⁻¹, inv_pos.2 hc, by rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩
  · rintro ⟨c, hc, hcx⟩
    exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩

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

Goal state before:
pp: case inr.hc
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
hpos : 0 < c
⊢ 0 < ↑⟨c, hc⟩

Tactic:
convert! hpos

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

Goal state before:
pp: case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ {x | -↑x - y ∈ s}.Nonempty

Tactic:
rcases dense (-y) with ⟨x, hx⟩
      rw [← neg_neg x, NegMemClass.coe_neg, ← sub_eq_add_neg] at hx
      exact ⟨_, hx⟩

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
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this✝ : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
this : ↑c * μ s ≤ ↑c * μ F + ε
⊢ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≤ ∫⁻ (x : α), ↑(F.indicator (fun x ↦ c) x) ∂μ + ε

Tactic:
simpa only [hs, F_closed.measurableSet, SimpleFunc.coe_const, Function.const_apply,
          lintegral_const, ENNReal.coe_indicator, Set.univ_inter, MeasurableSet.univ,
          SimpleFunc.const_zero, lintegral_indicator, SimpleFunc.coe_zero,
          Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, Measure.restrict_apply]

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

Goal state before:
pp: case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}

pp: case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}

Tactic:
· rw [setOfPred_gauge_le_eq hs h₀ absorbs ha]
    exact convex_iInter fun i => convex_iInter fun _ => hs.smul _

Goal state after:
case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
⊢ ∀ (m : ℝ) (x : Dual ℝ F), (m • x).extendRCLike = (RingHom.id ℝ) m • x.extendRCLike

Tactic:
by intros; ext; simp [extendRCLike_apply, real_smul_eq_coe_mul]; ring

Goal state after:
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
F : Type u_2
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
⊢ ∀ (m : ℝ) (x : StrongDual ℝ F), (m • x).extendRCLike = (RingHom.id ℝ) m • x.extendRCLike

Tactic:
by intros; ext; simp [extendRCLike_apply, real_smul_eq_coe_mul]; ring

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ gauge s y + ‖x - y‖ / ↑r = gauge s y + ↑r⁻¹ * dist x y

Tactic:
by rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
x : E
hx : x ≠ 0
⊢ ∃ f, f x ≠ 0

Tactic:
by
    rcases geometric_hahn_banach_point_point hx.symm with ⟨f, hf⟩
    simp only [map_zero] at hf
    exact ⟨f, hf.ne'⟩

Goal state after: