mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case refine_1
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n
⊢ orderHomOfSimplex z hn = OrderHom.id

pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id → z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n

Tactic:
· exact OrderHom.eq_id_of_injective _ (strictMono_orderHomOfSimplex ⟨z, h⟩ hn).injective

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id → z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝ : LocallySmall.{w, v, u} C
X : C
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨J, _, _, ⟨hX⟩⟩ := h.exists_colimitsOfShape X

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝ : LocallySmall.{w, v, u} C
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
⊢ IsPresentable.{w, v, u} X
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ isCardinalPresentable C κ = P.retractClosure

Tactic:
refine le_antisymm (fun X hX ↦ ?_) ?_
  · rw [isCardinalPresentable_iff] at hX
    obtain ⟨J, _, _, ⟨p⟩⟩ := h.exists_colimitsOfShape X
    have := essentiallySmall_of_small_of_locallySmall.{w} J
    obtain ⟨j, f, hf⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit (𝟙 X)
    exact ⟨_, p.prop_diag_obj j, ⟨{ i := _, r := _, retract := hf}⟩⟩
  · simpa only [ObjectProperty.retractClosure_le_iff] using h.le_isCardinalPresentable

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
⊢ ∃ J_1 x, ∃ (_ : IsCardinalFiltered J_1 κ), (⊤.map F).colimitsOfShape J_1 X

Tactic:
by
    have ip := F.denseAt X
    let e := equivSmallModel.{w} (CostructuredArrow F X)
    exact ⟨SmallModel.{w} (CostructuredArrow F X), inferInstance,
      IsCardinalFiltered.of_equivalence κ e,
      ⟨{  diag := _
          ι := _
          isColimit := (F.denseAt X).whiskerEquivalence e.symm
          prop_diag_obj j := ⟨_, by simp, ⟨Iso.refl _⟩⟩ }⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
Q : C
⊢ Q ◁ f ≫ Q ◁ inl = Q ◁ g ≫ Q ◁ inr

Tactic:
by
  simp [← MonoidalCategory.whiskerLeft_comp, hP.w]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ A
⊢ Z ◁ W ◁ g ≫ (α_ Z W Y).inv ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g) =
    (α_ Z W X).inv ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g)

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ← pushout.condition,
    ← comp_whiskerRight_assoc]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < (k.castSucc, (x.cast hd).simplex.2 (min x hd))

Tactic:
refine lt_of_le_of_ne ⟨?_, ?_⟩ ?_

Goal state after:
case inl.inr.refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ ((objEquiv (x.cast hd).simplex) i.castSucc).1 ≤ (k.castSucc, (x.cast hd).simplex.2 (min x hd)).1

case inl.inr.refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ ((objEquiv (x.cast hd).simplex) i.castSucc).2 ≤ (k.castSucc, (x.cast hd).simplex.2 (min x hd)).2

case inl.inr.refine_3
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ (objEquiv (x.cast hd).simplex) i.castSucc ≠ (k.castSucc, (x.cast hd).simplex.2 (min x hd))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
m : ℕ
X Y : SSet
k : Fin (m + 2)
⊢ HasLiftingProperty Λ[m + 1, k].ι sq₁₃.π

Tactic:
let sq₁₂ := Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι

Goal state after:
X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
m : ℕ
X Y : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
⊢ HasLiftingProperty Λ[m + 1, k].ι sq₁₃.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
⊢ (chainComplexFunctor C).Additive

Tactic:
dsimp [chainComplexFunctor, SimplicialObject.whiskering]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ parallelPair ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0)) 0 ≅
    parallelPair ((X.chainComplex R).d 1 0) 0

Tactic:
refine parallelPair.ext (-Iso.refl _) (Iso.refl _) ?_ (by simp)

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (parallelPair ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
            0).map
        WalkingParallelPairHom.left ≫
      (Iso.refl
          ((parallelPair
                ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                0).obj
            WalkingParallelPair.one)).hom =
    (-Iso.refl
            ((parallelPair
                  ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                  0).obj
              WalkingParallelPair.zero)).hom ≫
      (parallelPair ((X.chainComplex R).d 1 0) 0).map WalkingParallelPairHom.left
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.right
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
hf : Mono (SimplexCategory.δ it.succ)
Ss : Finset (Fin ((Subcomplex.N.mk s hs₁ hs₂).dim + 1)) := ⋯
St : Finset (Fin ((Subcomplex.N.mk t ht₁ ht₂).dim + 1)) := ⋯
Sδ : Finset (Fin (hs.δ.dim + 1)) := ⋯
hδ : ∀ (i : Fin (d + 1)), s.1 (is.castSucc.succAbove i) = t.1 (it.succ.succAbove i)
hSs : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ is.castSucc.succAbove i ∈ Ss
hSt : ∀ (i : Fin (d + 1)), i ∈ Sδ ↔ it.succ.succAbove i ∈ St
⊢ St.card = Sδ.card + 1

Tactic:
· suffices St = Finset.image it.succ.succAbove Sδ ∪ {it.succ} by
          rw [this, Finset.card_union_of_disjoint (by simp),
            Finset.card_image_of_injective _ Fin.succAbove_right_injective,
            Finset.card_singleton]
        ext i
        obtain rfl | ⟨i, rfl⟩ := it.succ.eq_self_or_eq_succAbove i
        · have : it.succ ∈ St := by
            simpa [St, mem_finset_iff] using ht.simplex_fst_succ
          simp [hSt, this]
        · simp [hSt]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case h₁
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.left
      (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
            whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
        x✝) =
    Arrow.Hom.left
      (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
            (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
        x✝)

pp: case h₂
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.right
      (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
            whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
        x✝) =
    Arrow.Hom.right
      (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
            (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
        x✝)

Tactic:
· simp [← homEquiv_naturality_one, ← homEquiv_naturality_three]

Goal state after:
case h₂
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : Arrow C₂
⊢ Arrow.Hom.right
      (((LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫
            whiskerRight (F.leibnizPushout.map x✝¹) (G.leibnizPullback.obj (op X₁✝))).app
        x✝) =
    Arrow.Hom.right
      (((LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫
            (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝¹.op)).app
        x✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (stdSimplex.δ k.rev ≫ h.map))) = const x

Tactic:
h.δ_map_of_lt _ (by grind)

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (const (opObjEquiv.symm x)))) = const x
Module: Mathlib.LinearAlgebra.Complex.Determinant

Goal state before:
pp: ⊢ LinearEquiv.det ↑conjAe = -1

Tactic:
simp [← Units.val_inj]

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
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 * (1 - (↑c * ↑f'symm.nnnorm) ^ n) ≤ ↑f'symm.nnnorm * dist (f b) y * 1

Tactic:
gcongr
        rw [sub_le_self_iff]
        positivity

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : u = w
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a w)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v w)) (z w)))
    atTop (𝓝 (Pi.single w (z w) u))

pp: case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a w)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v w)) (z w)))
    atTop (𝓝 (Pi.single w (z w) u))

Tactic:
· rw [← hw, Pi.single_eq_same]
      have hlt : (v u) (a u)⁻¹ < 1 := by
        simpa [← inv_pow, inv_lt_one_iff₀] using Or.inr (hx u).1
      simpa using (WithAbs.tendsto_one_div_one_add_pow_nhds_one hlt).mul_const (z u)

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : ¬u = w
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a w)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v w)) (z w)))
    atTop (𝓝 (Pi.single w (z w) u))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e₀₁.edge))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁
      (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) h.simplex)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)) = y

Tactic:
h'

Goal state after:
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁
      (F.map (homMk (Edge.mk' ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) h.simplex)))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)) = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e₁₂.edge))) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)) = y

Tactic:
h'

Goal state after:
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
y : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_14 })
h' :
  ∀ {a b : X.obj (op { obj := ⦋0⦌, property := ⋯ })} (e : Edge a b),
    ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 2 _proof_12 _proof_15).op)) y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (((truncation 2).obj (nerve C)).map (δ₂ 0 _proof_12 _proof_15).op)) y
⊢ ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)) = 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‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
⊢ ‖↑(hf.toPartialEquiv hc).symm x - ↑(hf.toPartialEquiv hc).symm y - ↑f'.symm (x - y)‖ ≤
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖

Tactic:
set A := hf.toPartialEquiv hc

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‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : PartialEquiv E F := hf.toPartialEquiv hc
⊢ ‖↑A.symm x - ↑A.symm y - ↑f'.symm (x - y)‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ConcreteCategory.hom ((homToNerveMk (descOfTruncation φ)).app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge

Tactic:
dsimp [nerve.homEquiv]

Goal state after:
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : X ⟶ (truncation 2).obj (nerve C)
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ConcreteCategory.hom ((homToNerveMk (descOfTruncation φ)).app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom (φ.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge
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
fa : AnalyticAt ℂ f x
ga : AnalyticAt ℂ g x
m : f x ∈ slitPlane
⊢ AnalyticAt ℂ (fun z ↦ f z ^ g z) x

Tactic:
rw [← analyticWithinAt_univ] at fa ga ⊢

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticWithinAt ℂ f univ x
ga : AnalyticWithinAt ℂ g univ x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) univ x
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s] x,
    ‖f x_1 - f x - f' (x_1 - x)‖ ≤ ε * ‖x_1 - x‖

Tactic:
set B := ball x δ

Goal state after:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
⊢ ∀ᶠ (x_1 : E) in 𝓝[closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s] x,
    ‖f x_1 - f x - f' (x_1 - x)‖ ≤ ε * ‖x_1 - x‖