mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
n : ℕ
w : E
hw : dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ ↑f'symm.nnnorm * dist (f b) y ≤ ↑f'symm.nnnorm * (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := ⋯
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := ⋯
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
n : ℕ
w : E
hw : dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ dist (f b) y ≤ ((↑f'symm.nnnorm)⁻¹ - ↑c) * ε
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
x✝ : ∃ g, AnalyticAt 𝕜 g z₀ ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
h : 𝕜 → E
hh : AnalyticAt 𝕜 h z₀
hfh : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • h z
⊢ n ≤ ⋯.choose

Tactic:
contrapose! hg_ne
      have : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀ := by fun_prop
      rw [tendsto_nhds_unique_of_eventuallyEq (l := 𝓝[≠] z₀)
        hg.continuousAt.continuousWithinAt this.continuousWithinAt ?_]
      · simp [m, Nat.sub_ne_zero_of_lt hg_ne]
      · filter_upwards [self_mem_nhdsWithin, hm.filter_mono nhdsWithin_le_nhds,
          hfh.filter_mono nhdsWithin_le_nhds] with z hz hf' hf''
        rw [← inv_smul_eq_iff₀ (pow_ne_zero _ <| sub_ne_zero_of_ne hz), hf'', smul_comm,
          ← mul_smul] at hf'
        rw [pow_sub₀ _ (sub_ne_zero_of_ne hz) (by lia), ← hf']

Goal state after:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Ign :
  dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n.succ) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ ↑c * ↑f'symm.nnnorm * dist (f (u n)) y ≤ ↑c * ↑f'symm.nnnorm * ((↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y)

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := ⋯
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := ⋯
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Ign :
  dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n.succ) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
n : ℕ
⊢ ↑f'symm.nnnorm * dist (f (u n)) y ≤ ↑f'symm.nnnorm * ((↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y)

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := ⋯
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := ⋯
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
n : ℕ
⊢ dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑f'.symm‖₊ * ‖↑A y' - ↑A x' - f' (y' - x')‖ ≤ ↑‖↑f'.symm‖₊ * (↑c * ‖y' - x'‖)

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := ⋯
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖↑A y' - ↑A x' - f' (y' - x')‖ ≤ ↑c * ‖y' - x'‖
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv hc
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ↑‖↑f'.symm‖₊ * (↑c * ‖y' - x'‖) ≤ ↑‖↑f'.symm‖₊ * (↑c * (↑(‖↑f'.symm‖₊⁻¹ - c)⁻¹ * ‖↑A y' - ↑A x'‖))

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
A : PartialEquiv E F := ⋯
Af : ∀ (z : E), ↑A z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖y' - x'‖ ≤ ↑(‖↑f'.symm‖₊⁻¹ - c)⁻¹ * ‖↑A y' - ↑A x'‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) s x

Tactic:
by
  have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ exp (log (f z) * g z) := by
    filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]
    intro z fz
    simp only [fz, cpow_def, if_false]
  apply AnalyticWithinAt.congr_of_eventuallyEq_insert _ e
  exact ((fa.clog m).mul ga).cexp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x : C
⊢ homEquiv ((SSet.Truncated.Edge.id (nerveEquiv.symm x)).map φ) =
    𝟙 (nerveEquiv ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _proof_11 }))) (nerveEquiv.symm x)))

Tactic:
SSet.Truncated.Edge.map_id

Goal state after:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
x : C
⊢ homEquiv
      (SSet.Truncated.Edge.id
        ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := SSet.Truncated.Edge._proof_1 })))
          (nerveEquiv.symm x))) =
    𝟙 (nerveEquiv ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _proof_11 }))) (nerveEquiv.symm x)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: D X : SSet
H : ∀ (m : ℕ), IsIso (prodComparison hoFunctor D Δ[m])
⊢ ∀ (X_1 : CostructuredArrow uliftYoneda.{u, 0, 0} X),
    IsIso
      (((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}).whiskerLeft
            (prodComparisonNatTrans hoFunctor D)).app
        X_1)

Tactic:
exact fun x ↦ H (x.left).len

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: D X : SSet
H : ∀ (m : ℕ), IsIso (prodComparison hoFunctor D Δ[m])
this :
  IsIso
    ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}).whiskerLeft
      (prodComparisonNatTrans hoFunctor D))
⊢ IsIso (prodComparison hoFunctor D X)

Tactic:
exact isIso_app_coconePt_of_preservesColimit _ (prodComparisonNatTrans hoFunctor _) _
    (Presheaf.isColimitTautologicalCocone' X)

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval a (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : ↑kn = -a
⊢ ↑kn = -a ∨ ↑kn = -b ∨ ↑kn = -c

Tactic:
by tauto

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval b (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : ↑kn = -b
⊢ ↑kn = -a ∨ ↑kn = -b ∨ ↑kn = -c

Tactic:
by tauto

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval c (ascPochhammer 𝕂 n) = 0
kn : ℕ
hkn : kn < n
hn : ↑kn = -c
⊢ ↑kn = -a ∨ ↑kn = -b ∨ ↑kn = -c

Tactic:
by tauto

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case left.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝 ↑z, f z = 0
⊢ ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

pp: case left.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
· -- Case: f is locally zero in a punctured neighborhood of z
      rw [← analyticOrderAt_eq_top] at h
      tauto

Goal state after:
case left.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | analyticOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
hU : IsConnected U
this✝ : ConnectedSpace ↑U
v : ↑U
this : (∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤) ∨ ∀ (u : ↑U), analyticOrderAt f ↑u = ⊤
⊢ (∃ u, analyticOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), analyticOrderAt f ↑u ≠ ⊤

Tactic:
by tauto

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case succ
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
hm : MeromorphicAt (f ^ m) x
⊢ MeromorphicAt (f ^ (m + 1)) x

Tactic:
| succ m hm =>

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n k : ℕ
⊢ multichoose (-↑n) (n + k + 1) = 0

Tactic:
by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_add, smul_zero]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ MeromorphicOn f univ ↔ Meromorphic f

Tactic:
by tauto

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case convert_7
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
z : ℂ
hz : z ∈ Metric.eball 0 (ENNReal.ofReal 1)
⊢ ‖(fun x ↦ x) z‖ < 1

Tactic:
Metric.eball_ofReal

Goal state after:
case convert_7
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
z : ℂ
hz : z ∈ Metric.ball 0 1
⊢ ‖(fun x ↦ x) z‖ < 1
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - (ij.1 + ij.2) • 1) * ↑((ij.1 + ij.2).choose ij.1) =
    ↑((ij.1 + ij.2).choose ij.1) * (s - ij.2 • 1) + ↑((ij.1 + ij.2).choose ij.1) * (r - ij.1 • 1)

Tactic:
← mul_add,

Goal state after:
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - (ij.1 + ij.2) • 1) * ↑((ij.1 + ij.2).choose ij.1) =
    ↑((ij.1 + ij.2).choose ij.1) * (s - ij.2 • 1 + (r - ij.1 • 1))
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case succ.e_a
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ (descPochhammer ℤ n).smeval a * (a - ↑n) = (descPochhammer ℤ (n + 1)).smeval a

Tactic:
simp [descPochhammer_succ_right, Polynomial.smeval_mul, Polynomial.smeval_natCast]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    ↑(k.choose x.1) * ↑x.1.factorial * (↑x.2.factorial * choose r x.1 * choose s x.2)

Tactic:
Nat.cast_commute x.2.factorial,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    ↑(k.choose x.1) * ↑x.1.factorial * (choose r x.1 * ↑x.2.factorial * choose s x.2)
Module: Mathlib.Analysis.Analytic.Polynomial

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
s : Set E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p✝ p q : A[X]
hp : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) p) s z
hq : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) q) s z
⊢ AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (p + q)) s z

Tactic:
aeval_add

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
s : Set E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f s z
p✝ p q : A[X]
hp : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) p) s z
hq : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) q) s z
⊢ AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) p + (aeval (f x)) q) s z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case succ
r x : ℝ
k : ℕ
IH : (deriv^[k] fun x ↦ x ^ r) = fun x ↦ Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - ↑k)
⊢ (deriv^[k + 1] fun x ↦ x ^ r) = fun x ↦ Polynomial.eval r (descPochhammer ℝ (k + 1)) * x ^ (r - ↑(k + 1))

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, Nat.cast_add, Nat.cast_one, IH]
    ext y
    simp only [deriv_const_mul_field, deriv_rpow_const, ← mul_assoc, descPochhammer_succ_right,
      Polynomial.eval_mul, Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_natCast,
      mul_eq_mul_left_iff, mul_eq_zero]
    grind

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ dist x z + dist y z < ↑r + ↑r

Tactic:
gcongr

Goal state after:
case h₁
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ dist x z < ↑r

case h₂
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ dist y z < ↑r
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ ↑r + ↑r ≤ ↑(D.packingRadius / 2) + ↑(D.packingRadius / 2)

Tactic:
gcongr

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
h : ↑a✝ < ⊥
⊢ (↑a✝).exp < ⊥.exp

pp: case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ (↑a✝¹).exp < (↑a✝).exp

pp: case coe.top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp

Tactic:
· simp at h

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ (↑a✝¹).exp < (↑a✝).exp

case coe.top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
y : ℝ
⊢ (x * ↑y).exp.log = (x.exp ^ y).log

Tactic:
log_rpow,

Goal state after:
x : EReal
y : ℝ
⊢ (x * ↑y).exp.log = ↑y * x.exp.log