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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ IsIso (Subcomplex.toOfSimplex x)

Tactic:
rw [Subcomplex.isIso_toOfSimplex_iff]

Goal state after:
X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Mono (yonedaEquiv.symm 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✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ f.filtration (Order.succ i) = f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex

Tactic:
apply le_antisymm

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ f.filtration (Order.succ i) ≤ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex

case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : SuccOrder ι
i : ι
hi : ¬IsMax i
⊢ f.filtration i ⊔ ⨆ c, (↑(P.p c.s)).subcomplex ≤ f.filtration (Order.succ i)
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✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ f.filtration i = ⨆ j, ⨆ (_ : j < i), f.filtration j

Tactic:
apply le_antisymm

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ f.filtration i ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j

case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ ⨆ j, ⨆ (_ : j < i), f.filtration j ≤ f.filtration i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j ∧
    ∀ i_1 < i, ∀ (i_3 : f.Cell i_1), (↑(P.p i_3.s)).subcomplex ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j

Tactic:
refine ⟨?_, fun j hj c ↦ ?_⟩

Goal state after:
case a.refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j

case a.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
c : f.Cell j
⊢ (↑(P.p c.s)).subcomplex ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j
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✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ i, f.filtration ↑i = f.filtration m

Tactic:
apply le_antisymm

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ⨆ i, f.filtration ↑i ≤ f.filtration m

case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ f.filtration m ≤ ⨆ i, f.filtration ↑i
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
j : ι
c : f.Cell j
⊢ (f.filtration j).preimage c.map = c.horn

Tactic:
apply le_antisymm

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ (f.filtration j).preimage c.map ≤ c.horn

case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ c.horn ≤ (f.filtration j).preimage c.map
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a.notMem.refine_2.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ ↑t < ↑(P.p c.s)

Tactic:
Subcomplex.N.lt_iff,

Goal state after:
case a.notMem.refine_2.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ (↑t).toN < (↑(P.p c.s)).toN
Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable

Goal state before:
pp: C : Type u
hC : Category.{v, u} C
inst✝ : IsAccessibleCategory.{w, v, u} C
X : C
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal C

Goal state after:
C : Type u
hC : Category.{v, u} C
inst✝ : IsAccessibleCategory.{w, v, u} C
X : C
κ : Cardinal.{w}
w✝ : Fact κ.IsRegular
h✝ : IsCardinalAccessibleCategory C κ
⊢ IsPresentable.{w, v, u} X
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
X✝ Y✝ Z✝ : ↑h.smallCategoryOfSet.obj
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ h.homEquiv (x✝¹ ≫ x✝) = h.homEquiv x✝¹ ≫ h.homEquiv x✝

Tactic:
by rw [SmallCategoryOfSet.comp_def]; simp

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)
⊢ ¬l.succ ≤ i ↔ i < l.succ

Tactic:
not_le

Goal state after:
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)
⊢ i < l.succ ↔ i < l.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

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

Tactic:
rw [Fin.succAbove_castSucc_self, ← hi, ← hl.simplex_snd_succ]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
inst✝ : X.IsConnected
⊢ IsIso (X.homology₀ε R)

Tactic:
dsimp [homology₀ε]
  simp only [isIso_comp_left_iff]
  let x : π₀ X := Classical.arbitrary _
  refine ⟨Sigma.ι (fun _ ↦ R) x, ?_, by simp⟩
  ext y
  obtain rfl : x = y := by subsingleton
  simp

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ j.castSucc.castSucc.succ ≤ i.succ.castSucc

Tactic:
by simpa using! Fin.le_of_lt hij

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

Goal state before:
pp: X : SSet
s : Cocone X.functorN
m : X.coconeN.pt ⟶ s.pt
hm : ∀ (j : X.N), X.coconeN.ι.app j ≫ m = s.ι.app j
⊢ m = desc s

Tactic:
rw [← cancel_epi (Subcomplex.topIso X).hom]
    exact Multicofork.IsColimit.hom_ext (multicoequalizerDiagram X).isColimit
      (fun x ↦ (hm _).trans (fac s x).symm)

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Nonempty (Unique (ZerothHomotopy ↑X))

Tactic:
unique_iff_subsingleton_and_nonempty

Goal state after:
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X) ∧ Nonempty (ZerothHomotopy ↑X)
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
R : C
⊢ (singularChainComplexFunctorAdjunction C n).unit.app R =
    Sigma.ι (fun x ↦ R)
      ((ConcreteCategory.hom ((stdSimplexToTop.app ⦋n⦌).app (Opposite.op ⦋n⦌))) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)))

Tactic:
dsimp [singularChainComplexFunctorAdjunction, Adjunction.ofNatIsoRight,
    Adjunction.equivHomsetRightOfNatIso, Adjunction.homEquiv,
    Adjunction.comp, singularChainComplexFunctor,
    SSet.chainComplexFunctorAdjunction, SSet.chainComplexFunctor]
  simp [stdSimplexToTop]
  rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑Set.univ ≤ a

Tactic:
exact mk_subtype_le_of_countable_eventually_mem (l := l) (fun x _ ↦ ht x) h'f

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ #α = a

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ #α ≤ a

case a
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) = a
⊢ a ≤ #α
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ Tendsto (fun n ↦ c⁻¹ ^ n) atTop (𝓝 0)

Tactic:
apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
x : E
⊢ ‖c⁻¹‖ < 1
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
⊢ #↑s = #E

Tactic:
have A : ∀ (x : E), ∀ᶠ n in (atTop : Filter ℕ), x ∈ c ^ n • s := by
    intro x
    have : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 ((0 : 𝕜) • x)) := by
      have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) := by
        simp_rw [← inv_pow]
        apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one
        rw [norm_inv]
        exact inv_lt_one_of_one_lt₀ hc
      exact Tendsto.smul_const this x
    rw [zero_smul] at this
    filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)
    exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Zero E
inst✝² : MulActionWithZero 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : 1 < ‖c‖
cn_ne : ∀ (n : ℕ), c ^ n ≠ 0
A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s
⊢ #↑s = #E
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1

Tactic:
let c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
⊢ ∃ k, 1 < (v i) k ∧ (∀ (j : ι), j ≠ i → (v j) k < 1) ∧ w k < 1
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁷ : Field R
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
inst✝¹ : OrderTopology S
ι : Type u_3
inst✝ : Finite ι
v : ι → AbsoluteValue R S
w : AbsoluteValue R S
a b : R
i : ι
ha : 1 < (v i) a
haj : ∀ (j : ι), j ≠ i → (v j) a < 1
haw : 1 < w a
hb : 1 < (v i) b
hbw : w b < 1
c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop (𝓝 ((v i) b))
hcₙ : Tendsto (fun n ↦ w (c n)) atTop (𝓝 (w b))
hcⱼ : ∀ (j : ι), j ≠ i → ∀ s ∈ {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}, 0 ∈ s → ∃ a, ∀ (b : ℕ), a ≤ b → (v j) (c b) ∈ s
r₁ : ℕ
hr₁ : ∀ (b : ℕ), r₁ ≤ b → 1 < (v i) (c b)
rₙ : (j : ι) → j ≠ i → ℕ
hrₙ : ∀ (j : ι) (hj : j ≠ i) (b : ℕ), rₙ j hj ≤ b → (v j) (c b) ∈ Set.Iio 1
rN : ℕ
hrN : ∀ (b : ℕ), rN ≤ b → w (c b) < 1
this : Fintype ι
r : ℕ := max (Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h) rN
⊢ r₁ ≤ r

Tactic:
exact le_max_iff.2 <| .inl <|
      Finset.le_sup_dite_pos (p := fun j ↦ j = i) (f := fun _ _ ↦ r₁) (Finset.mem_univ _) rfl

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝³ : CompleteSpace 𝕜
inst✝² : CharZero 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
⊢ AnalyticAt 𝕜 (g ∘ f) x ↔ AnalyticAt 𝕜 g (f x)

Tactic:
by
  refine ⟨fun hg ↦ ?_, (AnalyticAt.comp · hf)⟩
  let r := hf.hasStrictDerivAt.localInverse _ _ _ hf'
  have hra : AnalyticAt 𝕜 r (f x) := hf.analyticAt_localInverse hf'
  have : r (f x) = x := HasStrictFDerivAt.localInverse_apply_image ..
  rw [← this] at hg
  exact (hg.comp hra).congr <| .fun_comp (HasStrictDerivAt.eventually_right_inverse ..) g

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

Goal state before:
pp: case refine_1.succ.zero.«0»
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
hn : 0 + 1 < 2
⊢ naturalityProperty f₀ f₁ hδ₁ hδ₀ hY (δ 2 ((fun i ↦ i) ⟨0, ⋯⟩) ⋯ ⋯)

Tactic:
ext; apply hδ'₀ f₀ f₁ hδ₁ hδ₀ hY

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ 𝓝 0
⊢ ⇑(WithAbs.congr v w (RingEquiv.refl F)) ⁻¹' ⇑(WithAbs.congr v w (RingEquiv.refl F)) '' U ⊆ U

Tactic:
RingEquiv.image_eq_preimage_symm,

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
hU : U ∈ 𝓝 0
⊢ ⇑(WithAbs.congr v w (RingEquiv.refl F)) ⁻¹' ⇑(WithAbs.congr v w (RingEquiv.refl F)).symm ⁻¹' U ⊆ U
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case inr
𝕜 : 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
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
hx' : Tendsto u atTop (𝓝[closedBall b ε] x)
⊢ f x = y

Tactic:
have T1 : Tendsto (f ∘ u) atTop (𝓝 (f x)) :=
    (hf.continuousOn.mono hε x xmem).tendsto.comp hx'

Goal state after:
case inr
𝕜 : 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
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
hx' : Tendsto u atTop (𝓝[closedBall b ε] x)
T1 : Tendsto (f ∘ u) atTop (𝓝 (f x))
⊢ f x = y
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
⊢ analyticOrderAt (deriv f) x + 1 = analyticOrderAt (fun x_1 ↦ f x_1 - f x) x

Tactic:
by
  generalize h : analyticOrderAt (f · - f x) x = r
  cases r with
  | top =>
    suffices analyticOrderAt (deriv f) x = ⊤ by simp_all
    simp only [analyticOrderAt_eq_top, sub_eq_zero] at h ⊢
    obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp h
    filter_upwards [hUo.mem_nhds hUx] with y hy
    simp [(eventuallyEq_of_mem (hUo.mem_nhds hy) hUf).deriv_eq]
  | coe r =>
    have hrne : r ≠ 0 := by
      intro hr
      rw [hr, ENat.natCast_zero, AnalyticAt.analyticOrderAt_eq_zero (by fun_prop)] at h
      grind
    obtain ⟨s, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.pos_of_ne_zero hrne)
    rw [Nat.cast_succ]
    congr 1
    rw [analyticOrderAt_eq_natCast (by fun_prop)] at h
    obtain ⟨F, hFa, hFne, hfF⟩ := h
    simp only [sub_eq_iff_eq_add] at hfF
    obtain ⟨U, hUf, hUo, hUx⟩ := eventually_nhds_iff.mp (hfF.and hFa.eventually_analyticAt)
    have : ∀ y ∈ U, deriv f y =
        (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y := by
      intro y hy
      rw [EventuallyEq.deriv_eq (eventually_of_mem (hUo.mem_nhds hy) (fun u hu ↦ (hUf u hu).1)),
        deriv_add_const, deriv_fun_smul (by fun_prop) (hUf y hy).2.differentiableAt]
      simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]
    rw [analyticOrderAt_congr (eventually_of_mem (hUo.mem_nhds hUx) this)]
    have : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = s := by
      rw [analyticOrderAt_eq_natCast]
      · refine ⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩
        · simpa using ⟨by norm_cast, hFne⟩
        · simpa only [Nat.cast_smul_eq_nsmul] using smul_comm ..
      · simp_rw [← Nat.cast_smul_eq_nsmul 𝕜]
        fun_prop
    rwa [← Pi.add_def, analyticOrderAt_add_eq_right_of_lt]
    rw [this, ← ENat.add_one_le_iff (ENat.natCast_ne_top _), ← Nat.cast_add_one,
      natCast_le_analyticOrderAt (by fun_prop)]
    exact ⟨deriv F, hFa.deriv, by simp⟩

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

Goal state before:
pp: case succ
𝕜 : 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₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
Hn : ↑n = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
⊢ analyticOrderAt ((deriv ∘ deriv^[n']) f) z₀ = ↑(n - (n' + 1))

Tactic:
have horder : analyticOrderAt (deriv^[n'] f) z₀ = (n - n'.succ) + 1 := by
      refine (hk Hn Hpos (by lia)).trans ?_
      have : (n - n'.succ) + 1 = n - n' := by grind
      rw [← this]
      simp

Goal state after:
case succ
𝕜 : 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₀
inst✝ : CharZero 𝕜
n' : ℕ
hk : ∀ {n : ℕ}, ↑n = analyticOrderAt f z₀ → n ≠ 0 → n' ≤ n → analyticOrderAt (deriv^[n'] f) z₀ = ↑(n - n')
n : ℕ
Hn : ↑n = analyticOrderAt f z₀
Hpos : n ≠ 0
Hk : n' + 1 ≤ n
horder : analyticOrderAt (deriv^[n'] f) z₀ = ↑n - ↑n'.succ + 1
⊢ analyticOrderAt ((deriv ∘ deriv^[n']) f) z₀ = ↑(n - (n' + 1))