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

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
⊢ ∀ (hj : j ≤ n),
    i + (k + 1) = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
hj

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ i + (k + 1) = j →
    (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
      (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 })
ex : Edge x₀ x₁
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 })
ey : Edge y₀ y₁
⊢ homMk (ex.tensor (Edge.id y₀)) ≫ homMk ((Edge.id x₁).tensor ey) = homMk (ex.tensor ey)

Tactic:
homMk_comp_homMk ((Edge.CompStruct.compId ex).tensor (Edge.CompStruct.idComp ey))

Goal state after:
X Y : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 })
ex : Edge x₀ x₁
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 })
ey : Edge y₀ y₁
⊢ homMk (ex.tensor ey) = homMk (ex.tensor ey)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
⊢ j < x → i.succAbove j < x.castSucc

Tactic:
hj

Goal state after:
case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ i.succAbove j < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex ∈
    (y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌)

Tactic:
exact ⟨(SimplexCategory.δ _).op, rfl⟩

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
⊢ j < x → i.succAbove j < x.succ

Tactic:
hj

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
⊢ i.succAbove j < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d', simplex := y }
⊢ (opEquiv.symm { dim := d, simplex := x }).IsUniquelyCodimOneFace (opEquiv.symm { dim := d', simplex := y })

Tactic:
obtain rfl : d' = d + 1 := hxy.dim_eq

Goal state after:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ (opEquiv.symm { dim := d, simplex := x }).IsUniquelyCodimOneFace (opEquiv.symm { dim := d + 1, simplex := y })
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d', simplex := y }
⊢ { dim := { dim := d, simplex := x }.dim,
        simplex :=
          (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
            { dim := d, simplex := x }.simplex }.IsUniquelyCodimOneFace
    { dim := { dim := d', simplex := y }.dim,
      simplex :=
        (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d', simplex := y }.dim⦌)))
          { dim := d', simplex := y }.simplex }

Tactic:
obtain rfl : d' = d + 1 := hxy.dim_eq

Goal state after:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ { dim := { dim := d, simplex := x }.dim,
        simplex :=
          (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
            { dim := d, simplex := x }.simplex }.IsUniquelyCodimOneFace
    { dim := { dim := d + 1, simplex := y }.dim,
      simplex :=
        (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y }.dim⦌)))
          { dim := d + 1, simplex := y }.simplex }
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
hj

Goal state after:
case pos.right
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
⊢ i.predAbove j < x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg.right
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
⊢ j < x.castSucc → i.predAbove j < x

Tactic:
hj

Goal state after:
case neg.right
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
⊢ i.predAbove j < 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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ ofSimplex (yonedaEquiv c.map) = (↑(P.p c.s)).subcomplex

Tactic:
Equiv.apply_symm_apply,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ ofSimplex ((↑(P.p c.s)).cast ⋯).simplex = (↑(P.p c.s)).subcomplex
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 ι
i₁ i₂ : ι
h : i₁ ≤ i₂
j : ι
⊢ j < i₁ → ∀ (i : f.Cell j), (↑(P.p i.s)).subcomplex ≤ f.filtration i₂

Tactic:
hj

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
h : i₁ ≤ i₂
j : ι
hj : j < i₁
⊢ ∀ (i : f.Cell j), (↑(P.p i.s)).subcomplex ≤ 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
j : ι
⊢ j < i → f.filtration j ≤ f.filtration i

Tactic:
hj

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
j : ι
hj : 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 ι
m : ι
hm : Order.IsSuccLimit m
j : ι
⊢ j < m → f.filtration j ≤ f.filtration m

Tactic:
hj

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
j : ι
hj : j < m
⊢ f.filtration j ≤ f.filtration m
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
Y : C
x : ↑h.obj
f : (𝟭 C).obj (h.objEquiv x) ⟶ (𝟭 C).obj Y
⊢ ∃ a, h.functor.mapArrow.obj a = { left := h.objEquiv x, right := Y, hom := f }

Tactic:
obtain ⟨y, rfl⟩ := h.objEquiv.surjective Y

Goal state after:
case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.obj
f : (𝟭 C).obj (h.objEquiv x) ⟶ (𝟭 C).obj (h.objEquiv y)
⊢ ∃ a, h.functor.mapArrow.obj a = { left := h.objEquiv x, right := h.objEquiv y, hom := f }
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
X₁ X₂ : C
f : unop (op X₂) ⟶ unop (op X₁)
x : (yoneda.obj Y).obj (F.op.obj (op X₁))
⊢ (ConcreteCategory.hom
          (((restrictedULiftYoneda F).obj Y).map (op f) ≫
            match op X₂ with
            | op X =>
              ↾fun x ↦
                match x with
                | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) })).toFun
      { down := x } =
    (ConcreteCategory.hom
          ((match op X₁ with
            | op X =>
              ↾fun x ↦
                match x with
                | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) ≫
            ((restrictedULiftYoneda F).obj s.pt).map (op f))).toFun
      { down := x }

Tactic:
let α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x :=
            CostructuredArrow.homMk f

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
X₁ X₂ : C
f : unop (op X₂) ⟶ unop (op X₁)
x : (yoneda.obj Y).obj (F.op.obj (op X₁))
α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x := CostructuredArrow.homMk f ⋯
⊢ (ConcreteCategory.hom
          (((restrictedULiftYoneda F).obj Y).map (op f) ≫
            match op X₂ with
            | op X =>
              ↾fun x ↦
                match x with
                | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) })).toFun
      { down := x } =
    (ConcreteCategory.hom
          ((match op X₁ with
            | op X =>
              ↾fun x ↦
                match x with
                | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) ≫
            ((restrictedULiftYoneda F).obj s.pt).map (op f))).toFun
      { down := x }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
hA : strongInnerAnodyneExtensions A.ι
⊢ ∃ P, ∃ (x : P.IsRegular), P.IsInner

Tactic:
obtain ⟨_, P, _, ⟨_, rfl⟩⟩ :
        ∃ (B : X.Subcomplex) (P : B.Pairing) (h : P.IsRegular), P.IsInner ∧ B = A := by
      obtain ⟨_, P₁, _, P₂⟩ := hA
      exact ⟨_, P₁, inferInstance, ⟨P₂, by simp⟩⟩
    exact ⟨P, ⟨inferInstance, inferInstance⟩⟩

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
⊢ (objEquiv (objEquiv.symm { toFun := φ x hd, monotone' := ⋯ })) ((min x hd).castSucc.succAbove i) =
    (objEquiv (x.cast hd).simplex) i

Tactic:
Equiv.apply_symm_apply,

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
⊢ { toFun := φ x hd, monotone' := ⋯ } ((min x hd).castSucc.succAbove i) = (objEquiv (x.cast hd).simplex) i
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (𝟭 C₃).map
        (⋯.desc ((F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl)
          ((F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.obj f₁.right).map (Arrow.Hom.right sq))

Tactic:
apply PushoutObjObj.hom_ext
    · simp [← map_comp]
    · cat_disch

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

Goal state before:
pp: case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 2)
n : ℕ
hk : k ≠ Fin.last (m + 1)
⊢ (pairing k n).IsRegular

Tactic:
obtain ⟨k, rfl⟩ := Fin.eq_castSucc_of_ne_last hk
    rw [pairing_castSucc]
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm
        ((ConcreteCategory.hom (SimplicialObject.δ X j.castSucc.castSucc.rev))
          (opObjEquiv (opObjEquiv.symm (yonedaEquiv h.map))))) =
    f.op.map

Tactic:
Equiv.apply_symm_apply,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.δ X j.castSucc.castSucc.rev)) (yonedaEquiv h.map))) =
    f.op.map
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm
        ((ConcreteCategory.hom (SimplicialObject.δ X j.castSucc.succ.rev))
          (opObjEquiv (opObjEquiv.symm (yonedaEquiv h.map))))) =
    fg.op.map

Tactic:
Equiv.apply_symm_apply,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.δ X j.castSucc.succ.rev)) (yonedaEquiv h.map))) =
    fg.op.map
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm
        ((ConcreteCategory.hom (SimplicialObject.δ X j.succ.succ.rev))
          (opObjEquiv (opObjEquiv.symm (yonedaEquiv h.map))))) =
    g.op.map

Tactic:
Equiv.apply_symm_apply,

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm
      (opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.δ X j.succ.succ.rev)) (yonedaEquiv h.map))) =
    g.op.map
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: 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

Tactic:
apply mk_le_of_countable_eventually_mem ht (fun i ↦ (h'f i).le)

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

Goal state before:
pp: case refine_2.inr.inl.inr
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
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h✝ : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a = 1
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
k : ι
hk : k ≠ i
h : k ≠ j
⊢ (v k) c < 1

Tactic:
exact hc.2.1 ⟨k, h⟩ (by grind)

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

Goal state before:
pp: case refine_2.inr.inr.inr.inr
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
this : Fintype ι✝
P : (ι : Type u_3) → [Fintype ι] → Prop :=
  fun ι [Fintype ι] ↦
    ∀ (v : ι → AbsoluteValue R S),
      (∀ (i : ι), (v i).IsNontrivial) →
        (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ (i : ι), ∃ a, 1 < (v i) a ∧ ∀ (j : ι), j ≠ i → (v j) a < 1
ι : Type u_3
x✝¹ : Fintype ι
x✝ : Nontrivial ι
ih : ∀ (β : Type u_3) [inst : Fintype β], card β < card ι → P β
v : ι → AbsoluteValue R S
h✝ : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
i : ι
hc✝ : card ι ≠ 2
hlt : 2 < card ι
j : ι
hj : j ≠ i
a : R
ha :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) a ∧
    ∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) a < 1
b : R
hb :
  1 < (restrict (fun k ↦ k = i ∨ k = j) v ⟨i, ⋯⟩) b ∧
    ∀ (j_1 : { k // k = i ∨ k = j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k = i ∨ k = j) v j_1) b < 1
ha₁ : (v j) a ≠ 1
ha_gt : 1 < (v j) a
c : R
hc :
  1 < (restrict (fun k ↦ k ≠ j) v ⟨i, ⋯⟩) c ∧
    (∀ (j_1 : { k // k ≠ j }), j_1 ≠ ⟨i, ⋯⟩ → (restrict (fun k ↦ k ≠ j) v j_1) c < 1) ∧ (v j) c < 1
k : ι
hk : k ≠ i
h : k ≠ j
⊢ (v k) c < 1

Tactic:
exact hc.2.1 ⟨k, h⟩ (by grind)

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

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

Tactic:
contrapose h

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
n : ℕ
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀

Tactic:
by_cases hf' : analyticOrderAt f z₀ = ⊤
  · simp [analyticOrderAt_smul_eq_top_of_left, *]
  by_cases hg' : analyticOrderAt g z₀ = ⊤
  · simp [analyticOrderAt_smul_eq_top_of_right, *]
  -- Non-trivial case: both functions do not vanish around z₀
  obtain ⟨f', h₁f', h₂f', h₃f'⟩ := hf.analyticOrderAt_ne_top.1 hf'
  obtain ⟨g', h₁g', h₂g', h₃g'⟩ := hg.analyticOrderAt_ne_top.1 hg'
  rw [← Nat.cast_analyticOrderNatAt hf', ← Nat.cast_analyticOrderNatAt hg', ← ENat.natCast_add,
      (hf.smul hg).analyticOrderAt_eq_natCast]
  refine ⟨f' • g', h₁f'.smul h₁g', ?_, ?_⟩
  · simp
    tauto
  · obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃f'
    obtain ⟨s, h₁s, h₂s, h₃s⟩ := eventually_nhds_iff.1 h₃g'
    exact eventually_nhds_iff.2
      ⟨t ∩ s, fun y hy ↦ (by simp [h₁t y hy.1, h₁s y hy.2]; module), h₂t.inter h₂s, h₃t, h₃s⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 ↦ x) =
    ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n

Tactic:
by
  rw [ordinaryHypergeometricSeries, ofScalars_apply_eq]

Goal state after:
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 : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r : ℕ
hr : ↑r = analyticOrderAt f (g z₀)
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
← hr,

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₀) = ⊤
r : ℕ
hr : ↑r = analyticOrderAt f (g z₀)
s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
⊢ analyticOrderAt (f ∘ g) z₀ = ↑r * analyticOrderAt (fun x ↦ g x - g z₀) z₀
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 : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f + g) x

Tactic:
by
  rcases hf with ⟨m, hf⟩
  rcases hg with ⟨n, hg⟩
  refine ⟨max m n, ?_⟩
  have : (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦ (z - x) ^ (max m n - m) •
      ((z - x) ^ m • f z) + (z - x) ^ (max m n - n) • ((z - x) ^ n • g z) := by
    simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _),
      Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add]
  rw [this]
  exact (((analyticAt_id.sub analyticAt_const).pow _).smul hf).add
    (((analyticAt_id.sub analyticAt_const).pow _).smul hg)

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

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
⊢ iteratedDeriv (n + 1 + 1) cos = -iteratedDeriv (n + 1) sin

Tactic:
rw [iteratedDeriv_succ, ih, iteratedDeriv_succ, deriv.neg']

Goal state after:
case succ
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
⊢ (fun x ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f g : ℂ → ℂ
f' g' x : ℂ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasDerivAt (fun x ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Tactic:
by
  simpa using (hf.hasFDerivAt.cpow hg h0).hasDerivAt

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✝¹ : SecondCountableTopology 𝕜
inst✝ : CompleteSpace E
h : Meromorphic f
⊢ {z | AnalyticAt 𝕜 f z}ᶜ.Countable

Tactic:
by
  simpa using (h.meromorphicOn (s := univ)).countable_compl_analyticAt_inter

Goal state after: