mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
z : ℂ
h : z ∈ re ⁻¹' [[a, b]]
⊢ g z ∈ A

Tactic:
simpa using

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
z : ℂ
h : z ∈ re ⁻¹' [[a, b]]
⊢ z.re ≤ b ∧ a ≤ z.re
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
z : ℂ
hz : z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s
⊢ g z ∈ ball c (rexp b) \ closedBall c (rexp a)

Tactic:
simpa using

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
z : ℂ
hz : z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s
⊢ a < z.re ∧ z.re < b
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
hd : ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z
⊢ ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ)

Tactic:
simpa using

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
hd : ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z
⊢ ∫ (x : ℝ) in 0..2 * π, f (c + cexp (↑b + ↑x * I)) = ∫ (x : ℝ) in 0..2 * π, f (c + cexp (↑a + ↑x * I))
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (map (algebraMap F E) p).Splits
⊢ Function.Bijective (mapRoots p E)

Tactic:
by
  constructor
  · exact fun _ _ h => Subtype.ext (RingHom.injective _ (Subtype.ext_iff.mp h))
  · intro y
    -- this is just an equality of two different ways to write the roots of `p` as an `E`-polynomial
    have key := (IsSplittingField.splits p.SplittingField p).roots_map
      (IsScalarTower.toAlgHom F p.SplittingField E : p.SplittingField →+* E)
    rw [map_map, AlgHom.comp_algebraMap] at key
    have hy := Subtype.mem y
    simp only [rootSet, Finset.mem_coe, Multiset.mem_toFinset, key, Multiset.mem_map] at hy
    rcases hy with ⟨x, hx1, hx2⟩
    exact ⟨⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr hx1⟩, Subtype.ext hx2⟩

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

Goal state before:
pp: F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
simpa using

Goal state after:
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R
Module: Mathlib.Analysis.Complex.Liouville

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ f = const E c

Tactic:
convert hc'

Goal state after:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ c = c'
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
e : σ ≃ τ
h : ((rename ⇑e) φ).IsSymmetric
⊢ φ.IsSymmetric

Tactic:
simpa using

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
e : σ ≃ τ
h : ((rename ⇑e) φ).IsSymmetric
⊢ φ.IsSymmetric
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg : (restrictProd p q) f = (restrictProd p q) g
⊢ f = g

Tactic:
classical
  simp only [restrictProd, restrictDvd_def] at hfg
  simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk_inj] at hfg
  ext (x hx)
  rw [rootSet_def, aroots_mul hpq] at hx
  rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h
  · have : Fact ((p.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_right p q))⟩
    have key :
      x =
        algebraMap p.SplittingField (p * q).SplittingField
          ((rootsEquivRoots p _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots p _) ⟨x, _⟩).symm
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)
  · have : Fact ((q.map (algebraMap F (p * q).SplittingField)).Splits) :=
      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
        ((map_dvd_map' _).mpr (dvd_mul_left q p))⟩
    have key :
      x =
        algebraMap q.SplittingField (p * q).SplittingField
          ((rootsEquivRoots q _).invFun
            ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
      Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm
    rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
    exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.2 _)

Goal state after:
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 τ
n : ℕ
e : σ ≃ τ
⊢ (rename ⇑e) (esymm σ R n) = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i)

Tactic:
simp_rw [esymm, map_sum, map_prod, rename_X]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (esymm σ R n).support = image (fun t ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)

Tactic:
support_esymm'

Goal state after:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ ((powersetCard n univ).biUnion fun t ↦ {∑ i ∈ t, Finsupp.single i 1}) =
    image (fun t ↦ ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_2
E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.univ.pi fun i ↦ Set.Ioo (eL a i) (eL b i)) \ ⇑eL.symm ⁻¹' s
i : Fin (n + 1)
⊢ eL.symm x ∈ ⇑eL ⁻¹' interior (Set.Icc (eL a) (eL b))

Tactic:
simpa using

Goal state after:
case refine_2
E : Type u
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : Preorder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i, (f' i x) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.univ.pi fun i ↦ Set.Ioo (eL a i) (eL b i)) \ ⇑eL.symm ⁻¹' s
i : Fin (n + 1)
⊢ x ∈ Set.univ.pi fun i ↦ Set.Ioo (eL a i) (eL b i)
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
⊢ (map (algebraMap F (p.comp q).SplittingField) p).Splits

Tactic:
have key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂) := by
    intro p₁ p₂ hp₁ hp₂
    by_cases h₁ : p₁.comp q = 0
    · rcases comp_eq_zero_iff.mp h₁ with h | h
      · rw [h, zero_mul]
        simp [P]
      · exact False.elim (hq (by rw [h.2, natDegree_C]))
    by_cases h₂ : p₂.comp q = 0
    · rcases comp_eq_zero_iff.mp h₂ with h | h
      · simp [h, P]
      · exact False.elim (hq (by rw [h.2, natDegree_C]))
    have key := mul_splits_in_splittingField_of_mul h₁ h₂ hp₁ hp₂
    rwa [← mul_comp] at key

Goal state after:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂)
⊢ (map (algebraMap F (p.comp q).SplittingField) p).Splits
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ psum σ R 0 = ↑(Fintype.card σ)

Tactic:
simp [psum]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ psum σ R 1 = ∑ i, X i

Tactic:
simp [psum]

Goal state after:
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:
simpa using

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 (f a✝) * abv (z 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]
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:
simpa using

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✝) * abv (z x)) l atTop
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) + -f a)) l atTop

Tactic:
simpa using

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✝)) l atTop
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
n : ℕ
⊢ IsClosedMap fun x ↦ x ^ n

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
n : ℕ
⊢ IsClosedMap fun x ↦ x ^ n
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)

Tactic:
simpa using

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:
simpa using

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.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: 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
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
rcases le_total a b with hab | hab

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

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.Analysis.Complex.CauchyIntegral

Goal state before:
pp: R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
f : ℂ → ℂ
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), f z / (z - w) = 2 * ↑π * I * f w

Tactic:
simpa using

Goal state after:
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
f : ℂ → ℂ
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ * f z = 2 * ↑π * I * f w
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ z ∈ ball c ↑R \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ eball 0 ↑R
⊢ c + w ∈ ball c ↑R

Tactic:
simpa using

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ z ∈ ball c ↑R \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : w ∈ eball 0 ↑R
⊢ ‖w‖₊ < R
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 : ℝ
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
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
rcases le_total a b with hab | hab
  · simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *
    exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi
  · simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at *
    rw [intervalIntegral.integral_symm, neg_eq_iff_eq_neg, neg_sub]
    exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm

Goal state after:
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:
simpa using

Goal state after:
f : ℂ[X]
hf : 0 < f.degree
hf' : ∀ (z : ℂ), ¬f.IsRoot z
z : ℂ
⊢ Filter.Tendsto (fun x ↦ eval x f) (cobounded ℂ) (cobounded ℂ)
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
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * ↑π * I) • deriv f c

Tactic:
simpa using

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), ((z - c) ^ 2)⁻¹ • f z = (2 * ↑π * I) • deriv f c
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 : ℂ
h0 : 0 < R
hc : DiffContOnCl ℂ f (ball c R)
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * ↑π * I) • deriv f c

Tactic:
simpa using

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
h0 : 0 < R
hc : DiffContOnCl ℂ f (ball c R)
⊢ ∮ (z : ℂ) in C(c, R), ((z - c) ^ 2)⁻¹ • f z = (2 * ↑π * I) • deriv f c
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 : ℂ
h0 : 0 < R
hc : DifferentiableOn ℂ f (closedBall c R)
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * ↑π * I) • deriv f c

Tactic:
simpa using

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
h0 : 0 < R
hc : DifferentiableOn ℂ f (closedBall c R)
⊢ ∮ (z : ℂ) in C(c, R), ((z - c) ^ 2)⁻¹ • f z = (2 * ↑π * I) • deriv f c
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
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
⊢ (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
⊢ (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
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
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ 0 < ↑(u + v).den

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
u v : ℚ
x y : M
hu : u.num • 1 < u.den • x
hv : v.num • 1 < v.den • y
hu' : (u.num * ↑v.den) • 1 < (↑u.den * ↑v.den) • x
⊢ 0 < (u + v).den
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
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ den • x ≤ ↑den • n • 1

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedAddMonoid M
inst✝² : One M
inst✝¹ : ZeroLEOneClass M
inst✝ : NeZero 1
num : ℤ
den : ℕ
x : M
h : num • 1 ≤ den • x
n : ℤ
hn : x ≤ n • 1
⊢ den • x ≤ den • n • 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
x : k
⊢ (star (φ.comp f)) x = (φ.comp f) x

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
k : Type u_2
inst✝ : Field k
f : k →+* K
φ : K →+* ℂ
hφ : IsReal φ
x : k
⊢ (starRingEnd ℂ) (φ (f x)) = φ (f x)