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

Goal state before:
pp: x : ℝ
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ deriv (fun x ↦ (log x)⁻¹) x = -x⁻¹ / log x ^ 2

Tactic:
obtain (⟨_, _, _⟩ | rfl | rfl | rfl) :
      (x ≠ -1 ∧ x ≠ 0 ∧ x ≠ 1) ∨ x = -1 ∨ x = 0 ∨ x = 1 := by tauto

Goal state after:
case inl
x : ℝ
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
left✝¹ : x ≠ -1
left✝ : x ≠ 0
right✝ : x ≠ 1
⊢ deriv (fun x ↦ (log x)⁻¹) x = -x⁻¹ / log x ^ 2

case inr.inl
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ deriv (fun x ↦ (log x)⁻¹) (-1) = -(-1)⁻¹ / log (-1) ^ 2

case inr.inr.inl
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ deriv (fun x ↦ (log x)⁻¹) 0 = -0⁻¹ / log 0 ^ 2

case inr.inr.inr
this✝¹ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) (-1)
this✝ : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 1
this : ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0
⊢ deriv (fun x ↦ (log x)⁻¹) 1 = -1⁻¹ / log 1 ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: x : ℝ
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ deriv (fun x ↦ log (log x)) x = x⁻¹ / log x

Tactic:
obtain (⟨_, _, _⟩ | rfl | rfl | rfl) :
      (x ≠ -1 ∧ x ≠ 0 ∧ x ≠ 1) ∨ x = -1 ∨ x = 0 ∨ x = 1 := by tauto

Goal state after:
case inl
x : ℝ
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
left✝¹ : x ≠ -1
left✝ : x ≠ 0
right✝ : x ≠ 1
⊢ deriv (fun x ↦ log (log x)) x = x⁻¹ / log x

case inr.inl
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ deriv (fun x ↦ log (log x)) (-1) = (-1)⁻¹ / log (-1)

case inr.inr.inl
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ deriv (fun x ↦ log (log x)) 0 = 0⁻¹ / log 0

case inr.inr.inr
this✝¹ : ¬ContinuousAt (fun x ↦ log (log x)) (-1)
this✝ : ¬ContinuousAt (fun x ↦ log (log x)) 0
this : ¬ContinuousAt (fun x ↦ log (log x)) 1
⊢ deriv (fun x ↦ log (log x)) 1 = 1⁻¹ / log 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ x ∈ Set.Ioo (min 0 c) (max 0 c), HasDerivWithinAt (fun c ↦ ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x

Tactic:
refine fun x hx => (hasDerivAt_ofReal_cpow_const' ?_ ?_).hasDerivWithinAt
    · rcases le_total c 0 with (hc | hc)
      · rw [max_eq_left hc] at hx; exact hx.2.ne
      · rw [min_eq_left hc] at hx; exact hx.1.ne'
    · contrapose hr; rw [hr]; ring

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

Goal state before:

Tactic:
∫ x in 0..(π / 2), log (sin x)
    _ = ∫ x in 0..(π / 2), (log (sin (2 * x)) - log 2 - log (cos x)) := by
      apply intervalIntegral.integral_congr_codiscreteWithin
      apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)
      have t₀ : sin ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
        simp
      have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp
      filter_upwards [t₀, t₁] with y h₁y h₂y
      simp_all only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        sin_two_mul, ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, or_self, not_false_eq_true, log_mul]
      ring
    _ = (∫ x in 0..(π / 2), log (sin (2 * x))) - π / 2 * log 2
        - ∫ x in 0..(π / 2), log (cos x) := by
      rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
      · simp
      · simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · apply IntervalIntegrable.sub _ intervalIntegrable_const
        simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left
      · exact intervalIntegrable_log_cos
    _ = (∫ x in 0..(π / 2), log (sin (2 * x)))
        - π / 2 * log 2 - ∫ x in 0..(π / 2), log (sin x) := by
      simp [← sin_pi_div_two_sub,
        intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]
    _ = -log 2 * π / 2 := by
      simp only [intervalIntegral.integral_comp_mul_left (f := fun x ↦ log (sin x)) two_ne_zero,
        mul_zero, (by linarith : 2 * (π / 2) = π),
        integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two, smul_eq_mul, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_mul_cancel_left₀, sub_sub_cancel_left, neg_mul]
      linarith

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

Goal state before:
pp: a b : ℝ
h : 0 ∉ [[a, b]]
h' : ∀ x ∈ [[a, b]], x ≠ 0
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)

