mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
H :
  ∀ (k : K),
    ∃ j_1 f, (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₁ k) = (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₂ k)
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂

Tactic:
let j₁ (k : K) : J := (H k).choose

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
H :
  ∀ (k : K),
    ∃ j_1 f, (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₁ k) = (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₂ k)
j₁ : K → J := fun k ↦ ⋯.choose
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂
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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
hy :
  ↑((ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)) ∈
    (f.filtration j).obj (op ⦋d⦌)
⊢ b ∈ ((f.filtration j).preimage x.map).obj (op ⦋d⦌)

Tactic:
x.ι_b_app_apply

Goal state after:
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 : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
hy : ↑((ConcreteCategory.hom (x.mapToSucc.app (op ⦋d⦌))) b) ∈ (f.filtration j).obj (op ⦋d⦌)
⊢ b ∈ ((f.filtration j).preimage x.map).obj (op ⦋d⦌)
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
hY : F.DenseAt Y
G : C ⥤ D
e : F ≅ G
⊢ (Cocone.precompose
          (((CostructuredArrow.mapNatIso e.symm).functor.associator (CostructuredArrow.proj F Y) F).symm ≪≫
              ((CostructuredArrow.mapNatIso e.symm).functor ⋙ CostructuredArrow.proj F Y).isoWhiskerLeft e).inv).obj
      (Cocone.whisker (CostructuredArrow.mapNatIso e.symm).functor
        ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y)) ≅
    (LeftExtension.mk (𝟭 D) G.rightUnitor.inv).coconeAt Y

Tactic:
by exact Cocone.ext (Iso.refl _)

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 : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op X₁))
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal Y₃
hX₁ : IsTerminal ((G.obj (op X₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op X₁)) Y₃ h
hY₁ : IsTerminal ((G.obj (op Y₁)).obj Y₃) := IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h
⊢ IsPullback (𝟙 ((G.obj (op X₁)).obj X₃))
    ((IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h).from ((G.obj (op X₁)).obj X₃)) ((G.obj (op X₁)).map f₃)
    ((G.map f₁.op).app Y₃)

Tactic:
apply +allowSynthFailures IsPullback.of_horiz_isIso

Goal state after:
case inst
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 : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op X₁))
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal Y₃
hX₁ : IsTerminal ((G.obj (op X₁)).obj Y₃) := ⋯
hY₁ : IsTerminal ((G.obj (op Y₁)).obj Y₃) := ⋯
⊢ IsIso ((G.map f₁.op).app Y₃)

case sq
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 : G.PullbackObjObj f₁ f₃
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op X₁))
inst✝ : PreservesLimitsOfShape (Discrete PEmpty.{1}) (G.obj (op Y₁))
h : IsTerminal Y₃
hX₁ : IsTerminal ((G.obj (op X₁)).obj Y₃) := ⋯
hY₁ : IsTerminal ((G.obj (op Y₁)).obj Y₃) := ⋯
⊢ CommSq (𝟙 ((G.obj (op X₁)).obj X₃)) ((IsTerminal.isTerminalObj (G.obj (op Y₁)) Y₃ h).from ((G.obj (op X₁)).obj X₃))
    ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
f : I ⟶ X
⊢ toSSetObj₀Equiv
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 1))
        (toSSetObj₁Equiv.symm f)) =
    toSSetObj₀Equiv (toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) 0))

Tactic:
by simp [← toSSetObj₁Equiv_apply_zero]

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

Goal state before:
pp: X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I

Tactic:
apply CartesianMonoidalCategory.hom_ext

Goal state after:
case h_fst
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

case h_snd
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I

Tactic:
apply CartesianMonoidalCategory.hom_ext

Goal state after:
case h_fst
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

case h_snd
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: case inr
α ι : Type u
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
ha : ℵ₀ ≤ a
this : t ⊆ ⋃ i, f i
⊢ #↑t ≤ a

Tactic:
calc #t ≤ #(⋃ i, f i) := mk_le_mk_of_subset this
      _ ≤ sum (fun i ↦ #(f i)) := mk_iUnion_le_sum_mk
      _ ≤ sum (fun _ ↦ a) := sum_le_sum _ _ h'f
      _ = #ι * a := by simp
      _ ≤ ℵ₀ * a := by grw [mk_le_aleph0]
      _ = a := aleph0_mul_eq ha

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

Goal state before:
pp: n✝ : ℕ
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 := ⦋2⦌, property := _proof_14 })) (y : Y.obj (op { obj := ⦋2⦌, property := _proof_14 })),
    f₁ ((ConcreteCategory.hom (X.map (δ₂ 2 _proof_12 _proof_15).op)) x) =
        (ConcreteCategory.hom (Y.map (δ₂ 2 _proof_12 _proof_15).op)) y →
      f₁ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_12 _proof_15).op)) y →
        f₁ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_12 _proof_15).op)) x) =
          (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_12 _proof_15).op)) y
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
n : (SimplexCategory.Truncated 2)ᵒᵖ
⊢ X.obj n ⟶ Y.obj n

