mathlib-initiative/mathlib-tactics huggingface dataset:
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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →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)
⊢ ‖L e p q - L e p r‖ ≤ 4 * ‖c‖ * (1 / 2) ^ e

Tactic:
have I2 : x ∈ A f (L e p r) ((1 / 2) ^ p) ((1 / 2) ^ e) := (hn e p r hp (le_max_left _ _)).2.1

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
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →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 * ‖c‖ * (1 / 2) ^ e
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / (↑i + 1) ≤ |x| ^ (i + 1) / (0 + 1)

Tactic:
gcongr
      positivity

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
⊢ gauge (a • s) = gauge (|a| • s)

Tactic:
· rw [h, Set.neg_smul_set, ← Set.smul_set_neg]
    congr
    ext y
    refine ⟨symmetric _, fun hy => ?_⟩
    rw [← neg_neg y]
    exact symmetric _ hy

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
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ Tendsto (fun x_1 ↦ x_1 • x) (𝓝[<] 1) (𝓝 x)

Tactic:
exact Filter.Tendsto.mono_left (Continuous.tendsto' (by fun_prop) _ _ (one_smul _ _))
    inf_le_left

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ r * gauge s x ≤ ‖x‖

Tactic:
rw [mul_comm, ← le_div_iff₀ hr, ← gauge_ball hr.le]

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ gauge s x ≤ gauge (ball 0 r) x
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'
⊢ e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e

Tactic:
he'

Goal state after:
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'
⊢ ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
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)
⊢ ‖L e p q - L e p r‖ ≤ 4 * (1 / 2) ^ e

Tactic:
have I2 : x ∈ A f (L e p r) ((1 / 2) ^ p) ((1 / 2) ^ e) := (hn e p r hp (le_max_left _ _)).2.1

Goal state after:
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
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → ℝ → E
inst✝ : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
rcases l.eq_or_neBot with rfl | hl

Goal state after:
case inl
ι : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
F : ι → ℝ → E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : ⊥.IsCountablyGenerated
hF : ∀ᶠ (i : ι) in ⊥, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f ⊥ [[a, b]]
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) ⊥ (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

case inr
ι : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → ℝ → E
inst✝ : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ Integrable (fun x ↦ f (c * x))
    ((ENNReal.ofReal |c⁻¹| • Measure.map (fun x ↦ x * c⁻¹) volume).restrict [[a / c, b / c]])

Tactic:
Measure.restrict_smul,

Goal state after:
case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ Integrable (fun x ↦ f (c * x))
    (ENNReal.ofReal |c⁻¹| • (Measure.map (fun x ↦ x * c⁻¹) volume).restrict [[a / c, b / c]])
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ Integrable (fun x ↦ f (c * x)) ((Measure.map (fun x ↦ x * c⁻¹) volume).restrict [[a / c, b / c]])

Tactic:
← IntegrableOn,

Goal state after:
case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ IntegrableOn (fun x ↦ f (c * x)) [[a / c, b / c]] (Measure.map (fun x ↦ x * c⁻¹) volume)
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 ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
⊢ ∫ (x : ℝ) in Iic b, f x ∂μ - ∫ (x : ℝ) in Iic a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
wlog hab : a ≤ b generalizing a b
  · rw [integral_symm, ← this hb ha (le_of_not_ge hab), neg_sub]
  rw [sub_eq_iff_eq_add', integral_of_le hab, ← setIntegral_union (Iic_disjoint_Ioc le_rfl),
    Iic_union_Ioc_eq_Iic hab]
  exacts [measurableSet_Ioc, ha, hb.mono_set fun _ => And.right]

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

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
    (b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb))

Tactic:
refine ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩

Goal state after:
case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)

case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ ∫ (x : ℝ) in a₁..a₃, {x | x ≤ a₂}.indicator f x ∂μ = ∫ (x : ℝ) in a₁..a₂, f x ∂μ

Tactic:
rw [integral_of_le h.1, integral_of_le (h.1.trans h.2), integral_indicator,
    Measure.restrict_restrict, this]

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}

E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a₁ a₂ a₃ : ℝ
h : a₂ ∈ Icc a₁ a₃
this : {x | x ≤ a₂} ∩ Ioc a₁ a₃ = Ioc a₁ a₂
⊢ MeasurableSet {x | x ≤ a₂}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case e'_2
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn (fun t ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : ℝ → 𝕜 := fun t ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ t ∈ [[0, 1]], HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
⊢ z₁ • ∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y

Tactic:
simp_rw [← integral_smul, Function.comp_apply, γ]

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

Goal state before:
pp: case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᵐ[μ.restrict (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Tactic:
suffices (∫ x in a..b, f x ∂μ) ≤ 0 by simp only [this.not_gt, hba.not_gt, false_and]

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᵐ[μ.restrict (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ ≤ 0
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
⊢ c +ᵥ R • sphere 0 1 = sphere c |R|

Tactic:
smul_sphere R 0 zero_le_one

Goal state after:
c : ℂ
R : ℝ
⊢ c +ᵥ sphere (R • 0) (‖R‖ * 1) = sphere c |R|
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a₀

Tactic:
simp_rw [← integral_indicator measurableSet_Iio]
  apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f))
  · filter_upwards [self_mem_nhdsWithin] with a ha
    rw [aestronglyMeasurable_indicator_iff measurableSet_Iio]
    exact (hf.mono_set (Iio_subset_Iio ha)).aestronglyMeasurable
  · filter_upwards [self_mem_nhdsWithin] with a ha
    refine ae_of_all _ fun x ↦ ?_
    rw [norm_indicator_eq_indicator_norm]
    apply indicator_le_indicator_of_subset (Iio_subset_Iio (by grind)) (fun a ↦ norm_nonneg (f a))
  · simpa [integrable_indicator_iff measurableSet_Iio] using! hf.norm
  · refine ae_of_all _ fun x ↦ ?_
    simp only [indicator_apply, mem_Iio]
    by_cases hx : x < a₀ <;> apply tendsto_const_nhds.congr'
    · filter_upwards [mem_nhdsWithin_of_mem_nhds (Ioi_mem_nhds hx)] with a ha using by grind
    · filter_upwards [self_mem_nhdsWithin] with a ha using by grind

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

Goal state before:
pp: n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ ¬↑n + 1 = 0

Tactic:
← eq_neg_iff_add_eq_zero,

Goal state after:
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ ¬↑n = -1
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : 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 μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z ↦ ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i ↦ i) (𝓝 g) (𝓝 g)

Tactic:
exact tendsto_id

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hzne : z ≠ c
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))

Tactic:
rw [mem_sphere, dist_eq_norm] at hz

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hzne : z ≠ c
hz : ‖z - c‖ = r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ (rename ⇑e) (esymm σ R n) = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i)

Tactic:
by
      simp_rw [esymm, map_sum, map_prod, rename_X]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x ↦ x ∈ Set.univ) = fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∑ x, (Multiset.map X ↑↑x).prod = msymm σ R (Nat.Partition.indiscrete 1)

pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x ↦ x ∈ Set.univ) = fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∀ (x : σ), X x = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Tactic:
· apply Fintype.sum_equiv (Equiv.subtypeEquivProp this)
    intro x
    congr

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x ↦ x ∈ Set.univ) = fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∀ (x : σ), X x = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at *

Goal state after:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
Hc : ContinuousOn f (Set.Icc b a)
Hd : ∀ x ∈ Set.Ioo b a \ s, HasDerivAt f (f' x) x
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ Function.Bijective ⇑(galActionHom p ℂ)

Tactic:
have h1 : Fintype.card (p.rootSet ℂ) = p.natDegree := by
    simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
    rw [Multiset.toFinset_card_of_nodup, ← Splits.natDegree_eq_card_roots, natDegree_map]
    · exact IsAlgClosed.splits _
    · exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)
  let conj' := restrict p ℂ (Complex.conjAe.restrictScalars ℚ)
  refine
    ⟨galActionHom_injective p ℂ, fun x =>
      (congr_arg (x ∈ ·) (show (galActionHom p ℂ).range = ⊤ from ?_)).mpr
        (Subgroup.mem_top x)⟩
  apply Equiv.Perm.subgroup_eq_top_of_swap_mem
  · rwa [h1]
  · rw [h1]
    simpa only [Fintype.card_eq_nat_card,
      Nat.card_congr (MonoidHom.ofInjective (galActionHom_injective p ℂ)).toEquiv.symm]
      using prime_degree_dvd_card p_irr p_deg
  · exact ⟨conj', rfl⟩
  · rw [← Equiv.Perm.card_support_eq_two]
    apply Nat.add_left_cancel
    rw [← p_roots, ← Set.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]
    exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mpr
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a u : ℚ
hu : u ∈ ratLt x
v : ℚ
hv : v ∈ ratLt y
huv : u + v = a
⊢ u + v ∈ ratLt (x + y)

Tactic:
rw [Set.mem_ofPred_eq] at hu hv ⊢

Goal state after:
case mpr
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a u : ℚ
hu : u.num • 1 < u.den • x
v : ℚ
hv : v.num • 1 < v.den • y
huv : u + v = a
⊢ (u + v).num • 1 < (u + v).den • (x + y)
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
⊢ ∀ (y : ℚ), y.num • 1 < 0 → ↑y = x → x ≤ 0

Tactic:
intro y hy hyx

Goal state after:
case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
y : ℚ
hy : y.num • 1 < 0
hyx : ↑y = x
⊢ x ≤ 0
Module: Mathlib.RingTheory.Valuation.Discrete.RankOne

Goal state before:
pp: case neg
R : Type u_2
inst✝ : Ring R
v : Valuation R (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective ⇑v
x : R
h0 : ¬v x = 0
⊢ (map' ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm) ↑⟨Units.mk0 ((ofClass v) x) h0, ⋯⟩ = v x

Tactic:
rw [WithZero.map'_coe, ← coe_unzero h0, WithZero.coe_inj,
    ← (MulEquiv.injective (intEquivOfZPowersEqTop _
    (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top))).eq_iff]
    ext
    simp [generator', generator_eq_exp_neg_one_of_surjective hsurj, toAdd_unzero_eq_log h0,
      exp_log h0]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≤ 0
⊢ IsClosed (ball x r)

Tactic:
simp [ball_eq_empty.mpr hr]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : ∀ {γ : ℝ≥0}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (RankLeOne.hom' valuation) (valuation.restrict x) < γ
x : K
hx : x ≠ 0
hxy : (RankLeOne.hom' valuation) (valuation.restrict x) < ⟨ε, ⋯⟩
⊢ valuation.restrict x ≠ 0

Tactic:
by simp [Valuation.restrict_def, hx]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
⊢ s = 0

Tactic:
have := H (C s) (by rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs])

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
s : R
hrs : r * s = 0
this : C s = 0
⊢ s = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
⊢ s = 0

Tactic:
have := H (C s) (by rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs])

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
H : (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
s : R
hrs : s * r = 0
this : C s = 0
⊢ s = 0