mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Laplacian

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h : f₁ =ᶠ[𝓝[s] x] f₂
hs : UniqueDiffOn ℝ s
⊢ Δ[s] f₁ =ᶠ[𝓝[s] x] Δ[s] f₂

Tactic:
filter_upwards [EventuallyEq.iteratedFDerivWithin (𝕜 := ℝ) h 2,
    eventually_mem_nhdsWithin] with x h₁x h₂x

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x✝ : E
s : Set E
h : f₁ =ᶠ[𝓝[s] x✝] f₂
hs : UniqueDiffOn ℝ s
x : E
h₁x : iteratedFDerivWithin ℝ 2 f₁ s x = iteratedFDerivWithin ℝ 2 f₂ s x
h₂x : x ∈ s
⊢ (Δ[s] f₁) x = (Δ[s] f₂) x
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
· rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, integral_of_le h]

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ circleAverage f₁ c R ≤ circleAverage f₂ c R

Tactic:
by
  apply (mul_le_mul_iff_of_pos_left (by simp [pi_pos])).2
  apply intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf₁ hf₂
  exact fun x _ ↦ by simp [h (circleMap c R x)]

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
x✝¹ : ℂ
x✝ : x✝¹ ∈ sphere c |R|
⊢ (poissonKernel c w • f) x✝¹ = (re ∘ herglotzRieszKernel c w • f) x✝¹

Tactic:
← poissonKernel_eq_re_herglotzRieszKernel

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
x✝¹ : ℂ
x✝ : x✝¹ ∈ sphere c |R|
⊢ (poissonKernel c w • f) x✝¹ = (re ∘ herglotzRieszKernel c w • f) x✝¹

Tactic:
← poissonKernel_eq_re_herglotzRieszKernel

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

Goal state before:
pp: case mp
x : ℝ
h : DifferentiableAt ℝ (fun x ↦ -x * log x) x
eq0 : x = 0
⊢ False

Tactic:
simp only [neg_mul, differentiableAt_fun_neg_iff, eq0] at h

Goal state after:
case mp
x : ℝ
eq0 : x = 0
h : DifferentiableAt ℝ (fun y ↦ y * log y) 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case inr
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x.negMulLog ≤ 1 - x

Tactic:
exact le_of_lt (negMulLog_lt_one_sub_self h0 h1)

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

Goal state before:
pp: case inl
x : ℝ
hx : x < 0
⊢ sin x / x ≤ |x|⁻¹

pp: case inr.inl
⊢ sin 0 / 0 ≤ |0|⁻¹

pp: case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x / x ≤ |x|⁻¹

Tactic:
· rw [abs_of_nonpos hx.le, ← one_div, le_div_iff₀, div_eq_mul_inv]
    · ring_nf
      rw [mul_assoc, mul_inv_cancel₀ hx.ne, mul_one, neg_le]
      exact neg_one_le_sin x
    · simpa using hx

Goal state after:
case inr.inl
⊢ sin 0 / 0 ≤ |0|⁻¹

case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x / x ≤ |x|⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case refine_2
s t : ℝ
ht : 0 < t
h : -1 < s
⊢ IntervalIntegrable (fun x ↦ x ^ s) volume 0 t

Tactic:
apply intervalIntegrable_rpow' h (a := 0) (b := t)

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
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 : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
this : ‖f 0‖ = ‖f ↑x₀‖
⊢ ∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C

Tactic:
refine (h.not_ge <| this ▸ ?_).elim

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
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 : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
this : ‖f 0‖ = ‖f ↑x₀‖
⊢ ‖f 0‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv.refine_1.inr
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0

Tactic:
exact hx.1.ne'

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

Goal state before:
pp: ⊢ IntervalIntegrable (fun x ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)

Tactic:
apply IntervalIntegrable.sub _ intervalIntegrable_const
        simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left

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

Goal state before:
pp: a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ≤ 0

Tactic:
rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx

Goal state after:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ Set.Icc (b - a) 0
⊢ x ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
by
  calc circleAverage (log ‖· - a‖) 0 1
  _ = circleAverage (log ‖1 - ·⁻¹ * a‖) 0 1 := by
    apply circleAverage_congr_sphere
    intro z hz
    simp_all only [abs_one, mem_sphere_iff_norm, sub_zero]
    congr 1
    have : z ≠ 0 := fun h ↦ by simp [h] at hz
    calc ‖z - a‖
    _ = ‖z⁻¹ * (z - a)‖ := by simp [hz]
    _ = ‖1 - z⁻¹ * a‖ := by field_simp
  _ = 0 := by
    rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖),
      InnerProductSpace.HarmonicOnNhd.circleAverage_eq, zero_mul, sub_zero,
      CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one]
    intro x hx
    have : ‖x * a‖ < 1 := by
      calc ‖x * a‖
      _ = ‖x‖ * ‖a‖ := by simp
      _ ≤ ‖a‖ := mul_le_of_le_one_left (norm_nonneg _) (by aesop)
      _ < 1 := h
    apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
    rw [sub_ne_zero]
    by_contra! hCon
    rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this

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

Goal state before:
pp: b : ℝ
h : b < 0
| fun s ↦ log s

Tactic:
intro t

Goal state after:
b : ℝ
h : b < 0
t : ℝ
| log t
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

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

Tactic:
congr 1
    rcases hR.lt_or_gt with h | h
    · simp [abs_of_neg h]
    · rw [abs_of_pos h]

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

Tactic:
have h8 : IsPreconnected (ball z₀ r) := (convex_ball z₀ r).isPreconnected

Goal state after:
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)
⊢ False
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
⊢ HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z

Tactic:
simpa only [id_eq, mul_one] using! (((hasStrictDerivAt_id z).const_mul _).div_const _).cexp

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

Goal state before:
pp: x✝ : ℝ
h : -(π / 2) < x✝ ∧ x✝ ≤ π / 2
⊢ √(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2

Tactic:
← Real.cos_eq_sqrt_one_sub_sin_sq (le_of_lt h.1) h.2,

Goal state after:
x✝ : ℝ
h : -(π / 2) < x✝ ∧ x✝ ≤ π / 2
⊢ cos x✝ * cos x✝ = cos x✝ ^ 2
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ Complex.I * ((complexRingEquiv h) a).sqrt = (complexRingEquiv h) (I * sqrt a)

Tactic:
simp [h, sqrt, map_mul]

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

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ denom (g * h) z = denom g (num h z / denom h z) * denom h z

Tactic:
change _ = (_ * (_ / _) + _) * _

Goal state after:
g h : GL (Fin 2) ℝ
z : ℂ
hz : z.im ≠ 0
⊢ denom (g * h) z = (↑(↑g 1 0) * (num h z / denom h z) + ↑(↑g 1 1)) * denom h z
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z w : ℍ
g : GL (Fin 2) ℝ
hell : g.IsElliptic
⊢ 0 < ((↑(↑g 0 0) - ↑(↑g 1 1)) / (2 * ↑(↑g 1 0)) + Complex.I * (↑√(-(↑g).discr) / (2 * ↑|↑g 1 0|))).im

Tactic:
simpa [div_pos, Complex.div_re, Complex.div_im, hell.c_ne_zero]

Goal state after:
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)
n : ℕ
⊢ dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖

Tactic:
induction n with
    | zero => simp [g0]
    | succ n ihn =>
      rw [g_succ n, add_compContinuous, ← dist_sub_right, add_sub_cancel_left, pow_succ', mul_assoc]
      refine (hF_dist _).trans (mul_le_mul_of_nonneg_left ?_ (by norm_num1))
      rwa [← dist_eq_norm']

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

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖↑τ‖ ∧ r - ‖↑τ‖ < ε
hr' : r < 0
⊢ False

Tactic:
have : ‖(τ : ℂ)‖ < ε := by linarith

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖↑τ‖ ∧ r - ‖↑τ‖ < ε
hr' : r < 0
this : ‖↑τ‖ < ε
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
⊢ (g • z).im = z.im / Complex.normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)

Tactic:
by
  simpa using z.im_smul_eq_div_normSq g

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

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k i j : m
lt : (fun x ↦ x ≠ k) j < (fun x ↦ x ≠ k) i
⊢ auxMat M k i j = 0

Tactic:
simp_rw [lt_iff_not_ge, le_Prop_eq, Classical.not_imp, not_not] at lt
    rw [auxMat, of_apply, if_pos lt.2, if_neg lt.1]

Goal state after:
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 →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
cases isEmpty_or_nonempty X

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : IsEmpty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : Nonempty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
rw [norm_eq_one_of_not_module_finite h]

Goal state after:
case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z x✝ : ℂ
hg : 0 < (↑g).det
⊢ (smulFDeriv (J * g) z) x✝ = (-↑Complex.conjCLE ∘SL smulFDeriv g z) x✝

Tactic:
simp [smulFDeriv, σ, hg, hg.not_gt, neg_div]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (smulFDeriv g z).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4

Tactic:
by
  simp only [smulFDeriv, σ]
  rcases g.det_ne_zero.lt_or_gt with h | h
  · simp [h.not_gt, ContinuousLinearMap.det, LinearMap.det_restrictScalars,
      Algebra.norm_complex_eq, Complex.normSq_eq_norm_sq, ← pow_mul, sign_neg h, neg_div]
  · simp [ContinuousLinearMap.det, h, LinearMap.det_restrictScalars,
      Algebra.norm_complex_eq, Complex.normSq_eq_norm_sq, ← pow_mul]

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

Goal state before:
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 : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ (R / dist (inversion c R x) c) ^ 2 • (inversion c R x -ᵥ c) +ᵥ c = x

Tactic:
dist_inversion_center,

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 : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ (R / (R ^ 2 / dist x c)) ^ 2 • (inversion c R x -ᵥ c) +ᵥ c = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ logDeriv cosh = tanh

Tactic:
by
  ext
  rw [logDeriv, Complex.deriv_cosh, Pi.div_apply, Complex.tanh]

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✝ : ProperSMul G X
⊢ T2Space (Quotient (MulAction.orbitRel G X))

Tactic:
rw [t2_iff_isClosed_diagonal]

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✝ : ProperSMul G X
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient (MulAction.orbitRel G X)))
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
⊢ T2Space X

Tactic:
rw [t2_iff_isClosed_diagonal]

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
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x ↦ ↑(f x)) (comap some (𝓝 ∞)) (𝓝 (OnePoint.map f ∞)) ∧
      Continuous[inst✝¹, instTopologicalSpace] fun x ↦ ↑(f x)) ↔
    Continuous[inst✝¹, inst✝] f ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)

Tactic:
map_infty,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x ↦ ↑(f x)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧ Continuous[inst✝¹, instTopologicalSpace] fun x ↦ ↑(f x)) ↔
    Continuous[inst✝¹, inst✝] f ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
suffices ∀ (g : SL(2, ℝ)) (τ : ℍ),
        ContinuousAt (fun ⟨h, z⟩ ↦ (h 0 0 * (z : ℂ) + h 0 1) / (h 1 0 * z + h 1 1)) (g, τ) by
      simpa [continuous_induced_rng, continuous_iff_continuousAt, Function.comp_def,
        coe_specialLinearGroup_apply]
    intro g τ
    fun_prop (disch := exact denom_ne_zero g τ)

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, |(fun x ↦ log⁺ ‖f x‖) - fun x ↦ log⁺ ‖f x - a₀‖| x ≤ log⁺ ‖a₀‖ + log 2

Tactic:
intro θ hθ
    simp only [Pi.abs_apply, Pi.sub_apply]
    by_cases h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
    · simpa [abs_of_nonneg h, sub_le_iff_le_add, add_comm (log⁺ ‖a₀‖ + log 2), ← add_assoc]
        using (posLog_norm_add_le (f θ - a₀) a₀)
    · simp only [abs_of_nonpos (le_of_not_ge h), neg_sub, tsub_le_iff_right,
        add_comm (log⁺ ‖a₀‖ + log 2), ← add_assoc]
      convert! posLog_norm_add_le (-f θ) a₀ using 2
      · rw [← norm_neg]
        abel_nf
      · simp

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
a : α
l : List α
p : α → α → α → Prop
⊢ Triplewise p (a :: l) ↔ Pairwise (p a) l ∧ Triplewise p l

Tactic:
grind [triplewise_iff]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ : ℝ
hm : 0 ∈ φ '' Icc 0 s
⊢ φ 0 = 0

Tactic:
obtain ⟨x, xs, hx⟩ := hm

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
⊢ φ 0 = 0
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha :
  (image (fun z ↦ ↑z) s').Nonempty →
    image (fun z ↦ ↑z) s' ≠ univ → #(image (fun z ↦ ↑z) s') < #((image (fun z ↦ ↑z) s').biUnion t)
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)

Tactic:
rw [image_nonempty, Finset.card_image_of_injective s' Subtype.coe_injective] at ha

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
l : List R
h : l.SortedLE
i j k : ℕ
hij : i < j
hjk : j < k
⊢ ∀ (hk : k < l.length), Wbtw R l[i] l[j] l[k]

Tactic:
hk

Goal state after:
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
l : List R
h : l.SortedLE
i j k : ℕ
hij : i < j
hjk : j < k
hk : k < l.length
⊢ Wbtw R l[i] l[j] l[k]
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
hl : l ≠ []
x✝ : ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ List.Wbtw R l

pp: case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
hl : l ≠ []
h : List.Wbtw R l
⊢ ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l

Tactic:
· rw [← hl'l]
    exact Wbtw.map hl's.wbtw _

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
hl : l ≠ []
h : List.Wbtw R l
⊢ ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : List.Wbtw R (head :: tail)
ht : tail = []
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail

Tactic:
refine ⟨[0], ?_⟩

Goal state after:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : List.Wbtw R (head :: tail)
ht : tail = []
⊢ (∀ a ∈ [0], 0 ≤ a) ∧
    [0].SortedLE ∧ map ⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl)) [0] = head :: tail