mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt (f₁ - f₂) x = meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x

Tactic:
rw [sub_eq_add_neg, hf₁.meromorphicTrailingCoeffAt_add_eq_add (by fun_prop)]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x =
    meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x

case h₁
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt (-f₂) x

case h₂
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x ≠ 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u : 𝕜
h : u ∈ support d
⊢ ¬((fun x ↦ x - u) ^ d u) u = 1 u

Tactic:
simp_all [zero_zpow_eq_one₀]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case pos
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
ta : ↑I × A
_ : ¬ta.1 ≤ t n
hv : f ta ∈ (q e).target
⊢ p (↑(q e).symm (f ta)) = f ta

Tactic:
hpq e,

Goal state after:
case pos
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
x✝ :
  ∃ N,
    a ∈ N ∧
      IsOpen[inst✝] N ∧
        ∃ g',
          ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
            p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
g' : ↑I × A → E
cont_g' : ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N)
g'_lifts : p ∘ g' = ⇑f
g'_0 : ∀ (a : A), g' (0, a) = g (0, a)
g'_a : ∀ t' ≤ t n, g' (t', a) = g (t', a)
e : E
h_sub : Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q e).source
this : Set.Icc (t n) (t (n + 1)) ×ˢ {a} ⊆ ⇑f ⁻¹' (q e).target
u : Set ↑I
v : Set A
v_open : IsOpen[inst✝] v
hu : Set.Icc (t n) (t (n + 1)) ⊆ u
hav : {a} ⊆ v
huv : u ×ˢ v ⊆ ⇑f ⁻¹' (q e).target
ta : ↑I × A
_ : ¬ta.1 ≤ t n
hv : f ta ∈ (q e).target
⊢ ↑(q e) (↑(q e).symm (f ta)) = f ta
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
⊢ ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u = (fun x ↦ x - u₀) ^ d u₀ * ∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ update d u₀ 0 u

Tactic:
by
  by_cases h₁d : d u₀ = 0
  · simp [← eq_update_self_iff.2 h₁d, h₁d]
  · have : (fun u ↦ (fun x ↦ x - u) ^ d u).mulSupport ⊆ hd.toFinset := by
      simp [mulSupport]
    rw [finprod_eq_prod_of_mulSupport_subset _ this]
    have : u₀ ∈ hd.toFinset := by simp_all
    rw [← Finset.mul_prod_erase hd.toFinset _ this]
    congr 1
    have : (fun u ↦ (· - u) ^ (update d u₀ 0 u)).mulSupport ⊆ hd.toFinset.erase u₀ := by
      rw [mulSupport]
      intro x hx
      by_cases h₁x : x = u₀ <;> simp_all
    simp_all [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]

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

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
⊢ g ∈ Subgroup.center (GL n R) → ↑g ∈ Set.range ⇑(Matrix.scalar n)

Tactic:
intro hg

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
hg : g ∈ Subgroup.center (GL n R)
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar n)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
⊢ g ∈ Subgroup.center (GL n R) → g ∈ (scalar n).range

Tactic:
intro hg

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : GL n R
hg : g ∈ Subgroup.center (GL n R)
⊢ g ∈ (scalar n).range
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x) I = I • (fderivWithin ℝ f s x) 1
hs : UniqueDiffWithinAt ℝ s x
this : restrictScalars ℝ (fderivWithin ℂ f s x) = fderivWithin ℝ f s x
⊢ fderivWithin ℂ f s x = (fderivWithin ℝ f s x).complexOfReal h₂

Tactic:
simpa [DFunLike.ext_iff]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₂
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ ((divisor f B₀R) x + -(divisor f B₀R) x) = 1

pp: case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₂
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ≠ 0

Tactic:
add_neg_cancel,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₂
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ 0 = 1

case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₂
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ≠ 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
⊢ p ∘ ⇑({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp F) =
    ⇑({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f)

Tactic:
simp [← hF, Function.comp_def]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case h
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
p : E → X
G : Type u_4
inst✝² : Group G
inst✝¹ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
inst✝ : PathConnectedSpace E
g : Gᵐᵒᵖ
e' : ↑(p ⁻¹' {x}) := ⟨MulOpposite.unop g • ↑e, ⋯⟩
he' : e' = ⟨MulOpposite.unop g • ↑e, ⋯⟩
Γ : Path ↑e ↑e' := { toFun := ⇑(PathConnectedSpace.somePath ↑e ↑e'), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
γ : Path x x := (Γ.map ⋯).cast ⋯ ⋯
⊢ MulOpposite.unop g • ↑e = ↑(⋯.monodromy (FundamentalGroup.fromPath ⟦γ⟧) e)

Tactic:
change (e' : E) = _

Goal state after:
case h
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
p : E → X
G : Type u_4
inst✝² : Group G
inst✝¹ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
inst✝ : PathConnectedSpace E
g : Gᵐᵒᵖ
e' : ↑(p ⁻¹' {x}) := ⟨MulOpposite.unop g • ↑e, ⋯⟩
he' : e' = ⟨MulOpposite.unop g • ↑e, ⋯⟩
Γ : Path ↑e ↑e' := { toFun := ⇑(PathConnectedSpace.somePath ↑e ↑e'), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
γ : Path x x := (Γ.map ⋯).cast ⋯ ⋯
⊢ ↑e' = ↑(⋯.monodromy (FundamentalGroup.fromPath ⟦γ⟧) e)
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

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

Tactic:
congr 1 with m
    rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]
    · simp only [↓reduceIte, one_smul]
    simp only [orthonormal_iff_ite.1 w.orthonormal, ite_smul, one_smul, zero_smul,
      ite_eq_right_iff]
    tauto

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

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
rw [ne_comm] at h0 h1

Goal state after:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case neg.refine_2.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (fun x ↦ x) z

pp: case neg.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0 ∨ z ≠ 0

Tactic:
· apply differentiableAt_id

Goal state after:
case neg.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0 ∨ z ≠ 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
rw [ne_comm] at h0 h1

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F✝ : Type u_1
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : CompleteSpace F✝
f : ℂ → F✝
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
h₃F : DifferentiableOn ℂ F (closure (ball c |R|))
h₄F : Set.EqOn (⇑Complex.reCLM ∘ F) (⇑g ∘ f) (sphere c |R|)
⊢ CircleIntegrable F c R

Tactic:
· apply (h₁F.continuousOn.mono (fun _ _ ↦ by simp_all [dist_eq_norm])).circleIntegrable'

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

Goal state before:
pp: case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntervalIntegrable (cos (r * π) • fun x ↦ x ^ r) volume 0 (-c)
⊢ IntervalIntegrable (fun x ↦ (-x) ^ r) volume 0 (-c)

Tactic:
rw [intervalIntegrable_iff] at m ⊢

Goal state after:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
m : IntegrableOn (cos (r * π) • fun x ↦ x ^ r) (Ι 0 (-c)) volume
⊢ IntegrableOn (fun x ↦ (-x) ^ r) (Ι 0 (-c)) volume
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case neg
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)

Tactic:
suffices ∀ c : ℝ, (∫ x : ℝ in 0..c, (x : ℂ) ^ r) =
      (c : ℂ) ^ (r + 1) / (r + 1) - (0 : ℂ) ^ (r + 1) / (r + 1) by
    rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h)
      (@intervalIntegrable_cpow' 0 b r h), integral_symm, this a, this b, Complex.zero_cpow hr]
    ring

Goal state after:
case neg
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
⊢ ∀ (c : ℝ), ∫ (x : ℝ) in 0..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y ↦ Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Complex.exp (c * ↑b) / c - Complex.exp (c * ↑a) / c = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c

pp: a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y ↦ Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ContinuousOn (fun x ↦ Complex.exp (c * ↑x)) [[a, b]]

Tactic:
· ring

Goal state after:
a b : ℝ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y ↦ Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ContinuousOn (fun x ↦ Complex.exp (c * ↑x)) [[a, b]]
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
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 : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
n : ℕ
z : ℂ
⊢ ‖g n z‖ = expR z.re ^ n * ‖f z‖

Tactic:
by
    simp only [g, norm_smul, norm_pow, norm_exp]

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

Goal state before:
pp: a b : ℝ
⊢ -cos b - -cos a = cos a - cos b

pp: case hderiv
a b : ℝ
⊢ (deriv fun x ↦ -cos x) = sin

pp: case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ (fun x ↦ -cos x) x

pp: case hcont
a b : ℝ
⊢ ContinuousOn sin [[a, b]]

Tactic:
· ring

Goal state after:
case hderiv
a b : ℝ
⊢ (deriv fun x ↦ -cos x) = sin

case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ (fun x ↦ -cos x) x

case hcont
a b : ℝ
⊢ ContinuousOn sin [[a, b]]
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ sin x

pp: case hcont
a b : ℝ
⊢ ContinuousOn cos [[a, b]]

Tactic:
· simp only [differentiableAt_sin, implies_true]

Goal state after:
case hcont
a b : ℝ
⊢ ContinuousOn cos [[a, b]]
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖ = ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖

Tactic:
have : Function.Periodic (log ‖circleMap 0 1 · - 1‖) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]
    have := this.intervalIntegral_add_eq (t := 0) (s := ζ)
    simp_all [integral_comp_add_left (log ‖circleMap 0 1 · - 1‖)]

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

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ log √(Complex.normSq (circleMap 0 1 x - 1)) = log (4 * sin (x / 2) ^ 2) / 2

Tactic:
log_sqrt (circleMap 0 1 x - 1).normSq_nonneg

Goal state after:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ log (Complex.normSq (circleMap 0 1 x - 1)) / 2 = log (4 * sin (x / 2) ^ 2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case neg
a b c : ℝ
hc : ¬c = 0
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)

Tactic:
rw [integral_const_mul, integral_inv_sq_add_sq hc]
      field_simp

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

Goal state before:
pp: case e'_9
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ ↑x * (1 + ↑x ^ 2) ^ t = (1 + ↑x ^ 2) ^ t / 2 * (2 * ↑x)

pp: case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ 0 < (1 + ↑x ^ 2).re

Tactic:
· ring

Goal state after:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
g : ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z
⊢ 0 < (1 + ↑x ^ 2).re
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : ¬eval z P = 0
x : ℂ
hx : x ∈ s
⊢ (↑(rootMultiplicity x P) / ‖z - x‖ ^ 2) • (z - x) = (starRingEnd ℂ) (rootMultiplicity x P • (1 / (z - x)))

Tactic:
have : z - x ≠ 0 := by
        rw [sub_ne_zero]
        rintro rfl
        simp_all [s]

Goal state after:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : ¬eval z P = 0
x : ℂ
hx : x ∈ s
this : z - x ≠ 0
⊢ (↑(rootMultiplicity x P) / ‖z - x‖ ^ 2) • (z - x) = (starRingEnd ℂ) (rootMultiplicity x P • (1 / (z - x)))
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv n (fun x ↦ f x - f c) c

Tactic:
cases n with

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n (fun z ↦ f (-z)) (-c)

Tactic:
simpa only [iteratedDeriv_comp_neg, neg_neg, smul_eq_mul] using h n hn

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

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
⊢ circleAverage (∑ᶠ (u : ℂ), fun x ↦ ↑(D u) * log ‖x - u‖) c R = ∑ᶠ (u : ℂ), ↑(D u) * log R

Tactic:
by
  have h := D.finiteSupport (isCompact_closedBall c |R|)
  calc circleAverage (∑ᶠ u, (D u * log ‖· - u‖)) c R
  _ = circleAverage (∑ u ∈ h.toFinset, (D u * log ‖· - u‖)) c R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    contrapose
    aesop
  _ = ∑ i ∈ h.toFinset, circleAverage (fun x ↦ D i * log ‖x - i‖) c R := by
    rw [circleAverage_sum]
    intro u hu
    apply IntervalIntegrable.const_mul
    apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm
  _ = ∑ u ∈ h.toFinset, D u * log R := by
    apply Finset.sum_congr rfl
    intro u hu
    simp_rw [← smul_eq_mul, circleAverage_fun_smul]
    congr
    rw [circleAverage_log_norm_sub_const_of_mem_closedBall]
    apply D.supportWithinDomain
    simp_all
  _ = ∑ᶠ u, D u * log R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    aesop

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

Goal state before:
pp: ⊢ (-1).sqrt = I

Tactic:
by
  simp [sqrt_neg_of_nonneg (a := 1) (by simp)]

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

Goal state before:
pp: ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)

Tactic:
by
  rwa [Periodic.qParam, ofReal_one, div_one, Complex.norm_exp, Real.exp_le_exp,
    mul_right_comm, mul_I_re, neg_le_neg_iff, ← ofReal_ofNat, ← ofReal_mul, im_ofReal_mul,
    mul_comm _ π, mul_assoc, le_mul_iff_one_le_right Real.pi_pos, ← div_le_iff₀' two_pos]

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

Goal state before:
pp: ⊢ TietzeExtension ↑I

Tactic:
rw [unitInterval.eq_closedBall]
  exact Metric.instTietzeExtensionClosedBall ℝ _ (by norm_num)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ (↑g * m * (↑g)⁻¹).IsElliptic ↔ m.IsElliptic

Tactic:
by
  simp [IsElliptic]

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

Goal state before:
pp: case mp
g : GL (Fin 2) ℝ
⊢ (∀ (z : ℍ), g • z = z) → g ∈ Subgroup.center (GL (Fin 2) ℝ)

Tactic:
intro hg

Goal state after:
case mp
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
⊢ g ∈ Subgroup.center (GL (Fin 2) ℝ)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ ¬2 ^ 2 * (↑g).det = 0

Tactic:
mul_eq_zero,

Goal state after:
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ ¬(2 ^ 2 = 0 ∨ (↑g).det = 0)