mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl.left.refine_1
α : 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 : ℤ
⊢ 𝓝 s ×ˢ 𝓝[<] 1 ≤ 𝓝[univ ×ˢ Icc 0 1] (s, 1)

Tactic:
rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsLT one_pos]

Goal state after:
case inl.left.refine_1
α : 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 : ℤ
⊢ 𝓝 s ×ˢ 𝓝[Ico 0 1] 1 ≤ 𝓝 s ×ˢ 𝓝[Icc 0 1] 1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
⊢ -(T / 2) + T = T / 2

Tactic:
by linarith

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 ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ε < T / 2
⊢ 2 * ε ≤ T

Tactic:
by linarith

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 ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ¬ε < T / 2
⊢ T ≤ 2 * ε

Tactic:
by linarith

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := c • haarMeasure K
hμK : μ ↑K = c
⊢ QuotientMeasureEqMeasurePreimage ν μ

Tactic:
have : SigmaFinite μ := by
    clear_value c
    lift c to NNReal using c_ne_top
    exact SMul.sigmaFinite c

Goal state after:
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : IsTopologicalGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : PolishSpace G
Γ : Subgroup G
inst✝⁶ : Γ.Normal
inst✝⁵ : T2Space (G ⧸ Γ)
inst✝⁴ : SecondCountableTopology (G ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := c • haarMeasure K
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ QuotientMeasureEqMeasurePreimage ν μ
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
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ M + δ ≤ M + 1

Tactic:
by linarith

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

Goal state before:
pp: case h₂f
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
⊢ ∀ x ∈ univ, ¬EventuallyConst (circleMap c R) (𝓝 x)

Tactic:
intro x hx
    by_contra hCon
    obtain ⟨a, ha⟩ := eventuallyConst_iff_exists_eventuallyEq.1 hCon
    have := ha.deriv.eq_of_nhds
    simp [hR] at this

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

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
inst✝² : NormedSpace ℝ E✝
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
⊢ ∫ (x : ℝ) in Ioc t (t + T), f x ∂volume = ∫ (x : ℝ) in Ioc s (s + T), f x ∂volume

Tactic:
have : VAddInvariantMeasure (AddSubgroup.zmultiples T) ℝ volume :=
    ⟨fun c s _ => measure_preimage_add _ _ _⟩

Goal state after:
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
inst✝² : NormedSpace ℝ E✝
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
hT : 0 < T
this : VAddInvariantMeasure ↥(zmultiples T) ℝ volume
⊢ ∫ (x : ℝ) in Ioc t (t + T), f x ∂volume = ∫ (x : ℝ) in Ioc s (s + T), f x ∂volume
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: 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

Tactic:
· filter_upwards [self_mem_nhdsWithin] with a ha using by grind

Goal state after:
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:
rw [← Int.fract_div_mul_self_add_zsmul_eq T t hT.ne',
      ← integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]

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..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

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

Tactic:
· filter_upwards [self_mem_nhdsWithin] with a ha using by grind

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

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

Tactic:
exact (hf.mono_set Ioi_subset_Ici_self).continuousOn_Ici_primitive_Ioi

Goal state after:
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
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‖
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ENNReal.ofReal C * ‖f x‖ₑ * ‖g y‖ₑ ∂ν ∂μ ≤
    (ENNReal.ofReal C * ∫⁻ (x : α), ‖f x‖ₑ ∂μ) * ∫⁻ (y : β), ‖g y‖ₑ ∂ν

Tactic:
by
      simp [lintegral_const_mul', lintegral_mul_const', hg.2.ne, mul_assoc]

Goal state after:
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
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)
hop_norm : ∃ C, ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
⊢ Integrable (fun z ↦ op (f z.1) (g z.2)) (μ.prod ν)

Tactic:
use hop.comp_aestronglyMeasurable₂ hf.1.comp_fst hg.1.comp_snd
  rcases hop_norm with ⟨C, hC⟩
  calc
    ∫⁻ z, ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ z, .ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν := by
      gcongr with z
      simp only [enorm_eq_nnnorm, ENNReal.ofReal, ← ENNReal.coe_mul, ENNReal.coe_le_coe,
        ← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm]
      refine (hC _ _).trans ?_
      gcongr
      apply le_coe_toNNReal
    _ ≤ ∫⁻ x, ∫⁻ y, .ofReal C * ‖f x‖ₑ * ‖g y‖ₑ ∂ν ∂μ := lintegral_prod_le _
    _ ≤ .ofReal C * (∫⁻ x, ‖f x‖ₑ ∂μ) * ∫⁻ y, ‖g y‖ₑ ∂ν := by
      simp [lintegral_const_mul', lintegral_mul_const', hg.2.ne, mul_assoc]
    _ < ∞ := by apply_rules [ENNReal.mul_lt_top, hf.2, hg.2, ENNReal.ofReal_lt_top]

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 : ℝ≥0
n : ℕ
⊢ ‖cauchyPowerSeries f c (↑R) n‖ * ↑R ^ n ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖

Tactic:
refine (mul_le_mul_of_nonneg_right (norm_cauchyPowerSeries_le _ _ _ _)
    (pow_nonneg R.coe_nonneg _)).trans ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖) * |↑R|⁻¹ ^ n * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖
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)
this :
  ∀ (i : Fin (n + 1)) (c : ℕ → ℝ) (d : ℝ),
    (∀ (k : ℕ), c k ∈ Set.Icc (I.lower i) (I.upper i)) →
      Tendsto c atTop (𝓝 d) →
        Tendsto (fun k ↦ ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) atTop
          (𝓝 (∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth d x) i))
⊢ Tendsto
    (fun x ↦
      ∑ i,
        ((∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth ((J x).upper i) x_1) i) -
          ∫ (x_1 : Fin n → ℝ) in Box.Icc ((J x).face i), f (i.insertNth ((J x).lower i) x_1) i))
    atTop
    (𝓝
      (∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)))

Tactic:
by
    rw [Box.Icc_eq_pi] at hJ_sub'
    refine tendsto_finsetSum _ fun i _ => (this _ _ _ ?_ (hJu _)).sub (this _ _ _ ?_ (hJl _))
    exacts [fun k => hJ_sub' k (J k).upper_mem_Icc _ trivial, fun k =>
      hJ_sub' k (J k).lower_mem_Icc _ trivial]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ Nat.card p.Gal

Tactic:
Gal.card_of_separable p_irr.separable

Goal state after:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ finrank F p.SplittingField
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ msymm σ R (Nat.Partition.indiscrete 1) = ∑ i, X i

Tactic:
by
  have : (fun (x : Sym σ 1) ↦ x ∈ Set.univ) =
      (fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1) := by
    simp_rw [Set.mem_univ, Nat.Partition.ofSym_one]
  symm
  rw [Fintype.sum_equiv (Equiv.trans Sym.oneEquiv (Equiv.Set.univ (Sym σ 1)).symm)
    _ (fun s ↦ (s.1.1.map X).prod)]
  · apply Fintype.sum_equiv (Equiv.subtypeEquivProp this)
    intro x
    congr
  · intro x
    rw [← Multiset.prod_singleton (X x), ← Multiset.map_singleton]
    congr

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x ↦ p.sum fun e a ↦ f a * x ^ e

Tactic:
exact continuous_finsetSum _ fun c _ => continuous_const.mul (continuous_pow _)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ (map r s.val).esymm (s.val.card - k) = ∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i

Tactic:
Finset.esymm_map_val

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ ∑ t ∈ Finset.powersetCard (s.val.card - k) s, t.prod r = ∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i
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:
← 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:
← 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.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

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

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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this : (n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1) = (iteratedFDeriv ℂ n f c) fun x ↦ 1
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑π * I / ↑n.factorial) • iteratedDeriv n f c

Tactic:
iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod,

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this : (n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1) = (∏ i, 1) • iteratedDeriv n f c
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * ↑π * I / ↑n.factorial) • iteratedDeriv n f c
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ ↑‖s.prod‖₊ ≤ ↑B ^ ((map f p).natDegree - i)

Tactic:
← NNReal.coe_pow,

Goal state after:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ ↑‖s.prod‖₊ ≤ ↑(B ^ ((map f p).natDegree - i))
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case mp
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 : ℂ
⊢ (∃ a, (aeval a) p = 0 ∧ (IsScalarTower.toAlgHom ℚ ℝ ℂ) a = z) → (aeval z) p = 0 ∧ z.im = 0

Tactic:
rintro ⟨w, hw, rfl⟩

Goal state after:
case mp
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
w : ℝ
hw : (aeval w) p = 0
⊢ (aeval ((IsScalarTower.toAlgHom ℚ ℝ ℂ) w)) p = 0 ∧ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) w).im = 0
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: 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 Γ₀
v : F →*₀ Γ₀
a : ↥(MonoidHom.mrange v)
⊢ ⟨⊥, ⋯⟩ ≤ a

Tactic:
simp [bot_eq_zero, ← Subtype.coe_le_coe]

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

Goal state before:
pp: case inr
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✝ : MulArchimedean ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered ↑(Set.range ⇑v)
h✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
this✝¹ : IsDomain O
this✝ : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ ¬DenselyOrdered ↥(MonoidHom.mrange v)

Tactic:
exact H

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

Goal state before:
pp: case mp
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
z : ℂ
⊢ (∃ a ∈ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support, ↑a = z) →
    (aeval z) p = 0 ∧ z.im ≠ 0

Tactic:
rintro ⟨w, hw, rfl⟩

Goal state after:
case mp
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
hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0
hc0 :
  ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0
w : { x // x ∈ p.rootSet ℂ }
hw : w ∈ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support
⊢ (aeval ↑w) p = 0 ∧ (↑w).im ≠ 0
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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
hneg : x < 0
n : ℕ
hn : -x - x ≤ n • 1
⊢ -x < -x - x

Tactic:
by simpa using hneg

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

Goal state before:
pp: case neg.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
⊢ IsNontrivial R

Tactic:
rcases eq_or_ne a 1 with rfl | ha'

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

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
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff φ = 0 ∨ constantCoeff ψ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹

Tactic:
rcases h with h | h

Goal state after:
case pos.inl
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff φ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹

case pos.inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff ψ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ Multiset.count X (normalizedFactors ↑P) = Multiset.count Polynomial.X (normalizedFactors P)

Tactic:
by
  apply eq_of_forall_le_iff
  simp only [← Nat.cast_le (α := ℕ∞)]
  rw [X_eq_normalize, PowerSeries.X_eq_normalizeX, ← emultiplicity_eq_count_normalizedFactors
    irreducible_X hP, ← emultiplicity_eq_count_normalizedFactors X_irreducible] <;>
  simp only [← pow_dvd_iff_le_emultiplicity, Polynomial.X_pow_dvd_iff,
    PowerSeries.X_pow_dvd_iff, Polynomial.coeff_coe P, implies_true, ne_eq, coe_eq_zero_iff, hP,
    not_false_eq_true]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦P⟧ = ⟦v • Q⟧ ↔ ⟦P⟧ = ⟦Q⟧

Tactic:
smul_eq Q hv

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦P⟧ = ⟦Q⟧ ↔ ⟦P⟧ = ⟦Q⟧