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

Goal state before:
pp: V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₁✝ ≫ Quiver.Hom.toPath e₁₂✝)) =
    (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂✝))

Tactic:
simp only [Functor.map_comp]

Goal state after:
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₁✝)) ≫
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₁₂✝)) =
    (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂✝))
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: case neg
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₂ f
hf' : ¬MorphismProperty.identities C f
⊢ r.deg X ≤ r.deg Y

Tactic:
· exact (r.lt₂ f hf hf').le

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case inl.inl
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h✝ : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ δ i'.succ ≫ σ i.castSucc = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i.castSucc = σ j ≫ δ j'

Tactic:
exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_gt h]⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j < m + 1
m₁ : ℕ
hm₁ : m + L.length + 1 = m₁
⊢ m + (simplicialInsert j L).length = m₁

Tactic:
simpa only [simplicialInsert_length, add_assoc]

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

Goal state before:
pp: ι : Type u_1
K x✝¹ : PreAbstractSimplicialComplex ι
x✝ : (fun K ↦ K.faces) K = (fun K ↦ K.faces) x✝¹
⊢ K = x✝¹

Tactic:
cases K
    congr

Goal state after:
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:
rw [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:
rw [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:
rw [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.SimplicialNerve

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
⊢ functor OrderHom.id = EnrichedFunctor.id SSet (SimplicialThickening J)

Tactic:
by
  refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_
  ext
  exact Functor.ext (by cat_disch)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
⊢ functor (g.comp f) = EnrichedFunctor.comp SSet (functor f) (functor g)

Tactic:
by
  refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_
  ext
  exact Functor.ext (by cat_disch)

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

Goal state before:
pp: X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
i : Fin (d + 2)
hi : (fun i ↦ (ConcreteCategory.hom (SimplicialObject.δ X.op i)) (opObjEquiv.symm y) = opObjEquiv.symm x) i
⊢ i = (hxy.index ⋯).rev

Tactic:
obtain ⟨i, rfl⟩ := i.rev_surjective

Goal state after:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
i : Fin (d + 2)
hi : (ConcreteCategory.hom (SimplicialObject.δ X.op i.rev)) (opObjEquiv.symm y) = opObjEquiv.symm x
⊢ i.rev = (hxy.index ⋯).rev
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{?u.4, u_1} J
inst✝³ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst✝² : Finite ι
X : ι → SSet
inst✝¹ : HasCoproduct X
inst✝ : ∀ (j : ι), (X j).Finite
⊢ HasColimitsOfShape (Discrete ι) (Type u)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι

Goal state after:
J : Type u_1
inst✝⁴ : Category.{?u.4, u_1} J
inst✝³ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst✝² : Finite ι
X : ι → SSet
inst✝¹ : HasCoproduct X
inst✝ : ∀ (j : ι), (X j).Finite
n : ℕ
e : ι ≃ Fin n
⊢ HasColimitsOfShape (Discrete ι) (Type u)
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
⊢ ∑ x ∈ S, α x = -∑ y ∈ Finset.image γ₂ S, β y

Tactic:
rw [← Finset.sum_neg_distrib, Finset.sum_image hγ₂.injOn]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : ∑ x ∈ Sᶜ, α x = -∑ y ∈ Finset.image γ₁ Sᶜ, β y
⊢ ∑ x ∈ S, α x = ∑ x ∈ S, -β (γ₂ x)
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
⊢ ∃ j₁ α,
    ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')

Tactic:
let j {k k' : K} (φ : k ⟶ k') : J := (H φ).choose

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
⊢ ∃ j₁ α,
    ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Bijective h.functor.mapArrow.obj

Tactic:
by
    constructor
    · rintro ⟨x, y, f⟩ ⟨x', y', g⟩ hfg
      obtain rfl : x = x' := by simpa using! congr_arg Arrow.leftFunc.obj hfg
      obtain rfl : y = y' := by simpa using! congr_arg Arrow.rightFunc.obj hfg
      obtain rfl : f = g := by simpa [Arrow.mk_eq_mk_iff] using! hfg
      rfl
    · rintro ⟨X, Y, f⟩
      obtain ⟨x, rfl⟩ := h.objEquiv.surjective X
      obtain ⟨y, rfl⟩ := h.objEquiv.surjective Y
      obtain ⟨f, rfl⟩ := h.homEquiv.surjective f
      exact ⟨Arrow.mk f, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
⊢ Nonempty (C ↪ Ω)

Tactic:
refine ⟨Function.Embedding.trans { toFun X := Arrow.mk (𝟙 X), inj' := ?_ } ι⟩

Goal state after:
κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
⊢ Function.Injective fun X ↦ Arrow.mk (𝟙 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✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
⊢ Function.Injective f.mapN

Tactic:
intro s t h
  obtain ⟨c, rfl | rfl⟩ := f.exists_or_of_range_m_N s <;>
    obtain ⟨c', rfl | rfl⟩ := f.exists_or_of_range_m_N t <;>
    simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h
  · obtain rfl : c = c' := by ext : 1; exact P.p.injective h
    rfl
  · exact (P.ne _ _ h).elim
  · exact (P.ne _ _ h.symm).elim
  · congr; aesop

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
⊢ l.succ ∈ finset x hd

Tactic:
by simpa using hl.simplex_fst_succ

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : InnerFibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃' : internalHom.PullbackObjObj Λ[n✝ + 2, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[n✝ + 2, k].ι p
⊢ HasLiftingProperty sq₁₂.flipTensor.ι p

Tactic:
internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃'

Goal state after:
X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : InnerFibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
E B : SSet
p : E ⟶ B
hp : innerFibrations p
sq₁₃' : internalHom.PullbackObjObj Λ[n✝ + 2, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[n✝ + 2, k].ι p
⊢ HasLiftingProperty i sq₁₃'.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : Fibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
m : ℕ
X Y : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃' : internalHom.PullbackObjObj Λ[m + 1, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[m + 1, k].ι p
⊢ HasLiftingProperty sq₁₂.flipTensor.ι p

Tactic:
internalHomAdjunction₂.hasLiftingProperty_iff _ sq₁₃'

Goal state after:
X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : Fibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
m : ℕ
X Y : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
sq₁₃' : internalHom.PullbackObjObj Λ[m + 1, k].ι p := Functor.PullbackObjObj.ofHasPullback internalHom Λ[m + 1, k].ι p
⊢ HasLiftingProperty i sq₁₃'.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
l : Fin (u.dim + 1)
hl : IsIndex x hd l.succ
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
hi : i < l.castSucc
⊢ i = l.castSucc ∨ i = l.succ

Tactic:
obtain ⟨l, rfl⟩ := Fin.eq_succ_of_ne_zero (i := l) (by grind)
    refine (hu _ rfl l.succ ?_).elim
    simp [isIndex_succ, S.cast_simplex_rfl, hu', stdSimplex.δ_apply,
      Fin.succAbove_of_lt_succ i l.castSucc hi,
      Fin.succAbove_of_lt_succ i l.succ (by grind), dsimp% hl.simplex_fst_succ,
      dsimp% hl.simplex_snd_succ, dsimp% hl.simplex_fst_castSucc]

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

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝¹ : SSet
x✝ : X ⟶ x✝¹
⊢ x✝ = { app := fun x ↦ ↾fun x_1 ↦ isEmptyElim x_1, naturality := ⋯ }

Tactic:
by ext _ x; exact isEmptyElim x

Goal state after:
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₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := IsInitial.isInitialObj (F.obj X₁) X₂ h
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := IsInitial.isInitialObj (F.obj Y₁) X₂ h
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
apply +allowSynthFailures IsPushout.of_horiz_isIso

Goal state after:
case inst
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₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ IsIso ((F.map f₁).app X₂)

case sq
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₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ CommSq ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))
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✝ : G.PullbackObjObj f₁✝ f₃✝
f₁ f₁' : Arrow C₁
f₃ : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom
sq : f₁' ⟶ f₁
⊢ (𝟭 C₂).map ((G.map (Arrow.Hom.right sq).op).app f₃.left) ≫ (Arrow.mk sq₁₃'.π).hom =
    (Arrow.mk sq₁₃.π).hom ≫
      (𝟭 C₂).map
        (⋯.lift (sq₁₃.fst ≫ (G.map (Arrow.Hom.left sq).op).app f₃.left)
          (sq₁₃.snd ≫ (G.map (Arrow.Hom.right sq).op).app f₃.right) ⋯)

Tactic:
apply PullbackObjObj.hom_ext
    · simp [← NatTrans.comp_app, ← map_comp, ← op_comp]
    · cat_disch

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:
by
    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.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : log (v b) / log (v a) < ↑q.num / ↑q.den
hq₂ : ↑q.num / ↑q.den < log (w b) / log (w a)
⊢ False

Tactic:
rw [div_lt_div_iff₀ (log_pos ha) (by simp [q.den_pos]), mul_comm, ← log_pow, ← log_zpow,
    log_lt_log_iff (pow_pos (by linarith) _) (zpow_pos (by linarith) _),
    ← div_lt_one (zpow_pos (by linarith) _), ← map_pow, ← map_zpow₀, ← map_div₀] at hq₁

Goal state after:
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
a : F
ha₀ : a ≠ 0
ha₁ : v a ≠ 1
b : F
hb₀ : b ≠ 0
hb₁ : v b ≠ 1
h_ne : log (v b) / log (w b) ≠ log (v a) / log (w a)
ha : 1 < v a
hb : 1 < v b
h_lt : log (v b) / log (v a) < log (w b) / log (w a)
hwa : 1 < w a
hwb : 1 < w b
q : ℚ
hq₁ : v (b ^ q.den / a ^ q.num) < 1
hq₂ : ↑q.num / ↑q.den < log (w b) / log (w a)
⊢ False