mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hf : W₂.op f
hf' : ¬MorphismProperty.identities Cᵒᵖ f
⊢ ¬MorphismProperty.identities C f.unop

Tactic:
simpa [MorphismProperty.identities_op_iff] using hf'

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hf : W₁.op f
hf' : ¬MorphismProperty.identities Cᵒᵖ f
⊢ ¬MorphismProperty.identities C f.unop

Tactic:
simpa [MorphismProperty.identities_op_iff] using hf'

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.degHom e.hom ≤ r.deg Y

pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.deg Y ≤ r.degHom e.hom

Tactic:
· simpa using r.degHom_comp_le_right e.hom (𝟙 Y)

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
e : X ≅ Y
⊢ r.deg Y ≤ r.degHom e.hom
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

Tactic:
hv

Goal state after:
case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

Tactic:
hv

Goal state after:
case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

Tactic:
hv

Goal state after:
case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : Cat
⊢ (nerveFunctor₂.obj X).IsStrictSegal

Tactic:
dsimp [nerveFunctor₂]
  infer_instance

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

Goal state before:
pp: 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 : ∀ (i : Fin (n + 1)), (f i).castSucc < y.castSucc
i : Fin (n + 1)
⊢ f i < y

Tactic:
by simpa using hz i

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ y.dim = d + 1

Tactic:
hxy.dim_eq,

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ x.dim + 1 = d + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
⊢ y.dim = d + 1

Tactic:
hxy.dim_eq,

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
⊢ x.dim + 1 = d + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
⊢ y.dim = d + 1

Tactic:
hxy.dim_eq,

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
⊢ x.dim + 1 = d + 1
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x.castSucc = i.succ.castSucc.succAbove x.castSucc

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (by simpa), map'_eq_castSucc_iff]
      simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
      constructor
      · simp only [i.predAbove_of_le_castSucc x.castSucc (by simpa),
          Fin.castPred_castSucc, le_refl]
      · intro j hj
        by_cases! h : i.castSucc < j
        · rw [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
          exact hj.trans x.castSucc_lt_succ
        · rwa [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case h₁.h₁.h₁
w x y z : AugmentedSimplexCategory
⊢ w.inl x ≫
      (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    w.inl x ≫ (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

Tactic:
simp [-id_tensorHom, -tensorHom_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case h₁.h₁.h₂
w x y z : AugmentedSimplexCategory
⊢ w.inr x ≫
      (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    w.inr x ≫ (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

Tactic:
simp [-id_tensorHom, -tensorHom_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case h₁.h₂
w x y z : AugmentedSimplexCategory
⊢ (w ⊗ x).inr y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    (w ⊗ x).inr y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

Tactic:
simp [-id_tensorHom, -tensorHom_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case h₂
w x y z : AugmentedSimplexCategory
⊢ ((w ⊗ x) ⊗ y).inr z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    ((w ⊗ x) ⊗ y).inr z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

Tactic:
simp [-id_tensorHom, -tensorHom_id]

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

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
hij :
  (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) j
l : Fin (k + 1)
⊢ i l = j l

Tactic:
exact hx (Functor.congr_obj hij l)

Goal state after:
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]
  exact Nonsingular.mono' x hx

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 ι
i₁ i₂ : ι
h : i₁ ≤ i₂
⊢ A ⊔ ⨆ j, ⨆ (_ : j < i₁), ⨆ c, (↑(P.p c.s)).subcomplex ≤ f.filtration i₂

Tactic:
simp only [sup_le_iff, iSup_le_iff, le_filtration, true_and]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
h : i₁ ≤ i₂
⊢ ∀ i < i₁, ∀ (i_2 : f.Cell i), (↑(P.p i_2.s)).subcomplex ≤ f.filtration i₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: ⊢ anodyneExtensions =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts

Tactic:
anodyneExtensions_eq_llp_rlp,

Goal state after:
⊢ modelCategoryQuillen.J.rlp.llp =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: ⊢ anodyneExtensions =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
anodyneExtensions_eq_llp_rlp,

Goal state after:
⊢ modelCategoryQuillen.J.rlp.llp =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerAnodyneExtensions ≤ anodyneExtensions

Tactic:
anodyneExtensions_eq_llp_rlp,

Goal state after:
⊢ innerAnodyneExtensions ≤ modelCategoryQuillen.J.rlp.llp
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h : min x hd ≤ i
⊢ (x.cast hd).simplex.1 (min x hd) ≤ (x.cast hd).simplex.1 i

Tactic:
exact stdSimplex.monotone_apply _ h

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
i : Fin (d + 2)
hi : (min x hd).castSucc < i
⊢ φ x hd i = (objEquiv (x.cast hd).simplex) (i.pred ⋯)

Tactic:
by
  rw [φ_of_ne _ _ _ hi.ne', Fin.predAbove_of_castSucc_lt _ _ hi]

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

Goal state before:
pp: case refine_2
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
y : Fin (d + 1)
hy : (x.cast hd).simplex.1 (l.castSucc.succAbove y) = k.succ
this : y < l
⊢ False

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (by grind)] at hy

Goal state after:
case refine_2
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
y : Fin (d + 1)
hy : (x.cast hd).simplex.1 y.castSucc = k.succ
this : y < l
⊢ False
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✝ : BraidedCategory C
X : Arrow C
I : C
i : IsInitial I
W : C
this✝ : IsIso (I ◁ X.hom)
this : IsPushout (i.to W ▷ X.left) (I ◁ X.hom) (𝟙 (W ⊗ X.left)) ((i.ofIso (mulZero i).symm).to (W ⊗ X.left))
⊢ pushout.inl (((curriedTensor C).map (Arrow.mk (i.to W)).hom).app X.left)
        (((curriedTensor C).obj (Arrow.mk (i.to W)).left).map X.hom) ≫
      this.isoPushout.symm.hom ≫ W ◁ X.hom =
    pushout.inl (((curriedTensor C).map (Arrow.mk (i.to W)).hom).app X.left)
        (((curriedTensor C).obj (Arrow.mk (i.to W)).left).map X.hom) ≫
      (ofHasPushout (curriedTensor C) (Arrow.mk (i.to W)).hom X.hom).ι ≫
        (Iso.refl (((curriedTensor C).obj (Arrow.mk (i.to W)).right).obj X.right)).hom

Tactic:
by simp [pushout.inl_desc]

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

Goal state before:
pp: X : SSet
x : X.π₀
⊢ mapπ₀ (𝟙 X) x = x

Tactic:
induction x
  simp

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

Goal state before:
pp: X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
x : X.π₀
⊢ mapπ₀ (f ≫ g) x = mapπ₀ g (mapπ₀ f x)

Tactic:
induction x
  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✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₁ :
  { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } ≠
    { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }.x ⋯).card

Tactic:
simp only [ne_eq, pairingCore_ι, Type₁.ext_iff] at h₁

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
⊢ (finset { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }.x ⋯).card <
    (finset { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }.x ⋯).card
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₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝² x✝¹ : Arrow C₃
x✝ : x✝² ⟶ x✝¹
⊢ (G.leibnizPullback.obj (op X₁) ⋙ F.leibnizPushout.obj X₁).map x✝ ≫
      Arrow.homMk
        (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝¹).left))
          (adj₂.homEquiv.symm
            (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom) ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
          ⋯)
        (adj₂.homEquiv.symm
          (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝¹.hom) ((G.map (unop (op X₁)).hom.op).app x✝¹.right)))
        ⋯ =
    Arrow.homMk
        (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝²).left))
          (adj₂.homEquiv.symm
            (pullback.fst ((G.obj (op (unop (op X₁)).left)).map x✝².hom) ((G.map (unop (op X₁)).hom.op).app x✝².right)))
          ⋯)
        (adj₂.homEquiv.symm
          (pullback.snd ((G.obj (op (unop (op X₁)).left)).map x✝².hom) ((G.map (unop (op X₁)).hom.op).app x✝².right)))
        ⋯ ≫
      (𝟭 (Arrow C₃)).map x✝

Tactic:
by
    ext
    · apply pushout.hom_ext <;> simp [← homEquiv_symm_naturality_two,
        ← homEquiv_symm_naturality_three]
    · simp [← homEquiv_symm_naturality_two, ← homEquiv_symm_naturality_three]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Sigma.ι (fun x ↦ R) x ≫ PInfty.f n = Sigma.ι (fun x ↦ R) ⟨x, hx⟩ ≫ (X.fromNormalizedChainComplex R).f n

Tactic:
simp [fromNormalizedChainComplex, SimplicialObject.Splitting.fromNondegComplex_f]

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ ⇑m.toTopHomeo.symm ∘ stdSimplex.map ⇑(ConcreteCategory.hom f) =
    ⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) ∘ ⇑n.toTopHomeo.symm

Tactic:
by
  ext x : 1
  exact ConcreteCategory.congr_hom ((forget _).congr_map
    (toTopSimplex.inv.naturality f)) _

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)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : (fun x ↦ v x ^ c) = ⇑w
x : WithAbs w
hx : x ∈ Metric.ball 0 (ε ^ c)
⊢ (WithAbs.congr v w (RingEquiv.refl F)) ((WithAbs.congr v w (RingEquiv.refl F)).symm x) ∈
    ⇑(WithAbs.congr v w (RingEquiv.refl F)) '' U

Tactic:
refine Set.mem_image_of_mem _ (hU ?_)

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
U : Set (WithAbs v)
ε : ℝ
hε : ε > 0
hU : Metric.ball 0 ε ⊆ U
c : ℝ
hc : 0 < c
hvw : (fun x ↦ v x ^ c) = ⇑w
x : WithAbs w
hx : x ∈ Metric.ball 0 (ε ^ c)
⊢ (WithAbs.congr v w (RingEquiv.refl F)).symm x ∈ Metric.ball 0 ε
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
⊢ y ∈ f '' closedBall b ε

Tactic:
obtain ⟨x, hx⟩ : ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete this

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)
⊢ y ∈ f '' closedBall b ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Goal state before:
pp: z✝ : ℂ
m : z✝ ∈ slitPlane
z : ℂ
⊢ z ∈ slitPlane → DifferentiableAt ℂ log z

Tactic:
m

Goal state after:
z✝ : ℂ
m✝ : z✝ ∈ slitPlane
z : ℂ
m : z ∈ slitPlane
⊢ DifferentiableAt ℂ log z
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: case refine_1
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h :
  ((↑n ! = 0 ∨ Polynomial.eval a (ascPochhammer 𝕂 n) = 0) ∨ Polynomial.eval b (ascPochhammer 𝕂 n) = 0) ∨
    Polynomial.eval c (ascPochhammer 𝕂 n) = 0
⊢ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c

Tactic:
rcases h with ((hn | h) | h) | h

Goal state after:
case refine_1.inl.inl.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
hn : ↑n ! = 0
⊢ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c

case refine_1.inl.inl.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval a (ascPochhammer 𝕂 n) = 0
⊢ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c

case refine_1.inl.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval b (ascPochhammer 𝕂 n) = 0
⊢ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c

case refine_1.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b c : 𝕂
n : ℕ
h : Polynomial.eval c (ascPochhammer 𝕂 n) = 0
⊢ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • f z ≠ 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
· left
    filter_upwards [nhdsWithin_le_nhds h₁, self_mem_nhdsWithin] with y h₁y h₂y
    rw [Set.mem_compl_iff, Set.mem_singleton_iff, ← sub_eq_zero] at h₂y
    exact smul_eq_zero_iff_right (pow_ne_zero n h₂y) |>.mp h₁y

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt 𝕜 (fun z ↦ (z - z₀) ^ n • f z) z₀
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • f z ≠ 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_5
F : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ (i : ι), MeromorphicAt (F i) x
⊢ MeromorphicAt (∏ᶠ (i : ι), F i) x

Tactic:
by
  by_cases h₂f : Function.HasFiniteMulSupport F
  · simpa [finprod_eq_prod F h₂f] using prod (by aesop)
  · exact finprod_of_not_hasFiniteMulSupport h₂f ▸ const (1 : 𝕜') x

Goal state after: