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

Tactic:
ext m

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

Goal state before:
pp: case insert
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
f : ι → 𝔸
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : (↑s).Pairwise (Commute on f)), exp (∑ i ∈ s, f i) = s.noncommProd (fun i ↦ exp (f i)) ⋯
h : (↑(insert a s)).Pairwise (Commute on f)
⊢ exp (∑ i ∈ insert a s, f i) = (insert a s).noncommProd (fun i ↦ exp (f i)) ⋯

Tactic:
| insert a s ha ih =>

Goal state after:
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 ℝ
    have H₂ : ∀ m, (q₁ · (c.partSize m)) =O[l] (1 : α → ℝ) := fun m ↦
      (hq₁_bdd _ <| c.partSize_le _).isBigO_one ℝ
    have H₃ : ∀ m, (q₂ · (c.partSize m)) =O[l] (1 : α → ℝ) := fun m ↦
      (hq₂_bdd _ <| c.partSize_le _).isBigO_one ℝ
    have H₄ : ∀ m, (fun a ↦ q₁ a (c.partSize m) - q₂ a (c.partSize m)) =O[l] f := fun m ↦
      hqf _ <| c.partSize_le _
    rw [← Asymptotics.isBigO_pi] at H₂ H₃ H₄
    have H₅ := ((H₂.prod_left H₃).norm_left.pow (c.length - 1)).mul H₄.norm_norm
    simpa [mul_assoc] using! H₁.norm_left.mul <| H₅.const_mul_left c.length

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

Goal state before:
pp: ⊢ AnalyticOnNhd ℝ rexp univ

Tactic:
rw [Real.exp_eq_exp_ℝ]
  exact fun x _ ↦ NormedSpace.exp_analytic x

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (a : ℝ≥0) in 𝓝[>] 0, x + ↑a • y ∈ s
⊢ y ∈ posTangentConeAt s x

Tactic:
frequently_iff_neBot

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : (𝓝[>] 0 ⊓ 𝓟 {x_1 | x + ↑x_1 • y ∈ s}).NeBot
⊢ y ∈ posTangentConeAt s x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ 0 ≤ f' y

Tactic:
by simpa using h.hasFDerivWithinAt_nonpos hf hy'

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMin f a
⊢ fderiv ℝ f a = 0

Tactic:
classical
  exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
  else fderiv_zero_of_not_differentiableAt hf

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMax f a
⊢ fderiv ℝ f a = 0

Tactic:
classical
  exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
  else fderiv_zero_of_not_differentiableAt hf

Goal state after:
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' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst✝¹] V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst✝²] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
⊢ φ y ∈ V'

Tactic:
have hVy : V ∈ 𝓝 y := IsOpen.mem_nhds V_op hyV

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 : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen[inst✝²] V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : (𝓝[A] y).NeBot
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
⊢ φ y ∈ V'
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case succ.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
⊢ ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x

Tactic:
obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)

Goal state after:
case succ.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
⊢ ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: case pos
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 : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
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
z : ℝ
hz : z ∈ Icc a b
hz' : z = a
⊢ ContinuousWithinAt f (Icc a b) a

Tactic:
exact hcont_at_a.mono Icc_subset_Ici_self

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
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
⊢ ∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε

Tactic:
rcases exists_pos_lintegral_lt_of_sigmaFinite μ this with ⟨w, wpos, wmeas, wint⟩

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2
⊢ ∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
⊢ ∀ {a b : M}, a ∈ ↑C - ↑C → b ∈ ↑C - ↑C → a + b ∈ ↑C - ↑C

Tactic:
rintro _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩

Goal state after:
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
y₁ : M
hy₁ : y₁ ∈ ↑C
z₁ : M
hz₁ : z₁ ∈ ↑C
y₂ : M
hy₂ : y₂ ∈ ↑C
z₂ : M
hz₂ : z₂ ∈ ↑C
⊢ (fun x1 x2 ↦ x1 - x2) y₁ z₁ + (fun x1 x2 ↦ x1 - x2) y₂ z₂ ∈ ↑C - ↑C
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: f : ℝ → ℝ
x f' : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun y ↦ Real.log (f y)) (f' / f x) x

Tactic:
rw [← hasDerivWithinAt_univ] at *
  exact hf.log hx

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

Goal state before:
pp: x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Tactic:
push_cast

Goal state after:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n ↦ -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (2 * ↑n + 1)) + x ^ (2 * n + 1) / (2 * ↑n + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : x ∈ δ • s
⊢ (r⁻¹ * δ) • δ⁻¹ • x ∈ s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ δ_pos.ne'] at hδ

Goal state after:
case refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
h : gauge s x ≤ a
r : ℝ
hr : a < r
hr' : 0 < r
δ : ℝ
δ_pos : 0 < δ
hδr : δ < r
hδ : δ⁻¹ • x ∈ s
⊢ (r⁻¹ * δ) • δ⁻¹ • x ∈ s
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inr.inr.refine_1.refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
⊢ f ≠ 0

Tactic:
rintro rfl

Goal state after:
case inr.inr.refine_1.refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : x₀ ∉ C
hf₁ : 0 x₀ = 1
hf₂ : ∀ x ∈ C, 0 x < 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, 0 a ≤ 0 b
⊢ False
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inr.inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s✝, f a < s
hf₂ : ∀ b ∈ t, s ≤ f b
⊢ f ≠ 0

Tactic:
rintro rfl

Goal state after:
case inr.inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
s : ℝ
hf₁ : ∀ a ∈ s✝, 0 a < s
hf₂ : ∀ b ∈ t, s ≤ 0 b
⊢ False
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case pos.bound_summable
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → Summable fun n ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f n)‖

pp: case pos.bound_integrable
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f n)‖)
    volume a b

pp: case pos.h_lim
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n ↦ (f n) t) (∑' (i : ι), (f i) t)

Tactic:
· exact ae_of_all _ fun x _ => hf_sum

Goal state after:
case pos.bound_integrable
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ IntervalIntegrable (fun t ↦ ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f n)‖)
    volume a b

case pos.h_lim
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n ↦ (f n) t) (∑' (i : ι), (f i) t)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ (a', z).1 ∈ u

Tactic:
exact ha'x'.1

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ (a', y).1 ∈ u

Tactic:
exact ha'x'.1

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c • ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x

Tactic:
by
  by_cases hc : c = 0 <;> simp [hc, integral_comp_sub_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Tactic:
continuousOn_congr this

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x ↦ ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b)
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, ↑n)

Tactic:
rw [ContinuousAt, nhds_prod_eq, ← nhdsLT_sup_nhdsGE (n : α), prod_sup, tendsto_sup]

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 s ×ˢ 𝓝[<] ↑n) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n))) ∧
    Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 s ×ˢ 𝓝[≥] ↑n) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n)))
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ Continuous fun θ ↦ (circleMap z R θ - w)⁻¹

Tactic:
have : ∀ θ, circleMap z R θ - w ≠ 0 := by
    simp_rw [sub_ne_zero]
    exact fun θ => circleMap_ne_mem_ball hw θ

Goal state after:
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ ↦ (circleMap z R θ - w)⁻¹
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ y ∈ Box.Icc (I.face i),
    ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤ 2 * ε * diam (Box.Icc I)
⊢ ‖integral (I.face i) ⊥
        (fun x ↦ f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) x) - f (e (I.lower i) x)))
        BoxAdditiveMap.volume‖ ≤
    (volume ↑(I.face i)).toReal * (2 * ε * ↑c * (I.upper i - I.lower i))

Tactic:
by
      -- The hard part of the estimate was done above, here we just replace `diam I.Icc`
      -- with `c * (I.upper i - I.lower i)`
      refine norm_integral_le_of_le_const (fun y hy => (this y hy).trans ?_) volume
      rw [mul_assoc (2 * ε)]
      gcongr
      exact I.diam_Icc_le_of_distortion_le i hc

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case inl
n : ℤ
c w : ℂ
hn : n < 0
hw : w ∈ sphere c |0|
⊢ ∮ (z : ℂ) in C(c, 0), (z - w) ^ n = 0

Tactic:
apply integral_radius_zero

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
⊢ ∫ (x : α), f x • ∫ (a : β), g a ∂ν ∂μ = (∫ (x : α), f x ∂μ) • ∫ (a : β), g a ∂ν

Tactic:
integral_smul_const

Goal state after: