mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ (Multiset.map X ↑↑⟨Sym.nil, ⋯⟩).prod = 1

Tactic:
]

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ (Multiset.map X ↑↑⟨Sym.nil, ⋯⟩).prod = 1
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
⊢ 0 = 0

Tactic:
]

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 w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this✝ : w ∈ closure (ball c ↑R \ s)
this :
  HasFPowerSeriesOnBall (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) (cauchyPowerSeries f c ↑R) c
    ↑R
⊢ w ∈ ball c ↑R

Tactic:
]

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this✝ : w ∈ closure (ball c ↑R \ s)
this :
  HasFPowerSeriesOnBall (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) (cauchyPowerSeries f c ↑R) c
    ↑R
⊢ w ∈ ball c ↑R
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:
]

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, (Multiset.map X ↑↑x).prod = msymm σ R (Nat.Partition.indiscrete 1)

σ : 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: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
⊢ ∫ (x : ℝ) in Set.Icc a b, f' x ∂volume = ∫ (x : ℝ) in Set.Icc a b, f' x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map ?m.110 (range (s.card + 1))).sum = (map (fun j ↦ C (s.esymm j) * X ^ (s.card - j)) (range (s.card + 1))).sum

pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ∀ x ∈ range (s.card + 1),
    (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) (powersetCard x s)).sum =
      ?m.110 x

pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ℕ → R[X]

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ∀ x ∈ range (s.card + 1),
    (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) (powersetCard x s)).sum =
      C (s.esymm x) * X ^ (s.card - x)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ (map ?m.148 (powersetCard x✝ s)).sum = (map (fun i ↦ C i.prod * X ^ (s.card - x✝)) (powersetCard x✝ s)).sum

pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ ∀ x ∈ powersetCard x✝ s,
    ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) x = ?m.148 x

pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ Multiset R → R[X]

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ ∀ x ∈ powersetCard x✝ s,
    ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t)) x = C x.prod * X ^ (s.card - x✝)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s✝ - t, t)) s = C s.prod * X ^ (s✝.card - x✝)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s✝ - t, t)) s = C s.prod * X ^ (s✝.card - x✝)
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 = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Tactic:
]

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 : σ
⊢ (Multiset.map X {x}).prod = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ (map (fun r ↦ X) (s✝ - s)).prod * C (map (fun i ↦ i) s).prod = C s.prod * X ^ (s✝.card - x✝)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ (map (fun r ↦ X) (s✝ - s)).prod * C (map (fun i ↦ i) s).prod = C s.prod * X ^ (s✝.card - x✝)
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 τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ ∑ x, (rename ⇑e) (Multiset.map X ↑↑x).prod = msymm τ R μ

Tactic:
]

Goal state after:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ ∑ x, (rename ⇑e) (Multiset.map X ↑↑x).prod = msymm τ R μ
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 τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (Multiset.map (⇑(rename ⇑e) ∘ X) ↑↑x✝).prod =
    (Multiset.map X
        ↑↑({ toFun := fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩, invFun := fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩,
                left_inv := ⋯, right_inv := ⋯ }
              x✝)).prod

Tactic:
]

Goal state after:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (Multiset.map (⇑(rename ⇑e) ∘ X) ↑↑x✝).prod =
    (Multiset.map X
        ↑↑({ toFun := fun x ↦ ⟨(Sym.equivCongr e) ↑x, ⋯⟩, invFun := fun x ↦ ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩,
                left_inv := ⋯, right_inv := ⋯ }
              x✝)).prod
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = if k = s.card - (s.card - k) then s.esymm (s.card - k) else 0

pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ∀ b ∈ Finset.range (s.card + 1), b ≠ s.card - k → (if k = s.card - b then s.esymm b else 0) = 0

pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.card - k ∈ Finset.range (s.card + 1)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = if k = s.card - (s.card - k) then s.esymm (s.card - k) else 0

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ∀ b ∈ Finset.range (s.card + 1), b ≠ s.card - k → (if k = s.card - b then s.esymm b else 0) = 0

R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.card - k ∈ Finset.range (s.card + 1)
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this : w ∈ closure (ball c ↑R \ s)
A : ContinuousAt (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) w
B : ContinuousAt f w
z : ℂ
hz : z ∈ ball c ↑R \ s
⊢ f z = f z

pp: case ha
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this : w ∈ closure (ball c ↑R \ s)
A : ContinuousAt (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) w
B : ContinuousAt f w
z : ℂ
hz : z ∈ ball c ↑R \ s
⊢ 2 * ↑π * I ≠ 0

Tactic:
]

Goal state after:
case ha
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this : w ∈ closure (ball c ↑R \ s)
A : ContinuousAt (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) w
B : ContinuousAt f w
z : ℂ
hz : z ∈ ball c ↑R \ s
⊢ 2 * ↑π * I ≠ 0
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case refine_1
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
a✝ : R
hc : f a✝ ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (C a✝ * X))) l atTop

Tactic:
]

Goal state after:
case refine_1
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
a✝ : R
hc : f a✝ ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (C a✝ * X))) l atTop
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ (map r s).esymm ((map r s).card - k) = (map r s).esymm (s.card - k)

pp: case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ (map r s).card

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ (map r s).esymm ((map r s).card - k) = (map r s).esymm (s.card - k)

case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ (map r s).card
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ (map r s).esymm (s.card - k) = (map r s).esymm (s.card - k)

Tactic:
]

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ s.card

Tactic:
]

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

Tactic:
]

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.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]
a✝ : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ * X))) l atTop

Tactic:
]

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✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ * X))) l atTop
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 : Cardinal.continuum ≤ Cardinal.aleph0
⊢ False

Tactic:
]

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.continuum ≤ Cardinal.aleph0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ (map ?m.56 (powersetCard k s)).sum = (map (fun i ↦ (-1) ^ k * i.prod) (powersetCard k s)).sum

pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ ∀ x ∈ powersetCard k s, (prod ∘ map Neg.neg) x = ?m.56 x

pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ Multiset R → R

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ ∀ x ∈ powersetCard k s, (prod ∘ map Neg.neg) x = (-1) ^ k * x.prod
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case refine_3
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 : R
hd : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ + C a))) l atTop

Tactic:
]

Goal state after:
case refine_3
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 : R
hd : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ + C a))) l atTop
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

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

Tactic:
]

Goal state after:
case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hi : IntegrableOn f' (Set.Ioc a b) volume
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, HasDerivAt f (f' x) x
⊢ IntegrableOn f' (Set.Icc a b) volume
Module: Mathlib.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 = (map (Function.const R (-1)) x).prod * x.prod

Tactic:
]

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: 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 * (map (fun x ↦ x) x).prod

Tactic:
]

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 * (map (fun x ↦ x) x).prod
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
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z

pp: case ha
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
⊢ 2 * ↑π * I ≠ 0

Tactic:
]

Goal state after:
case ha
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
⊢ 2 * ↑π * I ≠ 0
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]
hp0 : ¬0 < p.degree
⊢ ∀ (y : R), ‖eval ((C (p.coeff 0)).coeff 0) (C (p.coeff 0))‖ ≤ ‖eval y (C (p.coeff 0))‖

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < p.degree
⊢ ∀ (y : R), ‖eval ((C (p.coeff 0)).coeff 0) (C (p.coeff 0))‖ ≤ ‖eval y (C (p.coeff 0))‖
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]
h : 0 < p.degree
⊢ Tendsto (fun x ↦ ‖eval x p‖) (Bornology.cobounded R) atTop

Tactic:
]

Goal state after:
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ Tendsto (fun x ↦ ‖eval x p‖) (Bornology.cobounded R) atTop
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
⊢ (map Neg.neg x).prod = (map ?m.101 x).prod

pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = ?m.101 x_1

pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ R → R

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = -x_1
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inl
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : p.degree ≤ 0
⊢ IsClosedMap fun x ↦ eval x (C (p.coeff 0))

Tactic:
]

Goal state after:
case inl
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : p.degree ≤ 0
⊢ IsClosedMap fun x ↦ eval x (C (p.coeff 0))
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inl
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : p.degree ≤ 0
⊢ IsClosedMap fun x ↦ eval x (C (p.coeff 0))

Tactic:
simpa using! isClosedMap_const

Goal state after:
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
B : ℝ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
⊢ 0 ≤ B

Tactic:
]

Goal state after:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
⊢ 0 ≤ B
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x ↦ X + C (-x)) s).prod = (map ((fun r ↦ X + C r) ∘ fun t ↦ -t) s).prod

Tactic:
]

Goal state after:
case e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ (map (fun x ↦ X + C (-x)) s).prod = (map ((fun r ↦ X + C r) ∘ fun t ↦ -t) s).prod
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inl
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 : B < 0
⊢ ‖if i = 0 then 1 else 0‖ ≤ ↑(Nat.choose 0 i)

Tactic:
]

Goal state after:
case inl
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 : B < 0
⊢ ‖if i = 0 then 1 else 0‖ ≤ ↑(Nat.choose 0 i)