mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
| cov.monodromy (Path.Homotopic.Quotient.refl (f a₀)) ⟨e₀, he⟩

Tactic:
monodromy_refl

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
| id ⟨e₀, he⟩
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
F' : C(A, E)
hF'₁ : F' a₀ = ↑(F a₀)
hF'₂ : ∀ (x : A), p (F' x) = ↑(f x)
hF_unique : { toFun := fun a ↦ ⟨F' a, ⋯⟩, continuous_toFun := ⋯ } = F
⊢ F' = { toFun := Subtype.val, continuous_toFun := ⋯ }.comp F

Tactic:
ext; simp [← hF_unique]

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

Goal state before:
pp: c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁
this : s ×ℂ {z.im} ⊆ ball c r
⊢ ↑x + ↑z.im * I ∈ s ×ℂ {z.im}

Tactic:
by simp [mem_reProdIm, hx]

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

Goal state before:
pp: c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2

Tactic:
cases mem_uIoc.mp y_in_I

Goal state after:
case inl
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h✝ : c.im < y ∧ y ≤ z.im
⊢ (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2

case inr
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h✝ : z.im < y ∧ y ≤ c.im
⊢ (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case zero
V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
m : Fin (0 + 1) → V
⊢ ∂^{m} f = ∂^{init m} (∂_{m (last 0)} f)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case zero
V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
y : V
f : E
⊢ ∂^{fun x ↦ y} f = ∂_{y}^[0] f

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case zero
V : Type u_5
E : Type u_6
inst✝³ : LineDeriv V E E
inst✝² : AddCommGroup V
inst✝¹ : AddCommGroup E
inst✝ : LineDerivAdd V E E
x y : E
m : Fin 0 → V
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case zero
R : Type u_4
V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
inst✝¹ : SMul R E
inst✝ : LineDerivSMul R V E E
r : R
x : E
m : Fin 0 → V
⊢ ∂^{m} (r • x) = r • ∂^{m} x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case zero
V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousLineDeriv V E E
m : Fin 0 → V
⊢ Continuous ∂^{m}

Tactic:
| zero =>

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ≤ ‖interpStrip f z‖

Tactic:
by
  apply le_on_closure (fun w hw ↦ norm_le_interpStrip_of_mem_verticalStrip_zero f w hd hB hw)
    (Continuous.comp_continuousOn' continuous_norm hd.2)
    (Continuous.comp_continuousOn' continuous_norm (diffContOnCl_interpStrip f).2)
  rwa [verticalClosedStrip, ← closure_Ioo zero_ne_one, ← closure_preimage_re] at hz

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
l u : ℝ
hul : l < u
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
hgoal : ‖f z‖ ≤ ‖interpStrip (scale f l u) ((z - ↑l) / (↑u - ↑l))‖
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖

Tactic:
interpStrip_scale f hul z

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
l u : ℝ
hul : l < u
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
hgoal : ‖f z‖ ≤ ‖interpStrip' f l u z‖
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε
⊢ ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f (↑x.re + ↑y * I) - f z‖ ≤ ε

Tactic:
obtain ⟨i, i_pos, hi⟩ := this

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
i : ℝ
i_pos : 0 < i
hi : ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε
⊢ ∃ i, 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f (↑x.re + ↑y * I) - f z‖ ≤ ε
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
h_subst : (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r)
⊢ R * R * normSq (cexp (↑θ * I)) + r * r * normSq (cexp (↑φ * I)) -
      2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
    R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)

Tactic:
simp [normSq_eq_norm_sq, Real.cos_sub]

Goal state after:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
h_subst : (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r)
⊢ R * R + r * r - 2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
    R ^ 2 + r ^ 2 - 2 * R * r * (Real.cos θ * Real.cos φ + Real.sin θ * Real.sin φ)
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun x ↦ x * log x) y = log y + 1
⊢ deriv (fun x ↦ log x + 1) x = x⁻¹

Tactic:
deriv_add_const,

Goal state after:
x : ℝ
hx : ¬x = 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun x ↦ x * log x) y = log y + 1
⊢ deriv log x = x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case refine_1
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
⊢ False

Tactic:
have I : 0 < min 1 t := lt_min zero_lt_one ht

Goal state after:
case refine_1
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ ↑x ^ s) (Ioo 0 t) volume
⊢ EqOn (fun a ↦ ‖↑a ^ s‖) (fun a ↦ a ^ s.re) (Ioo 0 t)

Tactic:
intro a

Goal state after:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ ↑x ^ s) (Ioo 0 t) volume
a : ℝ
⊢ a ∈ Ioo 0 t → (fun a ↦ ‖↑a ^ s‖) a = (fun a ↦ a ^ s.re) a
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖g (↑y * I)‖ ≤ C

Tactic:
· rw [hgn, re_ofReal_mul, I_re, mul_zero, mul_zero, Real.exp_zero,
      one_mul]
    exact him y

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2) = ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x)

Tactic:
apply integral_congr_codiscreteWithin
    apply codiscreteWithin_mono (by tauto : Ι 0 π ⊆ Set.univ)
    have : AnalyticOnNhd ℝ (4 * sin · ^ 2) Set.univ := fun _ _ ↦ by fun_prop
    have := this.preimage_zero_mem_codiscrete (x := π / 2)
    simp only [sin_pi_div_two, one_pow, mul_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
      Set.preimage_compl, forall_const] at this
    filter_upwards [this] with a ha
    simp only [Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, mul_eq_zero,
      OfNat.ofNat_ne_zero, ne_eq, not_false_eq_true, pow_eq_zero_iff, false_or] at ha
    rw [log_mul (by simp) (by simp_all), log_pow, Nat.cast_ofNat]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : ∀ (n : ℕ), ‖g n z‖ ≤ C
⊢ f z = 0

Tactic:
by
    contrapose! H
    simp only [hg]
    exact (((tendsto_pow_atTop_atTop_of_one_lt (Real.one_lt_exp_iff.2 hz)).atTop_mul_const
      (norm_pos_iff.2 H)).eventually (eventually_gt_atTop C)).exists

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t = log (log b) - log (log a)

Tactic:
← intervalIntegral.integral_congr (fun _ _ ↦ deriv_log_log_apply)

Goal state after:
a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (x : ℝ) in a..b, deriv (fun x ↦ log (log x)) x = log (log b) - log (log a)
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ¬∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u ≠ ⊤
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R

Tactic:
rw [← hf.exists_meromorphicOrderAt_ne_top_iff_forall (isConnected_sphere (by simp) c
      (abs_nonneg R))] at t₀

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ¬∃ u, meromorphicOrderAt f ↑u ≠ ⊤
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hint
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ ∀ (a : ℝ), 1 + ↑a ^ 2 ∈ slitPlane

Tactic:
intro a

Goal state after:
case hint
a✝ b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
a : ℝ
⊢ 1 + ↑a ^ 2 ∈ slitPlane
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
⊢ ContinuousAt (herglotzLogIntegrand w ρ) z

Tactic:
have : ‖z - ρ‖ ≠ 0 := by simp_all [sub_eq_zero]
  simp only [herglotzLogIntegrand, herglotzRieszKernel_fun_def, sub_zero, smul_eq_mul]
  fun_prop (disch := grind)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case zero
n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * 0 + 1) = 2 * ∏ i ∈ Finset.range 0, (2 * ↑i + 2) / (2 * ↑i + 3)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case zero
n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * 0) = π * ∏ i ∈ Finset.range 0, (2 * ↑i + 1) / (2 * ↑i + 2)

Tactic:
| zero =>

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
let q := 𝕢 h z
  have qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * π * I / h)) z := by
    simpa only [id_eq, mul_one] using! (((hasStrictDerivAt_id z).const_mul _).div_const _).cexp
  -- Now show that the q-map has a differentiable local inverse at z, say L : ℂ → ℂ with L q = z.
  have diff_ne : q * (2 * π * I / h) ≠ 0 :=
    mul_ne_zero (exp_ne_zero _) (div_ne_zero two_pi_I_ne_zero <| mod_cast hh)
  let L := (qdiff.localInverse (𝕢 h) _ z) diff_ne
  have diff_L : DifferentiableAt ℂ L q :=
    (qdiff.to_localInverse diff_ne).hasStrictFDerivAt.differentiableAt
  have hL : 𝕢 h ∘ L =ᶠ[𝓝 q] (id : ℂ → ℂ) :=
    (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_right_inverse
  -- Thus, if F = cuspFunction h f, we have F q' = f (L q') for q' near q.
  -- Since L is differentiable at q, and f is differentiable at L q [ = z], we conclude
  -- that F is differentiable at q.
  have hF := hL.fun_comp (cuspFunction h f)
  have : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L := funext fun z ↦ eq_cuspFunction hh hf (L z)
  rw [this] at hF
  rw [← EventuallyEq.eq_of_nhds (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_left_inverse]
    at hol_z
  exact (hol_z.comp q diff_L).congr_of_eventuallyEq hF.symm

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : c ≤ z
hz₂ : z ∈ Metric.ball c r
⊢ 0 ≤ f z

Tactic:
by
  have H := taylorSeries_eq_on_ball' hz₂ hf
  rw [← sub_nonneg] at hz₁
  have hz' := eq_re_of_ofReal_le hz₁
  rw [hz'] at hz₁ H
  refine H ▸ tsum_nonneg fun n ↦ ?_
  rw [← ofReal_natCast, ← ofReal_pow, ← ofReal_inv, eq_re_of_ofReal_le (h n), ← ofReal_mul,
    ← ofReal_mul]
  norm_cast at hz₁ ⊢
  positivity [zero_re ▸ (Complex.le_def.mp (h n)).1]

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

Goal state before:
pp: case zero
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ 0 ≤ iteratedDeriv 0 (fun x ↦ f x - f c) c

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
⊢ -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n = ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n

Tactic:
by
      simp only [_root_.pow_succ, pow_mul, _root_.pow_zero, one_mul, mul_neg, neg_mul,
        integral_neg, neg_inj]
      congr! 5
      rw [← sq, ← sq, sin_sq]

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : w ∈ ball 0 R
hR : 0 < R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖

Tactic:
rw [mem_ball_iff_norm, sub_zero] at hw

Goal state after:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ InjOn (fun z ↦ ↑ε / (f z - x)) U

Tactic:
intro z hz w hw heq
    simpa [div_eq_mul_inv, hε₀.ne', hf_inj.eq_iff] using heq

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

Goal state before:
pp: case hf
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log R

pp: case hg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log ‖c - u‖

Tactic:
repeat apply h₃f.subset (fun _ ↦ (by simp_all))

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

Goal state before:
pp: case neg
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
x : E
hx : x ∉ Metric.closedBall 0 1
⊢ (Metric.closedBall 0 1).piecewise id g x ∈ Metric.closedBall 0 1

Tactic:
· simp only [g, piecewise_eq_of_notMem (hi := hx), RCLike.real_smul_eq_coe_smul (K := 𝕜)]
        by_cases hx' : x = 0 <;> simp [hx']

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
⊢ A.discr = A.trace ^ 2 - 4 * A.det

Tactic:
nontriviality R
  rw [discr, Polynomial.discr_of_degree_eq_two (by simp; norm_cast)]
  simp [A.charpoly_of_card_eq_two hn]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case zero
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
⊢ dist ((g 0).compContinuous e) f ≤ (2 / 3) ^ 0 * ‖f‖

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case neg
w : ℂ
hw : ¬0 < w.im
⊢ ↑ofComplex w = Classical.choice ⋯

Tactic:
change (Function.invFunOn UpperHalfPlane.coe Set.univ w) = _
    simp only [invFunOn, dite_eq_right_iff, mem_univ, true_and]
    rintro ⟨a, rfl⟩
    exact (a.im_pos.not_ge (by simpa using hw)).elim

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((compRingEquiv m n R).toRingHom (f.mapMatrix ((evalRingHom 0).mapMatrix (cornerAddX M k)))).det =
    (↑(compRingEquiv m n R) (f.mapMatrix M)).det

Tactic:
congr with i j

Goal state after:
case e_6.e_6
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
i j : m
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) i j = M i j
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case zero
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = 0
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c

Tactic:
· simp [dist_comm, mul_comm]

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case zero
⊢ iteratedDeriv (0 + 1) sinh = iteratedDeriv 0 cosh

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case zero
⊢ iteratedDeriv (0 + 1) cosh = iteratedDeriv 0 sinh

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case zero
⊢ iteratedDeriv (2 * 0) sinh = sinh

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case zero
⊢ iteratedDeriv (2 * 0) cosh = cosh

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = Function.diag
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)

Tactic:
rw [← range_gf]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = Function.diag
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed[instTopologicalSpaceProd] (range (g ∘ f))