mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
n : ℕ
⊢ |∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)

Tactic:
let F : ℝ → ℝ := fun x => (∑ i ∈ range n, x ^ (i + 1) / (i + 1)) + log (1 - x)

Goal state after:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
⊢ |∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
⊢ {t | s ⊆ ↑t} = {t | (convexHull 𝕜) s ⊆ ↑t}

Tactic:
ext t

Goal state after:
𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
t : ConvexCone 𝕜 M
⊢ t ∈ {t | s ⊆ ↑t} ↔ t ∈ {t | (convexHull 𝕜) s ⊆ ↑t}
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : y ^ 2 ≤ x ^ 2
⊢ (y ^ 2) ^ n / |1 - y ^ 2| = (y ^ 2) ^ n / (1 - y ^ 2)

Tactic:
by rw [abs_of_pos (by simpa [abs_lt] using hI hy)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)

Tactic:
norm_eq_abs,

Goal state after:
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ |x ^ (i + 1) / (↑i + 1)| = |x| ^ (i + 1) / (↑i + 1)
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
absorbs : Absorbent ℝ s
hgauge : gauge s x < 1
⊢ ∃ y ∈ s, x ∈ openSegment ℝ 0 y

Tactic:
rcases exists_lt_of_gauge_lt absorbs hgauge with ⟨r, hr₀, hr₁, y, hy, rfl⟩

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
y : E
hy : y ∈ s
hgauge : gauge s ((fun x ↦ r • x) y) < 1
⊢ ∃ y_1 ∈ s, (fun x ↦ r • x) y ∈ openSegment ℝ 0 y_1
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.mp
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s → ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r

pp: case inr.mpr
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ (∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r) → r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s

Tactic:
· rintro ⟨hr, hx⟩
    simp_rw [mem_Ioi] at hr ⊢
    rw [← mem_smul_set_iff_inv_smul_mem₀ hr.ne'] at hx
    have := smul_pos (inv_pos.2 ha') hr
    refine ⟨a⁻¹ • r, ⟨this, ?_⟩, smul_inv_smul₀ ha'.ne' _⟩
    rwa [← mem_smul_set_iff_inv_smul_mem₀ this.ne', smul_assoc,
      mem_smul_set_iff_inv_smul_mem₀ (inv_ne_zero ha'.ne'), inv_inv]

Goal state after:
case inr.mpr
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
⊢ (∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r) → r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
F : Type u_2
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
f : StrongDual 𝕜 F
x✝ : F
⊢ (extendRCLike ((fun f ↦ reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f) f)) x✝ = f x✝

Tactic:
apply RCLike.ext <;> simp [extendRCLike_apply]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case inr.inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s✝, f a < s
hf₂ : ∀ b ∈ t, s ≤ f b
⊢ ⇑f '' t ⊆ Ioi s

Tactic:
rw [← interior_Ici]

Goal state after:
case inr.inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s✝, f a < s
hf₂ : ∀ b ∈ t, s ≤ f b
⊢ ⇑f '' t ⊆ interior (Ici s)
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
⊢ gauge (closedBall 0 r) x ≤ gauge s x

Tactic:
exact gauge_mono hs hsr _

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : LocallyCompactSpace E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁵ : TopologicalSpace α
f : α → E → F
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : CompleteSpace F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  (fun p ↦ fderiv 𝕜 (f p.1) p.2) ⁻¹' s =
    {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s}
⊢ MeasurableSet
    ({p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ s} ∪
      {p | ¬DifferentiableAt 𝕜 (f p.1) p.2} ∩ {_p | 0 ∈ s})

Tactic:
exact
    (measurableSet_of_differentiableAt_of_isComplete_with_param hf hs.isComplete).union
      ((measurableSet_of_differentiableAt_with_param _ hf).compl.inter (MeasurableSet.const _))

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

Goal state before:
pp: case hf
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ 0 ≤ᵐ[μ.restrict (Icc (b₀ - δ) (b₀ + δ))] fun t ↦ ‖f p t‖

Tactic:
exact Eventually.of_forall (fun x ↦ norm_nonneg _)

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

Goal state before:
pp: case hf
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ 0 ≤ᵐ[μ.restrict (Icc a b)] fun t ↦ ‖f p t - f q t‖

Tactic:
exact Eventually.of_forall (fun x ↦ norm_nonneg _)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto floor (𝓝[<] ↑n) (pure (n - 1))

Tactic:
by
  simpa only [ceil_intCast] using tendsto_floor_left_pure_ceil_sub_one (n : α)

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl.left.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[<] 1 ≤ 𝓝[univ] s ×ˢ 𝓝[Icc 0 1] 1

Tactic:
nhdsWithin_univ,

Goal state after:
case inl.left.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[<] 1 ≤ 𝓝 s ×ˢ 𝓝[Icc 0 1] 1
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, ↑n)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : ¬∃ n, t = ↑n
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)

Tactic:
· rw [ContinuousAt, nhds_prod_eq, ← nhdsLT_sup_nhdsGE (n : α), prod_sup, tendsto_sup]
    constructor
    · refine (((h (s, 1) ⟨trivial, zero_le_one, le_rfl⟩).tendsto.mono_left ?_).comp
        (tendsto_id.prodMap (tendsto_fract_left _))).mono_right (le_of_eq ?_)
      · rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsLT one_pos]
        exact Filter.prod_mono le_rfl (nhdsWithin_mono _ Ico_subset_Icc_self)
      · simp [hf]
    · refine (((h (s, 0) ⟨trivial, le_rfl, zero_le_one⟩).tendsto.mono_left <| le_of_eq ?_).comp
        (tendsto_id.prodMap (tendsto_fract_right _))).mono_right (le_of_eq ?_) <;>
        simp [nhdsWithin_prod_eq, nhdsWithin_univ]

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : ¬∃ n, t = ↑n
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
⊢ AnalyticOnNhd ℝ (circleMap c R) univ

Tactic:
intro z hz

Goal state after:
c : ℂ
R z : ℝ
hz : z ∈ univ
⊢ AnalyticAt ℝ (circleMap c R) z
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
⊢ ∫ (x : ℝ) in 0..t, g x ≤ sSup ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x

Tactic:
by
  let h'_int := hg.intervalIntegrable₀ hT.ne' h_int
  let ε := Int.fract (t / T) * T
  conv_lhs =>
    rw [← Int.fract_div_mul_self_add_zsmul_eq T t hT.ne', ←
      integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]
  rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε h'_int, hg.intervalIntegral_add_eq ε 0, zero_add,
    add_le_add_iff_right]
  exact (continuous_primitive h'_int 0).continuousOn.le_sSup_image_Icc
    (mem_Icc_of_Ico (Int.fract_div_mul_self_mem_Ico T t hT))

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
hE : ¬CompleteSpace E
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

Tactic:
simp only [integral, dif_neg hE]

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

Goal state before:
pp: case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
hE : CompleteSpace E
h0 : 0 < R
⊢ ∮ (z : ℂ) in C(c, R), f z = 0

Tactic:
calc
    (∮ z in C(c, R), f z) = ∮ z in C(c, R), (z - c)⁻¹ • (z - c) • f z :=
      (circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _).symm
    _ = (2 * ↑π * I : ℂ) • (c - c) • f c :=
      (circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable h0 hs
        ((continuousOn_id.sub continuousOn_const).smul hc) fun z hz =>
        (differentiableAt_id.sub_const _).smul (hd z hz))
    _ = 0 := by rw [sub_self, zero_smul, smul_zero]

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 = (powersetCard n univ).biUnion fun t ↦ {∑ i ∈ t, Finsupp.single i 1}

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 ↦ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) =
    (powersetCard n univ).biUnion fun t ↦ {∑ i ∈ t, Finsupp.single i 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
⊢ ∀ x ∈ ball c ↑R \ s, (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - x)⁻¹ • f z = f x

Tactic:
intro z hz

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)
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)⁻¹ • ∮ (z_1 : ℂ) in C(c, ↑R), (z_1 - z)⁻¹ • f z_1 = f z
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
φ : k →+* ℂ
⊢ (lift K φ).comp (algebraMap k K) = φ

Tactic:
unfold lift

Goal state after:
K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
φ : k →+* ℂ
⊢ IsAlgClosed.lift.comp (algebraMap k K) = φ
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : (ofClass v).ValueGroup₀
hx : (hom v) x = 0
⊢ x = 0

Tactic:
by
  refine (eq_of_le_of_not_lt (zero_le (a := x)) fun h_lt ↦ ?_).symm
  have hs := strictMono v h_lt
  rw [map_zero, hx] at hs
  exact hs.false

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

Goal state before:
pp: case refine_1
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ofClass v.restrict).ValueGroup₀ˣ
h : (hom v.restrict) ↑x < γ
k : K
hk : (restrict₀ (ofClass v.restrict)) k = ↑x
⊢ k ≠ 0

Tactic:
simp only [restrict₀_apply, MonoidWithZeroHom.coe_ofClass, restrict_def, map_eq_zero,
      dite_eq_left_iff, coe_ne_zero, imp_false, not_not] at hk
    by_contra h0
    rw [dif_pos (by rw [dif_pos ((zero_iff v).mpr h0)]), eq_comm] at hk
    simp at hk

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
⊢ embedRealFun x < embedRealFun y

Tactic:
have hy : y = y - x + x := (sub_add_cancel y x).symm

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
inst✝ : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
⊢ embedRealFun x < embedRealFun y
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case neg.inr
M✝ : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M✝
inst✝¹ : IsUltrametricDist M✝
inst✝ : Nonempty ι
f : ι → M✝
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ ∃ i, (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
refine ⟨M, ?_, ?_⟩
          · simp [hMs ht]
          rw [Multiset.map_cons, Multiset.prod_cons]
          exact le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case cons.inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ ‖∏ i ∈ Finset.cons a s ha, f i‖₊ = (Finset.cons a s ha).sup fun i ↦ ‖f i‖₊

Tactic:
suffices ‖f a‖₊ ≠ ‖∏ x ∈ s, f x‖₊ by simp [← IH, nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm this]

Goal state after:
case cons.inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ ‖f a‖₊ ≠ ‖∏ x ∈ s, f x‖₊
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R) → r ∈ nonZeroDivisorsLeft R

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ r ∈ nonZeroDivisorsLeft R → (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)

Tactic:
· intro H s hrs
    have := H (C s) (by rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs])
    simpa using congr(coeff 0 $(this))

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ r ∈ nonZeroDivisorsLeft R → (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R) → r ∈ nonZeroDivisorsRight R

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ r ∈ nonZeroDivisorsRight R → (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)

Tactic:
· intro H s hrs
    have := H (C s) (by rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs])
    simpa using congr(coeff 0 $(this))

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ r ∈ nonZeroDivisorsRight R → (monomial n) r ∈ nonZeroDivisorsRight (MvPowerSeries σ R)
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ False

Tactic:
refine weightedHomogeneousComponent_of_weightedOrder ?_ H

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ ↑p = weightedOrder w f
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ False

Tactic:
refine weightedHomogeneousComponent_of_weightedOrder ?_ H

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ ↑q = weightedOrder w g