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

Goal state before:
pp: case mpr.refine_2
𝕜 : 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
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v
⊢ (∀ x ∈ v ∩ u, ((p' x).unshift (f x) 0).curry0 = f x) ∧
    (∀ x ∈ v ∩ u, HasFDerivWithinAt (fun y ↦ (p' y).unshift (f y) 0) ((p' x).unshift (f x) 1).curryLeft (v ∩ u) x) ∧
      HasFTaylorSeriesUpToOn n (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) ((p' x).unshift (f x) 1))
        (fun x ↦ ((p' x).unshift (f x)).shift) (v ∩ u)

Tactic:
refine ⟨fun y _ => rfl, fun y hy => ?_, ?_⟩

Goal state after:
case mpr.refine_2.refine_1
𝕜 : 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
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v
y : E
hy : y ∈ v ∩ u
⊢ HasFDerivWithinAt (fun y ↦ (p' y).unshift (f y) 0) ((p' y).unshift (f y) 1).curryLeft (v ∩ u) y

case mpr.refine_2.refine_2
𝕜 : 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
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v
⊢ HasFTaylorSeriesUpToOn n (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) ((p' x).unshift (f x) 1))
    (fun x ↦ ((p' x).unshift (f x)).shift) (v ∩ u)
Module: Mathlib.Analysis.Calculus.Deriv.Inverse

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
c : F
hf : DifferentiableWithinAt 𝕜 f s x
h : derivWithin f s x ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {x}] x, f x ≠ c

Tactic:
exact hf.hasDerivWithinAt.eventually_ne h

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

Goal state before:
pp: case 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✝ c : OrderedFinpartition n
k m : Fin c.length
hm : m ≠ k
⊢ 0 < update c.partSize k (c.partSize k + 1) m

Tactic:
· simpa [hm] using c.partSize_pos m

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' b' : Fin (c.partSize m + 1)
h' : a' < b'
⊢ cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'

Tactic:
induction b' using Fin.induction with

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

Goal state before:
pp: case fderivWithin
𝕜 : 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
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
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

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
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
a' : Fin (c.partSize i)
b' : Fin (c.partSize j + 1)
⊢ (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) b'

Tactic:
induction b' using Fin.induction with

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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
m : ℕ
x : E
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 (↑m + 1) f s x

Tactic:
rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp),
      insert_eq_of_mem hx]

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
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y ↦ fderivWithin 𝕜 f s y) s
m : ℕ
x : E
hx : x ∈ s
⊢ ∃ u ∈ 𝓝[s] x,
    (↑m = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑m) f' u x
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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x

Tactic:
rcases (contDiffWithinAt_succ_iff_hasFDerivWithinAt (n := m) (ne_of_beq_false rfl)).1
      (H.of_le (by gcongr) x hx) with ⟨u, hu, -, f', hff', hf'⟩

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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
f' : E → E →L[𝕜] F
hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 (↑m) f' u x
⊢ ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo ω f p
h'p : ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x ↦ p x i) univ
x : E
a✝ : x ∈ univ
⊢ ContDiffWithinAt 𝕜 ω f univ x

Tactic:
exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le le_top,
        fun i ↦ (h'p i).analyticOn⟩

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

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

Tactic:
rw [index_extendMiddle_zero]

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 a ((c.extendMiddle a).partSize a - 1) a
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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

Tactic:
rw [index_extendMiddle_zero]

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 i ((c.extendMiddle i).partSize i - 1) a
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ ((↑(kl.1 + kl.2)!)⁻¹ * (↑(kl.1 + kl.2)! / (↑kl.1! * ↑kl.2!))) • (x ^ kl.1 * y ^ kl.2) =
    ((↑kl.1!)⁻¹ * (↑kl.2!)⁻¹) • (x ^ kl.1 * y ^ kl.2)

Tactic:
Finset.mem_antidiagonal.mp hkl

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ ((↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!))) • (x ^ kl.1 * y ^ kl.2) = ((↑kl.1!)⁻¹ * (↑kl.2!)⁻¹) • (x ^ kl.1 * y ^ kl.2)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Summable fun n ↦ ‖x ^ n / ↑n !‖

Tactic:
change Summable (norm ∘ _)
  rw [← expSeries_apply_eq_div' (𝕂 := 𝕂) x]
  exact norm_expSeries_summable_of_mem_ball x hx

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 : α
lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ContinuousOn (f ∘ ⇑OrderDual.ofDual) (Ioo (OrderDual.toDual b) (OrderDual.toDual a)) →
    Tendsto (f ∘ ⇑OrderDual.ofDual) (𝓝[>] OrderDual.toDual b) (𝓝 lb) →
      ContinuousOn (extendFrom (Ioo (OrderDual.toDual b) (OrderDual.toDual a)) (f ∘ ⇑OrderDual.ofDual))
        (Ico (OrderDual.toDual b) (OrderDual.toDual a))
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Tactic:
rw [Ico_toDual, Ioi_toDual, Ioo_toDual] at this

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
lb : β
inst✝ : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ContinuousOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' Ioo a b) →
    Tendsto (f ∘ ⇑OrderDual.ofDual) (𝓝[⇑OrderDual.ofDual ⁻¹' Iio b] OrderDual.toDual b) (𝓝 lb) →
      ContinuousOn (extendFrom (⇑OrderDual.ofDual ⁻¹' Ioo a b) (f ∘ ⇑OrderDual.ofDual)) (⇑OrderDual.ofDual ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
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 : ℕ∞ω
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 n (Prod.map f g)

Tactic:
by
  rw [contDiff_iff_contDiffAt] at *
  exact fun ⟨x, y⟩ => (hf x).prodMap (hg y)

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

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
hcont : ContinuousOn f (Icc a b)
x : ℝ
hb : max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hx₁ : x ∈ Ioo a b
hx₂ : derivWithin f (Ioi a) x = slope f a b
⊢ False

Tactic:
rw [hx₂, max_lt_iff] at hb

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
hcont : ContinuousOn f (Icc a b)
x : ℝ
hb : derivWithin f (Ioi a) a + 1 < slope f a b ∧ 0 < slope f a b
hx₁ : x ∈ Ioo a b
hx₂ : derivWithin f (Ioi a) x = slope f a b
⊢ False
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
x : M
hx : x ∈ ⇑f ⁻¹' ↑C
y : M
hy : y ∈ ⇑f ⁻¹' ↑C
⊢ x + y ∈ ⇑f ⁻¹' ↑C

Tactic:
rw [mem_preimage, f.map_add]
    exact add_mem hx hy

Goal state after:
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✝¹ : AddCommGroup G
inst✝ : SMul R G
C✝ C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
⊢ a = b

Tactic:
by_contra h

Goal state after:
𝕜 : 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✝¹ : AddCommGroup G
inst✝ : SMul R G
C✝ C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
⊢ False
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
fr : Dual ℝ F
x : F
⊢ re ((starRingEnd 𝕜) (fr.extendRCLike x) * fr.extendRCLike x) = fr ((starRingEnd 𝕜) (fr.extendRCLike x) • x)

Tactic:
by
    rw [← smul_eq_mul, ← map_smul, re_extendRCLike_apply]

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

Goal state before:
pp: E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
hrc : r < c⁻¹
z : E
hz : z ∈ u
hy : (fun x ↦ c⁻¹ • x) z ∈ s
hx : gauge s ((fun x ↦ c • x) ((fun x ↦ c⁻¹ • x) z)) < r⁻¹
⊢ (fun x ↦ c • x) ((fun x ↦ c⁻¹ • x) z) ∈ u

Tactic:
simpa only [smul_inv_smul₀ hc₀.ne']

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

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
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:
rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one]
    at h_gauge_lt

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

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
⊢ 0 = p x

Tactic:
by_contra h

Goal state after:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
⊢ False
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:
rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv]

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

Goal state before:
pp: E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
x y : E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : StrongDual ℝ E
s t : ℝ
hs : ∀ a ∈ {x}, f a < s
st : s < t
ht : ∀ b ∈ {y}, t < f b
⊢ f x < f y

Tactic:
by linarith [hs x rfl, ht y rfl]

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

Goal state before:
pp: E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, i x ≤ i y}
⊢ x ∈ s

Tactic:
by_contra h

Goal state after:
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : StrongDual ℝ E), ∃ y ∈ s, i x ≤ i y}
h : x ∉ s
⊢ False
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
x y : E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : StrongDual 𝕜 E
s t : ℝ
hs : ∀ a ∈ {x}, re (f a) < s
st : s < t
ht : ∀ b ∈ {y}, t < re (f b)
⊢ re (f x) < re (f y)

Tactic:
by linarith [hs x rfl, ht y rfl]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : StrongDual 𝕜 E), ∃ y ∈ s, re (i x) ≤ re (i y)}
⊢ x ∈ s

Tactic:
by_contra h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : StrongDual 𝕜 E), ∃ y ∈ s, re (i x) ≤ re (i y)}
h : x ∉ s
⊢ False
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : StrongDual 𝕜 E) (i_1 : ℝ), (∀ y ∈ s, re (i y) ≤ i_1) → re (i x) ≤ i_1}
⊢ x ∈ s

Tactic:
by_contra h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : StrongDual 𝕜 E) (i_1 : ℝ), (∀ y ∈ s, re (i y) ≤ i_1) → re (i x) ≤ i_1}
h : x ∉ s
⊢ False