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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk (e.tensor (Edge.id (y, z))) ≫
      𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x₁)).obj
              (mk y)).obj
          (mk z)) =
    𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x₀)).obj
              (mk y)).obj
          (mk z)) ≫
      (inverse X (Y ⊗ Z)).map (Prod.mkHom (homMk e) ((inverse Y Z).map (𝟙 (mk y), 𝟙 (mk z))))

Tactic:
simp only [Category.comp_id, Category.id_comp, ← prod_id',
          CategoryTheory.Functor.map_id, inverse_obj, inverse_map_mkHom_homMk_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
i : Fin (y.len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom
          (𝟙 (WithInitial.of y) ≫
            𝟙 (WithInitial.of y) ≫ SimplexCategory.Hom.mk (Fin.natAddOrderEmb (x.len + 1)).toOrderHom ≫ eqToHom ⋯))
        i) =
    ↑(Fin.cast ⋯ (Fin.natAdd (x.len + 1) i))

Tactic:
simp [OrderEmbedding.toOrderHom]

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

Goal state before:
pp: case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
⊢ (∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) →
    { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }

Tactic:
rintro ⟨i, h₁, h₂⟩

Goal state after:
case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ : (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
h₂ : ∀ (y_1 : Fin (d + 2)), (fun i ↦ (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) y_1 → y_1 = i
⊢ { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ ↑((ConcreteCategory.hom (c.mapToSucc.app (op ⦋c.dim + 1⦌))) (stdSimplex.objEquiv.symm (𝟙 ⦋c.dim + 1⦌))) =
    ((↑(P.p c.s)).cast ⋯).simplex

Tactic:
apply yonedaEquiv_symm_app_id

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
left✝ : Mono A.ι
P : (Subcomplex.range A.ι).Pairing
h✝ : P.IsRegular
⊢ ∃ B P, P.IsRegular ∧ B = A

Tactic:
exact ⟨_, P, inferInstance, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: A B X Y : SSet
i : A ⟶ B
hi : innerHornInclusions i
f : X ⟶ Y
hf : RelativeCellComplex (fun x ↦ innerHornInclusions.homFamily) f
⊢ IsFinitelyPresentable A

Tactic:
simp only [innerHornInclusions_eq_iSup, iSup_iff] at hi

Goal state after:
A B X Y : SSet
i : A ⟶ B
f : X ⟶ Y
hf : RelativeCellComplex (fun x ↦ innerHornInclusions.homFamily) f
hi : ∃ i_1, ofHoms (fun p ↦ Λ[i_1 + 2, ↑p].ι) i
⊢ IsFinitelyPresentable A
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)
⊢ (x.cast hd).simplex.1 i ≤ k.castSucc ↔ i < min x hd

Tactic:
contrapose!

Goal state after:
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
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : InnerFibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃' : internalHom.PullbackObjObj Λ[n✝ + 2, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[n✝ + 2, k].ι p
⊢ HasLiftingProperty i sq₁₃'.π

Tactic:
suffices (MorphismProperty.monomorphisms _).rlp sq₁₃'.π from this _ inferInstance

Goal state after:
X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : InnerFibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃' : internalHom.PullbackObjObj Λ[n✝ + 2, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[n✝ + 2, k].ι p
⊢ (MorphismProperty.monomorphisms SSet).rlp sq₁₃'.π
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)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃' : internalHom.PullbackObjObj Λ[m + 1, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[m + 1, k].ι p
⊢ HasLiftingProperty i sq₁₃'.π

Tactic:
suffices (MorphismProperty.monomorphisms _).rlp sq₁₃'.π from this _ inferInstance

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].ι
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃' : internalHom.PullbackObjObj Λ[m + 1, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[m + 1, k].ι p
⊢ (MorphismProperty.monomorphisms SSet).rlp sq₁₃'.π
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
⊢ Fibration sq₁₃.π

Tactic:
by
  rw [fibration_iff]
  intro _ _ _ h
  simp only [J, MorphismProperty.iSup_iff] at h
  obtain ⟨m, ⟨k⟩⟩ := h
  let sq₁₂ := Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
  rw [← internalHomAdjunction₂.hasLiftingProperty_iff sq₁₂]
  suffices anodyneExtensions sq₁₂.ι from
    this _ (by rwa [← HomotopicalAlgebra.fibration_iff])
  intro E B p hp
  rw [HasLiftingProperty.iff_of_arrow_iso_left
    (show Arrow.mk sq₁₂.ι ≅ Arrow.mk sq₁₂.flipTensor.ι from
      Arrow.isoMk (Iso.refl _) (β_ _ _))]
  let sq₁₃' := Functor.PullbackObjObj.ofHasPullback MonoidalClosed.internalHom Λ[m + 1, k].ι p
  rw [internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃']
  suffices (MorphismProperty.monomorphisms _).rlp sq₁₃'.π from this _ inferInstance
  rw [rlp_monomorphisms]
  rintro _ _ _ ⟨n⟩
  rw [← internalHomAdjunction₂.hasLiftingProperty_iff
    (Subcomplex.unionProd.pushoutObjObj.{u} _ _),
    Subcomplex.unionProd.pushoutObjObj_ι]
  exact prodStdSimplex.anodyneExtensions_unionProd_ι _ _ _ hp

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

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
Y : WalkingIso
f : zero ⟶ Y
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
induction Y

Goal state after:
case zero.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ zero
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

case zero.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : zero ⟶ one
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
Y : WalkingIso
f : one ⟶ Y
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
induction Y

Goal state after:
case one.zero
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ zero
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

case one.one
C : Type u
inst✝ : Category.{v, u} C
F : WalkingIso ⥤ C
f : one ⟶ one
⊢ ((fun p ↦ fromIso p.snd.snd) ((fun F ↦ ⟨F.obj zero, ⟨F.obj one, toIso F⟩⟩) F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
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 m : ℕ
k : Fin (m + 1)
n : ℕ
s t : Type₁ k n
h :
  { dim := s.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex } =
    { dim := t.d,
      simplex := (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) t.index.castSucc)) (t.x.cast ⋯).simplex }
⊢ s = t

Tactic:
by
    replace h : s.δ = t.δ := by rwa [Subcomplex.N.ext_iff, N.ext_iff]
    generalize hs : s.δ = u
    have hu' : IsType₂ u := by simpa only [hs] using s.isType₂_δ
    rw [← hu'.type₁_eq_of_δ_eq _ hs rfl,
      hu'.type₁_eq_of_δ_eq _ (h.symm.trans hs) rfl]

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₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₃ : Arrow C₃
⊢ (F.map X₁.hom).app ((G.leibnizPullback.obj (op X₁)).obj X₃).left ≫
      adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left) =
    (F.obj X₁.left).map ((G.leibnizPullback.obj (op X₁)).obj X₃).hom ≫
      adj₂.homEquiv.symm
        (pullback.fst ((G.obj (op (unop (op X₁)).left)).map X₃.hom) ((G.map (unop (op X₁)).hom.op).app X₃.right))

Tactic:
simp [← homEquiv_symm_naturality_one, ← homEquiv_symm_naturality_two]

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

Goal state before:
pp: 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✝⟩

Tactic:
exact ⟨i, nonDegenerate_ext₂ rfl rfl⟩

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

Goal state before:
pp: case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 2)
n : ℕ
hk : k ≠ Fin.last (m + 1)
⊢ (pairing k n).IsRegular

Tactic:
obtain ⟨k, rfl⟩ := Fin.eq_castSucc_of_ne_last hk

Goal state after:
case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
k : Fin (m + 1)
hk : k.castSucc ≠ Fin.last (m + 1)
⊢ (pairing k.castSucc n).IsRegular
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 : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ dist (f (g z)) y = ‖f (z + v) - y‖

Tactic:
rw [dist_eq_norm]

Goal state after:
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 g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
hf : AnalyticAt 𝕜 f z₀
n : ℕ
x✝ : 𝕜 → E
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • x✝ z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, g z = (z - z₀) ^ n • x✝ z

Tactic:
exact hfg.congr_left

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
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
⊢ f '' s ∈ 𝓝 (f x)

Tactic:
obtain ⟨t, hts, ht, xt⟩ : ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := _root_.mem_nhds_iff.1 hs
  grw [← hts]
  exact IsOpen.mem_nhds ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt)

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

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ (x - x) ^ r • deriv F x + deriv (fun x_1 ↦ (x_1 - x) ^ r) x • F x = 0

Tactic:
deriv_fun_pow (by fun_prop),

Goal state after:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hf' : 1 < r
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ r • F z + f x
⊢ (x - x) ^ r • deriv F x + (↑r * (x - x) ^ (r - 1) * deriv (fun x_1 ↦ x_1 - x) x) • F x = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
k n : ℕ
inst✝ : CharZero 𝕜
⊢ ↑n = analyticOrderAt f z₀ → n ≠ 0 → k ≤ n → analyticOrderAt (deriv^[k] f) z₀ = ↑(n - k)

Tactic:
induction k generalizing n with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: z : ℂ
m : z ∈ slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 z, DifferentiableAt ℂ log z

Tactic:
filter_upwards [isOpen_slitPlane.eventually_mem m]

Goal state after:
z : ℂ
m : z ∈ slitPlane
⊢ ∀ a ∈ slitPlane, DifferentiableAt ℂ log a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: z✝ : ℂ
m✝ : z✝ ∈ slitPlane
z : ℂ
m : z ∈ slitPlane
⊢ DifferentiableAt ℂ log z

Tactic:
exact differentiableAt_id.clog m

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

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
kn : ℕ
hkn : kn < n
⊢ ↑kn ≠ -c

Tactic:
by simp [habc kn hkn]

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

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
kn : ℕ
hkn : kn < n
⊢ ↑kn ≠ -b

Tactic:
by simp [habc kn hkn]

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

Goal state before:
pp: 𝕂 : Type u_1
inst✝ : RCLike 𝕂
a b c : 𝕂
n : ℕ
habc : ∀ kn < n, ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c
kn : ℕ
hkn : kn < n
⊢ ↑kn ≠ -a

Tactic:
by simp [habc kn hkn]

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

Goal state before:
pp: 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
z : ℂ
hz : z ∈ B
⊢ derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B z =
    derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B z

Tactic:
derivWithin_congr (fun _ hz ↦ ih hz) (ih hz)

Goal state after:
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
z : ℂ
hz : z ∈ B
⊢ derivWithin (fun x ↦ (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) x) B z =
    derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B z
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 + (r - ij.1 • 1))

Tactic:
Nat.cast_comm,

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) =
    (s - ij.2 • 1 + (r - ij.1 • 1)) * ↑((ij.1 + ij.2).choose ij.1)
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

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
p : FormalMultilinearSeries 𝕜 E F
k n : ℕ
h : p (n + k) = 0
⊢ p.iteratedFDerivSeries k n = 0

Tactic:
induction k generalizing n with

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

Tactic:
obtain ⟨N, hNA, hN_finite, hN⟩ := hs ε (by positivity)

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y ↑ε
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case neg
x : ℝ≥0∞
hx_top : ¬x = ∞
⊢ x.log.exp = x

Tactic:
by_cases hx_zero : x = 0

Goal state after:
case pos
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : x = 0
⊢ x.log.exp = x

case neg
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
⊢ x.log.exp = x
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case neg
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
⊢ ENNReal.ofReal (Real.exp (Real.log x.toReal)) = ENNReal.ofReal x.toReal

Tactic:
Real.exp_log hx_pos

Goal state after:
case neg
x : ℝ≥0∞
hx_top : ¬x = ∞
hx_zero : ¬x = 0
hx_pos : 0 < x.toReal
⊢ ENNReal.ofReal x.toReal = ENNReal.ofReal x.toReal
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
x : X
hx : x ∈ s
⊢ (∀ ε > 0, ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε) ↔ ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x

Tactic:
simp [frequently_filterAt_iff, ← and_assoc, and_right_comm]

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

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : u = ⊥
⊢ (linearGrowthInf fun n ↦ ↑(v n)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)

Tactic:
rw [u_0, linearGrowthSup_bot, mul_bot_of_pos v_0]; exact bot_le

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
a : ι
ha : a ∈ t'
⊢ r a ≤ 1

Tactic:
apply ha.2.trans (hR1 (c a))

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))

Tactic:
· ext t
    rw [withDensity_indicator hs, ← restrict_withDensity hs, ← Measure.restrict_add,
      ← μ.haveLebesgueDecomposition_add ν]

Goal state after: