mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hab : a < b
g g' : ℝ → ℝ
lfa lga lfb lgb : ℝ
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)
hga : Tendsto g (𝓝[>] a) (𝓝 lga)
hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)
h : ℝ → ℝ := fun x ↦ (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[>] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[<] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x ↦ (lgb - lga) * f' x - (lfb - lfa) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x

Tactic:
exact ((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)

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))
⊢ ∃ 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:
rw [(nhdsGT_basis a).tendsto_left_iff] at hf

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))
⊢ ∃ 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 : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
⊢ ∀ x ∈ D, ∀ y ∈ D, x < y → C * (y - x) < f y - f x

Tactic:
by
  intro x hx y hy hxy
  have hxyD : Icc x y ⊆ D := hD.ordConnected.out hx hy
  have hxyD' : Ioo x y ⊆ interior D :=
    subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
  obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
    exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD')
  have : C < (f y - f x) / (y - x) := ha ▸ hf'_gt _ (hxyD' a_mem)
  exact (lt_div_iff₀ (sub_pos.2 hxy)).1 this

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✝⁵ : 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]

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✝⁵ : 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
⊢ f x + f y ∈ ↑C
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case h₁
𝕜 : 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
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ ‖f (x + y) - f x - L₂ (x + y - x)‖ ≤ ε * r

Tactic:
apply le_of_mem_A h₂
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]

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

Goal state before:
pp: n : ℕ∞ω
x : ℝ
hx : ¬x = 0
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x

Tactic:
exact (contDiffAt_log.2 hx).contDiffWithinAt

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

Goal state before:
pp: n : ℕ∞ω
⊢ ContDiffOn ℝ n log {0}ᶜ

Tactic:
intro x hx
  push _ ∈ _ at hx
  exact (contDiffAt_log.2 hx).contDiffWithinAt

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✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ConvexCone 𝕜 M

Tactic:
apply ConvexCone.mk (⋃ (c : 𝕜) (_ : 0 < c), c • s)

Goal state after:
case smul_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃c : 𝕜⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → c • x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s

case add_mem'
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ ∀ ⦃x : M⦄,
    x ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → ∀ ⦃y : M⦄, y ∈ ⋃ c, ⋃ (_ : 0 < c), c • s → x + y ∈ ⋃ c, ⋃ (_ : 0 < c), c • s
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
⊢ Summable fun n ↦ x ^ (n + 1) / (↑n + 1)

Tactic:
refine .of_norm_bounded (summable_geometric_of_lt_one (abs_nonneg _) h) fun i => ?_

Goal state after:
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ ≤ |x| ^ i
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑(fs x) ≤ ↑(f x)
int_fs : ∫⁻ (x : α), ↑(f x) ∂μ < (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ + ε / 2
⊢ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(fs x) ∂μ + ε / 2

Tactic:
convert! int_fs.le

Goal state after:
case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), ↑(fs x) ≤ ↑(f x)
int_fs : ∫⁻ (x : α), ↑(f x) ∂μ < (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ + ε / 2
⊢ ∫⁻ (x : α), ↑(fs x) ∂μ = (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
⊢ gauge s x = 0 ↔ x = 0

Tactic:
refine ⟨fun h₀ ↦ by_contra fun (hne : x ≠ 0) ↦ ?_, fun h ↦ h.symm ▸ gauge_zero⟩
  have : {x}ᶜ ∈ comap (gauge s) (𝓝 0) :=
    comap_gauge_nhds_zero_le hs hb (isOpen_compl_singleton.mem_nhds hne.symm)
  rcases ((nhds_basis_zero_abs_lt _).comap _).mem_iff.1 this with ⟨r, hr₀, hr⟩
  exact hr (by simpa [h₀]) 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
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
this : ContinuousSMul ℝ E
g : StrongDual ℝ E
hg : g x₀ = 1 ∧ ∀ x ∈ s, g x < 1
⊢ ∃ f, re (f x₀) = 1 ∧ ∀ x ∈ s, re (f x) < 1

Tactic:
use g.extendRCLikeₗ

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
this : ContinuousSMul ℝ E
g : StrongDual ℝ E
hg : g x₀ = 1 ∧ ∀ x ∈ s, g x < 1
⊢ re ((StrongDual.extendRCLikeₗ g) x₀) = 1 ∧ ∀ x ∈ s, re ((StrongDual.extendRCLikeₗ g) x) < 1
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 t : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
this : ContinuousSMul ℝ E
g : StrongDual ℝ E
u v : ℝ
h1 : (∀ a ∈ s, g a < u) ∧ u < v ∧ ∀ b ∈ t, v < g b
⊢ ∃ f u v, (∀ a ∈ s, re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < re (f b)

Tactic:
use g.extendRCLikeₗ

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s t : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
this : ContinuousSMul ℝ E
g : StrongDual ℝ E
u v : ℝ
h1 : (∀ a ∈ s, g a < u) ∧ u < v ∧ ∀ b ∈ t, v < g b
⊢ ∃ u v, (∀ a ∈ s, re ((StrongDual.extendRCLikeₗ g) a) < u) ∧ u < v ∧ ∀ b ∈ t, v < re ((StrongDual.extendRCLikeₗ g) b)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
e p q e' p' q' : ℕ
hp : n e ≤ p
hq : n e ≤ q
hp' : n e' ≤ p'
hq' : n e' ≤ q'
he' : e ≤ e'
r : ℕ := max (n e) (n e')
I : (1 / 2) ^ e' ≤ (1 / 2) ^ e
I1 : x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e)
I2 : x ∈ A f (L e p r) ((1 / 2) ^ p) ((1 / 2) ^ e)
⊢ ‖L e p q - L e p r‖ ≤ 4 * (1 / 2) ^ e

Tactic:
exact norm_sub_le_of_mem_A P _ I1 I2

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u : X → E
⊢ ∀ ⦃g : X → E⦄,
    u =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g →
      Integrable u (μ.withDensity fun x ↦ ↑(f x)) →
        (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ →
          (∫ (x : X), g x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • g x ∂μ

Tactic:
v

Goal state after:
case pos.refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u v : X → E
⊢ u =ᵐ[μ.withDensity fun x ↦ ↑(f x)] v →
    Integrable u (μ.withDensity fun x ↦ ↑(f x)) →
      (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ →
        (∫ (x : X), v x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • v x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (c + x)) volume (a - c) (b - c)

Tactic:
by
  simpa [add_comm] using IntervalIntegrable.comp_add_right hf c h

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
μ : Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ |∫ (x : ℝ) in Ι a b, g x ∂μ|

Tactic:
exact (norm_integral_le_of_norm_le hbound.def' h).trans (le_abs_self _)

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 C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * |b - a| = C * (max a b - min a b)

Tactic:
max_sub_min_eq_abs

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ C * |b - a| = C * |b - a|
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
⊢ ({t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty

Tactic:
have I3 : ∀ᶠ u in 𝓝[>] t, g u - g t ≤ ∫ w in t..u, (G' w).toReal := by
      filter_upwards [I1, I2] with u hu1 hu2 using hu2.trans hu1

Goal state after:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
⊢ ({t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n ↦ ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ), f x ∂μ)

Tactic:
← setIntegral_univ,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n ↦ ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ) in univ, f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) μ

Tactic:
by
  refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_
  have : Bijective (codRestrict (fun n : ℤ => n • T) (AddSubgroup.zmultiples T) _) :=
    (Equiv.ofInjective (fun n : ℤ => n • T) (zsmul_left_strictMono hT).injective).bijective
  refine this.existsUnique_iff.2 ?_
  simpa only [add_comm x] using! existsUnique_add_zsmul_mem_Ioc hT x t

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

Goal state before:
pp: case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
⊢ Tendsto (fun n ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))

Tactic:
by_cases hx : a₀ < x <;> apply tendsto_const_nhds.congr'

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
⊢ (fun x_1 ↦ if a₀ < x then f x else 0) =ᶠ[𝓝[≥] a₀] fun n ↦ if n < x then f x else 0

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
⊢ (fun x_1 ↦ if a₀ < x then f x else 0) =ᶠ[𝓝[≥] a₀] fun n ↦ if n < x then f x else 0
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Icc a₀ a) a

Tactic:
have h_split : ∀ b ∈ Icc a₀ a, ∫ x in Ioi b, f x ∂μ =
        (∫ x in Ioi a₀, f x ∂μ) - ∫ x in a₀..b, f x ∂μ := by
      intro b hb
      simp [← integral_Ioi_sub_Ioi hf hb.1]

Goal state after:
case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
h_split : ∀ b ∈ Icc a₀ a, ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a₀, f x ∂μ - ∫ (x : ℝ) in a₀..b, f x ∂μ
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Icc a₀ a) a
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn f' (Set.Icc a b) volume

Tactic:
intervalIntegrable_iff_integrableOn_Ioc_of_le hle

Goal state after:
case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntegrableOn f' (Set.Ioc a b) volume
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn f' (Set.Icc a b) volume
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case a
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : p.Monic
h2 : (map f p).Splits
h3 : p.natDegree ≤ d
h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ p.natDegree.choose i ≤ d.choose (d / 2)

Tactic:
exact (i.choose_mono h3).trans (i.choose_le_middle d)

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = z.im

Tactic:
rw [hz2]

Goal state after:
case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := (p.rootSet ℂ).toFinset
b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset
c : Finset ℂ :=
  Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
A : Type u_2
inst✝³ : Field A
inst✝² : CharZero A
inst✝¹ : NumberField K
inst✝ : IsAlgClosed A
⊢ Fintype.card (K →+* A) = finrank ℚ K

Tactic:
Fintype.ofEquiv_card (RingHom.equivRatAlgHom K A).symm,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
A : Type u_2
inst✝³ : Field A
inst✝² : CharZero A
inst✝¹ : NumberField K
inst✝ : IsAlgClosed A
⊢ Fintype.card (K →ₐ[ℚ] A) = finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ ↦ φ x) = (minpoly ℚ x).rootSet A

Tactic:
convert! (NumberField.isAlgebraic K).range_eval_eq_rootSet_minpoly A x using 1

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ ↦ φ x) = range fun ψ ↦ ψ x
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case refine_3
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ Set.MapsTo (fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) (Set.range (⇑v ∘ ⇑(algebraMap O F)))
    {x | x ≤ 1}

pp: case refine_4
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)),
    ∀ b ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)),
      a > b → ((fun x1 x2 ↦ x1 > x2) on fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) a b

Tactic:
· intro
    simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_ofPred_eq,
      forall_exists_index]
    rintro x rfl
    simp [← Subtype.coe_le_coe, hv.map_le_one]

Goal state after:
case refine_4
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)),
    ∀ b ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)),
      a > b → ((fun x1 x2 ↦ x1 > x2) on fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) a b
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ ↑(s.sup fun i ↦ ‖f i‖₊) = s.sup' hs' fun i ↦ ‖f i‖

pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ (↑s).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊

Tactic:
← Finset.sup'_eq_sup hs'

Goal state after:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ ↑(s.sup' hs' fun i ↦ ‖f i‖₊) = s.sup' hs' fun i ↦ ‖f i‖

M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s).Pairwise fun i j ↦ ‖f i‖ ≠ ‖f j‖
⊢ (↑s).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