Tactic:
rw [integral_deriv_eq_sub' _ deriv_log' (fun x hx => differentiableAt_log (h' x hx))
      (continuousOn_inv₀.mono <| subset_compl_singleton_iff.mpr h),
    log_div (h' b right_mem_uIcc) (h' a left_mem_uIcc)]

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

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

Tactic:
rw [integral_add _root_.intervalIntegrable_const
      (by apply intervalIntegrable_log_sin.const_mul 2), intervalIntegral.integral_const_mul]

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

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ ↑((1 + x ^ 2) ^ s) = ↑(1 + x ^ 2) ^ ↑s

Tactic:
rw [ofReal_cpow, ofReal_add, ofReal_pow, ofReal_one]

Goal state after:
case hx
a b t : ℝ
ht : t ≠ -1
x s : ℝ
⊢ 0 ≤ 1 + x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑((1 + b ^ 2) ^ (t + 1)) / ↑(2 * (t + 1)) - (1 + ↑a ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))

Tactic:
this b (t + 1)

Goal state after:
case e'_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ (1 + ↑b ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) - (1 + ↑a ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case e_a
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
rcases hR.lt_or_gt with h | h

Goal state after:
case e_a.inl
a c : ℂ
R : ℝ
hR : R ≠ 0
h : R < 0
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)

case e_a.inr
a c : ℂ
R : ℝ
hR : R ≠ 0
h : 0 < R
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case e_a.inr
a c : ℂ
R : ℝ
hR : R ≠ 0
h : 0 < R
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
abs_of_pos h

Goal state after:
case e_a.inr
a c : ℂ
R : ℝ
hR : R ≠ 0
h : 0 < R
⊢ log⁺ (R⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ l.BoundedAtFilter (f * g)

Tactic:
refine (hf.mul hg).trans ?_
  convert! Asymptotics.isBigO_refl (E := ℝ) _ l
  simp

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

Goal state before:
pp: h : ℝ
hh : 0 < h
⊢ Tendsto (fun x ↦ -h / (2 * π) * Real.log ‖x‖) (𝓝[≠] 0) atTop

Tactic:
apply Tendsto.const_mul_atBot_of_neg (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) (by positivity))

Goal state after:
h : ℝ
hh : 0 < h
⊢ Tendsto (fun x ↦ Real.log ‖x‖) (𝓝[≠] 0) atBot
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case pos
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}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : z ≠ z₀
⊢ g z = g z₀

Tactic:
replace h' : ‖z - z₀‖ ≠ 0 := by simpa only [Ne, norm_eq_zero, sub_eq_zero]

Goal state after:
case pos
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}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
⊢ g z = g z₀
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: case h
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ 𝕢 h z ≠ 0

Tactic:
exact exp_ne_zero _

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

Goal state before:
pp: case pos
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}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ t ∈ ball 0 r, gray w t = g z₀
h4 : ↑‖z - z₀‖ ∈ ball 0 r
⊢ g z = g z₀

Tactic:
simpa only [ray, gray, w, smul_smul, mul_inv_cancel₀ h', one_smul, add_sub_cancel,
      Function.comp_apply, coe_smul] using! h3 (↑‖z - z₀‖) h4

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
⊢ ∀ᶠ (q : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) q

Tactic:
refine ((invQParam_tendsto hh).eventually h_hol).mp ?_
  refine eventually_nhdsWithin_of_forall (fun q hq h_diff ↦ ?_)
  rw [← qParam_right_inv hh.ne' hq]
  exact differentiableAt_cuspFunction hh.ne' hf h_diff

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

Goal state before:
pp: n : ℕ
H : ∀ x ∈ Set.Icc 0 π, sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h ↦ pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
refine integral_mono_on pi_pos.le ?_ ?_ H

Goal state after:
case refine_1
n : ℕ
H : ∀ x ∈ Set.Icc 0 π, sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h ↦ pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ IntervalIntegrable (fun x ↦ sin x ^ (n + 1)) MeasureTheory.volume 0 π

case refine_2
n : ℕ
H : ∀ x ∈ Set.Icc 0 π, sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h ↦ pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ IntervalIntegrable (fun x ↦ sin x ^ n) MeasureTheory.volume 0 π
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case pos
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

pp: case neg
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

Tactic:
· simp [derivRootWeight, hPz, hP₀]

Goal state after:
case neg
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
have hz' : z - c ∈ Metric.eball 0 r' := by
    rw [Metric.eball_coe]
    simpa only [mem_ball_iff_norm, sub_zero] using hzr'

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ Metric.eball 0 ↑r'
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < r
⊢ DifferentiableOn ℂ f (Metric.ball c ↑r')

Tactic:
← Metric.eball_coe

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < r
⊢ DifferentiableOn ℂ f (Metric.eball c ↑r')
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

Tactic:
by
  simp [pow_mul, sin_sq, cos_sq, ← sub_sub]
  field_simp
  norm_num

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

Goal state before:
pp: ⊢ I.sqrt = ↑√2⁻¹ * (1 + I)

Tactic:
by
  rw [sqrt, ← re_add_im (I ^ 2⁻¹), cpow_inv_two_im_eq_sqrt (by simp), cpow_inv_two_re]
  simp [mul_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
u : Rˣ
⊢ mk ((GeneralLinearGroup.scalar n) u) = 1

Tactic:
rw [← MonoidHom.mem_ker, ker_mk, GeneralLinearGroup.center_eq_range_scalar]

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
u : Rˣ
⊢ (GeneralLinearGroup.scalar n) u ∈ (GeneralLinearGroup.scalar n).range
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: 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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : f x ≤ -‖f‖ / 3
⊢ |-‖f‖ / 3 - f x| = -‖f‖ / 3 - f x

Tactic:
abs_of_nonneg (sub_nonneg.2 hle₁)

Goal state after:
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
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : f x ≤ -‖f‖ / 3
⊢ -‖f‖ / 3 - f x = -‖f‖ / 3 - f x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) (num g z / denom g z)).im =
    |↑(GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g z)

Tactic:
abs_of_pos h

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) (num g z / denom g z)).im =
    ↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ m.IsParabolic ↔ ∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0

Tactic:
constructor
  · exact fun hm ↦ ⟨_, _, (add_sub_cancel ..).symm, sub_ne_zero.mpr fun h ↦ hm.1 ⟨_, h.symm⟩,
      hm.sub_eigenvalue_sq_eq_zero⟩
  · rintro ⟨a, n, hm, hn0, hnsq⟩
    constructor
    · refine fun ⟨b, hb⟩ ↦ hn0 ?_
      rw [← sub_eq_iff_eq_add'] at hm
      simpa only [← hm, ← hb, ← map_sub, ← map_pow, ← map_zero (scalar (Fin 2)), scalar_inj,
        sq_eq_zero_iff] using hnsq
    · suffices scalar (Fin 2) (m.discr / 4) = 0 by
        rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
        have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
        tauto
      rw [← sub_scalar_sq_eq_discr, hm, trace_add, scalar_apply, trace_diagonal]
      simp [mul_div_cancel_left₀ _ (NeZero.ne (2 : K)),
        (Matrix.isNilpotent_trace_of_isNilpotent ⟨2, hnsq⟩).eq_zero, hnsq]

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

Goal state before:
pp: ⊢ FaithfulSMul PGL(2, ℝ) ℍ

Tactic:
rw [faithfulSMul_iff]

Goal state after:
⊢ ∀ (g : PGL(2, ℝ)), (∀ (a : ℍ), g • a = a) → g = 1
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℍ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z) =
    |↑(GeneralLinearGroup.det g)| * (↑z).im / Complex.normSq (denom g ↑z)

Tactic:
abs_of_pos h

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℍ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z) =
    ↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: 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)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
⊢ Tendsto (fun t ↦ (2 / 3) ^ t * ‖f‖) atTop (𝓝 (0 * ‖f‖))

Tactic:
refine (tendsto_pow_atTop_nhds_zero_of_lt_one ?_ ?_).mul tendsto_const_nhds <;> norm_num1

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

Goal state before:
pp: ⊢ σ J = Complex.conjCAE

Tactic:
simp [σ, J]

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

Goal state before:
pp: n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑ofComplex) z

Tactic:
contMDiffAt_iff

Goal state after:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z ∧
    ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
      (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ sinh 0 ≤ sinh (arsinh x) ↔ 0 ≤ x

Tactic:
sinh_zero,

Goal state after:
x : ℝ
⊢ 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ sinh (arsinh x) ≤ sinh 0 ↔ x ≤ 0

Tactic:
sinh_zero,

Goal state after:
x : ℝ
⊢ sinh (arsinh x) ≤ 0 ↔ x ≤ 0
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
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion x R (inversion x R x) = x

Tactic:
rw [inversion_self, inversion_self]

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

Goal state before:
pp: x : ℂ
⊢ HasStrictDerivAt sinh (cosh x) x

Tactic:
simp only [cosh, div_eq_mul_inv]
  convert!
    ((hasStrictDerivAt_exp x).sub (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
  rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < deriv cosh x

Tactic:
mem_Ioi

Goal state after:
x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv cosh x

Tactic:
rw [interior_Ici, mem_Ioi] at hx

Goal state after:
x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case refine_2
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < deriv (fun x ↦ sinh x - x) x

Tactic:
mem_Ioi

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x ↦ sinh x - x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case refine_2
x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv (fun x ↦ sinh x - x) x

Tactic:
rw [interior_Ici, mem_Ioi] at hx

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x ↦ sinh x - x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x✝ : ℂ
⊢ (sinh / cosh) x✝ = tanh x✝

Tactic:
Pi.div_apply,

Goal state after:
x✝ : ℂ
⊢ sinh x✝ / cosh x✝ = tanh x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x✝ : ℝ
⊢ (sinh / cosh) x✝ = tanh x✝

Tactic:
Pi.div_apply,

Goal state after:
x✝ : ℝ
⊢ sinh x✝ / cosh x✝ = tanh x✝