mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i j : Fin (x₁.len + 1 + (x₂.len + 1))
h : i ≤ j
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      i ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      j

Tactic:
cases i using Fin.addCases <;>
        cases j using Fin.addCases <;>
        rw [Fin.le_def] at h ⊢ <;>
        simp at h ⊢ <;>
        grind only [OrderHom.apply_mono]

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

Goal state before:
pp: case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ z.castSucc = map' (g.comp f) x.castSucc

Tactic:
Eq.comm

Goal state after:
case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ map' (g.comp f) x.castSucc = z.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
x✝³ : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((𝟙_ SSet).map x✝ ≫ ↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝¹).len + 1))).obj (𝟙 x✝³)) =
    (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝²).len + 1))).obj (𝟙 x✝³)) ≫ (nerve (x✝³ ⟶ x✝³)).map x✝

Tactic:
simp; rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((nerve (i ⟶ j) ⊗ nerve (j ⟶ k)).map x✝ ≫ ↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) =
    (↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) ≫ (nerve (i ⟶ k)).map x✝

Tactic:
simp; rfl

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

Goal state before:
pp: case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ Fin.last (n + 1) = map' (g.comp f) x.castSucc

Tactic:
Eq.comm

Goal state after:
case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)

Tactic:
e₂,

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd y.len.succ i))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x : Fin (n + 3)
⊢ map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x

Tactic:
obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
  · by_cases! hx : x ≤ i
    · rw [Fin.predAbove_of_le_castSucc _ _ (by simpa), Fin.castPred_castSucc]
      obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
      · simp only [map'_eq_castSucc_iff, OrderEmbedding.toOrderHom_coe,
          Fin.succAboveOrderEmb_apply, Fin.castSucc_le_castSucc_iff,
          Fin.castSucc_lt_castSucc_iff]
        constructor
        · obtain hx | rfl := hx.lt_or_eq
          · rwa [Fin.succAbove_of_castSucc_lt]
          · simpa only [Fin.succAbove_castSucc_self] using Fin.castSucc_le_succ x
        · intro j hj
          rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),
            Fin.castSucc_lt_castSucc_iff]
      · obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx
        simp [map'_eq_last_iff]
    · obtain ⟨x, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hx)
      rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.le_castSucc_iff]),
        Fin.pred_castSucc_succ, map'_eq_castSucc_iff]
      simp only [Fin.succAbove_of_lt_succ _ _ hx,
        OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
        le_refl, Fin.castSucc_lt_castSucc_iff, true_and]
      intro j hj
      by_cases! h : j.castSucc < i
      · simpa [Fin.succAbove_of_castSucc_lt _ _ h] using hj.le
      · rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]
  · simp

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

Goal state before:
pp: X : SSet
y : X.S
Y : SSet
e : X ≅ Y
d dx : ℕ
x : X _⦋dx⦌
hxy : { dim := dx, simplex := x }.IsUniquelyCodimOneFace y
hd : { dim := dx, simplex := x }.dim = d
⊢ ⋯.index hd = hxy.index hd

Tactic:
obtain ⟨dy, y, rfl⟩ := y.mk_surjective

Goal state after:
X Y : SSet
e : X ≅ Y
d dx : ℕ
x : X _⦋dx⦌
hd : { dim := dx, simplex := x }.dim = d
dy : ℕ
y : X _⦋dy⦌
hxy : { dim := dx, simplex := x }.IsUniquelyCodimOneFace { dim := dy, simplex := y }
⊢ ⋯.index hd = hxy.index hd
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.left
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ x ≤ i.predAbove x.succ

pp: case pos.right
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ ∀ i_1 < x.succ, i.predAbove i_1 < x

Tactic:
· rw [Fin.predAbove_of_castSucc_lt _ _
          (by simpa only [Fin.castSucc_lt_succ_iff] using hi.le), Fin.pred_succ]

Goal state after:
case pos.right
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ ∀ i_1 < x.succ, i.predAbove i_1 < x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i = Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i))) =
    (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i

Tactic:
e₂,

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i = Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i))) =
    Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) ((SimplexCategory.Hom.toOrderHom (inr' x y)) i)) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i))

Tactic:
e₂,

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (y.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' y z)) i = Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' x y)) i = Fin.cast ⋯ (Fin.natAdd x.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)))
e₄ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.natAdd x.len.succ i))) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.castAdd (z.len + 1) i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex ∈ X.nonDegenerate (↑s).dim

Tactic:
rw [(P.isUniquelyCodimOneFace s).δ_index rfl]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ((↑s).cast ⋯).simplex ∈ X.nonDegenerate (↑s).dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s).dim⦌)

Tactic:
rw [(P.isUniquelyCodimOneFace s).δ_index rfl]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ((↑s).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s).dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsRegular
⊢ h.IsProper

Tactic:
← isProper_pairing_iff

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsRegular
⊢ h.pairing.IsProper
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x✝ : ↑h.smallCategoryOfSet.obj
⊢ h.homEquiv (𝟙 x✝) = 𝟙 (h.objEquiv x✝)

Tactic:
rw [SmallCategoryOfSet.id_def]; simp

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

Goal state before:
pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x

Tactic:
· rw [← c.range_map, ← c.mapToSucc_ι, ← c.ι_b_assoc] at hx
      obtain ⟨y, hy⟩ := hx
      exact Or.inr ⟨_, hy⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ f.mapN (Cell.type₂ f c) = { dim := (↑c.s).dim, simplex := (↑c.s).simplex }

Tactic:
dsimp [mapN]

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 : ι
c : f.Cell j
⊢ { dim := c.dim,
      simplex :=
        ↑((ConcreteCategory.hom ((f.b j).app (op ⦋c.dim⦌)))
            ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌)))
              (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)))) } =
    { dim := (↑c.s).dim, simplex := (↑c.s).simplex }
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
hP : P.IsStrongGenerator
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
⊢ (ObjectProperty.ofObj fun T ↦ freeYoneda T.1 ↑T.2).IsStrongGenerator

Tactic:
ObjectProperty.isStrongGenerator_iff

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
hP : P.IsSeparating ∧ ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
⊢ (ObjectProperty.ofObj fun T ↦ freeYoneda T.1 ↑T.2).IsSeparating ∧
    ∀ ⦃X Y : Cᵒᵖ ⥤ A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i) →
        IsIso i
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ (X □ Arrow.mk (initial.to (𝟙_ C))) ≅ X

Tactic:
refine Arrow.isoMk ?_ (ρ_ X.right) ?_

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ (X □ Arrow.mk (initial.to (𝟙_ C))).left ≅ X.left

case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ Iso.hom ?refine_1 ≫ X.hom = (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism

Goal state before:
pp: X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f✝ g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f' g' : RelativeMorphism B C ψ
h : f'.Homotopy g'
f : RelativeMorphism A B φ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ φ ▷ Δ[1] ≫ B.ι ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι

Tactic:
h.rel,

Goal state after:
X Y Z : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f✝ g : RelativeMorphism A B φ
C : Z.Subcomplex
ψ : B.toSSet ⟶ C.toSSet
f' g' : RelativeMorphism B C ψ
h : f'.Homotopy g'
f : RelativeMorphism A B φ
φψ : A.toSSet ⟶ C.toSSet
fac : φ ≫ ψ = φψ
⊢ φ ▷ Δ[1] ≫ fst B.toSSet Δ[1] ≫ ψ ≫ C.ι = fst A.toSSet Δ[1] ≫ φ ≫ ψ ≫ C.ι
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

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
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
⊢ ∃ 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:
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
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)

Tactic:
let i : 𝕜 ≃L[𝕜] 𝕜 := .unitsEquivAut 𝕜 (.mk0 _ hf')

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 (deriv f x) hf')
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt f (↑i) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)

Tactic:
refine R.hasFPowerSeriesAt_symm hx hf.hasFPowerSeriesAt (i := i) ?_ |>.analyticAt

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt f (↑i) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
⊢ FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / ↑n.factorial) 1 =
    (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜).symm ↑i
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
⊢ y ∈ f '' closedBall b ε

Tactic:
have Icf' : (c : ℝ) * f'symm.nnnorm < 1 := by rwa [inv_eq_one_div, lt_div_iff₀ If'] at hc

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
⊢ y ∈ f '' closedBall b ε
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u w : ι
x✝ : w ∈ Finset.univ
hw : u = w
⊢ Tendsto
    (fun i ↦
      (WithAbs.equiv (v u)).symm (1 / (1 + (a w)⁻¹ ^ i)) * (WithAbs.equiv (v u)).symm ((WithAbs.equiv (v w)) (z w)))
    atTop (𝓝 (Pi.single w (z w) u))

Tactic:
rw [← hw, Pi.single_eq_same]
      have hlt : (v u) (a u)⁻¹ < 1 := by
        simpa [← inv_pow, inv_lt_one_iff₀] using Or.inr (hx u).1
      simpa using (WithAbs.tendsto_one_div_one_add_pow_nhds_one hlt).mul_const (z u)

Goal state after:
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 g : 𝕜 → E
z₀ : 𝕜
hfg : f =ᶠ[𝓝 z₀] g
⊢ analyticOrderAt f z₀ = analyticOrderAt g z₀

Tactic:
by
  by_cases hf : AnalyticAt 𝕜 f z₀
  · refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ?_
    simp only [natCast_le_analyticOrderAt, hf, hf.congr hfg]
    congr! 3
    exact hfg.congr_left
  · rw [analyticOrderAt_of_not_analyticAt hf,
      analyticOrderAt_of_not_analyticAt fun hg ↦ hf <| hg.congr hfg.symm]

Goal state after: