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

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
        ↑(ENat.map Nat.cast 0).untop₀ * Real.log R +
      Real.log ‖f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖

Tactic:
simp

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

Goal state before:
pp: ⊢ 0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ 0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: ⊢ 0 ≤ I.im

Tactic:
simp

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

Goal state before:
pp: ⊢ (-I).im < 0

Tactic:
simp

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

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

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

Goal state after:
⊢ ↑√((‖-I‖ + (-I).re) / 2) + ↑(-√((‖-I‖ - (-I).re) / 2)) * I = ↑√2⁻¹ * (1 - I)
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: case refine_2
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := ⋯
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
x : ↑(Metric.closedBall 0 1)
⊢ ↑(({ toFun := codRestrict ((Metric.closedBall 0 1).piecewise id g) (Metric.closedBall 0 1) ⋯,
              continuous_toFun := ⋯ }.comp
          { toFun := Subtype.val, continuous_toFun := ⋯ })
        x) =
    ↑((ContinuousMap.id ↑(Metric.closedBall 0 1)) x)

Tactic:
simp

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

Goal state before:
pp: case refine_1
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
x : E
hx : ‖x‖ = 1
⊢ id x = g x

Tactic:
simp [g, hx]

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

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u = c
⊢ c ∈ closedBall c |R|

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed[inst✝²] s
Y : Type v
inst✝ : TopologicalSpace Y
f : C(↑s, Y)
t : Set Y
hf : ∀ (x : ↑s), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : restrict s g = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
⊢ ∀ (x : X), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp g) x ∈ t

Tactic:
simp

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

Goal state before:
pp: case pos
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u = c
⊢ ↑(ENat.map Nat.cast 0).untop₀ * Real.log (R / r) ≤ ↑(ENat.map Nat.cast 0).untop₀ * Real.log (R * ‖c - c‖⁻¹)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝³ : TopologicalSpace X₁
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst✝ : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
⊢ ∀ (x : X), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp g) x ∈ t

Tactic:
simp

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

Goal state before:
pp: case ha
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
⊢ 0 ≤ ↑(ENat.map Nat.cast (analyticOrderAt f u)).untop₀

Tactic:
simp

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ˣ
⊢ (GeneralLinearGroup.scalar n) u ∈ (GeneralLinearGroup.scalar n).range

Tactic:
simp

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

Goal state before:
pp: case h
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
hR : ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r
g : GL n R
r : Rˣ
hr : (↑r • ↑g).det = 1
⊢ toPGL ↑⟨↑r • ↑g, hr⟩ = mk g

Tactic:
simp only [ProjectiveSpecialLinearGroup.toPGL_mk, mk_eq_mk_iff]

Goal state after:
case h
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
hR : ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r
g : GL n R
r : Rˣ
hr : (↑r • ↑g).det = 1
⊢ ∃ u, toGL ⟨↑r • ↑g, hr⟩ * (GeneralLinearGroup.scalar n) u = g
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: Y : Type v
Z : Type w
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TietzeExtension Z
e : Y ≃ₜ Z
⊢ (↑e.symm).comp ↑e = ContinuousMap.id Y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ∃ g, ‖g‖ ≤ ‖0‖ / 3 ∧ dist (g.compContinuous e) 0 ≤ 2 / 3 * ‖0‖

Tactic:
simp

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

Goal state before:
pp: case mk
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
S : Type u_4
T : Type u_5
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g✝ : S →+* T
g : GL n R
⊢ (map (g✝.comp f)) (mk g) = ((map g✝).comp (map f)) (mk g)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ A.charpoly.degree = 2

Tactic:
simp

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ ↑(Fintype.card n) = 2
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((starRingEnd ℂ) z) = (starRingEnd ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z)

Tactic:
simp

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

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE ((starRingEnd ℂ) z) = (starRingEnd ℂ) (Complex.conjCAE z)

Tactic:
simp

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

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
y : ℝ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ↑y = ↑y

Tactic:
simp

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

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
y : ℝ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE ↑y = ↑y

Tactic:
simp

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

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z) = z

Tactic:
simp

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

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE (Complex.conjCAE z) = z

Tactic:
simp

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

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) z).im ≠ 0 ↔ z.im ≠ 0

Tactic:
simp

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

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ (Complex.conjCAE z).im ≠ 0 ↔ z.im ≠ 0

Tactic:
simp

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsReduced R
a : R
hm : (scalar (Fin 2)) a 1 0 = 0
aux : ((scalar (Fin 2)) a).discr = 0 ↔ (scalar (Fin 2)) a 0 0 = (scalar (Fin 2)) a 1 1
h : (scalar (Fin 2)) a 0 0 = (scalar (Fin 2)) a 1 1
⊢ (scalar (Fin 2)) a 0 1 = 0

Tactic:
simp

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

Goal state before:
pp: case pos
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : 0 < ↑(GeneralLinearGroup.det g)
h✝ : 0 < ↑(GeneralLinearGroup.det h)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z) =
    (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z)

Tactic:
simp

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

Goal state before:
pp: case neg
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : 0 < ↑(GeneralLinearGroup.det g)
h✝ : ¬0 < ↑(GeneralLinearGroup.det h)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) (Complex.conjCAE z) = Complex.conjCAE ((ContinuousAlgEquiv.refl ℝ ℂ) z)

Tactic:
simp

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

Goal state before:
pp: case pos
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : ¬0 < ↑(GeneralLinearGroup.det g)
h✝ : 0 < ↑(GeneralLinearGroup.det h)
⊢ Complex.conjCAE ((ContinuousAlgEquiv.refl ℝ ℂ) z) = (ContinuousAlgEquiv.refl ℝ ℂ) (Complex.conjCAE z)

Tactic:
simp

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

Goal state before:
pp: case neg
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : ¬0 < ↑(GeneralLinearGroup.det g)
h✝ : ¬0 < ↑(GeneralLinearGroup.det h)
⊢ Complex.conjCAE (Complex.conjCAE z) = Complex.conjCAE (Complex.conjCAE z)

Tactic:
simp

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

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ ‖(ContinuousAlgEquiv.refl ℝ ℂ) z‖ = ‖z‖

Tactic:
simp

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

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ ‖Complex.conjCAE z‖ = ‖z‖

Tactic:
simp

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

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu : (σ g) ((σ h) ↑z) = u
⊢ u.im ≠ 0

Tactic:
simpa only [← hu, σ_im_ne_zero] using! z.im_ne_zero

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : (↑g).trace = 0
hb : ↑g 0 1 = ↑g 1 0
hc : ↑g 1 0 = 0
⊢ 0 < (1 + Complex.I).im

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ g.fixpointPolynomial = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

Tactic:
rw [fixpointPolynomial]

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 → ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

Tactic:
refine fun hP ↦ ⟨g 0 0, ?_⟩

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) = ↑g
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
⊢ z.im ≤ (↑(↑N * -n) +ᵥ z).im

Tactic:
simp

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

Goal state before:
pp: ⊢ Continuous
    (UpperHalfPlane.coe ∘
      (Ioi 0).domRestrict fun t ↦
        if hw : 0 < (↑I * ↑t).im then { coe := ↑I * ↑t, coe_im_pos := hw } else Classical.choice ⋯)

Tactic:
have : Continuous (fun t : ℝ ↦ Complex.I * t) := by fun_prop

Goal state after:
this : Continuous fun t ↦ Complex.I * ↑t
⊢ Continuous
    (UpperHalfPlane.coe ∘
      (Ioi 0).domRestrict fun t ↦
        if hw : 0 < (↑I * ↑t).im then { coe := ↑I * ↑t, coe_im_pos := hw } else Classical.choice ⋯)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case refine_1.base
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
⊢ ((Matrix.scalar (Fin 2)) a + m) ^ 1 = (Matrix.scalar (Fin 2)) (a ^ 1) + (↑1 * a ^ (1 - 1)) • m

Tactic:
simp

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

Goal state before:
pp: u : ℝˣ
z : ℍ
⊢ { coe := num ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z / denom ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z,
      coe_im_pos := ⋯ } =
    z

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ 0 < ↑(GeneralLinearGroup.det ((mapGL ℝ) g))

Tactic:
simp

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 ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ↑r / ↑‖↑τ‖ * ↑τ - ↑τ = ↑(r / ‖↑τ‖ - 1) * ↑τ

Tactic:
simp

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 ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ↑r / ↑‖↑τ‖ * ↑τ - ↑τ = (↑r / ↑‖↑τ‖ - 1) * ↑τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: t : ℝ
ht : 0 < t
⊢ { coe := ↑I * ↑t, coe_im_pos := ⋯ }.im = t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddGroup α
f : ℍ → α
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ im ⁻¹' Set.Ici ia, f x ∈ Metric.closedBall 0 ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ z.im → ‖f z‖ ≤ ε

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 * !![z.re, -z.im; z.im, z.re] 1 1 -
      !![z.re, -z.im; z.im, z.re] 0 1 * !![z.re, -z.im; z.im, z.re] 1 0 =
    z.re * z.re + z.im * z.im

Tactic:
simp

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

Goal state before:
pp: ⊢ !![-1, 0; 0, 1].det ≠ 0

Tactic:
simp

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

Goal state before:
pp: τ : ℍ
⊢ ¬1 < 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det * ((blockDiagonal fun m ↦ f (M k k)).det * (blockDiagonal fun m ↦ f 1).det)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (blockDiagonal fun m ↦ 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 =
    (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

Tactic:
simp

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

Goal state before:
pp: g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
⊢ Set.InjOn ((fun z ↦ ↑(g • ↑ofComplex z)) ∘ UpperHalfPlane.coe) s

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: 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 →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)
hgf : ⇑g ∘ e = ⇑f
y : Y
⊢ g y ∈ t

Tactic:
rcases hg y with ⟨xl, xu, h⟩

Goal state after:
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 →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)
hgf : ⇑g ∘ e = ⇑f
y : Y
xl xu : X
h : g y ∈ Icc (f xl) (f xu)
⊢ g y ∈ t
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : y ∈ (minpoly K x).aroots (AlgebraicClosure ↥F)
⊢ (aeval x) (Polynomial.map (algebraMap R K) (minpoly R x)) = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : ∏ i ∈ s, f i = 0
⊢ ∀ (x : ℍ), ∏ i ∈ s, f i x = 0

Tactic:
simpa using congrFun h0

Goal state after:
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
hx : ¬IsIntegral K x
⊢ 1 = 1 ^ finrank (↥K⟮x⟯) L

Tactic:
simp

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
a✝ : ℝ≥0
⊢ ↑(({ toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal }.comp
          { toFun := toReal, continuous_toFun := continuous_coe })
        a✝) =
    ↑((ContinuousMap.id ℝ≥0) a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ (-x) ^ 2 < 1 + x ^ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x

Tactic:
simp

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

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P
R : ℝ
⊢ dist (inversion x R x) x = R ^ 2 / dist x x

Tactic:
simp

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

Goal state before:
pp: case e'_12
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
e_4✝ : Complex.addCommGroup = Complex.instNormedAddCommGroup.toAddCommGroup
e_5✝ : instInnerProductSpaceRealComplex.toModule ≍ instInnerProductSpaceRealComplex.toModule
x✝ : ℂ
⊢ (smulFDeriv g ↑τ) x✝ = ((-↑Complex.conjCLE) ∘SL smulFDeriv (J * g) ↑τ) x✝

Tactic:
simp

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

Goal state before:
pp: case hre
z : ℍ
⊢ (z.center 0).re = z.re

Tactic:
simp

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

Goal state before:
pp: case him
z : ℍ
⊢ (z.center 0).im = z.im

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ sinh (-x) - -x = -(sinh x - x)

Tactic:
simp

Goal state after:
x : ℝ
⊢ -sinh x + x = x - sinh x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ x ≤ sinh x ↔ sinh 0 - 0 ≤ sinh x - x

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ sinh x ≤ x ↔ sinh x - x ≤ sinh 0 - 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n + 1) sinh = cosh

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n + 1) cosh = sinh

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 sinh)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 sinh)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 cosh)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 cosh)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 sinh)

Tactic:
simp

Goal state after: