mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case a
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 := ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ (minpoly F α).natDegree ≤ p.natDegree

pp: case a
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 := ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ p.natDegree ≤ (minpoly F α).natDegree

Tactic:
·

Goal state after:
case a
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 := ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ (minpoly F α).natDegree ≤ p.natDegree
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case a
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 := ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ p.natDegree ≤ (minpoly F α).natDegree

Tactic:
·

Goal state after:
case a
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 := ⋯
hα : IsIntegral F α
this : minpoly F α ∣ p
key : p ∣ minpoly F α
⊢ p.natDegree ≤ (minpoly F α).natDegree
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)
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 : σ), 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 : σ), X x = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_1
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 : IntervalIntegrable f' volume a b
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
⊢ ∀ (x y : ℝ), e x ≤ e y ↔ x ≤ y

pp: case refine_2
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 : IntervalIntegrable f' volume a b
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
⊢ MeasurePreserving (⇑e) volume volume

pp: case refine_3
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 : IntervalIntegrable f' volume a b
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
⊢ ∀ (x : ℝ), f' x = ∑ i, (F' x) (e.symm (Pi.single i 1))

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 : IntervalIntegrable f' volume a b
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_1
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 : IntervalIntegrable f' volume a b
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
⊢ ∀ (x y : ℝ), e x ≤ e y ↔ x ≤ y
Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyCoherentSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)

Tactic:
simp_rw [isProperMap_iff_isCompact_preimage,
    hasBasis_cocompact.tendsto_right_iff, ← mem_preimage, eventually_mem_set, preimage_compl]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyCoherentSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔
    Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
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}, a ≠ 0 → f (C a * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (C a * X))) l atTop

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

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},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p + C a))) 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}, a ≠ 0 → f (C a * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (C a * X))) l atTop
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

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},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p + C a))) 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]},
    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
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_2
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 : IntervalIntegrable f' volume a b
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
⊢ MeasurePreserving (⇑e) volume volume

pp: case refine_3
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 : IntervalIntegrable f' volume a b
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
⊢ ∀ (x : ℝ), f' x = ∑ i, (F' x) (e.symm (Pi.single i 1))

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 : IntervalIntegrable f' volume a b
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_2
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 : IntervalIntegrable f' volume a b
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
⊢ MeasurePreserving (⇑e) volume volume
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_3
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 : IntervalIntegrable f' volume a b
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
⊢ ∀ (x : ℝ), f' x = ∑ i, (F' x) (e.symm (Pi.single i 1))

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 : IntervalIntegrable f' volume a b
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_3
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 : IntervalIntegrable f' volume a b
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
⊢ ∀ (x : ℝ), f' x = ∑ i, (F' x) (e.symm (Pi.single i 1))
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},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).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},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).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 : IntervalIntegrable f' volume a b
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 : IntervalIntegrable f' volume a b
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.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 p

pp: case inr
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ IsClosedMap fun x ↦ eval x p

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 p
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inr
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ IsClosedMap fun x ↦ eval x p

Tactic:
·

Goal state after:
case inr
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
h : 0 < p.degree
⊢ IsClosedMap fun x ↦ eval x p
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: case refine_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ContinuousOn f (closedBall c R)

pp: case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x

Tactic:
·

Goal state after:
case refine_1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ContinuousOn f (closedBall c R)
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x

Tactic:
·

Goal state after:
case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x
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) (map (fun t ↦ -t) s)).prod

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j)) =
    ∑ j ∈ Finset.range ((map (fun t ↦ -t) s).card + 1),
      C ((map (fun t ↦ -t) s).esymm j) * X ^ ((map (fun t ↦ -t) s).card - j)

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) (map (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
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)

pp: case 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
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose 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
⊢ ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * ↑(p.natDegree.choose i)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j)) =
    ∑ j ∈ Finset.range ((map (fun t ↦ -t) s).card + 1),
      C ((map (fun t ↦ -t) s).esymm j) * X ^ ((map (fun t ↦ -t) s).card - j)

Tactic:
·

Goal state after:
case e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j)) =
    ∑ j ∈ Finset.range ((map (fun t ↦ -t) s).card + 1),
      C ((map (fun t ↦ -t) s).esymm j) * X ^ ((map (fun t ↦ -t) s).card - j)
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

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

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

Tactic:
·

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| (map (fun t ↦ X - C t) s).prod.coeff k

Tactic:
congr
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    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.MeasureTheory.Integral.DivergenceTheorem

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

Tactic:
·

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

Goal state before:
pp: case e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x ↦ X + C (-x)) s).prod.coeff k = (map (fun r ↦ X + C r) (map (fun t ↦ -t) s)).prod.coeff ?convert_1

pp: case e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (-1) ^ (s.card - k) * s.esymm (s.card - k) = (map (fun t ↦ -t) s).esymm ((map (fun t ↦ -t) s).card - ?convert_1)

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

pp: case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ?convert_1 ≤ (map (fun t ↦ -t) s).card

Tactic:
·

Goal state after:
case e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (map (fun x ↦ X + C (-x)) s).prod.coeff k = (map (fun r ↦ X + C r) (map (fun t ↦ -t) s)).prod.coeff ?convert_1
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (-1) ^ (s.card - k) * s.esymm (s.card - k) = (map (fun t ↦ -t) s).esymm ((map (fun t ↦ -t) s).card - k)

pp: case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ k ≤ (map (fun t ↦ -t) s).card

Tactic:
·

Goal state after:
case e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ (-1) ^ (s.card - k) * s.esymm (s.card - k) = (map (fun t ↦ -t) s).esymm ((map (fun t ↦ -t) s).card - k)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ k ≤ (map (fun t ↦ -t) s).card

Tactic:
·

Goal state after:
case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ k ≤ (map (fun t ↦ -t) s).card