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

Goal state before:
pp: case «1»
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 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_15 _proof_12).op)) x))).arrow
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))).arrow
      ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
dsimp

Goal state after:
case «1»
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 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_15 _proof_12).op)) x))).arrow
      1 =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))).arrow 1
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := ⋯
x : E := ⋯
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] ⊆ {c + x}

Tactic:
apply Eq.subset

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := ⋯
x : E := ⋯
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
t t' : ℝ
htt' : t ≠ t'
N : {c + x} ∩ s = ∅
⊢ [c + x -[ℝ] c + t • y] ∩ [c + x -[ℝ] c + t' • y] = {c + x}
Module: Mathlib.Analysis.Normed.Module.Connected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := 2⁻¹ • (a + b)
x : E := 2⁻¹ • (b - a)
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c + -x -[ℝ] c + t • y] ∩ [c + -x -[ℝ] c + t' • y] ⊆ {c + -x}

Tactic:
apply Eq.subset

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
h : 1 < Module.rank ℝ E
s : Set E
hs : s.Countable
this : Nontrivial E
a : E
ha : a ∈ sᶜ
b : E
hb : b ∈ sᶜ
hab : a ≠ b
c : E := ⋯
x : E := ⋯
Ia : c - x = a
Ib : c + x = b
x_ne_zero : x ≠ 0
y : E
hy : LinearIndependent ℝ ![x, y]
A : {t | ([c + x -[ℝ] c + t • y] ∩ s).Nonempty}.Countable
t t' : ℝ
htt' : t ≠ t'
N : {c - x} ∩ s = ∅
⊢ [c + -x -[ℝ] c + t • y] ∩ [c + -x -[ℝ] c + t' • y] = {c + -x}
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv

Goal state before:
pp: case inl
𝕜 : 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
c : ℝ≥0
hE : Subsingleton E
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
refine ⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => ?_⟩
    simp [@Subsingleton.elim E hE x y]

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

Goal state before:
pp: case pos.mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0 → ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z

Tactic:
exact fun hz ↦ ⟨f, hf, hz.resolve_left <| not_not_intro hf, by simp⟩

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

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

Tactic:
dsimp

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

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

Tactic:
dsimp

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

Goal state before:
pp: case coe
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
⊢ r = 1

Tactic:
obtain ⟨F, hFa, hFne, hfF⟩ := (analyticOrderAt_eq_natCast (by fun_prop)).mp h

Goal state after:
case coe
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : ℕ
h : analyticOrderAt (fun x_1 ↦ f x_1 - f x) x = ↑r
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z - f x = (z - x) ^ r • F z
⊢ r = 1
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 * ‖y' - x'‖) ≤ ↑‖↑f'.symm‖₊ * (↑c * (↑(‖↑f'.symm‖₊⁻¹ - c)⁻¹ * ‖↑A y' - ↑A x'‖))

Tactic:
by
      gcongr
      rw [← dist_eq_norm, ← dist_eq_norm]
      exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩

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

Goal state before:
pp: X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
f : Edge x y
⊢ (descOfTruncation (homToNerveMk F)).map (homMk f) = eqToHom ⋯ ≫ F.map (homMk f) ≫ eqToHom ⋯

Tactic:
dsimp

Goal state after:
X : Truncated 2
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
x y : X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
f : Edge x y
⊢ (descOfTruncation (homToNerveMk F)).map (homMk f) =
    𝟙 (nerveEquiv (nerveEquiv.symm (F.obj (mk x)))) ≫ F.map (homMk f) ≫ 𝟙 (F.obj (mk y))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: X : Truncated 2
C : Type u
inst✝¹ : SmallCategory C
D : Type u
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ConcreteCategory.hom ((homToNerveMk (F ⋙ G)).app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom ((homToNerveMk F ≫ (truncation 2).map (nerveMap G)).app (op { obj := ⦋1⦌, property := ⋯ })))
      f.edge

Tactic:
dsimp

Goal state after:
X : Truncated 2
C : Type u
inst✝¹ : SmallCategory C
D : Type u
inst✝ : SmallCategory D
F : X.HomotopyCategory ⥤ C
G : C ⥤ D
x₀ x₁ : X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })
f : Edge x₀ x₁
⊢ (ConcreteCategory.hom ((homToNerveMk (F ⋙ G)).app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge =
    (ConcreteCategory.hom (((truncation 2).map (nerveMap G)).app (op { obj := ⦋1⦌, property := ⋯ })))
      ((ConcreteCategory.hom ((homToNerveMk F).app (op { obj := ⦋1⦌, property := ⋯ }))) f.edge)
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
⊢ analyticOrderAt (deriv f) z₀ = ⊤ ↔ analyticOrderAt f z₀ = ⊤

Tactic:
simp_rw [ENat.eq_top_iff_forall_ge, analyticOrderAt_deriv_ge_iff hf hzero]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
⊢ (∀ (m : ℕ), ↑m + 1 ≤ analyticOrderAt f z₀) ↔ ∀ (m : ℕ), ↑m ≤ analyticOrderAt f z₀
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 : ¬EventuallyConst g (𝓝 z₀)
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc

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₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℂ
⊢ (deriv sin / sin) x✝ = x✝.cot

Tactic:
Complex.deriv_sin,

Goal state after:
x✝ : ℂ
⊢ (cos / sin) x✝ = x✝.cot
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 g : 𝕜 → E
hf : MeromorphicOn f univ
h₁ : f =ᶠ[codiscrete 𝕜] g
⊢ MeromorphicOn g univ

Tactic:
exact hf.congr_codiscreteWithin (eventuallyEq_of_mem h₁ fun ⦃x⦄ a ↦ a) isOpen_univ

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
f : 𝕜 → E
inst✝⁵ : MeasurableSpace 𝕜
inst✝⁴ : SecondCountableTopology 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : MeasurableSpace E
inst✝¹ : CompleteSpace E
inst✝ : BorelSpace E
h : Meromorphic f
⊢ Measurable f

Tactic:
set s := {z : 𝕜 | AnalyticAt 𝕜 f z}
  have h₁ : sᶜ.Countable := by simpa using h.countable_compl_analyticAt
  have h₁' := h₁.to_subtype
  have h₂ : IsOpen s := isOpen_analyticAt 𝕜 f
  have h₃ : ContinuousOn f s := fun z hz ↦ hz.continuousAt.continuousWithinAt
  exact .of_union_range_cover (.subtype_coe h₂.measurableSet) (.subtype_coe h₁.measurableSet)
    (by simp [-mem_compl_iff]) h₃.domRestrict.measurable (measurable_of_countable _)

Goal state after:
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
⊢ HasDerivWithinAt f e (Iic a) a

Tactic:
have t_cont : ∀ y ∈ closure t, ContinuousWithinAt f t y := by
    rw [t_closure]
    intro y hy
    by_cases h : y = a
    · rw [h]; exact f_lim.mono ts
    · have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩
      exact (f_diff.continuousOn y this).mono ts

Goal state after:
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
⊢ HasDerivWithinAt f e (Iic a) a
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • choose r n = choose r k * choose (r - ↑k) (n - k)

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero n),
    nsmul_left_comm, ← descPochhammer_eq_factorial_smul_choose,
    ← Nat.choose_mul_factorial_mul_factorial hkn, ← smul_mul_smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, mul_nsmul',
    ← descPochhammer_eq_factorial_smul_choose, smul_mul_assoc]
  nth_rw 2 [← Nat.sub_add_cancel hkn]
  rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
    ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]

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

Goal state before:
pp: case convert_7
a : ℂ
this : binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ fun n ↦ iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0 / ↑n !
z : ℂ
hz : z ∈ Metric.ball 0 1
⊢ ‖(fun x ↦ x) z‖ < 1

Tactic:
simpa using hz

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
⊢ n.choose k • choose r n = choose r k * choose (r - ↑k) (n - k)

Tactic:
by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero n),
    nsmul_left_comm, ← descPochhammer_eq_factorial_smul_choose,
    ← Nat.choose_mul_factorial_mul_factorial hkn, ← smul_mul_smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, mul_nsmul',
    ← descPochhammer_eq_factorial_smul_choose, smul_mul_assoc]
  nth_rw 2 [← Nat.sub_add_cancel hkn]
  rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
    ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]

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

Goal state before:
pp: a : ℕ
z : ℂ
hz : z ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) 0 1
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖z‖ₑ

Tactic:
rw [← map_zero (z⁻¹ • 1 : ℂ →L[ℂ] ℂ)] at this

Goal state after:
a : ℕ
z : ℂ
hz : z ≠ 0
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖z‖ₑ
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε δ : ℝ≥0
s N : Set X
hεδ : ε ≤ δ
hε : IsCover ε s N
xy : X × X
hxy : xy ∈ {(x, y) | edist x y ≤ ↑ε}
⊢ xy ∈ {(x, y) | edist x y ≤ ↑δ}

Tactic:
dsimp at *

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε δ : ℝ≥0
s N : Set X
hεδ : ε ≤ δ
hε : IsCover ε s N
xy : X × X
hxy : edist xy.1 xy.2 ≤ ↑ε
⊢ edist xy.1 xy.2 ≤ ↑δ
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
x₀ : X
hx₀ : x₀ ∈ N
hcover : (x, x₀) ∈ {(x, y) | edist x y ≤ ↑ε}
⊢ ∃ y ∈ f '' N, (f x, y) ∈ {(x, y) | edist x y ≤ ↑(K₂ * ε)}

Tactic:
dsimp at *

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
x₀ : X
hx₀ : x₀ ∈ N
hcover : edist x x₀ ≤ ↑ε
⊢ ∃ y ∈ f '' N, edist (f x) y ≤ ↑K₂ * ↑ε
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthInf (u ⊓ v) = min (expGrowthInf u) (expGrowthInf v)

Tactic:
rw [expGrowthInf, expGrowthInf, expGrowthInf, ← liminf_min]

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

Goal state before:
pp: case neg.a
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : limsup (fun n ↦ ↑(v n) / ↑n) atTop ≠ 0
ha' : limsup (fun n ↦ ↑(v n) / ↑n) atTop ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ linearGrowthInf (u ∘ v) ≤ limsup (fun n ↦ ↑(v n) / ↑n) atTop * linearGrowthInf u

Tactic:
exact h.linearGrowthInf_comp_le ha ha'

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hs₀ : μ s ≠ 0
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
⊢ (μ s + μ t) / (μ s + μ t) = 1

Tactic:
ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hs₀ : μ s ≠ 0
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
⊢ 1 = 1