mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.Cone.Pointed

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
C : PointedCone R E
⊢ (↑C).Salient ↔ ↑C ∩ -↑C = {0}

Tactic:
by
  simp [ConvexCone.Salient, Set.eq_singleton_iff_unique_mem, not_imp_not]

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
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)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
⊢ x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}

Tactic:
have : CauchySeq L0 := by
    rw [Metric.cauchySeq_iff']
    intro ε εpos
    obtain ⟨e, he⟩ : ∃ e : ℕ, (1 / 2) ^ e < ε / (12 * ‖c‖) :=
      exists_pow_lt_of_lt_one (by positivity) (by norm_num)
    refine ⟨e, fun e' he' => ?_⟩
    rw [dist_comm, dist_eq_norm]
    calc
      ‖L0 e - L0 e'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e := M _ _ _ _ _ _ le_rfl le_rfl le_rfl le_rfl he'
      _ < 12 * ‖c‖ * (ε / (12 * ‖c‖)) := by gcongr
      _ = ε := by field

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)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
⊢ x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
h : x ≠ y
f : StrongDual R V
hf : f (x - y) ≠ 0
⊢ f x ≠ f y

Tactic:
by simpa [sub_ne_zero] using hf

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

Goal state before:
pp: case right
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε x r' : ℝ
rr' : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : ℝ
hx' : x' ∈ Ioo x (x + r' - s)
A : Icc x' (x' + s) ⊆ Icc x (x + r')
y : ℝ
hy : y ∈ Icc x' (x' + s)
z : ℝ
hz : z ∈ Icc x' (x' + s)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
exact hr' y (A hy) z (A hz)

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

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ (1 / 2) ^ p ≤ (1 / 2) ^ n

Tactic:
exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

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

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ (1 / 2) ^ q ≤ (1 / 2) ^ n

Tactic:
exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

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

Goal state before:
pp: case refine_2
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst✝ : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a n)) →
        (∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a (n + 1))

Tactic:
intro p

Goal state after:
case refine_2
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst✝ : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
⊢ m ≤ p →
    ((∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a p)) →
      (∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a (p + 1))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
R : Type u_8
inst✝³ : NormedRing R
inst✝² : Module R E
inst✝¹ : IsBoundedSMul R E
inst✝ : SMulCommClass ℝ R E
f : ℝ → E
r : R
hf : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
by
  simp only [intervalIntegral, smul_sub, hf.1.integral_smul, hf.2.integral_smul]

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
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c
⊢ ∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume =
    c⁻¹ •
      (ENNReal.ofReal |c|).toReal •
        (∫ (x : ℝ) in Ioc (a * c) (b * c), f x ∂Measure.map (fun x ↦ x * c) volume -
          ∫ (x : ℝ) in Ioc (b * c) (a * c), f x ∂Measure.map (fun x ↦ x * c) volume)

Tactic:
A.setIntegral_map,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c
⊢ ∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume =
    c⁻¹ •
      (ENNReal.ofReal |c|).toReal •
        (∫ (x : ℝ) in (fun x ↦ x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume -
          ∫ (x : ℝ) in (fun x ↦ x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case refine_2
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) →
          ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ) →
        (∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))) →
          ∑ k ∈ Finset.Ico m (n + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a (n + 1), f x ∂μ

Tactic:
intro p

Goal state after:
case refine_2
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
⊢ m ≤ p →
    ((∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
        ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ) →
      (∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))) →
        ∑ k ∈ Finset.Ico m (p + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a (p + 1), f x ∂μ
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: case inl
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

pp: case inr
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

Tactic:
· refine ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, ?_⟩
      rw [← Iic_sdiff_right]
      exact sdiff_mem_nhdsWithin_sdiff (Icc_mem_nhdsLE_of_mem ⟨hlt, hc.2⟩) _

Goal state after:
case inr
E : Type u_1
F : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (fun x ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ ∃ l, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ b₀ ∈ Icc (b₀ - δ) (b₀ + δ)

Tactic:
simp [δpos.le]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑(⌈x⌉ - 1) < x

Tactic:
by rw [cast_sub, cast_one, sub_lt_iff_lt_add]; exact ceil_lt_add_one _

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

Goal state before:
pp: case e'_3.e_μ
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
this : (fun x ↦ ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T))) =
    Measure.map QuotientAddGroup.mk (Measure.map Subtype.val volume)

Tactic:
← map_comap_subtype_coe m

Goal state after:
case e'_3.e_μ
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
this : (fun x ↦ ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ Measure.map QuotientAddGroup.mk (Measure.map Subtype.val (Measure.comap Subtype.val volume)) =
    Measure.map QuotientAddGroup.mk (Measure.map Subtype.val volume)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x ↦ ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val volume) =
    ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))

Tactic:
← map_comap_subtype_coe m

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
m : MeasurableSet (Ioc t (t + T))
this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x ↦ ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x
this : (fun x ↦ ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val
⊢ ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val volume) =
    ∫ (y : AddCircle T),
      f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val (Measure.comap Subtype.val volume))
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
⊢ Integrable (fun x ↦ ν.real (Prod.mk x ⁻¹' s)) μ

Tactic:
by
  refine ⟨(measurable_measure_prodMk_left hs).ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩
  simp_rw [hasFiniteIntegral_iff_enorm, measureReal_def, enorm_eq_ofReal toReal_nonneg]
  convert! h2s.lt_top using 1
  rw [prod_apply hs]
  apply lintegral_congr_ae
  filter_upwards [ae_measure_lt_top hs h2s] with x hx
  rw [lt_top_iff_ne_top] at hx
  simp [ofReal_toReal, hx]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ (2 * π)⁻¹ * ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C

Tactic:
← div_eq_inv_mul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ / (2 * π) ≤ R * C
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : Integrable (uncurry f) ((volume.restrict (uIoc a b)).prod μ)
⊢ ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ

Tactic:
rcases le_total a b with (hab | hab)

Goal state after:
case inl
α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : Integrable (uncurry f) ((volume.restrict (uIoc a b)).prod μ)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ

case inr
α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : Integrable (uncurry f) ((volume.restrict (uIoc a b)).prod μ)
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
h_int : Integrable (uncurry f) ((volume.restrict (uIoc a b)).prod μ)
⊢ ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ

Tactic:
rcases le_total a b with (hab | hab)
  · simp_rw [intervalIntegral.integral_of_le hab]
    simp only [hab, Set.uIoc_of_le] at h_int
    exact integral_integral_swap h_int
  · simp_rw [intervalIntegral.integral_of_ge hab]
    simp only [hab, Set.uIoc_of_ge] at h_int
    rw [integral_integral_swap h_int, integral_neg]

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.lower ∘ ⇑J) i x) atTop (𝓝 (I.lower x))
hJu : ∀ (x : Fin (n + 1)), Tendsto (fun i ↦ (Box.upper ∘ ⇑J) i x) atTop (𝓝 (I.upper x))
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i, (f' x) (e i) i =
      ∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
i : Fin (n + 1)
c : ℕ → ℝ
d : ℝ
hc : ∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)
hcd : Tendsto c atTop (𝓝 d)
hd : d ∈ Set.Icc (I.lower i) (I.upper i)
Hic : ∀ (k : ℕ), IntegrableOn (fun x ↦ f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) volume
Hid : IntegrableOn (fun x ↦ f (i.insertNth d x) i) (Box.Icc (I.face i)) volume
H :
  Tendsto (fun k ↦ ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop
    (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
ε : ℝ
εpos : 0 < ε
hvol_pos : ∀ (J : Box (Fin n)), 0 < ∏ j, (J.upper j - J.lower j)
δ : ℝ
δpos : δ > 0
hδ :
  ∀ x ∈ Box.Icc I, ∀ y ∈ Box.Icc I, dist x y ≤ δ → dist (f x) (f y) ≤ ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)
k : ℕ
hk : dist (c k) d < δ
Hsub : Box.Icc ((J k).face i) ⊆ Box.Icc (I.face i)
⊢ ‖∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth d x) i - f (i.insertNth (c k) x) i‖ ≤
    (ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)) * (volume (Box.Icc ((J k).face i))).toReal

Tactic:
by
      refine norm_setIntegral_le_of_norm_le_const (((J k).face i).measure_Icc_lt_top _)
        fun x hx => ?_
      rw [← dist_eq_norm]
      calc
        dist (f (i.insertNth d x) i) (f (i.insertNth (c k) x) i) ≤
            dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) :=
          dist_le_pi_dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) i
        _ ≤ ε / ∏ j, ((I.face i).upper j - (I.face i).lower j) :=
          hδ _ (I.mapsTo_insertNth_face_Icc hd <| Hsub hx) _
            (I.mapsTo_insertNth_face_Icc (hc _) <| Hsub hx) ?_
      rw [Fin.dist_insertNth_insertNth, dist_self, dist_comm]
      exact max_le hk.le δpos.lt.le

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
⊢ f x = g x

Tactic:
have : Fact ((q.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_left q p))⟩

Goal state after:
case neg.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
this : Fact (map (algebraMap F (p * q).SplittingField) q).Splits
⊢ f x = g x
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun x ↦ w + ↑x
this✝ : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
this : (Ioo l u).Countable
⊢ False

Tactic:
← Cardinal.le_aleph0_iff_set_countable,

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun x ↦ w + ↑x
this✝ : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
this : Cardinal.mk ↑(Ioo l u) ≤ Cardinal.aleph0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (-1) ^ k * x.prod

Tactic:
rw [(mem_powersetCard.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const]

Goal state after:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (map (Function.const R (-1)) x).prod * x.prod
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
x : R
| X + -C x

pp: case a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| s

Tactic:
rw [← map_neg C x]

Goal state after:
case a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
x : R
| X + C (-x)

case a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| s
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case a.a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
x : R
| X + -C x

pp: case a.a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| s

pp: case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k

Tactic:
rw [← map_neg C x]

Goal state after:
case a.a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
x : R
| X + C (-x)

case a.a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| s

case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k
Module: Mathlib.Topology.Algebra.Polynomial

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

Tactic:
norm_pow,

Goal state after:
case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ ‖-1‖ ^ ((map f p).natDegree - i) * ‖(map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)