Tactic:
by
  obtain ⟨⟨n⟩, hn⟩ := n
  match n with
  | 0 => exact ↾f₀
  | 1 => exact ↾f₁
  | 2 => exact ↾(f₂ f₀ f₁ hδ₁ hδ₀ hY)

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
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ ↑c * (↑f'symm.nnnorm * dist (f z) y) = ↑c * ↑f'symm.nnnorm * dist (f z) y

Tactic:
ring

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

Tactic:
ring

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
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ 1 - ↑f'symm.nnnorm * ↑c = 1 - ↑c * ↑f'symm.nnnorm

Tactic:
ring

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
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Jcf' : 1 - ↑f'symm.nnnorm * ↑c ≠ 0
⊢ dist (f b) y * ((↑c * ↑f'symm.nnnorm) ^ n * (1 - ↑f'symm.nnnorm * ↑c) + (1 - (↑c * ↑f'symm.nnnorm) ^ n)) =
    dist (f b) y * (1 - (↑c * ↑f'symm.nnnorm) ^ n * ↑f'symm.nnnorm * ↑c)

Tactic:
ring

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
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Ign :
  dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n.succ) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ ↑c * ↑f'symm.nnnorm * ((↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y) =
    ↑c * ↑f'symm.nnnorm * (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y

Tactic:
ring

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
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
n : ℕ
⊢ ↑f'symm.nnnorm * ((↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y) =
    ↑f'symm.nnnorm * dist (f b) y * (↑c * ↑f'symm.nnnorm) ^ n

Tactic:
ring

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
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
⊢ ↑‖↑f'.symm‖₊ * (↑c * (↑(‖↑f'.symm‖₊⁻¹ - c)⁻¹ * ‖↑A x' - ↑A y'‖)) =
    ↑‖↑f'.symm‖₊ * ↑(‖↑f'.symm‖₊⁻¹ - c)⁻¹ * ↑c * ‖↑A x' - ↑A y'‖

Tactic:
ring

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

Goal state before:
pp: case e'_9
x✝ : ℂ
⊢ 1 + x✝ = x✝ - -1

Tactic:
ring

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

Goal state before:
pp: case e'_11
⊢ 0 = 1 + -1

Tactic:
ring

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

Goal state before:
pp: case e'_9
x✝ : ℝ
⊢ 1 + x✝ = x✝ - -1

Tactic:
ring

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
inst✝ : SMulCommClass 𝕜 R E
x : 𝕜
f : 𝕜 → E
c : R
m : ℕ
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ m • f z) x
⊢ MeromorphicAt (c • f) x

Tactic:
exact ⟨m, by simpa [smul_comm _ c _] using hf.fun_const_smul⟩

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

Goal state before:
pp: case e'_9
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (x * I) * (1 * I) + cexp (-x * I) * (-1 * I)) * 2⁻¹

Tactic:
ring

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 : ℕ
⊢ r * (ascPochhammer ℕ k).smeval (r + 1) +
      (↑↑k * (ascPochhammer ℕ k).smeval (r + 1) + 1 * (ascPochhammer ℕ k).smeval (r + 1)) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)

Tactic:
rw [← @nsmul_eq_mul, @add_rotate', @succ_nsmul, add_assoc]

Goal state after:
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))
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
h : MeromorphicAt (f ∘ fun x ↦ x + c) x
⊢ x = x + c - c

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n : ℕ
⊢ 0 = (n + 1).factorial • 0

Tactic:
smul_zero

Goal state after:
n : ℕ
⊢ 0 = 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n k : ℕ
⊢ 0 = (n + k + 1).factorial • 0

Tactic:
smul_zero

Goal state after:
n k : ℕ
⊢ 0 = 0
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: n k : ℕ
h : n < k
⊢ 0 = k.factorial • 0

Tactic:
smul_zero

Goal state after:
n k : ℕ
h : n < k
⊢ 0 = 0
Module: Mathlib.Analysis.Meromorphic.Basic

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

Tactic:
rw [Meromorphic, Meromorphic, (Equiv.subRight c).surjective.forall]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
⊢ (∀ (x : 𝕜), MeromorphicAt (f ∘ fun x ↦ x + c) ((Equiv.subRight c) x)) ↔ ∀ (x : 𝕜), MeromorphicAt f x
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[<] a
f_lim' : Tendsto (fun x ↦ deriv f x) (𝓝[<] a) (𝓝 e)
b : ℝ
ba : b ∈ Iio a
sab : Ico b a ⊆ s
t : Set ℝ := Ioo b a
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc b a
t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y
t_diff' : Tendsto (fun x ↦ fderiv ℝ f x) (𝓝[t] a) (𝓝 (smulRight 1 e))
this : HasDerivWithinAt f e (Icc b a) a
⊢ HasDerivWithinAt f e (Iic a) a

Tactic:
exact this.mono_of_mem_nhdsWithin (Icc_mem_nhdsLE ba)

Goal state after: