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

Goal state before:
pp: case mp
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = 1 ∧ f (↑l + x * (↑u - ↑l)) = e) → ∃ x, x.re = u ∧ f x = e

Tactic:
intro h

Goal state after:
case mp
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ x, x.re = 1 ∧ f (↑l + x * (↑u - ↑l)) = e
⊢ ∃ x, x.re = u ∧ f x = e
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = u ∧ f x = e) → ∃ x, x.re = 1 ∧ f (↑l + x * (↑u - ↑l)) = e

Tactic:
intro h

Goal state after:
case mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ x, x.re = u ∧ f x = e
⊢ ∃ x, x.re = 1 ∧ f (↑l + x * (↑u - ↑l)) = e
Module: Mathlib.Analysis.Distribution.DerivNotation

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

Tactic:
induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_smul]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: case mp
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt (⇑l ∘ f) x → HarmonicAt f x

Tactic:
intro h

Goal state after:
case mp
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
h : HarmonicAt (⇑l ∘ f) x
⊢ HarmonicAt f x
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: case mpr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt f x → HarmonicAt (⇑l ∘ f) x

Tactic:
intro h

Goal state after:
case mpr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
h : HarmonicAt f x
⊢ HarmonicAt (⇑l ∘ f) x
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

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

Tactic:
by
  rcases le_or_gt a b with h | h
  · rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, integral_of_le h]
  · rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]

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

Goal state before:

Tactic:
(circleAverage (fun ζ ↦ herglotzRieszKernel 0 w ζ • (g ζ : ℂ)) 0 R).re
      = circleAverage (Complex.reCLM ∘ fun ζ ↦ herglotzRieszKernel 0 w ζ • (g ζ : ℂ)) 0 R :=
        (Complex.reCLM.circleAverage_comp_comm h₂).symm
    _ = circleAverage ((Complex.re ∘ herglotzRieszKernel 0 w) • g) 0 R := by
        simp [Function.comp_def, Complex.mul_re, Pi.mul_def]

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

Goal state before:
pp: case mp
x : ℝ
⊢ DifferentiableAt ℝ (fun x ↦ -x * log x) x → x ≠ 0

Tactic:
intro h

Goal state after:
case mp
x : ℝ
h : DifferentiableAt ℝ (fun x ↦ -x * log x) x
⊢ x ≠ 0
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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 : 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
⊢ ‖g z‖ ≤ C

Tactic:
replace hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re} :=
    (differentiable_id.const_mul _).cexp.diffContOnCl.smul hd

Goal state after:
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}
⊢ ‖g z‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: ⊢ (fun x ↦ log (sin x)) =ᶠ[codiscreteWithin (Ι 0 (π / 2))] fun x ↦ log (sin (2 * x)) - log 2 - log (cos x)

Tactic:
apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)

Goal state after:
⊢ {x | (fun x ↦ (fun x ↦ log (sin x)) x = (fun x ↦ log (sin (2 * x)) - log 2 - log (cos x)) x) x} ∈
    codiscreteWithin Set.univ
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (↑t * Complex.I) = 2 * ↑r * ↑(sinc r)

Tactic:
integral_exp_mul_I_eq_sin

Goal state after:
r : ℝ
⊢ 2 * ↑(sin r) = 2 * ↑r * ↑(sinc r)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x = sin b - sin a

Tactic:
by
  rw [integral_deriv_eq_sub']
  · simp
  · simp only [differentiableAt_sin, implies_true]
  · exact continuousOn_cos

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

Goal state before:
pp: case hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (fun x ↦ 2⁻¹ * log ‖f x‖) c R

pp: case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (fun x ↦ 2⁻¹ * |log ‖f x‖|) c R

Tactic:
· apply hf.circleIntegrable_log_norm.const_mul

Goal state after:
case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (fun x ↦ 2⁻¹ * |log ‖f x‖|) c R
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ 2 * sin x ^ n =
    C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2)

Tactic:
by
        simp [cos_sq', sub_mul, ← pow_add, add_comm]

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

Goal state before:
pp: a : ℂ
⊢ a.sqrt = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I

Tactic:
sqrt

Goal state after:
a : ℂ
⊢ a ^ 2⁻¹ = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ (-↑α).sqrt = I * ↑√α

Tactic:
rw [← re_add_im (-(α : ℂ)).sqrt]

Goal state after:
α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ ↑(-↑α).sqrt.re + ↑(-↑α).sqrt.im * I = I * ↑√α
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
inst✝ : Nonempty n
⊢ Function.Surjective ⇑toPGL ↔ ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r

Tactic:
refine ⟨fun h r ↦ ?_, ProjectiveSpecialLinearGroup.toPGL_surj_of_roots⟩

Goal state after:
n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Nonempty n
h : Function.Surjective ⇑toPGL
r : Rˣ
⊢ ∃ k, k ^ Fintype.card n = r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0|

Tactic:
gl_smul_eq_self_iff_dist_sq_eq h htrace hc,

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2 ↔
    dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0|
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case inr
g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g).det
hell : g.IsElliptic
this : ∀ {g : GL (Fin 2) ℝ}, 0 < (↑g).det → ∀ (hell : g.IsElliptic), 0 < ↑g 1 0 → (g • z = z ↔ z = fixedPt g hell)
hc : ¬0 < ↑g 1 0
⊢ g • z = z ↔ z = fixedPt g hell

Tactic:
replace hc := hell.c_ne_zero.lt_or_gt.resolve_right hc
    simpa using @this (-g) (by simpa [Matrix.det_neg]) hell.neg (by simpa)

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

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ ¬↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))

Tactic:
intro h

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
h : ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))
⊢ False
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ (trace ℝ ℂ) z = 2 * z.re

Tactic:
by
  rw [Algebra.trace_eq_matrix_trace Complex.basisOneI, Algebra.leftMulMatrix_complex,
    Matrix.trace_fin_two]
  exact (two_mul _).symm

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

Goal state before:
pp: a b : SL(2, ℤ)
i j : Fin 2
h : ∀ (i j : Fin 2), ↑↑(coe a) i j = ↑↑(coe b) i j
⊢ ↑a i j = ↑b i j

Tactic:
simpa [coe] using h i j

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

Goal state before:
pp: case refine_2
⊢ ∀ (x : ℍ), NNReal.mk x.im ⋯ ≠ 0

Tactic:
exact fun x ↦ NNReal.ne_iff.mp x.im_ne_zero

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

Goal state before:
pp: case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
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 = l✝ + 1
k : m
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
let f' := f.polyToMatrix

Goal state after:
case succ
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
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 = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
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 = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (-f (M k k)).charmatrix.det ∈ nonZeroDivisors R[X]

Tactic:
← charpoly

Goal state after:
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
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 = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (-f (M k k)).charpoly ∈ nonZeroDivisors R[X]
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
let ⟨ιA, bA⟩ := Module.Free.exists_basis (R := S) (M := A)

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist z w ≤ dist ↑z ↑w / √(z.im * w.im)

Tactic:
by
  rw [dist_le_iff_le_sinh, ← div_mul_eq_div_div_swap, self_le_sinh_iff]
  positivity

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

Goal state before:
pp: z w : ℍ
⊢ dist { coe := { re := 0, im := z.im }, coe_im_pos := ⋯ } { coe := { re := 0, im := w.im }, coe_im_pos := ⋯ } ≤
    dist z w

Tactic:
dist_eq

Goal state after:
z w : ℍ
⊢ 2 *
      arsinh
        (dist { re := 0, im := z.im } { re := 0, im := w.im } /
          (2 *
            √({ coe := { re := 0, im := z.im }, coe_im_pos := ⋯ }.im *
                { coe := { re := 0, im := w.im }, coe_im_pos := ⋯ }.im))) ≤
    2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s ↦ {u | s ∈ u}) → i ∈ ↑u) → ∀ s ∈ x, {v | s ∈ v} ∈ u

Tactic:
intro h

Goal state after:
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s ↦ {u | s ∈ u}) → i ∈ ↑u
⊢ ∀ s ∈ x, {v | s ∈ v} ∈ u
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case pos
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
h : R = 0
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|

Tactic:
simp [h, characteristic_sub_characteristic_inv_at_zero hf]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
⊢ locallyFinsupp E ℤ →+ locallyFinsuppWithin (closedBall 0 |r|) ℤ

Tactic:
apply restrictMonoidHom

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
⊢ closedBall 0 |r| ⊆ univ
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l ↔
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
refine ⟨fun h x xs y ys _ => h xs ys, fun h x xs y ys => ?_⟩

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: case e_a
f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
β : ℝ
⊢ β ∈ uIcc 0 (2 * π) → (fun x ↦ (2 * π)⁻¹ * ∫ (α : ℝ) in 0..2 * π, F α x) β = (fun x ↦ log⁺ ‖f (circleMap 0 R x)‖) β

Tactic:
hβ

Goal state after:
case e_a
f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
β : ℝ
hβ : β ∈ uIcc 0 (2 * π)
⊢ (fun x ↦ (2 * π)⁻¹ * ∫ (α : ℝ) in 0..2 * π, F α x) β = (fun x ↦ log⁺ ‖f (circleMap 0 R x)‖) β
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
⊢ (convexHull ℝ) (connectedComponentIn (s ∪ t) x) = univ

Tactic:
rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h] <;>
  rw [← Set.univ_subset_iff, ← hx] <;>
  apply convexHull_mono

Goal state after:
case inl
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : (convexHull ℝ) (connectedComponentIn s x) = univ
⊢ connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x

case inr
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : (convexHull ℝ) (connectedComponentIn t x) = univ
⊢ connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l ↔
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)

Tactic:
constructor
  · rintro h; refine ⟨h.hasLocallyBoundedVariationOn, fun x xs y ys => ?_⟩
    rw [hasConstantSpeedOnWith_iff_ordered] at h
    rcases le_total x y with (xy | yx)
    · rw [variationOnFromTo.eq_of_le f s xy, h xs ys xy]
      exact ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr xy))
    · rw [variationOnFromTo.eq_of_ge f s yx, h ys xs yx]
      have := ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr yx))
      simp_all only [NNReal.val_eq_coe]; ring
  · rw [hasConstantSpeedOnWith_iff_ordered]
    rintro h x xs y ys xy
    rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
⊢ ∃ b_1, b ≤ b_1 ∧ 1 < a * |logCounting D b_1|

Tactic:
have h₁ℓ : c ≤ ℓ := by grind

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
⊢ ∃ b_1, b ≤ b_1 ∧ 1 < a * |logCounting D b_1|
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ StrictMonoOn (logCounting (single e 1) + logCounting (D - single e 1)) (Ioi ‖e‖)

Tactic:
apply StrictMonoOn.add_monotone

Goal state after:
case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ StrictMonoOn (logCounting (single e 1)) (Ioi ‖e‖)

case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ MonotoneOn (logCounting (D - single e 1)) (Ioi ‖e‖)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ ↑((divisor f univ) 0) * log R = ↑((divisor f (closedBall 0 |R|)) 0) * log R

Tactic:
rw [divisor_apply, divisor_apply]

Goal state after:
case e_a.hf
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ MeromorphicOn f (closedBall 0 |R|)

case e_a.hz
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ 0 ∈ closedBall 0 |R|

case e_a.hf
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ MeromorphicOn f univ

case e_a.hz
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ 0 ∈ univ
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
yz : y ≤ z
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
← Set.Icc_union_Icc_eq_Icc xy yz

Goal state after:
case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
yz : y ≤ z
⊢ HasConstantSpeedOnWith f (Icc x y ∪ Icc y z) l
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c
hl : Triplewise p' (map f l)
⊢ Triplewise p l

Tactic:
rw [triplewise_map] at hl
  exact hl.imp h

Goal state after:
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
h : (Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]

Tactic:
rcases h with ⟨⟨hp, ht⟩, hpne⟩

Goal state after:
case cons.refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]