mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case e'_4
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
x : ℝ
⊢ f x = f (x - (↑k - ↑n₁) * T)

Tactic:
simpa using (h₁f.sub_int_mul_eq (k - n₁)).symm

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t₁ t₂ : ℝ
hf : Periodic f T
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)

Tactic:
wlog hT : T ≠ 0

Goal state after:
case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t₁ t₂ : ℝ
hf : Periodic f T
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t₁ t₂ : ℝ},
    Periodic f T → T ≠ 0 → (IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T))
hT : ¬T ≠ 0
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)

E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t₁ t₂ : ℝ
hf : Periodic f T
hT : T ≠ 0
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)
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 : ℝ
⊢ x ∈ univ → ¬EventuallyConst (circleMap c R) (𝓝 x)

Tactic:
hx

Goal state after:
case h₂f
c : ℂ
R : ℝ
hR : R ≠ 0
s : Set ℂ
hs : s ∈ codiscreteWithin (sphere c |R|)
x : ℝ
hx : x ∈ univ
⊢ ¬EventuallyConst (circleMap c R) (𝓝 x)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
x : α
⊢ ν (Prod.mk x ⁻¹' s) < ∞ → ENNReal.ofReal (ν (Prod.mk x ⁻¹' s)).toReal = ν (Prod.mk x ⁻¹' s)

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ∞
x : α
hx : ν (Prod.mk x ⁻¹' s) < ∞
⊢ ENNReal.ofReal (ν (Prod.mk x ⁻¹' s)).toReal = ν (Prod.mk x ⁻¹' s)
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
inst✝¹ : SFinite ν
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : AEStronglyMeasurable f (μ.prod ν)
a✝ : α
⊢ (∀ᵐ (y : β) ∂ν, f (a✝, y) = AEStronglyMeasurable.mk f hf (a✝, y)) →
    ∫ (y : β), f (a✝, y) ∂ν = ∫ (y : β), AEStronglyMeasurable.mk f hf (a✝, y) ∂ν

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : AEStronglyMeasurable f (μ.prod ν)
a✝ : α
hx : ∀ᵐ (y : β) ∂ν, f (a✝, y) = AEStronglyMeasurable.mk f hf (a✝, y)
⊢ ∫ (y : β), f (a✝, y) ∂ν = ∫ (y : β), AEStronglyMeasurable.mk f hf (a✝, y) ∂ν
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : SFinite ν
f : α × β → X
hf : AEStronglyMeasurable f (μ.prod ν)
x : α
⊢ (∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)) → AEStronglyMeasurable (fun y ↦ f (x, y)) ν

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : SFinite ν
f : α × β → X
hf : AEStronglyMeasurable f (μ.prod ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)
⊢ AEStronglyMeasurable (fun y ↦ f (x, y)) ν
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C

Tactic:
by
  have : ‖(2 * π * I : ℂ)⁻¹‖ = (2 * π)⁻¹ := by simp [Real.pi_pos.le]
  rw [norm_smul, this, ← div_eq_inv_mul, div_le_iff₀ Real.two_pi_pos, mul_comm (R * C), ← mul_assoc]
  exact norm_integral_le_of_norm_le_const hR hf

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
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞ → ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν = ENNReal.ofReal (∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν).toReal

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν = ENNReal.ofReal (∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν).toReal
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
inst✝ : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
x : α
⊢ (∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)) →
    (HasFiniteIntegral (fun y ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν ↔ HasFiniteIntegral (fun y ↦ f (x, y)) ν)

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)
⊢ HasFiniteIntegral (fun y ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν ↔ HasFiniteIntegral (fun y ↦ f (x, y)) ν
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
inst✝ : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
a✝ : α
⊢ (∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (a✝, y) = f (a✝, y)) →
    ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (a✝, y)‖ ∂ν = ∫ (y : β), ‖f (a✝, y)‖ ∂ν

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
a✝ : α
hx : ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (a✝, y) = f (a✝, y)
⊢ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (a✝, y)‖ ∂ν = ∫ (y : β), ‖f (a✝, y)‖ ∂ν
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
⊢ x ∈ Box.Icc I ∩ s →
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ J ≤ I,
          Box.Icc J ⊆ closedBall x δ →
            x ∈ Box.Icc J →
              (GP.bDistortion = true → J.distortion ≤ c) →
                dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε

Tactic:
hx

Goal state after:
case refine_3
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ J ≤ I,
        Box.Icc J ⊆ closedBall x δ →
          x ∈ Box.Icc J →
            (GP.bDistortion = true → J.distortion ≤ c) →
              dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
⊢ x ∈ Box.Icc I \ s →
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ J ≤ I,
          Box.Icc J ⊆ closedBall x δ →
            x ∈ Box.Icc J →
              (GP.bDistortion = true → J.distortion ≤ c) →
                dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤
                  ε * (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
hx

Goal state after:
case refine_4
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ J ≤ I,
        Box.Icc J ⊆ closedBall x δ →
          x ∈ Box.Icc J →
            (GP.bDistortion = true → J.distortion ≤ c) →
              dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤
                ε * (volume.toBoxAdditive.restrict ↑I ⋯) J
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:

Tactic:
‖(∮ z in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ =
        ‖(∮ z in C(c, r), (z - c)⁻¹ • f z) - ∮ z in C(c, r), (z - c)⁻¹ • y‖ := by
      congr 2
      · exact circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable hr0
          hrR hs (hc.mono hsub) fun z hz => hd z ⟨hsub' hz.1, hz.2⟩
      · simp [hr0.ne']
    _ = ‖∮ z in C(c, r), (z - c)⁻¹ • (f z - y)‖ := by
      simp only [smul_sub]
      have hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r) :=
        (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hzne _ hz
      rw [circleIntegral.integral_sub] <;> refine (hc'.smul ?_).circleIntegrable hr0.le
      · exact hc.mono <| subset_inter
          (sphere_subset_closedBall.trans <| closedBall_subset_closedBall hrR) hzne
      · exact continuousOn_const
    _ ≤ 2 * π * r * (r⁻¹ * (ε / (2 * π))) := by
      refine circleIntegral.norm_integral_le_of_norm_le_const hr0.le fun z hz => ?_
      specialize hzne z hz
      rw [mem_sphere, dist_eq_norm] at hz
      rw [norm_smul, norm_inv, hz, ← dist_eq_norm]
      refine mul_le_mul_of_nonneg_left (hδ _ ⟨?_, hzne⟩).le (inv_nonneg.2 hr0.le)
      rwa [mem_closedBall_iff_norm, hz]
    _ = ε := by field

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 σ
⊢ esymm σ R 1 = ∑ i, X i

Tactic:
by simp [esymm, powersetCard_one]

Goal state after:
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 ∈ interior (Set.Icc a b)

Tactic:
rw [← hIcc]

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)
⊢ eL.symm x ∈ interior (⇑eL ⁻¹' Set.Icc (eL a) (eL b))
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 \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑π * I) • f w

Tactic:
have hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R) := fun z hz ↦
    calc
      F z = (z - w)⁻¹ • (f z - f w) := update_of_ne (hne z hz) ..
      _ = (z - w)⁻¹ • f z - (z - w)⁻¹ • f w := smul_sub _ _ _

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 \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
⊢ ∮ (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 : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z ↦ (z - w)⁻¹) (sphere c R)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) - ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f w = 0

Tactic:
← circleIntegral.integral_sub,

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 \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z ↦ (z - w)⁻¹) (sphere c R)
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z - (z - w)⁻¹ • f w = 0

case hf
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 \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z ↦ (z - w)⁻¹) (sphere c R)
⊢ CircleIntegrable (fun z ↦ (z - w)⁻¹ • f z) c R

case hg
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 \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : (insert w s).Countable
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z
HI : ∮ (z : ℂ) in C(c, R), F z = 0
hne : ∀ z ∈ sphere c R, z ≠ w
hFeq : EqOn F (fun z ↦ (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z ↦ (z - w)⁻¹) (sphere c R)
⊢ CircleIntegrable (fun z ↦ (z - w)⁻¹ • f w) c R
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
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
this : (minpoly F α).natDegree = p.natDegree
⊢ finrank F p.SplittingField = p.natDegree * finrank (↥F⟮α⟯) p.SplittingField

Tactic:
let _ : AddCommGroup F⟮α⟯ := Ring.toAddCommGroup
    rw [← Module.finrank_mul_finrank F F⟮α⟯ p.SplittingField,
      IntermediateField.adjoin.finrank hα, this]

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 σ
this : (fun x ↦ x ∈ Set.univ) = fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∑ i, X i = msymm σ R (Nat.Partition.indiscrete 1)

Tactic:
Fintype.sum_equiv (Equiv.trans Sym.oneEquiv (Equiv.Set.univ (Sym σ 1)).symm)
    _ (fun s ↦ (s.1.1.map X).prod)

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.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
⊢ False

Tactic:
have : (Ioo l u).Countable :=
      (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub

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 : (Ioo l u).Countable
⊢ False
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
⊢ x ∈ powersetCard k s → (prod ∘ map Neg.neg) x = (-1) ^ k * x.prod

Tactic:
hx

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 = (-1) ^ k * x.prod
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: case mpr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
s : Set ℂ
d : ∀ y ∈ s, DifferentiableAt ℂ f y
o : IsOpen s
m : c ∈ s
h : AnalyticOnNhd ℂ f s
⊢ AnalyticAt ℂ f c

Tactic:
exact h _ m

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

Goal state before:
pp: 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
⊢ (IsScalarTower.toAlgHom ℚ ℝ ℂ) 0 = 0

Tactic:
map_zero

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