mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ f z =
    colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫
      colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
        ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Tactic:
ι_colimMap_assoc,

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
j : J
⊢ colimit.ι (pullback c.ι ((Functor.const J).map z)) j ≫ f z =
    (pullback.snd c.ι ((Functor.const J).map z)).app j ≫
      colimit.ι ((Functor.const J).obj X) j ≫
        ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
X Y : C
f : X ⟶ Y
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
j : J
i i' : ↑(Set.Iic j)
φ : i ⟶ i'
⊢ (⋯.functor ⋙ c.F).map φ ≫ c.F.map (homOfLE ⋯) =
    c.F.map (homOfLE ⋯) ≫ ((Functor.const ↑(Set.Iic j)).obj (c.F.obj j)).map φ

Tactic:
dsimp
        rw [← Functor.map_comp, Category.comp_id]
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f

Tactic:
obtain ⟨J, _, _, _, _, hf⟩ := hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
J : Type w
w✝³ : LinearOrder J
w✝² : SuccOrder J
w✝¹ : OrderBot J
w✝ : WellFoundedLT J
hf : W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f
⊢ W f

Tactic:
obtain ⟨J, _, _, _, _, hf⟩ := hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
J : Type w
w✝³ : LinearOrder J
w✝² : SuccOrder J
w✝¹ : OrderBot J
w✝ : WellFoundedLT J
hf : W.transfiniteCompositionsOfShape J f
⊢ W f
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
⊢ iter.F.obj ⟨⊥, ⋯⟩ = Φ.X₀

Tactic:
obj_bot

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
⊢ Φ.X₀ = Φ.X₀
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁✝¹ : i < Order.succ j
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁),

Goal state after:
case inl
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁✝¹ : i < Order.succ j
hi₁✝ : i ≤ j
hi₁ : i < j
⊢ arrowMap iter.F i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).obj ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
⊢ (ConcreteCategory.hom ((sqFunctor c p f g).map (homOfLE ⋯).op))
      (have this := ⋯;
      have this_1 := ⋯;
      { f' := ⋯.lift, w₁ := ⋯, w₂ := ⋯ }) =
    sq'

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
⊢ ∀ {g_1 : B ⟶ Y} (sq : CommSq g i (πObj I κ f) g_1), sq.HasLift

Tactic:
b

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
⊢ ∀ (sq : CommSq g i (πObj I κ f) b), sq.HasLift
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝¹ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
⊢ ((relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f) ≫
      (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).symm.hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).hom ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom

Tactic:
dsimp; rw [πFunctorObj_eq, assoc, Iso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (p ^ n * q ^ m) = m

Tactic:
rw [mul_comm (p ^ n) (q ^ m)]
  exact padicValNat_mul_pow_left m n ne

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Prime p)
⊢ max (log p n) (padicValNat p (n + 1)) = log p (n + 1)

Tactic:
apply le_antisymm (max_le (le_log_of_pow_le hp.out.one_lt (pow_log_le_add_one p n))
    (padicValNat_le_nat_log (n + 1)))
  rw [le_max_iff, or_iff_not_imp_left, not_le]
  intro h
  replace h := le_antisymm (add_one_le_iff.mpr (lt_pow_of_log_lt hp.out.one_lt h))
    (pow_log_le_self p n.succ_ne_zero)
  rw [h, padicValNat.prime_pow, ← h]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ ↑(p ^ n) ∣ a

Tactic:
Int.natCast_pow

Goal state after:
p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ ↑p ^ n ∣ a
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
f : X ⟶ Y
hf✝ : (ConcreteCategory.hom (F.map f)) x = y
g : X ⟶ Y
hf : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
hg : (ConcreteCategory.hom (F.map g)) x = y
h : IsLimit (Fork.ofι (F.map (equalizer.ι f g)) ⋯) := ⋯
h' : IsLimit Types.equalizerLimit.cone := ⋯
⊢ ↑(⟨equalizer.ι f g, ⋯⟩ ≫ ⟨f, hf✝⟩) = ↑(⟨equalizer.ι f g, ⋯⟩ ≫ ⟨g, hg⟩)

Tactic:
exact equalizer.condition f g

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : C
x : F.obj X
X✝ Y✝ : Over (F.elementsMk X x)
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom ((fromOverFunctor F x).map (Over.homMk ↑(Over.Hom.left f) ⋯)))
      ((fromOverFunctor F x).elementsMk (Over.mk ↑X✝.hom) ⟨X✝.left.snd, ⋯⟩).snd =
    ((fromOverFunctor F x).elementsMk (Over.mk ↑Y✝.hom) ⟨Y✝.left.snd, ⋯⟩).snd

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ (if ↑f (stationaryPoint hf) = 0 then 0 else ↑p ^ (-padicValRat p (↑f (stationaryPoint hf)))) =
    ↑p ^ (-padicValRat p (↑f (stationaryPoint hf)))

Tactic:
if_neg

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ ↑p ^ (-padicValRat p (↑f (stationaryPoint hf))) = ↑p ^ (-padicValRat p (↑f (stationaryPoint hf)))

case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ ¬↑f (stationaryPoint hf) = 0
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
inst✝¹ : HasEqualizers C
inst✝ : ∀ (i : I), PreservesLimitsOfShape WalkingParallelPair (F i)
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [Mono f], (∀ (i : I), IsIso ((F i).map f)) → IsIso f
X Y : C
f g : X ⟶ Y
hfg : ∀ (i : I), (F i).map f = (F i).map g
i : I
hc : IsLimit (Fork.ofι ((F i).map (equalizer.ι f g)) ⋯) := isLimitForkMapOfIsLimit (F i) ⋯ (equalizerIsEqualizer f g)
l : (F i).obj X ⟶ (Fork.ofι ((F i).map (equalizer.ι f g)) ⋯).pt
hl : l ≫ (Fork.ofι ((F i).map (equalizer.ι f g)) ⋯).ι = 𝟙 ((F i).obj X)
⊢ ((F i).map (equalizer.ι f g) ≫ l) ≫ (Fork.ofι ((F i).map (equalizer.ι f g)) ⋯).ι =
    𝟙 ((F i).obj (equalizer f g)) ≫ (Fork.ofι ((F i).map (equalizer.ι f g)) ⋯).ι

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
inst✝¹ : HasEqualizers C
inst✝ : ∀ (i : I), PreservesLimitsOfShape WalkingParallelPair (F i)
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [Mono f], (∀ (i : I), IsIso ((F i).map f)) → IsIso f
X Y : C
f g : X ⟶ Y
hfg : ∀ (i : I), (F i).map f = (F i).map g
i : I
hc : IsLimit (Fork.ofι ((F i).map (equalizer.ι f g)) ⋯) := isLimitForkMapOfIsLimit (F i) ⋯ (equalizerIsEqualizer f g)
l : (F i).obj X ⟶ (Fork.ofι ((F i).map (equalizer.ι f g)) ⋯).pt
hl : l ≫ (Fork.ofι ((F i).map (equalizer.ι f g)) ⋯).ι = 𝟙 ((F i).obj X)
⊢ l ≫ (F i).map (equalizer.ι f g) = 𝟙 ((F i).obj X)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
P Q : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
⊢ (fun g ↦ Φ.presheafFiberDesc (fun X x ↦ g.app (op X) ≫ Pi.π (fun t ↦ M) x) ⋯)
      ((fun f ↦ { app := fun X ↦ Pi.lift fun x ↦ Φ.toPresheafFiber (unop X) x P ≫ f, naturality := ⋯ }) f) =
    f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasProducts A
P Q : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
g : P ⟶ Φ.skyscraperPresheaf M
⊢ (fun f ↦ { app := fun X ↦ Pi.lift fun x ↦ Φ.toPresheafFiber (unop X) x P ≫ f, naturality := ⋯ })
      ((fun g ↦ Φ.presheafFiberDesc (fun X x ↦ g.app (op X) ≫ Pi.π (fun t ↦ M) x) ⋯) g) =
    g

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
have hcfg : (f + g).norm = g.norm := norm_equiv hfg'

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : (f + g).norm = g.norm
⊢ (f + g).norm ≤ max f.norm g.norm
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
R : CommRingCat
j : Spec (CommRingCat.of ↑R) ⟶ Y
w✝ : IsOpenImmersion j
y' : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of ↑R)
hy : (y' ≫ j) ≫ f = s
⊢ (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map (MorphismProperty.Over.homMk j ⋯ ⋯)))
      ((Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).obj
          ((AffineEtale.Spec S ⋙ Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).elementsMk (AffineEtale.mk (j ≫ f))
            (Over.homMk y' ⋯))).snd =
    ⟨Etale.mk f, Over.homMk (y' ≫ j) ⋯⟩.snd

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : Scheme
f : X ⟶ S
x✝ : Etale f
R : Sieve (Etale.mk f)
hR : R ∈ S.smallEtaleTopology (Etale.mk f)
φ : Spec (CommRingCat.of Ω) ⟶ X
𝒰 : Cover (precoverage @Etale) (Etale.mk f).left
h : Cover.Over S 𝒰
w✝ : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ S)
le : 𝒰.toPresieveOverProp w✝ ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = φ default
l : Spec (CommRingCat.of Ω) ⟶ 𝒰.X i
hl₁ : l ≫ 𝒰.f i = φ
hl₂ : l default = y
this : 𝒰.f i ≫ f = 𝒰.X i ↘ S
⊢ (ConcreteCategory.hom
        ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk (φ ≫ f)))).map (MorphismProperty.Over.homMk (𝒰.f i) ⋯ True.intro)))
      (Over.homMk l ⋯) =
    Over.homMk φ ⋯

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a : C
g : F.obj a ⟶ Y
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ ∃ b snd fst, IsPullback fst (F.map snd) f g

Tactic:
refine ⟨c, g_snd, g_fst, BC⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a : yoneda.obj X ⟶ F
⊢ ∀ {b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b

Tactic:
b

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type v₁
f : F ⟶ G
hf : (monomorphisms C).presheaf f
X : C
a b : yoneda.obj X ⟶ F
⊢ a ≫ f = b ≫ f → a = b
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (fun i j hij ↦ ((alternatingFaceMapComplex C).map f).f i ≫ hσ' q i j hij) = fun i j hij ↦
    hσ' q i j hij ≫ ((alternatingFaceMapComplex C).map f).f j

Tactic:
ext n m hnm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
n m : ℕ
hnm : (ComplexShape.down ℕ).Rel m n
⊢ ((alternatingFaceMapComplex C).map f).f n ≫ hσ' q n m hnm = hσ' q n m hnm ≫ ((alternatingFaceMapComplex C).map f).f m
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
X : D
h : F.relativelyRepresentable (Limits.diag X)
a : C
g : F.obj a ⟶ X
⊢ Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv

Tactic:
by cat_disch

Goal state after:
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
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
⊢ (limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
        (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
          (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯) ≫
      (prodIsoPullback X X).inv =
    (pullback.congrHom ⋯ ⋯ ≪≫
          (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
            (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom ≫
      prodMap

Tactic:
by cat_disch

Goal state after:
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
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
pbRepr : (PullbackCone.mk ⋯.choose (F.map ⋯.choose) ⋯).pt ≅
  ((PullbackCone.mk
          ((limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
            (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
              (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯))
          (pullback.congrHom ⋯ ⋯ ≪≫
              (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
                (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom
          ⋯).pasteHoriz
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
          ⋯)
        ⋯)
      ⋯).pt :=
  ⋯.some.conePointUniqueUpToIso (pasteHorizIsPullback ⋯ ⋯.some left)
⊢ pbRepr.hom ≫ pullback.fst g g' = pbRepr.hom ≫ pullback.fst g g'

Tactic:
by cat_disch

Goal state after:
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
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
g' : F.obj a' ⟶ X
toCommSq✝ :
  CommSq (pullback.fst g g' ≫ g)
    (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯ ⋯)
    (pullback.diagonal (terminal.from X))
    (pullback.map (g ≫ terminal.from X) (g' ≫ terminal.from X) (terminal.from X) (terminal.from X) g g' (𝟙 (⊤_ D)) ⋯ ⋯)
left :
  IsLimit
    (PullbackCone.mk (pullback.fst g g' ≫ g)
      (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
        ⋯)
      ⋯)
prodMap : F.obj (a ⨯ a') ⟶ X ⨯ X :=
  (preservesLimitIso F (pair a a') ≪≫ HasLimit.isoOfNatIso (pairComp a a' F)).hom ≫ prod.map g g'
pbRepr : (PullbackCone.mk ⋯.choose (F.map ⋯.choose) ⋯).pt ≅
  ((PullbackCone.mk
          ((limit.isLimit (cospan (terminal.from X) (terminal.from X))).1
            (PullbackCone.mk (pullback.fst (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g)
              (pullback.snd (g ≫ terminal.from X) (g' ≫ terminal.from X) ≫ g') ⋯))
          (pullback.congrHom ⋯ ⋯ ≪≫
              (prodIsoPullback (F.obj a) (F.obj a')).symm ≪≫
                (HasLimit.isoOfNatIso (pairComp a a' F)).symm ≪≫ (preservesLimitIso F (pair a a')).symm).hom
          ⋯).pasteHoriz
      (PullbackCone.mk (pullback.fst g g' ≫ g)
        (pullback.map g g' (g ≫ terminal.from X) (g' ≫ terminal.from X) (𝟙 (F.obj a)) (𝟙 (F.obj a')) (terminal.from X) ⋯
          ⋯)
        ⋯)
      ⋯).pt :=
  ⋯.some.conePointUniqueUpToIso (pasteHorizIsPullback ⋯ ⋯.some left)
⊢ pbRepr.hom ≫ pullback.snd g g' = F.map (F.preimage (pbRepr.hom ≫ pullback.snd g g'))

Tactic:
by cat_disch

Goal state after:
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✝ F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
a : C
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
g : F.obj a ⟶ Limits.pullback (terminal.from X) (terminal.from X)
⊢ 𝟙 (F.obj a) ≫ (g ≫ pullback.fst (terminal.from X) (terminal.from X)) ≫ terminal.from X =
    𝟙 (F.obj a) ≫ (g ≫ pullback.snd (terminal.from X) (terminal.from X)) ≫ terminal.from X

Tactic:
by cat_disch

Goal state after: