mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
⊢ Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∑ x, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x))) • φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ x,
        ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x)) * (-1) ^ (a + 1)) •
          φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) =
    -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩

Tactic:
conv_lhs =>
    congr
    · rw [Fin.sum_univ_castSucc]
    · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∑ i,
          ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc))) •
            φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc)) ≫ X.σ ⟨a, ⋯⟩ +
        ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1))))) •
          φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)))) ≫ X.σ ⟨a, ⋯⟩ +
      (∑ i,
            ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) * (-1) ^ (a + 1)) •
              φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i.castSucc.castSucc)) +
          ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)).castSucc)) * (-1) ^ (a + 1)) •
            φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 1)).castSucc)) +
        ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2)))) * (-1) ^ (a + 1)) •
          φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q (Fin.last (a + 2))))) =
    -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a : Y ⟶ X _⦋n + 1⦌
⊢ ∀ (b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f

Tactic:
b

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b : Y ⟶ X _⦋n + 1⦌
⊢ ∀ (c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
norm_eq_zpow_neg_valuation hx0

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ↑p ^ (-x.valuation) ≤ ↑p ^ n ↔ ↑p ^ (-x.valuation) < ↑p ^ (n + 1)
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ Sigma.ι (summand K Δ') (A.pull θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Tactic:
obtain rfl := SimplexCategory.image_eq fac

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ Sigma.ι (summand K Δ') (A.pull θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ PInftyToNormalizedMooreComplex X ≫ inclusionOfMooreComplexMap X = PInfty

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi C) c
⊢ ((inverse ⋙ functor).obj P).X = ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P).X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ∀ (X Y : HomologicalComplex (Karoubi C) c) (f : X ⟶ Y),
    (inverse ⋙ functor).map f = eqToHom ⋯ ≫ (𝟭 (HomologicalComplex (Karoubi C) c)).map f ≫ eqToHom ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ (X : Karoubi C), (𝟭 (Karoubi C)).obj X = (toKaroubi (Karoubi C) ⋙ inverse C).obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.πSummand A = 𝟙 (summand s.N Δ A)

Tactic:
by
  simp [πSummand]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
G : ReflPrefunctor V W
F_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := F_obj, map := map✝, map_id := map_id✝ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))
⊢ { obj := F_obj, map := map✝, map_id := map_id✝ } = G

Tactic:
obtain ⟨⟨G_obj⟩⟩ := G

Goal state after:
V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : V), { obj := G_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := G_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := G_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := G_obj, map := map✝, map_id := map_id✝ }.map f))
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹ } = { obj := G_obj, map := map✝, map_id := map_id✝ }
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ cast hu hv e = e' ↔ e ≍ e'

Tactic:
by
  rw [Hom.cast_eq_cast]
  exact _root_.cast_eq_iff_heq

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Path.cast ⋯ ⋯ p = p'

Tactic:
by
  rw [Path.cast_eq_iff_heq]
  exact heq_of_cons_eq_cons h

Goal state after:
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : SingleObj α ⥤q SingleObj β
g : SingleObj β ⥤q SingleObj γ
⊢ toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f

Tactic:
simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝² : Monoid M
inst✝¹ : Group G
N : Type v
inst✝ : Monoid N
⊢ Function.LeftInverse (fun f ↦ { toFun := fun x ↦ f.map ((toEnd M) x), map_one' := ⋯, map_mul' := ⋯ }) fun f ↦
    { obj := id, map := fun {X Y} ↦ ⇑f, map_id := ⋯, map_comp := ⋯ }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.SingleObj

Goal state before:
pp: M G : Type u
inst✝² : Monoid M
inst✝¹ : Group G
N : Type v
inst✝ : Monoid N
⊢ Function.RightInverse (fun f ↦ { toFun := fun x ↦ f.map ((toEnd M) x), map_one' := ⋯, map_mul' := ⋯ }) fun f ↦
    { obj := id, map := fun {X Y} ↦ ⇑f, map_id := ⋯, map_comp := ⋯ }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝¹ Y✝¹ X✝ Y✝ Z : TopPair
X Y : TopPair
f : X ⟶ Y
⊢ ((𝟭 TopPair).map f ≫ ofHom (𝟙 fst) map ⋯).right = (ofHom (𝟙 fst) map ⋯ ≫ (proj₁ ⋙ diag).map f).right

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
⊢ pi γ₀ ⬝ pi γ₁ = pi fun i ↦ γ₀ i ⬝ γ₁ i

Tactic:
induction γ₁ using Quotient.induction_on_pi with | _ a =>
  induction γ₀ using Quotient.induction_on_pi
  simp only [Quotient.mk''_eq_mk, pi_lift]
  rw [← Path.Homotopic.Quotient.mk_trans, Path.trans_pi_eq_pi_trans, ← pi_lift]
  rfl

Goal state after:
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: case mpr.refine_1
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ((const Unit p).comp (const Y ())).Homotopic (ContinuousMap.id Y)

pp: case mpr.refine_2
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ((const Y ()).comp (const Unit p)).Homotopic (ContinuousMap.id Unit)

Tactic:
· exact h.symm

Goal state after:
case mpr.refine_2
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : (ContinuousMap.id Y).Homotopic (const Y p)
⊢ ((const Y ()).comp (const Unit p)).Homotopic (ContinuousMap.id Unit)
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ toHoCat.map (homMk (resolutionMap (𝟙 X))) = toHoCat.map (𝟙 (mk (resolutionObj X)))

Tactic:
exact resolutionObj_hom_ext (by simpa using .refl _)

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ toHoCat.map (homMk (resolutionMap (f ≫ g))) = toHoCat.map (homMk (resolutionMap f) ≫ homMk (resolutionMap g))

Tactic:
exact resolutionObj_hom_ext (by simpa using .refl _)

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
sq :
  CommSq (ι.map (f ≫ X₂.iBifibrantResolutionObj)) X₁.iBifibrantResolutionObj.hom
    (terminal.from (ι.obj (BifibrantObject.ιCofibrantObject.obj X₂.bifibrantResolutionObj)))
    (terminal.from (BifibrantObject.ιCofibrantObject.obj X₁.bifibrantResolutionObj).obj)
⊢ X₁.iBifibrantResolutionObj ≫ BifibrantObject.ιCofibrantObject.map (BifibrantObject.homMk sq.lift) =
    f ≫ X₂.iBifibrantResolutionObj

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
inst✝ : CategoryWithCofibrations C
X Y : Over S
f : X ⟶ Y
⊢ Cofibration f ↔ Cofibration (Over.Hom.left f)

Tactic:
by
  simp only [cofibration_iff, cofibrations_over_def, MorphismProperty.over_iff]

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
X : SSet
inst✝ : IsFilteredOrEmpty J
F : J ⥤ X.Subcomplex
j : SimplexCategoryᵒᵖ
⊢ (Preorder.colimitCoconeOfIsLUB (F ⋙ evaluation X j) ⋯).cocone.pt = (Preorder.colimitCoconeOfIsLUB F ⋯).cocone.pt.obj j

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₁ : X₁
hyz :
  (ConcreteCategory.hom f) s✝ = z₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) x₀ ∧ z₁ = (ConcreteCategory.hom f) y₀
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl z₁)

Tactic:
obtain rfl | ⟨_, _, h, h', rfl⟩ := hyz

Goal state after:
case inr_inl.inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) s✝))

case inr_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝¹ w✝ : S
h : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
h' : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) w✝¹
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
⊢ pushout.inl t l ≫ φ ≫ k = r'

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
⊢ pushout.inr t l ≫ φ ≫ k = b'

Tactic:
by cat_disch

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

Goal state before:
pp: case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton (n + 1) ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
simp only [sup_le_iff, iSup_le_iff, skeleton_succ]

Goal state after:
case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ≤
      Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ∧
    Y.skeleton n ≤
        Subcomplex.range i ⊔ Y.skeleton n ⊔
          ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ∧
      ∀ (i_1 : ↑(Y.nonDegenerate n)),
        Subcomplex.ofSimplex ↑i_1 ≤
          Subcomplex.range i ⊔ Y.skeleton n ⊔
            ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton (n + 1)

Tactic:
· simp only [sup_le_iff, iSup_le_iff]
    exact ⟨⟨le_sup_left, (Y.skeleton.monotone (by simp)).trans le_sup_right⟩,
      fun _ _ ↦ (Y.ofSimplex_le_skeleton _ (by simp)).trans le_sup_right⟩

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ t i d ≫ r i d = l i d ≫ b i d

Tactic:
ext c : 1
  simp [← cancel_mono (Subcomplex.ι _)]

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin m
f : X.Path m
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) (sx.spineToSimplex m h f) = f.arrow i

Tactic:
by
  rw [← spine_arrow, spine_spineToSimplex_apply]

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    sx.spineToDiagonal l ⋯ (f.interval j l hjl)

Tactic:
dsimp only [spineToDiagonal, Function.comp_apply]

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map (tr (diag l) ⋯ ⋯).op)) (sx.spineToSimplex l ⋯ (f.interval j l hjl))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).arrow i =
    ((X.spine m hₘ Δ).interval j l h).arrow i

Tactic:
· dsimp only [spine_arrow, Path.interval]
    rw [← Functor.map_comp_apply, ← op_comp, ← tr_comp,
      mkOfSucc_subinterval_eq]

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) (sx.spineToSimplex f) = f.arrow i

Tactic:
by
  rw [← spine_arrow, spine_spineToSimplex_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
    (((coyoneda.obj (op (𝟙_ C))).map f ⊗ₘ (coyoneda.obj (op (𝟙_ C))).map g) ≫ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) =
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (f ⊗ₘ g)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
f : nerve C _⦋1⦌
s : nerve C _⦋n⦌
h :
  (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) f =
    (ConcreteCategory.hom ((nerve C).map (⦋0⦌.const ⦋n⦌ 0).op)) s
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom ((nerve C).map (mkOfSucc 0).op))
        (ComposableArrows.precomp s (ComposableArrows.hom f ≫ eqToHom ⋯))) =
    eqToHom ⋯ ≫ ComposableArrows.hom f ≫ eqToHom ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
x : a✝ ⟶ d✝
w : b✝ ⟶ e✝
⊢ ∀ (h1 : x = f ≫ g ≫ h) (h2 : (f ≫ g ≫ h) ≫ i = f ≫ w) (h3 : w = g ≫ h ≫ i) (h4 : x ≫ i = (f ≫ g) ≫ h ≫ i),
    hComp (eqToIso h1).hom (𝟙 i) ≫ (eqToIso h2).hom ≫ hComp (𝟙 f) (eqToIso h3).hom =
      (eqToIso h4).hom ≫ (eqToIso pf✝).hom

Tactic:
rintro rfl _ rfl _

Goal state after:
C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
pf✝ : (f ≫ g) ≫ h ≫ i = f ≫ g ≫ h ≫ i
h2✝ : (f ≫ g ≫ h) ≫ i = f ≫ g ≫ h ≫ i
h4✝ : (f ≫ g ≫ h) ≫ i = (f ≫ g) ≫ h ≫ i
⊢ hComp (eqToIso ⋯).hom (𝟙 i) ≫ (eqToIso h2✝).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = (eqToIso h4✝).hom ≫ (eqToIso pf✝).hom
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
⊢ ∀ {X Y : Type vᵒᵖ} (f : X ⟶ Y),
    (enrichedNatTransYoneda F G).map f ≫
        { hom := ↾fun σ ↦ ↾fun x ↦ { app := fun X ↦ (ConcreteCategory.hom (σ.app X)) x, naturality := ⋯ },
            inv := ↾fun σ ↦ { app := fun X ↦ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X, naturality := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom =
      { hom := ↾fun σ ↦ ↾fun x ↦ { app := fun X_1 ↦ (ConcreteCategory.hom (σ.app X_1)) x, naturality := ⋯ },
            inv := ↾fun σ ↦ { app := fun X_1 ↦ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X_1, naturality := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_3
W : Type u_4
inst✝¹ : ReflQuiver V
inst✝ : ReflQuiver W
F : V ⥤rq W
⊢ ∀ (a b : V) (e : a ⟶ b),
    (FreeRefl.quotientFunctor V ⋙ freeReflMap F).map e.toPath =
      eqToHom ⋯ ≫ (freeMap F.toPrefunctor ⋙ FreeRefl.quotientFunctor W).map e.toPath ≫ eqToHom ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor.obj =
    ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor.obj

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v w : ReflQuiv
f : v ⟶ w
⊢ ∀ (a b : ↑(Quiv.of ↑v)) (e : a ⟶ b),
    ((ReflQuiv.forgetToQuiv ⋙ free).map f ≫ (FreeRefl.quotientFunctor ↑w).toCatHom).toFunctor.map e.toPath =
      eqToHom ⋯ ≫ ((FreeRefl.quotientFunctor ↑v).toCatHom ≫ freeRefl.map f).toFunctor.map e.toPath ≫ eqToHom ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : ReflQuiver W
inst✝² : ReflQuiver V
C : Type u_3
D : Type u_4
inst✝¹ : Category.{v_1, u_3} C
inst✝ : Category.{v_2, u_4} D
F : Cat.FreeRefl V ⥤ C
⊢ ∀ (v : V),
    (Cat.FreeRefl.lift ((fun F ↦ Cat.toFreeRefl V ⋙rq F.toReflPrefunctor) F)).obj (Cat.FreeRefl.mk v) =
      F.obj (Cat.FreeRefl.mk v)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : ReflQuiver W
inst✝² : ReflQuiver V
C : Type u_3
D : Type u_4
inst✝¹ : Category.{v_1, u_3} C
inst✝ : Category.{v_2, u_4} D
F : Cat.FreeRefl V ⥤ C
⊢ ∀ {v w : V} (f : v ⟶ w),
    (Cat.FreeRefl.lift ((fun F ↦ Cat.toFreeRefl V ⋙rq F.toReflPrefunctor) F)).map (Cat.FreeRefl.homMk f) =
      eqToHom ⋯ ≫ F.map (Cat.FreeRefl.homMk f) ≫ eqToHom ⋯

Tactic:
by cat_disch

Goal state after: