mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Tactic:
refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩

Goal state after:
case inl.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y

case inl.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Tactic:
refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y

case inr.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
⊢ b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)

Tactic:
· rfl

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
val✝ : X.X
⊢ ↑(ConcreteCategory.hom
          ((fun f ↦
                {
                  hom :=
                    { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
              ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom f.hom) (some val✝)

Tactic:
· rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
j : J
h : X = Y
⊢ (hom (limit.π (homDiagram X Y) j)) (eqToHom h) = eqToHom ⋯

Tactic:
subst h

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j : J
⊢ (hom (limit.π (homDiagram X X) j)) (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : ↑s.pt
⊢ ∀ (Y : ↑s.pt) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
Y

Goal state after:
case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X Y : ↑s.pt
⊢ ∀ (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂L X Y Z).hom = X ◁ coprod.inl

Tactic:
by
  rw [leftDistrib_hom, coprod.inl_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: case h₁
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ coprod.inl ≫ curry (∂L X Y Z).inv = coprod.inl ≫ coprod.desc (curry coprod.inl) (curry coprod.inr)

Tactic:
simp [← curry_natural_left]

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: case h₂
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ coprod.inr ≫ curry (∂L X Y Z).inv = coprod.inr ≫ coprod.desc (curry coprod.inl) (curry coprod.inr)

Tactic:
simp [← curry_natural_left]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ (h.from { V := F.obj A.V, str := F.map A.str }).f ≫ A.str = 𝟙 (F.obj A.V)

Tactic:
← (h.from ⟨F.obj A.V, F.map A.str⟩).h,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ { V := F.obj A.V, str := F.map A.str }.str ≫ F.map (h.from { V := F.obj A.V, str := F.map A.str }).f = 𝟙 (F.obj A.V)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
j : J
⊢ (homEquiv V) τ ≫ enrichedHomπ V F₁ F₂ j = (eHomEquiv V) (τ.app j)

Tactic:
simp [homEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
hRS : R = S
b : 𝒳
hb : p.obj b = S
⊢ p.IsHomLift (eqToHom hRS) (𝟙 b)

Tactic:
subst hRS hb

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
b : 𝒳
⊢ p.IsHomLift (eqToHom ⋯) (𝟙 b)
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : a' = a
⊢ p.IsHomLift f (eqToHom h ≫ φ)

Tactic:
subst h

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
b : 𝒳
f : R ⟶ S
a' : 𝒳
φ : a' ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift f (eqToHom ⋯ ≫ φ)
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
b' : 𝒳
h : b = b'
⊢ p.IsHomLift f (φ ≫ eqToHom h)

Tactic:
subst h

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift f (φ ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
R' : 𝒮
h : R' = R
⊢ p.IsHomLift (eqToHom h ≫ f) φ

Tactic:
subst h

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
R' : 𝒮
f : R' ⟶ S
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift (eqToHom ⋯ ≫ f) φ
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
S' : 𝒮
h : S = S'
⊢ p.IsHomLift (f ≫ eqToHom h) φ

Tactic:
subst h

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.IsHomLift (f ≫ eqToHom ⋯) φ
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a' a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : a' = a
hφ' : p.IsHomLift f (eqToHom h ≫ φ)
⊢ p.IsHomLift f φ

Tactic:
subst h

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a' b : 𝒳
f : R ⟶ S
φ : a' ⟶ b
hφ' : p.IsHomLift f (eqToHom ⋯ ≫ φ)
⊢ p.IsHomLift f φ
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b b' : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : b = b'
hφ' : p.IsHomLift f (φ ≫ eqToHom h)
⊢ p.IsHomLift f φ

Tactic:
subst h

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
hφ' : p.IsHomLift f (φ ≫ eqToHom ⋯)
⊢ p.IsHomLift f φ
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R' R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : R' = R
hφ' : p.IsHomLift (eqToHom h ≫ f) φ
⊢ p.IsHomLift f φ

Tactic:
subst h

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R' S : 𝒮
a b : 𝒳
φ : a ⟶ b
f : R' ⟶ S
hφ' : p.IsHomLift (eqToHom ⋯ ≫ f) φ
⊢ p.IsHomLift f φ
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S S' : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : S = S'
hφ' : p.IsHomLift (f ≫ eqToHom h) φ
⊢ p.IsHomLift f φ

Tactic:
subst h

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
hφ' : p.IsHomLift (f ≫ eqToHom ⋯) φ
⊢ p.IsHomLift f φ
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
toNatTrans✝ : NatTrans F.toFunctor G.toFunctor
isHomLift'✝ : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (toNatTrans✝.app a)
h : { toNatTrans := toNatTrans✝, isHomLift' := isHomLift'✝ }.toNatTrans = β.toNatTrans
⊢ { toNatTrans := toNatTrans✝, isHomLift' := isHomLift'✝ } = β

Tactic:
subst h

Goal state after:
case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
isHomLift'✝ : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (β.app a)
⊢ { toNatTrans := β.toNatTrans, isHomLift' := isHomLift'✝ } = β
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ (enrichedHomπ V F₁ F₂ (G.obj i) ≫
        eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫ eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i)) ≫
      ((diagram V F₁' F₂').obj (Opposite.op i)).map f =
    (enrichedHomπ V F₁ F₂ (G.obj j) ≫
        eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫ eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j)) ≫
      ((diagram V F₁' F₂').map f.op).app j

Tactic:
dsimp
      rw [assoc, assoc, assoc, assoc, ← eHomWhiskerLeft_comp,
        ← eHom_whisker_exchange, ← e₂.hom.naturality f,
        eHomWhiskerLeft_comp_assoc]
      dsimp
      rw [enrichedHom_condition_assoc, eHom_whisker_exchange,
        eHom_whisker_exchange, ← eHomWhiskerRight_comp_assoc,
        ← eHomWhiskerRight_comp_assoc, NatTrans.naturality]
      dsimp

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case refine_1
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ homCartesianLift f g φ' ≫ cartesianLift a f = φ'

pp: case refine_2
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ ∀ (y : a' ⟶ domainCartesianLift a f),
    (fun χ ↦ (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ') y → y = homCartesianLift f g φ'

Tactic:
· exact Hom.ext _ _ (by simpa using IsHomLift.fac (forget F) (g ≫ f) φ')
        (by simp [← Cat.Hom₂.comp_app])

Goal state after:
case refine_2
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ ∀ (y : a' ⟶ domainCartesianLift a f),
    (fun χ ↦ (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ') y → y = homCartesianLift f g φ'
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ W.Q.HasRightKanExtension F ↔ F'.HasLeftDerivedFunctor W

Tactic:
hasLeftDerivedFunctor_iff F' W.Q W,

Goal state after:
C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ W.Q.HasRightKanExtension F ↔ W.Q.HasRightKanExtension F'
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
m : s.pt ⟶ G.obj (L.obj Y)
hm : ∀ (j : StructuredArrow (L.obj Y) L), m ≫ G.map j.hom ≫ e.inv.app j.right = s.π.app j
this : m ≫ G.map (𝟙 (L.obj Y)) ≫ e.inv.app Y = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y)))
⊢ m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y

Tactic:
simp [← reassoc_of% this]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
⊢ β ≫
      L₂.whiskerLeft
        (F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom) =
    β ≫ L₂.whiskerLeft (𝟙 F')

Tactic:
ext X₂

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
⊢ (β ≫
          L₂.whiskerLeft
            (F'.leftUnitor.inv ≫
              F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom)).app
      X₂ =
    (β ≫ L₂.whiskerLeft (𝟙 F')).app X₂
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ ∀ {Y : C} (f : X ⟶ Y), Mono (F.map f) → Mono f

Tactic:
Y

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
⊢ ∀ (f : X ⟶ Y), Mono (F.map f) → Mono f
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
⊢ ∀ (X : C), n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
induction n using Nat.strongRecOn with | _ n hi
  intro X hn
  by_cases h : IsConnected X
  · exact has_decomp_connected_components_aux_conn X
  by_cases nhi : IsInitial X → False
  · obtain ⟨Y, v, hni, hvmono, hvnoiso⟩ :=
      has_non_trivial_subobject_of_not_isConnected_of_not_initial X h nhi
    obtain ⟨Z, u, ⟨c⟩⟩ := PreGaloisCategory.monoInducesIsoOnDirectSummand v
    let t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
    have hn1 : Nat.card (F.obj Y) < n := by
      rw [hn]
      exact lt_card_fiber_of_mono_of_notIso F v hvnoiso
    have i : X ≅ Y ⨿ Z := (colimit.isoColimitCocone t).symm
    have hnn : Nat.card (F.obj X) = Nat.card (F.obj Y) + Nat.card (F.obj Z) := by
      rw [card_fiber_eq_of_iso F i]
      exact card_fiber_coprod_eq_sum F Y Z
    have hn2 : Nat.card (F.obj Z) < n := by
      rw [hn, hnn, lt_add_iff_pos_left]
      exact Nat.pos_of_ne_zero (non_zero_card_fiber_of_not_initial F Y hni)
    let ⟨ι₁, f₁, g₁, hc₁, hf₁, he₁⟩ := hi (Nat.card (F.obj Y)) hn1 Y rfl
    let ⟨ι₂, f₂, g₂, hc₂, hf₂, he₂⟩ := hi (Nat.card (F.obj Z)) hn2 Z rfl
    refine ⟨ι₁ ⊕ ι₂, Sum.elim f₁ f₂,
      Cofan.combPairHoms (Cofan.mk Y g₁) (Cofan.mk Z g₂) (BinaryCofan.mk v u), ?_⟩
    use Cofan.combPairIsColimit hc₁ hc₂ c
    refine ⟨fun i ↦ ?_, inferInstance⟩
    cases i
    · exact hf₁ _
    · exact hf₂ _
  · simp only [not_forall, not_false_eq_true] at nhi
    obtain ⟨hi⟩ := nhi
    exact has_decomp_connected_components_aux_initial X hi

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
⊢ inj bc WalkingPair.right ≫ m =
    inj bc WalkingPair.right ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯

Tactic:
refine Cofan.IsColimit.hom_ext h₂ _ _ (fun a ↦ by aesop)

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).obj
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
j : ι
z : ToType ((Discrete.functor f ⋙ F).obj { as := j })
h : (ConcreteCategory.hom (s.ι.app { as := j })) z = x
⊢ (ConcreteCategory.hom (F.map (g j))) z = x

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
ι : Type
f : ι → C
g : (i : ι) → f i ⟶ X
hl : IsColimit (Cofan.mk X g)
hc : ∀ (i : ι), IsConnected (f i)
he : Finite ι
s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
s' : IsColimit s := isColimitOfPreserves F hl
j : ι
z : ToType ((Discrete.functor f ⋙ F).obj { as := j })
⊢ (ConcreteCategory.hom (F.map (g j))) z = (ConcreteCategory.hom (s.ι.app { as := j })) z
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b

Tactic:
let Y : C := pullback i j
  let u : Y ⟶ A := pullback.fst i j
  let v : Y ⟶ B := pullback.snd i j
  let G := F ⋙ FintypeCat.incl
  let e : F.obj Y ≃ { p : F.obj A × F.obj B // F.map i p.1 = F.map j p.2 } :=
    fiberPullbackEquiv F i j
  let y : F.obj Y := e.symm ⟨(a, b), h⟩
  have hn : IsInitial Y → False := not_initial_of_inhabited F y
  have : IsIso u := IsConnected.noTrivialComponent Y u hn
  have : IsIso v := IsConnected.noTrivialComponent Y v hn
  use (asIso u).symm ≪≫ asIso v
  have hu : G.map u y = a := fiberPullbackEquiv_symm_fst_apply _ _ _ h
  have hv : G.map v y = b := fiberPullbackEquiv_symm_snd_apply _ _ _ h
  rw [← hu, ← hv]
  change (F.map u ≫ F.map _) y = F.map v y
  simp only [← F.map_comp, Iso.trans_hom, Iso.symm_hom, asIso_inv, asIso_hom,
    IsIso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Type

Goal state before:
pp: X : Type u
⊢ ∀ ⦃Y : Type u⦄ (f g : X ⟶ Y),
    (∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g

Tactic:
Y

Goal state after:
X Y : Type u
⊢ ∀ (f g : X ⟶ Y), (∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
g : G
X : C
⊢ ∀ {Y : C} (f : X ⟶ Y), F.map f ≫ (isoOnObj F g Y).hom = (isoOnObj F g X).hom ≫ F.map f

Tactic:
Y

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
g : G
X Y : C
⊢ ∀ (f : X ⟶ Y), F.map f ≫ (isoOnObj F g Y).hom = (isoOnObj F g X).hom ≫ F.map f