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

Goal state before:
pp: case hx
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
s₂ : (range (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₂.simplex = x₂
⊢ (ConcreteCategory.hom ((f.b j).app (op ⦋s₁.dim⦌))) s₁.simplex ∈
    (f.filtration (Order.succ j)).toSSet.nonDegenerate s₁.dim

Tactic:
rw [Subcomplex.mem_nonDegenerate_iff]
        apply f.isPushout_aux₁

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

Goal state before:
pp: case hy
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
s₂ : (range (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₂.simplex = x₂
⊢ (ConcreteCategory.hom ((f.b j).app (op ⦋s₂.dim⦌))) s₂.simplex ∈
    (f.filtration (Order.succ j)).toSSet.nonDegenerate s₂.dim

Tactic:
rw [Subcomplex.mem_nonDegenerate_iff]
        apply f.isPushout_aux₁

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
⊢ k.castSucc < (x.cast hd).simplex.1 i ↔ min x hd ≤ i

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : k.castSucc < (x.cast hd).simplex.1 i
⊢ min x hd ≤ i

case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : min x hd ≤ i
⊢ k.castSucc < (x.cast hd).simplex.1 i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : k.castSucc < (x.cast hd).simplex.1 i
⊢ min x hd ≤ i

Tactic:
rw [Fin.castSucc_lt_iff_succ_le] at h

Goal state after:
case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : k.succ ≤ (x.cast hd).simplex.1 i
⊢ min x hd ≤ i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (n + 1)
i : Fin ((x.cast hd).dim + 1)
hi : (x.cast hd).simplex.2 i = j
⊢ ∃ x_1, (x.cast hd).simplex.2 (l.castSucc.succAbove x_1) = j

Tactic:
dsimp at hi

Goal state after:
case refine_1
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (n + 1)
i : Fin ((x.cast hd).dim + 1)
hi : (x.cast hd).simplex.2 i = j
⊢ ∃ x_1, (x.cast hd).simplex.2 (l.castSucc.succAbove x_1) = j
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (m + 1 + 1)
hj : ¬j = k.castSucc
i : Fin ((x.cast hd).dim + 1)
hi : (x.cast hd).simplex.1 i = j
⊢ ∃ x_1, (x.cast hd).simplex.1 (l.castSucc.succAbove x_1) = j

Tactic:
dsimp at hi

Goal state after:
case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
j : Fin (m + 1 + 1)
hj : ¬j = k.castSucc
i : Fin ((x.cast hd).dim + 1)
hi : (x.cast hd).simplex.1 i = j
⊢ ∃ x_1, (x.cast hd).simplex.1 (l.castSucc.succAbove x_1) = j
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_1
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ ((X₁ □ X₂) □ X₃).left ⟶ (X₁ □ X₂ □ X₃).left

Tactic:
exact pushout.desc ((α_ _ _ _).hom ≫ _ ◁ pushout.inl _ _ ≫ pushout.inl _ _)
        ((whiskerRightIso _ _).hom.left ≫
          pushout.desc (_ ◁ pushout.inr _ _ ≫ pushout.inl _ _) (pushout.inr _ _)
          (by simp [Limits.pushout.associator_naturality_left_condition]))
        (((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [Limits.pushout.whiskerLeft_condition_assoc, ← whisker_exchange_assoc,
            ← comp_whiskerRight_assoc])
          (by simp [← whisker_exchange_assoc, Limits.pushout.associator_naturality_left_condition,
            ← comp_whiskerRight_assoc]))

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

Goal state before:
pp: 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₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
by
    let hX₁ := IsInitial.isInitialObj (F.obj X₁) _ h
    let hY₁ := IsInitial.isInitialObj (F.obj Y₁) _ h
    apply +allowSynthFailures IsPushout.of_horiz_isIso
    · exact isIso_of_isInitial hX₁ hY₁ _
    · exact ⟨hX₁.hom_ext _ _⟩

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

Goal state before:
pp: case refine_2
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 2)
hs✝ : (s₁, objMk₁ i.succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ i.succ) ⋯ = OrderHom.id
⊢ ∃ a,
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a =
      ⟨(s₁, objMk₁ i.succ), hs✝⟩

Tactic:
obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last

Goal state after:
case refine_2.inl
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 1)
hs✝ : (s₁, objMk₁ i.castSucc.succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ i.castSucc.succ) ⋯ = OrderHom.id
⊢ ∃ a,
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a =
      ⟨(s₁, objMk₁ i.castSucc.succ), hs✝⟩

case refine_2.inr
p : ℕ
x✝ : ↑((Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1))
s₁ : Δ[p] _⦋p + 1⦌
hs✝ : (s₁, objMk₁ (Fin.last (p + 1)).succ) ∈ (Δ[p] ⊗ Δ[1]).nonDegenerate (p + 1)
hs : orderHomOfSimplex (s₁, objMk₁ (Fin.last (p + 1)).succ) ⋯ = OrderHom.id
⊢ ∃ a,
    (fun i ↦ ⟨(stdSimplex.objEquiv.symm (SimplexCategory.σ i), objMk₁ i.succ.castSucc), ⋯⟩) a =
      ⟨(s₁, objMk₁ (Fin.last (p + 1)).succ), hs✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
⊢ A.image f.map ≤ B

Tactic:
by
  rintro n _ ⟨a, ha, rfl⟩
  have := f.map_coe ⟨a, ha⟩
  aesop

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ IsZero ((X.normalizedChainComplex R).X n)

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ 𝟙 ((X.normalizedChainComplex R).X n) = 0
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 : k < j.castSucc.castSucc
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (const (opObjEquiv.symm x)))) = const x

Tactic:
simp [opObjEquiv_yonedaEquiv_const]

Goal state after:
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 : k < j.castSucc.castSucc
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = const x

Tactic:
rw [stdSimplex.δ_comp_yonedaEquiv_symm, δ_opObjEquiv,
      ← stdSimplex.yonedaEquiv_δ_comp, h.δ_map_of_gt _ (by grind)]
    simp [opObjEquiv_yonedaEquiv_const]

Goal state after:
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 (const (opObjEquiv.symm x)))) = const x

Tactic:
simp [opObjEquiv_yonedaEquiv_const]

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

Goal state before:
pp: 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₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_15 _proof_12).op)) x) =
    (ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x)

Tactic:
by
  apply (hY.spineEquiv 2).injective
  ext i
  fin_cases i
  · dsimp
    rw [spineEquiv_f₂_arrow_zero]
    simp [StrictSegal.spineEquiv, SimplexCategory.mkOfSucc_zero_eq_δ,
      ← Functor.map_comp_apply, ← op_comp]
  · dsimp
    rw [spineEquiv_f₂_arrow_one]
    dsimp [StrictSegal.spineEquiv]
    rw [← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_σ₂_one, op_comp,
      Functor.map_comp_apply, hσ, SimplexCategory.mkOfSucc_one_eq_δ,
      ← Functor.map_comp_apply, ← op_comp, δ₂_zero_comp_σ₂_one,
      op_comp, Functor.map_comp_apply, hδ₀]

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

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
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s,
    a ∈ s ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ∧ ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)

Tactic:
simp only [← and_assoc]

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
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s,
    (a ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ∧
      ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)
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
⊢ ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y

Tactic:
intro z hz hgz

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
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
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
⊢ dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : log (v b) / log (v a) < ↑q.num / ↑↑q.den
hq₂ : ↑q.num / ↑↑q.den < log (w b) / log (w a)
⊢ False

Tactic:
Rat.cast_natCast

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : log (v b) / log (v a) < ↑q.num / ↑q.den
hq₂ : ↑q.num / ↑q.den < log (w b) / log (w a)
⊢ False
Module: Mathlib.Analysis.Analytic.Order

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

Tactic:
rw [AnalyticAt.unique_eventuallyEq_pow_smul_nonzero h.choose_spec h']

Goal state after:
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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h✝ : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
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
hg_ne : ⋯.choose < n
this : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀
⊢ g =ᶠ[𝓝[≠] z₀] fun z ↦ (z - z₀) ^ (n - m) • h z

Tactic:
filter_upwards [self_mem_nhdsWithin, hm.filter_mono nhdsWithin_le_nhds,
          hfh.filter_mono nhdsWithin_le_nhds] with z hz hf' hf''

Goal state after:
𝕜 : 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₀
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
hg_ne : ⋯.choose < n
this : ContinuousAt (fun z ↦ (z - z₀) ^ (n - m) • h z) z₀
z : 𝕜
hz : z ∈ {z₀}ᶜ
hf' : f z = (z - z₀) ^ ⋯.choose • g z
hf'' : f z = (z - z₀) ^ n • h z
⊢ g z = (z - z₀) ^ (n - m) • h z
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 (f x') - ↑A.symm (f y') - ↑f'.symm (f x' - f y')‖ ≤
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - f y'‖

Tactic:
← Af x',

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
⊢ ‖↑A.symm (↑A x') - ↑A.symm (f y') - ↑f'.symm (↑A x' - f y')‖ ≤
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - f y'‖
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ ordinaryHypergeometricSeries 𝔸 a b c = ordinaryHypergeometricSeries 𝔸 b a c

Tactic:
unfold ordinaryHypergeometricSeries ordinaryHypergeometricCoefficient

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ (ofScalars 𝔸 fun n ↦
      (↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) =
    ofScalars 𝔸 fun n ↦
      (↑n !)⁻¹ * Polynomial.eval b (ascPochhammer 𝕂 n) * Polynomial.eval a (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ↑r = analyticOrderAt f (g z₀)
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = ↑r * ↑s

Tactic:
← ENat.natCast_mul,

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ↑r = analyticOrderAt f (g z₀)
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = ↑(r * s)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f * g) x

Tactic:
by
  simpa using hf.smul hg

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ↑k • (ascPochhammer ℕ k).smeval (r + 1) +
      (1 * (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)) =
    k • (ascPochhammer ℕ k).smeval (r + 1) +
      ((ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1))

Tactic:
simp_all only [Nat.cast_id, nsmul_eq_mul, one_mul]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (ascPochhammer ℕ (k + 1)).smeval (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r

Tactic:
ascPochhammer_succ_succ r k

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ (k + 1).factorial • multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r =
    (k + 1).factorial • multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) x ↔ MeromorphicAt f (x + c)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicAt f (x + c)

case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicAt f (x + c)
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) x