mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcⱼ : ∀ (j : ι), j ≠ i → Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))

Tactic:
have : w a⁻¹ < 1 := map_inv₀ w _ ▸ inv_lt_one_of_one_lt₀ haw

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcⱼ : ∀ (j : ι), j ≠ i → Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0)
this : w a⁻¹ < 1
⊢ Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «1»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ f₁
      ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op))
        ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_15 _proof_12).op)) x)) =
    (ConcreteCategory.hom (Y.map (Hom.tr (SimplexCategory.mkOfSucc 1) ⋯ f₂._proof_4).op))
      ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))

Tactic:
← Functor.map_comp_apply,

Goal state after:
case «1»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ f₁ ((ConcreteCategory.hom (X.map ((σ₂ 1 _proof_15 _proof_12).op ≫ (δ₂ 0 _proof_12 _proof_15).op))) x) =
    (ConcreteCategory.hom (Y.map (Hom.tr (SimplexCategory.mkOfSucc 1) ⋯ f₂._proof_4).op))
      ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «1»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op))
      (f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op)) x)) =
    (ConcreteCategory.hom (Y.map (Hom.tr (SimplexCategory.δ 0) ⋯ f₂._proof_4).op))
      ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))

Tactic:
← Functor.map_comp_apply,

Goal state after:
case «1»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op))
      (f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op)) x)) =
    (ConcreteCategory.hom (Y.map ((σ₂ 1 _proof_15 _proof_12).op ≫ (Hom.tr (SimplexCategory.δ 0) ⋯ f₂._proof_4).op)))
      (f₁ x)
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
this : Fintype ι
P : (ι : Type ?u.69) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
⊢ (∀ (i : ι), (v i).IsNontrivial) →
    (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

Tactic:
refine induction_subsingleton_or_nontrivial (P := P) ι (fun ι _ _ v h hv i ↦ ?_)
    (fun ι _ _ ih v h hv i ↦ ?_) v

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Subsingleton ι
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1

case refine_2
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι✝ : Type u_3
inst✝ : Finite ι✝
v✝ : ι✝ → AbsoluteValue R S
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
⊢ ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ EventuallyConst f (𝓝 z₀) ↔ analyticOrderAt (fun x ↦ f x - f z₀) z₀ = ⊤

Tactic:
by
  simpa [eventuallyConst_iff_exists_eventuallyEq, analyticOrderAt_eq_top, sub_eq_zero]
    using ⟨fun ⟨c, hc⟩ ↦ (show f z₀ = c from hc.self_of_nhds) ▸ hc, fun h ↦ ⟨_, h⟩⟩

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

Goal state before:
pp: case succ
𝕜 : 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
⊢ dist (f (u (n + 1))) y ≤ (↑c * ↑f'symm.nnnorm) ^ (n + 1) * dist (f b) y ∧
    dist (u (n + 1)) b ≤
      ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ (n + 1)) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y

Tactic:
rw [usucc]

Goal state after:
case succ
𝕜 : 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
⊢ dist (f (g (u n))) y ≤ (↑c * ↑f'symm.nnnorm) ^ (n + 1) * dist (f b) y ∧
    dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ (n + 1)) / (1 - ↑c * ↑f'symm.nnnorm) * 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
⊢ ‖↑A.symm (↑A x') - ↑A.symm (↑A y') - ↑f'.symm (↑A x' - ↑A y')‖ ≤
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖

Tactic:
A.left_inv x's,

Goal state after:
𝕜 : 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
⊢ ‖x' - ↑A.symm (↑A y') - ↑f'.symm (↑A x' - ↑A y')‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : Category.{u, u} C
inst✝ : Category.{u, u} D
⊢ IsIso (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))

Tactic:
have : IsIso (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D)) :=
      IsIso.of_isIso_fac_left
        (prodComparison_comp nerveFunctor (hoFunctor ⋙ nerveFunctor)
          (A := Cat.of C) (B := Cat.of D)).symm

Goal state after:
C D : Type u
inst✝¹ : Category.{u, u} C
inst✝ : Category.{u, u} D
this : IsIso (prodComparison (hoFunctor ⋙ nerveFunctor) (nerve C) (nerve D))
⊢ IsIso (nerveFunctor.map (prodComparison hoFunctor (nerve C) (nerve D)))
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
⊢ ↑n ≤ analyticOrderAt (deriv f) z₀ ↔ ↑n + 1 ≤ analyticOrderAt f z₀

Tactic:
natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero hf.deriv,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
⊢ (∀ i < n, iteratedDeriv i (deriv f) z₀ = 0) ↔ ↑n + 1 ≤ analyticOrderAt f z₀
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hg : AnalyticAt 𝕜 g z₀
hg' : deriv g z₀ ≠ 0
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)

Tactic:
simp [hf.analyticOrderAt_comp hg, hg.analyticOrderAt_sub_eq_one_of_deriv_ne_zero hg']

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) sin = iteratedDeriv n cos

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

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
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
h : ∃ n g, AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicAt (deriv f) x

Tactic:
obtain ⟨n, g, h₁g, h₂g⟩ := h

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ MeromorphicAt (deriv f) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y ↦ x ^ y) (x ^ y * log x) y

Tactic:
rcases em (x = 0) with (rfl | hx)

Goal state after:
case inl
y : ℂ
h : 0 ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun y ↦ 0 ^ y) (0 ^ y * log 0) y

case inr
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun y ↦ x ^ y) (x ^ y * log x) y
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 g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
⊢ U ∈ 𝓝[≠] x

Tactic:
apply mem_nhdsWithin.mpr

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h₂ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : 𝕜
hx : x ∈ U
h₁ : ∀ x ∈ U, (U \ {x | f x = g x})ᶜ ∈ 𝓝[≠] x
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
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 g : 𝕜 → E
hf : Meromorphic f
h₁ : f =ᶠ[codiscrete 𝕜] g
⊢ Meromorphic g

Tactic:
← meromorphicOn_univ

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
hf : MeromorphicOn f univ
h₁ : f =ᶠ[codiscrete 𝕜] g
⊢ MeromorphicOn g univ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (r + 1) * ↑x ^ r = (r + 1) * ↑x ^ r * ?inl.convert_4.convert_2

Tactic:
exact (mul_one _).symm

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
inst✝⁵ : MeasurableSpace 𝕜
inst✝⁴ : SecondCountableTopology 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : MeasurableSpace E
inst✝¹ : CompleteSpace E
inst✝ : BorelSpace E
h : Meromorphic f
⊢ Measurable f

Tactic:
set s := {z : 𝕜 | AnalyticAt 𝕜 f z}

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
f : 𝕜 → E
inst✝⁵ : MeasurableSpace 𝕜
inst✝⁴ : SecondCountableTopology 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : MeasurableSpace E
inst✝¹ : CompleteSpace E
inst✝ : BorelSpace E
h : Meromorphic f
s : Set 𝕜 := {z | AnalyticAt 𝕜 f z}
⊢ Measurable f
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ (r + 1) * ↑(-x) ^ r = (r + 1) * ↑(-x) ^ r * ?inr.convert_2

Tactic:
exact (mul_one _).symm

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

Goal state before:
pp: 𝕜 : 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✝ : A[X]
p : ℕ
i : A
hp : AnalyticWithinAt 𝕜 (fun x ↦ (aeval (f x)) (C i * X ^ p)) s z
x✝ : E
⊢ (aeval (f x✝)) (C i * X ^ (p + 1)) = (aeval (f x✝)) (C i * X ^ p) * f x✝

Tactic:
simp_rw [pow_succ, aeval_mul, ← mul_assoc, aeval_X]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
x : E
s : Set E
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
h : f x ≠ 0
⊢ ContDiffWithinAt ℝ n (fun x ↦ f x ^ g x) s x

Tactic:
by
  -- `by exact` to deal with tricky unification.
  exact (contDiffAt_rpow_of_ne (f x, g x) h).comp_contDiffWithinAt x (hf.prodMk hg)

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (-↑a✝).exp = (↑a✝).exp⁻¹

Tactic:
rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
      Real.exp_neg]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v + 0 = linearGrowthInf v

pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ 0 ≠ ⊤

pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ 0 ≠ ⊥

Tactic:
· exact add_zero (linearGrowthInf v)

Goal state after:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ 0 ≠ ⊤

u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ 0 ≠ ⊥
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
this : linearGrowthInfTopHom (hs.toFinset.inf u) = hs.toFinset.inf (⇑linearGrowthInfTopHom ∘ u)
⊢ linearGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, linearGrowthInf (u x)

Tactic:
simpa only [linearGrowthInfTopHom, InfTopHom.coe_mk, InfHom.coe_mk, Finset.inf_eq_iInf,
    hs.mem_toFinset, comp_apply]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ f =O[l] fun a ↦ k a ^ z

Tactic:
refine isBigO_of_div_tendsto_nhds (hk0.mono fun x hx hxz ↦ absurd hxz (zpow_ne_zero _ hx)) 0 ?_
    have : (fun a : α => k a ^ z)⁻¹ = fun a : α => k a ^ (-z) := funext fun x => by simp
    rw [div_eq_mul_inv, mul_comm f, this]
    exact h (-z)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
⊢ (linearGrowthInf fun n ↦ ↑(v n)) * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)

Tactic:
apply EReal.mul_le_of_forall_lt_of_nonneg (linearGrowthInf_natCast_nonneg v) uv_0

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
⊢ ∀ a' ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n)),
    ∀ b' ∈ Set.Ioo 0 (linearGrowthInf u), a' * b' ≤ linearGrowthInf (u ∘ v)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Finset α
⊢ expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset,
    expGrowthSup_zero]
  | insert a t a_t ha => rw [Finset.sum_insert a_t, expGrowthSup_add, ← Finset.iSup_coe,
    Finset.coe_insert a t, iSup_insert, Finset.iSup_coe, ha]

Goal state after: