mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CompactSpace Y
R : Type u_8
inst✝³ : NormedCommRing R
inst✝² : Zero Y
inst✝¹ : NormedAlgebra ℝ R
inst✝ : CompleteSpace R
f : X → C(Y, R)₀
hf : Integrable f μ
y : Y
⊢ (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ

Tactic:
calc (∫ x, f x ∂μ) y = ContinuousMapZero.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
    _ = ∫ x, ContinuousMapZero.evalCLM ℝ y (f x) ∂μ :=
          (ContinuousLinearMap.integral_comp_comm _ hf).symm
    _ = _ := rfl

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

Goal state before:
pp: ε : 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⁻¹
⊢ ENNReal.ofReal |c⁻¹| ≠ 0

Tactic:
by simpa

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
this : IntervalIntegrable (fun x ↦ ‖f x‖) μ b₁ b₂
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
refine continuousWithinAt_of_dominated_interval ?_ ?_ this ?_

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
this : IntervalIntegrable (fun x ↦ ‖f x‖) μ b₁ b₂
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, AEStronglyMeasurable ({x_1 | x_1 ≤ x}.indicator f) (μ.restrict (Ι b₁ b₂))

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
this : IntervalIntegrable (fun x ↦ ‖f x‖) μ b₁ b₂
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖{x_1 | x_1 ≤ x}.indicator f t‖ ≤ ‖f t‖

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this✝ :
  (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ
this : IntervalIntegrable (fun x ↦ ‖f x‖) μ b₁ b₂
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ContinuousWithinAt (fun x ↦ {x_1 | x_1 ≤ x}.indicator f t) (Icc b₁ b₂) b₀
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
⊢ StronglyMeasurable fun x ↦ derivWithin f (Ioi x) x

Tactic:
by
  simpa [derivWithin_Ioi_eq_Ici] using stronglyMeasurable_derivWithin_Ici f

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

Goal state before:

Tactic:
‖F x s - F x₀ s‖ ≤ ‖F x s‖ + ‖F x₀ s‖ := norm_sub_le _ _
          _ ≤ 2 * bound s := by linarith only [hs₁, hs₂]

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 t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
⊢ IsOpen[instTopologicalSpaceProd] {p | p.2 ∈ B (f p.1) K r s t}

Tactic:
suffices H : IsOpen (⋃ L ∈ K,
      {p : α × E | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}) by
    convert! H; ext p; simp [B]

Goal state after:
𝕜 : 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 t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
⊢ IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
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
⊢ [[a, b]] \ {c} ∈ 𝓝[<] c

Tactic:
← Iic_sdiff_right

Goal state after:
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
⊢ [[a, b]] \ {c} ∈ 𝓝[Iic c \ {c}] c
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl.right
α : 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)))

Tactic:
· refine (((h (s, 0) ⟨trivial, le_rfl, zero_le_one⟩).tendsto.mono_left <| le_of_eq ?_).comp
        (tendsto_id.prodMap (tendsto_fract_right _))).mono_right (le_of_eq ?_) <;>
        simp [nhdsWithin_prod_eq, nhdsWithin_univ]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := ⋯
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ I ⊆ Metric.closedBall 0 (|T| / 2)

Tactic:
simpa only [hT', Real.closedBall_eq_Icc, zero_add, zero_sub] using Ioc_subset_Icc_self

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

Goal state before:
pp: E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
⊢ max a₁ a₂ ≤ t + ↑n₂ * T

Tactic:
linarith [(div_le_iff₀ hT).1 hn₂]

Goal state after:
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)
⊢ ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
        (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j, (I.upper j - I.lower j)

Tactic:
have Hi : ∀ x ∈ Icc (I.lower i) (I.upper i),
      Integrable.{0, u, u} (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume := fun x hx =>
    integrable_of_continuousOn _ (Box.continuousOn_face_Icc hfc hx) volume

Goal state after:
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
⊢ ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
        (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j, (I.upper j - I.lower j)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
| ∫ (x : ℝ) in 0..t, g x

Tactic:
← Int.fract_div_mul_self_add_zsmul_eq T t hT.ne',

Goal state after:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
| ∫ (x : ℝ) in 0..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case hfg
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
F : Type u_4
G : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
z : α × β
⊢ ‖op (f z.1) (g z.2)‖ₑ ≤ ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ

Tactic:
simp only [enorm_eq_nnnorm, ENNReal.ofReal, ← ENNReal.coe_mul, ENNReal.coe_le_coe,
        ← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm]

Goal state after:
case hfg
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
F : Type u_4
G : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
z : α × β
⊢ ‖op (f z.1) (g z.2)‖ ≤ ↑C.toNNReal * ‖f z.1‖ * ‖g z.2‖
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inl.inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
i : Fin (n + 1)
hi : a i = b i
hi' : Set.Ioc (a i) (b i) = ∅
this : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
hne : i ≠ j
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0

Tactic:
rcases Fin.exists_succAbove_eq hne with ⟨i, rfl⟩

Goal state after:
case inl.inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
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 (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
this : (Set.univ.pi fun j ↦ Set.Ioc (a j) (b j)) = ∅
j : Fin (n + 1)
i : Fin n
hi : a (j.succAbove i) = b (j.succAbove i)
hi' : Set.Ioc (a (j.succAbove i)) (b (j.succAbove i)) = ∅
hne : j.succAbove i ≠ j
⊢ (∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (b j) x) j) -
      ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ j.succAbove) (b ∘ j.succAbove), f (j.insertNth (a j) x) j =
    0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ s ^ n • (map prod (powersetCard n m)).sum = (map (fun x ↦ s • x) m).esymm n

Tactic:
smul_sum,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ (map (fun x ↦ s ^ n • x) (map prod (powersetCard n m))).sum = (map (fun x ↦ s • x) m).esymm n
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits
h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits
⊢ (map (algebraMap F (q₁ * q₂).SplittingField) (p₁ * p₂)).Splits

Tactic:
rw [Polynomial.map_mul]
  apply Splits.mul
  · rw [←
      (SplittingField.lift q₁
          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
             ((map_dvd_map' _).mpr (dvd_mul_right q₁ q₂)))).comp_algebraMap, ← map_map]
    exact h₁.map _
  · rw [←
      (SplittingField.lift q₂
          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
             ((map_dvd_map' _).mpr (dvd_mul_left q₂ q₁)))).comp_algebraMap, ← map_map]
    exact h₂.map _

Goal state after:
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p * X))) l atTop

Tactic:
intro _ _ ihp hf

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f (p✝ * X).leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ * X))) l atTop
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
⊢ IsClosedMap fun x ↦ eval x p

Tactic:
by
  obtain h | h := le_or_gt p.degree 0
  · rw [degree_le_zero_iff.mp h]; simpa using! isClosedMap_const
  · exact (p.isProperMap_eval h).isClosedMap

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ (C p.leadingCoeff * (map (fun a ↦ X - C a) p.roots).prod).coeff k =
    p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
coeff_C_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ p.leadingCoeff * (map (fun a ↦ X - C a) p.roots).prod.coeff k =
    p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
⊢ ∏ i, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

Tactic:
have : Fintype.card σ = Multiset.card s := by
    rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
this : Fintype.card σ = s.card
⊢ ∏ i, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: case mp
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ AnalyticAt ℂ f c → ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z

pp: case mpr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ (∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z) → AnalyticAt ℂ f c

Tactic:
· intro fa
    filter_upwards [fa.eventually_analyticAt]
    apply AnalyticAt.differentiableAt

Goal state after:
case mpr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ (∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z) → AnalyticAt ℂ f c
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
⊢ (∏ i, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)

Tactic:
have : Fintype.card σ = Multiset.card s := by
    rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
this : Fintype.card σ = s.card
⊢ (∏ i, (Polynomial.X + Polynomial.C (X i))).coeff k = esymm σ R (Fintype.card σ - k)
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
z : ℂ
⊢ Filter.Tendsto (fun x ↦ eval x f) (cobounded ℂ) (cobounded ℂ)

Tactic:
by
        simpa only [tendsto_norm_atTop_iff_cobounded]
          using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop

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

Goal state before:
pp: f : ℂ[X]
hf : 0 < f.degree
⊢ ∃ z, f.IsRoot z

Tactic:
by
  by_contra! hf'
  /- Since `f` has no roots, `f⁻¹` is differentiable. And since `f` is a polynomial, it tends to
  infinity at infinity, thus `f⁻¹` tends to zero at infinity. By Liouville's theorem, `f⁻¹ = 0`. -/
  have (z : ℂ) : (f.eval z)⁻¹ = 0 :=
    (f.differentiable.inv hf').apply_eq_of_tendsto_cocompact z <|
      Metric.cobounded_eq_cocompact (α := ℂ) ▸ (Filter.tendsto_inv₀_cobounded.comp <| by
        simpa only [tendsto_norm_atTop_iff_cobounded]
          using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop)
  -- Thus `f = 0`, contradicting the fact that `0 < degree f`.
  obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]
  simp at hf

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

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden : den ≠ 0
x : M
⊢ mkRat num den ∈ ratLt x ↔ num • 1 < den • x

Tactic:
by
  rw [Set.mem_ofPred]
  obtain ⟨m, hm0, hnum, hden⟩ := Rat.mkRat_num_den hden (show mkRat num den = _ by rfl)
  conv in num • 1 => rw [hnum, mul_comm, ← smul_smul, natCast_zsmul]
  conv in den • x => rw [hden, mul_comm, ← smul_smul]
  exact (smul_lt_smul_iff_of_pos_left (Nat.zero_lt_of_ne_zero hm0)).symm

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : R
hx0 : v x ≠ 0
hx1 : v x ≠ 1
⊢ v.restrict x ≠ 1

Tactic:
by simpa

Goal state after:
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
⊢ embedRealFun 0 ≤ 0

Tactic:
apply csSup_le (ratLt'_nonempty 0)

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
⊢ ∀ b ∈ ratLt' 0, b ≤ 0
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ (X - C ((starRingEnd ℂ) z)) * (X - C z) ∣ map (algebraMap ℝ ℂ) p

Tactic:
by
  apply IsCoprime.mul_dvd
  · exact isCoprime_X_sub_C_of_isUnit_sub <| .mk0 _ <| sub_ne_zero.2 <| mt conj_eq_iff_im.1 hz
  · simpa [dvd_iff_isRoot, aeval_conj]
  · simpa [dvd_iff_isRoot]

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case neg.inr.inr
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
a b : ValueGroupWithZero R
H : a < b
H' : 1 b ≤ 1 a
ha : a ≠ 0
ha' : a ≠ 1
⊢ IsNontrivial R

Tactic:
· exact ⟨⟨a, ha, ha'⟩⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
h₁ : closedBall x r = closedBall h.some r
⊢ closedBall x r = closedBall y r

Tactic:
have h₂ := closedBall_eq_of_mem <| Set.inter_subset_right h.some_mem

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (closedBall x r ∩ closedBall y r).Nonempty
h₁ : closedBall x r = closedBall h.some r
h₂ : closedBall y r = closedBall h.some r
⊢ closedBall x r = closedBall y r
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) < φ.lexOrder
hφ : φ = 0
⊢ (coeff d) φ = 0

Tactic:
simp only [hφ, map_zero]

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

Goal state before:
pp: σ : 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
⊢ (monomial n) r * C s = 0

Tactic:
rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs]

Goal state after: