mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ { toPrefunctor := e.inv, map_id := ⋯ } ≫ { toPrefunctor := e.hom, map_id := h_id } = 𝟙 (of W)

Tactic:
apply forgetToQuiv.map_injective

Goal state after:
V W : Type u
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ forgetToQuiv.map ({ toPrefunctor := e.inv, map_id := ⋯ } ≫ { toPrefunctor := e.hom, map_id := h_id }) =
    forgetToQuiv.map (𝟙 (of W))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝ : Category.{u, u} C
F G : X ⟶ (truncation 2).obj (nerve C)
h : map F = map G
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })
f : Truncated.Edge x₀ x₁
⊢ (ConcreteCategory.hom (F.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom (G.app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge

Tactic:
simpa using congr_arg Truncated.Edge.edge (ReflPrefunctor.congr_hom h f)

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
⊢ r.degHom f ≤ r.deg Y

Tactic:
by
  simpa using r.degHom_le f (𝟙 Y)

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
e✝ : X✝ ≅ Y✝
X Y : C
e : X ≅ Y
⊢ r.degHom (𝟙 X) ≤ r.deg Y

Tactic:
← e.hom_inv_id

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
e✝ : X✝ ≅ Y✝
X Y : C
e : X ≅ Y
⊢ r.degHom (e.hom ≫ e.inv) ≤ r.deg Y
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L₁ L₂ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + L₂.length = m₂
⊢ standardσ L₁ h ≫ standardσ L₂ h' = standardσ (L₂ ++ L₁) ⋯

Tactic:
induction L₂ generalizing L₁ m₁ m₂ m₃ with

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
⊢ (ConcreteCategory.hom m).toFun x = (ConcreteCategory.hom (↾fun x ↦ lift sx s x)).toFun x

Tactic:
apply sx.spineInjective (X := X)

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
⊢ (sx.spineEquiv n) ((ConcreteCategory.hom m).toFun x) =
    (sx.spineEquiv n) ((ConcreteCategory.hom (↾fun x ↦ lift sx s x)).toFun x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
x y : A.N
⊢ x = y ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }

Tactic:
by
  rw [N.ext_iff, SSet.N.ext_iff]

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X i)) (y.cast ⋯).simplex = (x.cast hd).simplex

Tactic:
by
  simpa only [S.cast, iff] using hxy.cast hd

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
this : Mono (yonedaEquiv.symm ((ConcreteCategory.hom (f.app (op ⦋n⦌))) x))
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)

Tactic:
← SSet.yonedaEquiv_symm_comp

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n
this : Mono (yonedaEquiv.symm x ≫ f)
⊢ Mono (yonedaEquiv.symm ↑⟨x, hx✝⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsRegular
this : IsEmpty { f // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }

Tactic:
exact ⟨fun ⟨f, hf⟩ ↦ this.false
      ⟨fun n ↦ h.equivII.symm (f n), fun n ↦ by simpa [ancestralRel_iff] using hf n⟩⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
⊢ P.rank' hy = ⨆ x, P.rank' ⋯ + 1

Tactic:
by
  change P.rank' (Acc.intro y fun _ => hy.inv) = _
  rfl

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ P.IsRegular ↔ Nonempty (P.RankFunction ℕ)

Tactic:
rw [← isRegular_pairing_iff, Pairing.isRegular_iff_nonempty_rankFunction]
  exact (P.rankFunctionEquiv ℕ).symm.nonempty_congr

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
⊢ ((-1) ^ ↑x.1 * (-1) ^ ↑x.2) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
    ((-1) ^ ↑x.2 * (-1) ^ ↑x.1) • H.h x.1.castSucc ≫ Y.δ x.2.succ

Tactic:
rw [mul_comm]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ Sᶜ
⊢ ((-1) ^ ↑x.1 * (-1) ^ ↑x.2) • H.h x.1.succ ≫ Y.δ x.2.castSucc =
    ((-1) ^ ↑x.2 * (-1) ^ ↑x.1) • H.h x.1.succ ≫ Y.δ x.2.castSucc

Tactic:
rw [mul_comm]

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

Goal state before:
pp: case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
⊢ ↑c.s ≤ ↑(P.p c'.s)

Tactic:
rw [← ofSimplex_le_iff] at h
    rwa [Subcomplex.N.le_iff, SSet.N.le_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ S
⊢ ((-1) ^ ↑x.1 * (-1) ^ ↑x.2) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
    ((-1) ^ ↑x.2 * (-1) ^ ↑x.1) • H.h x.1.castSucc ≫ Y.δ x.2.succ

Tactic:
rw [mul_comm]

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
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
⊢ k.succ ≤ (x.cast hd).simplex.1 i ↔ l.succ ≤ i

Tactic:
refine ⟨fun hi ↦ ?_, fun hi ↦ ?_⟩
  · by_contra!
    rw [← not_lt] at hi
    apply hi
    rw [← Fin.le_castSucc_iff] at this ⊢
    conv_rhs => rw [← hl.simplex_fst_castSucc]
    exact stdSimplex.monotone_apply _ this
  · rw [← hl.simplex_fst_succ]
    exact stdSimplex.monotone_apply _ hi

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
hx : IsType₂ x
d : ℕ
hd : x.dim = d
⊢ objEquiv ((ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) (min x hd).castSucc)) (hx.simplex hd)) =
    objEquiv (x.cast hd).simplex

Tactic:
ext i : 2

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
⊢ (objEquiv ((ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) (min x hd).castSucc)) (hx.simplex hd))) i =
    (objEquiv (x.cast hd).simplex) i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ objEquiv ((ht.type₁ ⋯).x.cast ⋯).simplex = objEquiv (s.x.cast ⋯).simplex

Tactic:
ext i : 2

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
i : Fin (((ht.type₁ ⋯).x.cast ⋯).dim + 1)
⊢ (objEquiv ((ht.type₁ ⋯).x.cast ⋯).simplex) i = (objEquiv (s.x.cast ⋯).simplex) i
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₃
⊢ {
            app := fun X₂ ↦
              Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                  (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                ⋯,
            naturality := ⋯ }.app
        ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
      (G.leibnizPullback.obj (op X₁)).map
        ({
              app := fun X₃ ↦
                Arrow.homMk
                  (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left))
                    (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)))
                    ⋯)
                  (adj₂.homEquiv.symm
                    (pullback.snd ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                      ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                  ⋯,
              naturality := ⋯ }.app
          x✝) =
    𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)

Tactic:
ext
    · simp [← homEquiv_naturality_three]
    · apply pullback.hom_ext <;> simp [← homEquiv_naturality_three]

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:
by
  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.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_4
inst✝⁴ : NormedRing R
inst✝³ : Module R E
inst✝² : IsBoundedSMul R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
z : 𝕜
⊢ (z - x) ^ (m + n) • f z • g z = ((z - x) ^ m • f z) • (z - x) ^ n • g z

Tactic:
smul_smul_smul_comm,

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_4
inst✝⁴ : NormedRing R
inst✝³ : Module R E
inst✝² : IsBoundedSMul R E
x : 𝕜
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : IsScalarTower 𝕜 R E
f : 𝕜 → R
g : 𝕜 → E
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x
z : 𝕜
⊢ (z - x) ^ (m + n) • f z • g z = ((z - x) ^ m • (z - x) ^ n) • f z • g z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
⊢ derivWithin (fun x ↦ 0 ^ f x) s x = 0

Tactic:
apply derivWithin_zero_of_frequently_mem {0, 1} (mt Set.Infinite.of_accPt (by simp))

Goal state after:
case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
⊢ ∃ᶠ (y : ℂ) in 𝓝[s \ {x}] x, 0 ^ f y ∈ {0, 1}
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
⊢ ↑x ^ r = ?inl.convert_3 / (r + 1)

pp: case inl.convert_3
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ ℂ

pp: case inl.convert_4
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y ↦ y ^ (r + 1)) ?inl.convert_3 ↑x

Tactic:
· exact (mul_div_cancel_right₀ _ hr).symm

Goal state after:
case inl.convert_4
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun y ↦ y ^ (r + 1)) (↑x ^ r * (r + 1)) ↑x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
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)
⊢ HasDerivAt (fun y ↦ ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x

Tactic:
refine HasDerivAt.congr_of_eventuallyEq ?_ this

Goal state after:
case inr
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)
⊢ HasDerivAt (fun x ↦ (-↑x) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)) (↑x ^ r) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: a x : ℝ
ha : a < 0
⊢ HasStrictDerivAt (fun x ↦ a ^ x) (a ^ x * log a - rexp (log a * x) * sin (x * π) * π) x

Tactic:
by
  simpa using! (hasStrictFDerivAt_rpow_of_neg (a, x) ha).comp_hasStrictDerivAt x
    ((hasStrictDerivAt_const _ _).prodMk (hasStrictDerivAt_id _))

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ edist x y ≤ edist (f x) (f y) * ↑K₁

Tactic:
rw [mul_comm]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ edist x y ≤ ↑K₁ * edist (f x) (f y)
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
hI : I.Finite
s : Set X
t : ι → Set X
⊢ AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i)

Tactic:
simpa only [@comm _ _ s] using finite_iUnion_left_iff hI

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

Goal state before:
pp: case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ Real.log (x * y).toReal = Real.log x.toReal + Real.log y.toReal

pp: case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < (x * y).toReal

Tactic:
ENNReal.toReal_mul

Goal state after:
case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ Real.log (x.toReal * y.toReal) = Real.log x.toReal + Real.log y.toReal

case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ 0 < (x * y).toReal
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthSup u + linearGrowthInf v ≤ linearGrowthSup (u + v)

Tactic:
refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))

Goal state after:
u v : ℕ → EReal
n : ℕ
⊢ ((fun n ↦ u n / ↑n) + fun n ↦ v n / ↑n) n = (u + v) n / ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: x✝ : ℕ
⊢ log 0 = ⊥

Tactic:
log_zero

Goal state after:
x✝ : ℕ
⊢ ⊥ = ⊥
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case refine_2
α : 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 : ℤ), f =O[l] fun a ↦ k a ^ z
z : ℤ
⊢ Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
· suffices (fun a : α => k a ^ z * f a) =O[l] fun a : α => (k a)⁻¹ from
      IsBigO.trans_tendsto this hk.inv_tendsto_atTop
    refine ((isBigO_refl (fun a => k a ^ z) l).mul (h (-(z + 1)))).trans ?_
    refine .of_bound' <| hk0.mono fun a ha0 => ?_
    simp [← zpow_add₀ ha0]

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v)

Tactic:
refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))

Goal state after:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((fun n ↦ (u n).log / ↑n) + fun n ↦ (v n).log / ↑n) n = ((u * v) n).log / ↑n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case inl
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m = ⊤
⊢ 0 ≤ linearGrowthInf fun x ↦ u m

pp: case inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m ≠ ⊤
⊢ 0 ≤ linearGrowthInf fun x ↦ u m

Tactic:
· rw [hum', ← Pi.top_def, linearGrowthInf_top]; exact le_top

Goal state after:
case inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m ≠ ⊤
⊢ 0 ≤ linearGrowthInf fun x ↦ u m
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun n ↦ ↑(v n)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
n : ℕ
vn_a' : ↑(v n) / ↑n < a'
n_0 : 0 < n
⊢ ↑(v n) ≤ a' * ↑n

Tactic:
rw [mul_comm]

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun n ↦ ↑(v n)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
n : ℕ
vn_a' : ↑(v n) / ↑n < a'
n_0 : 0 < n
⊢ ↑(v n) ≤ ↑n * a'