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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ (f - g) =O[cobounded ℂ ⊓ l] fun z ↦ expR (max 0 (max Bf Bg) * ‖z‖ ^ max cf cg)

Tactic:
refine (hOf.trans <| this ?_ ?_ ?_).sub (hOg.trans <| this ?_ ?_ ?_)

Goal state after:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ cf ≤ max cf cg

case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ 0 ≤ max 0 (max Bf Bg)

case refine_3
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ Bf ≤ max 0 (max Bf Bg)

case refine_4
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ cg ≤ max cf cg

case refine_5
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ 0 ≤ max 0 (max Bf Bg)

case refine_6
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ Bg ≤ max 0 (max Bf Bg)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hmero : MeromorphicAt f x
g : 𝕜 → E
hga : AnalyticAt 𝕜 g x
hg0 : g x ≠ 0
hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
z : 𝕜
hgz : AnalyticAt 𝕜 g z
hmem : z ∈ {x}ᶜ
hz : deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z
hzx : z - x ≠ 0
⊢ (z - x) ^ n • deriv g z + deriv ((fun x ↦ x ^ n) ∘ fun x_1 ↦ x_1 - x) z • g z =
    (z - x) ^ n • deriv g z + (↑n * (z - x) ^ (n - 1)) • g z

Tactic:
by
      rw [deriv_comp _ (by fun_prop (disch := grind)) (by fun_prop)]
      simp [deriv_zpow]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Tactic:
replace h : (0 < sSupNormIm f 0) ∧ (0 < sSupNormIm f 1) :=
      ⟨(lt_of_le_of_ne (sSupNormIm_nonneg f 0) (ne_comm.mp h.1)),
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) (ne_comm.mp h.2))⟩

Goal state after:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : 0 < sSupNormIm f 0 ∧ 0 < sSupNormIm f 1
⊢ interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∑ m, w m ⊗ₜ[ℝ] w m = ∑ m, ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n

Tactic:
congr 1 with m

Goal state after:
case e_f
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ w m ⊗ₜ[ℝ] w m = ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (1 - z.re)) ^ (-1) * ((ε + sSupNormIm f 1) ^ z.re)⁻¹ ≤ 1

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 1) ^ z.re

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)

Tactic:
← Real.rpow_neg_one

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (1 - z.re)) ^ (-1) * ((ε + sSupNormIm f 1) ^ z.re) ^ (-1) ≤ 1

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 1) ^ z.re

E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)

Tactic:
by
  rw [interval_average_eq, smul_eq_mul, div_eq_inv_mul]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage (fun z ↦ f (z + c)) 0 R = circleAverage f c R

Tactic:
by
  unfold circleAverage circleMap
  congr
  ext θ
  simp only [zero_add]
  congr 1
  ring

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

Goal state before:
pp: ⊢ Tendsto (deriv fun x ↦ x * log x) (𝓝[>] 0) atBot

Tactic:
have : (deriv (fun x ↦ x * log x)) =ᶠ[𝓝[>] 0] (fun x ↦ log x + 1) := by
    apply eventuallyEq_nhdsWithin_of_eqOn
    intro x hx
    rw [Set.mem_Ioi] at hx
    exact deriv_mul_log hx.ne'
  simp only [tendsto_congr' this, tendsto_atBot_add_const_right, tendsto_log_nhdsGT_zero]

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

Goal state before:
pp: case hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 0 1

Tactic:
rw [← neg_neg log]

Goal state after:
case hab
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable (- -log) volume 0 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ∫ (x : ℝ) in a..b, x ^ r = (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re

pp: case e'_3
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re

Tactic:
· simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.re_ofReal_mul, rpow_def,
      ← RCLike.re_eq_complex_re, smul_eq_mul]
    rw [integral_re]
    refine intervalIntegrable_iff.mp ?_
    rcases h' with h' | h'
    · exact intervalIntegrable_cpow' h'
    · exact intervalIntegrable_cpow (Or.inr h'.2)

Goal state after:
case e'_3
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ log⁺ ‖f x‖) volume a b

Tactic:
simp_rw [← half_mul_log_add_log_abs, mul_add]
  apply IntervalIntegrable.add
  · apply hf.intervalIntegrable_log_norm.const_mul
  · apply hf.intervalIntegrable_log_norm.abs.const_mul

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

Goal state before:
pp: case hab
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume a 0

pp: case hbc
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume 0 b

Tactic:
all_goals exact intervalIntegrable_log'

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

Goal state before:
pp: a : ℂ
h : 1 < ‖a‖
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log ‖a‖

Tactic:
rw [InnerProductSpace.HarmonicOnNhd.circleAverage_eq, zero_sub, norm_neg]

Goal state after:
a : ℂ
h : 1 < ‖a‖
⊢ InnerProductSpace.HarmonicOnNhd (fun x ↦ log ‖x - a‖) (closedBall 0 |1|)
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z ↦ ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z ↦ f z - v) y
key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v
h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z
h8 : IsPreconnected (ball z₀ r)
h9 : EqOn f (fun x ↦ f z) (ball z₀ r)
h10 : f z = f z₀
⊢ False

Tactic:
exact not_eventually.mpr hz₀ (mem_of_superset (ball_mem_nhds z₀ hr) (h10 ▸ h9))

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z | 0 < z.re}
hgd : DiffContOnCl ℂ g {z | 0 < z.re}
hfexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x - g ↑x‖
hfim : ∃ C, ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hgim : ∃ C, ∀ (x : ℝ), ‖g (↑x * I)‖ ≤ C
⊢ ∃ C, ∀ (x : ℝ), ‖(f - g) (↑x * I)‖ ≤ C

Tactic:
rcases hfim with ⟨Cf, hCf⟩

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z | 0 < z.re}
hgd : DiffContOnCl ℂ g {z | 0 < z.re}
hfexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x - g ↑x‖
hgim : ∃ C, ∀ (x : ℝ), ‖g (↑x * I)‖ ≤ C
Cf : ℝ
hCf : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ Cf
⊢ ∃ C, ∀ (x : ℝ), ‖(f - g) (↑x * I)‖ ≤ C
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
this : (circleMap 0 r₁ θ * (starRingEnd ℂ) ρ).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
⊢ ↑(normSq (circleMap 0 r₁ θ) + normSq ρ - 2 * (circleMap 0 r₁ θ * (starRingEnd ℂ) ρ).re) =
    ↑(r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg))

Tactic:
by
      simp [normSq_eq_norm_sq, hρ, -mul_re, this, mul_assoc]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
z : E
h1 : AnalyticAt ℂ (gray z) 0
hz : z ∈ sphere 0 1
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
h10 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun t ↦ z₀ + t • z
⊢ map (ray z) (𝓝 0) ≤ 𝓝 z₀

Tactic:
simpa using! h10.tendsto 0

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

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
⊢ z = P.roots.toFinset.centerMass (P.derivRootWeight z) id

Tactic:
set weight : ℂ → ℝ := P.derivRootWeight z

Goal state after:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
⊢ z = P.roots.toFinset.centerMass weight id
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
g' : ℤ[X]
hg' : p = q * g'
⊢ (aeval z) p = 0

Tactic:
rw [hg', aeval_mul, hz, zero_mul]

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

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
g' : ℤ[X]
hg' : p.mirror = q * g'
⊢ (aeval z) p.mirror = 0

Tactic:
rw [hg', aeval_mul, hz, zero_mul]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ sqrt I = ↑√2⁻¹ * (1 - I) * I

Tactic:
sqrt_eq_ite

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) I).sqrt else ↑√(re I)) = ↑√2⁻¹ * (1 - I) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ ((complexRingEquiv h) I).sqrt = (complexRingEquiv h) ↑√2⁻¹ * (complexRingEquiv h) (1 - I) * (complexRingEquiv h) I

Tactic:
simp [h, mul_assoc, mul_add, add_comm, Complex.sqrt_I, add_mul]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ sqrt (-I) = ↑√2⁻¹ * (1 + I) * -I

Tactic:
sqrt_eq_ite

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ (if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) (-I)).sqrt else ↑√(re (-I))) =
    ↑√2⁻¹ * (1 + I) * -I
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f

Tactic:
by_cases hf : ‖f‖ = 0

Goal state after:
case pos
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ‖f‖ = 0
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f

case neg
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ -m ∉ Set.range ⇑(scalar (Fin 2))

pp: case right
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ (-m).discr = 0

Tactic:
· rw [← RingHom.coe_range, SetLike.mem_coe, neg_mem_iff]
    exact h.1

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ (-m).discr = 0
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
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M.det * M k k ^ (Fintype.card m - 1))).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0

Tactic:
det_mul_corner_pow,

Goal state after:
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
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M k k * ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det)).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist z w / 2 = r / 2 ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2)

Tactic:
← sinh_inj,

Goal state after:
z w : ℍ
r : ℝ
⊢ sinh (dist z w / 2) = sinh (r / 2) ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2)
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝 c) (𝓝 0)

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ ∀ x ∈ {c}ᶜ, dist c x ∈ Ioi 0

Tactic:
· rw [← dist_self c]
      exact ContinuousAt.tendsto <| by fun_prop

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ ∀ x ∈ {c}ᶜ, dist c x ∈ Ioi 0
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
X✝ Y✝ : J
f : X✝ ⟶ Y✝
x : (j : J) → ↑(FF.obj j)
hx : x ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (FF.map f)) (u i) = u j}
⊢ (ConcreteCategory.hom
        (((Functor.const J).obj
                { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial }).map
            f ≫
          InducedCategory.homMk ((TopCat.limitCone FF).π.app Y✝)))
      ⟨x, hx⟩ =
    (ConcreteCategory.hom (InducedCategory.homMk ((TopCat.limitCone FF).π.app X✝) ≫ F.map f)) ⟨x, hx⟩

Tactic:
simp only [Functor.const_obj_map]

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
X✝ Y✝ : J
f : X✝ ⟶ Y✝
x : (j : J) → ↑(FF.obj j)
hx : x ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (FF.map f)) (u i) = u j}
⊢ (ConcreteCategory.hom
        (𝟙 { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial } ≫
          InducedCategory.homMk ((TopCat.limitCone FF).π.app Y✝)))
      ⟨x, hx⟩ =
    (ConcreteCategory.hom (InducedCategory.homMk ((TopCat.limitCone FF).π.app X✝) ≫ F.map f)) ⟨x, hx⟩
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ compactlyGenerated X ≤ t

Tactic:
· simp only [compactlyGenerated, ← continuous_iff_coinduced_le, continuous_sigma_iff,
      Sigma.forall]
    exact fun S f ↦ f.2

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
X✝ Y✝ : J
f : X✝ ⟶ Y✝
x : (j : J) → ↑(FF.obj j)
hx : x ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (FF.map f)) (u i) = u j}
⊢ (ConcreteCategory.hom
        (𝟙 { toTop := (TopCat.limitCone FF).pt, is_compact := ⋯, is_hausdorff := ⋯, prop := trivial } ≫
          InducedCategory.homMk ((TopCat.limitCone FF).π.app Y✝)))
      ⟨x, hx⟩ =
    (ConcreteCategory.hom (InducedCategory.homMk ((TopCat.limitCone FF).π.app X✝) ≫ F.map f)) ⟨x, hx⟩

Tactic:
exact (hx f).symm

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
inst✝ : IsTopologicalGroup G
⊢ IsProperMap fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
let Φ : Gᵐᵒᵖ × G ≃ₜ G × G :=
    { toFun := fun gh ↦ (gh.2 * (unop gh.1), gh.2)
      invFun := fun gh ↦ (op (gh.2⁻¹ * gh.1), gh.2)
      left_inv := fun _ ↦ by simp
      right_inv := fun _ ↦ by simp }

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : IsTopologicalGroup G
Φ : Gᵐᵒᵖ × G ≃ₜ G × G :=
  { toFun := fun gh ↦ (gh.2 * unop gh.1, gh.2), invFun := fun gh ↦ (op (gh.2⁻¹ * gh.1), gh.2), left_inv := ⋯,
    right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsProperMap fun gx ↦ (gx.1 • gx.2, gx.2)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ ContinuousSMul (GL (Fin 2) ℝ) ℍ

Tactic:
by
  constructor
  simp only [continuous_induced_rng, Function.comp_def, coe_smul, continuous_iff_continuousAt,
    Prod.forall]
  refine fun g τ ↦ .congr ?_ (f := fun x ↦ (σ g) (num x.1 x.2 / denom x.1 x.2))
    (by filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual)
  fun_prop (disch := apply denom_ne_zero)

Goal state after: