mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
X : B
⊢ otherMap L U' adj₁ adj₂ X ≫ U'.map (adj₁.counit.app (F.obj X)) = 𝟙 (U'.obj (F.obj ((𝟭 B).obj X)))

Tactic:
simp only [otherMap, assoc, ← Functor.map_comp]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
X : B
⊢ adj₂.unit.app (U'.1 (F.obj X)) ≫
      U'.map
        (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X))) ≫ adj₁.counit.app (F.obj X)) =
    𝟙 (U'.obj (F.obj ((𝟭 B).obj X)))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
X : B
⊢ otherMap L U' adj₁ adj₂ X ≫ U'.map (adj₁.counit.app (F.obj X)) = 𝟙 (U'.obj (F.obj ((𝟭 B).obj X)))

Tactic:
simp only [otherMap, assoc, ← Functor.map_comp]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
⊢ Function.Injective (⇑(q.adj₁.homEquiv (F.obj (G.obj Y)) X) ∘ fun g ↦ L.map (q.adj₂.counit.app Y) ≫ g) ↔
    Function.Injective fun g ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
Function.comp_def,

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
⊢ (Function.Injective fun x ↦ (q.adj₁.homEquiv (F.obj (G.obj Y)) X) (L.map (q.adj₂.counit.app Y) ≫ x)) ↔
    Function.Injective fun g ↦ g ≫ q.adj₃.unit.app (F.obj X)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
⊢ [Inhabited B] → Inhabited (FreeBicategory B)

Tactic:
by
  intro h
  exact id h

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ⟶ t
x : B
h : c ⟶ x
⊢ StructuredArrow.hom (s.whisker h) ≫ (precomp x f).map (StructuredArrow.Hom.right i ▷ h) =
    StructuredArrow.hom (t.whisker h)

Tactic:
rw [← cancel_mono (α_ _ _ _).inv]
    calc
      _ = (unit s ≫ f ◁ i.right) ▷ h := by simp [-LeftExtension.w]
      _ = unit t ▷ h := congrArg (· ▷ h) (LeftExtension.w i)
      _ = _ := by simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' f (𝟙 b₁) f ⋯).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv

Tactic:
by
  simp [mapComp'_comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.mapComp' f (𝟙 b₁) f ⋯).inv = F.map f ◁ (F.mapId b₁).hom ≫ (ρ_ (F.map f)).hom

Tactic:
by
  simp [mapComp'_comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_have 1 → 2
  | h => IsAbsKan.hasAbsLeftKanLift (Adjunction.ofIsRightAdjoint u).isAbsoluteLeftKanLift

Goal state after:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).inv =
    F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
        (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).inv

Tactic:
simp [← whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv _ _ _ _ _ _ f h₀₂ h₁₃ hf]

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
i : J
hi : i ∈ l
⊢ Zigzag i j₂

Tactic:
apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := ⋯
i : J
hi : i ∈ l
⊢ ∀ ⦃x y : J⦄, Zag x y → Zigzag y j₂ → Zigzag x j₂

J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := ⋯
i : J
hi : i ∈ l
⊢ Zigzag j₂ j₂
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ fixInduction h H = H a h fun x h' ↦ fixInduction ⋯ H

Tactic:
unfold fixInduction

Goal state after:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
⊢ (have h₂ := ⋯;
    (fun pf pf_1 h₂ ↦
        Acc.rec (motive := fun {a} pf_2 ↦
          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 pf_2 →
            C a)
          (fun a ha IH h₂ ↦
            have h := ⋯;
            H a h fun a' fa' ↦ IH a' fa' ⋯)
          pf_1 h₂)
      ⋯ ⋯ h₂) =
    H a h fun x h' ↦
      have h₂ := ⋯;
      (fun pf pf_1 h₂ ↦
          Acc.rec (motive := fun {a} pf_2 ↦
            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 pf_2 →
              (fun x ↦ C x) a)
            (fun a ha IH h₂ ↦
              have h := ⋯;
              H a h fun a' fa' ↦ IH a' fa' ⋯)
            pf_1 h₂)
        ⋯ ⋯ h₂
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ (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) =
    f

Tactic:
ext (_ | _) : 4
            · exact f.hom.map_snd.symm
            · rfl

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} D₁
inst✝² : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝¹ : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
inst✝ : W₂.ContainsIdentities
hF : (W₁.prod W₂).IsInvertedBy F
x✝¹ x✝ : C₁
f₁ : x✝¹ ⟶ x✝
hf₁ : W₁ f₁
this : ∀ (X₂ : C₂), IsIso (((curry.obj F).map f₁).app X₂)
⊢ IsIso ((curry.obj F).map f₁)

Tactic:
apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
X✝ Y✝ : C₂
f₂ : X✝ ⟶ Y✝
hf₂ : W₂ f₂
this : ∀ (X₁ : W₁.Localization), IsIso (((prodLift₁ F hF).flip.map f₂).app X₁)
⊢ IsIso ((prodLift₁ F hF).flip.map f₂)

Tactic:
apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
⊢ Functor.whiskerRight (pullbackId X).hom (map (𝟙 X)) ≫ (mapPullbackAdj (𝟙 X)).counit = (mapPullbackAdj (𝟙 X)).counit

Tactic:
by
  have := Adjunction.rightAdjointUniq_hom_counit (mapPullbackAdj (𝟙 X)) (id X).mapPullbackAdj
  rw [pullbackId, Adjunction.rightAdjointUniq_hom_counit]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (f ⊗ₘ g)

Tactic:
tensorHom_def

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (f ▷ Y₁ ≫ X₂ ◁ g)
Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : HasFibers p
S : 𝒮
a b : Fib p S
φ : a ⟶ b
⊢ 𝟙 S = eqToHom ⋯ ≫ p.map ((ι S).map φ) ≫ eqToHom ⋯

Tactic:
rw [← Functor.comp_map, Functor.congr_hom (comp_const S)]

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : HasFibers p
S : 𝒮
a b : Fib p S
φ : a ⟶ b
⊢ 𝟙 S = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ ((const (Fib p S)).obj S).map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∀ (y : Aut B),
    (fun τ ↦ f ≫ τ.hom = σ.hom ≫ f) y →
      y =
        (evaluationEquivOfIsGalois F B ((ConcreteCategory.hom (F.map f)) a)).symm
          ((ConcreteCategory.hom (F.map (σ.hom ≫ f))) a)

Tactic:
intro τ

Goal state after:
case refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
τ : Aut B
⊢ (fun τ ↦ f ≫ τ.hom = σ.hom ≫ f) τ →
    τ =
      (evaluationEquivOfIsGalois F B ((ConcreteCategory.hom (F.map f)) a)).symm
        ((ConcreteCategory.hom (F.map (σ.hom ≫ f))) a)
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.EssSurj

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)
⊢ (coconeQuotientDiag h u hUinV).ι.app j ≫ coconeQuotientDiagDesc h u hUinV s = s.ι.app j

Tactic:
apply (cancel_epi u.inv).mp

Goal state after:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)
⊢ u.inv ≫ (coconeQuotientDiag h u hUinV).ι.app j ≫ coconeQuotientDiagDesc h u hUinV s = u.inv ≫ s.ι.app j
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ Symmetrify.of ⋙q Symmetrify.lift φ = φ

Tactic:
Quiver.Symmetrify.lift_spec

Goal state after:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ φ = φ
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Groupoid E
F : C ⥤ D
G : D ⥤ E
⊢ map F ⋙ lift G = lift (F ⋙ G)

Tactic:
by
  apply lift_unique
  rw [← Functor.assoc, of_comp_map, Functor.assoc, lift_spec G]

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
⊢ (Over.forget (F.obj X)).map
        (Over.homMk
          (prod.lift
              (have this := W.hom;
              this)
              g ≫
            inv (prodComparison F X Z))
          ⋯) ≫
      (TwoSquare.overPost F X).app (Over.mk prod.fst) ≫ F.map prod.snd =
    g

Tactic:
by simp [inv_prodComparison_map_snd]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
h1 : ∀ σ ∈ U, σ.hom.app A = 𝟙 (F.obj A)
σ : Aut F
σinU : σ ∈ U
X : C
hX : X ∈ I
x : (F.obj X).obj
p : A ⟶ X := f ≫ Pi.π (fun Z ↦ ↑Z) ⟨X, hX⟩
⊢ (ConcreteCategory.hom (σ.hom.app ↑⟨X, hX⟩)) x = (ConcreteCategory.hom (𝟙 (F.obj ↑⟨X, hX⟩))) x

Tactic:
have : IsConnected X := hc X hX

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝¹ : ∀ (X : ↑I), IsConnected ↑X
this✝ : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
h1 : ∀ σ ∈ U, σ.hom.app A = 𝟙 (F.obj A)
σ : Aut F
σinU : σ ∈ U
X : C
hX : X ∈ I
x : (F.obj X).obj
p : A ⟶ X := f ≫ Pi.π (fun Z ↦ ↑Z) ⟨X, hX⟩
this : IsConnected X
⊢ (ConcreteCategory.hom (σ.hom.app ↑⟨X, hX⟩)) x = (ConcreteCategory.hom (𝟙 (F.obj ↑⟨X, hX⟩))) x
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul (Aut F) X.V.obj
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Tactic:
obtain ⟨ι, hfin, f, ⟨u⟩⟩ := has_decomp_quotients X
  choose g gu using (fun i ↦ exists_lift_of_quotient_openSubgroup (f i))
  exact ⟨∐ g, ⟨PreservesCoproduct.iso (functorToAction F) g ≪≫
    Sigma.mapIso (fun i ↦ (gu i).some) ≪≫ u⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : HasPullbacks C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal Y
⊢ HasLiftingProperty g (Opposite.op (Arrow.mk f) ⋔ Arrow.mk (t.from X)).hom ↔
    HasLiftingProperty g ((MonoidalClosed.pre f).app X)

Tactic:
exact HasLiftingProperty.iff_of_arrow_iso_right g (PullbackHom.isTerminalIso _ t)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
j : J
x : ↑(F.obj j)
j' : J
i y : j ⟶ j'
g : (ConcreteCategory.hom (F.map i)) x = (ConcreteCategory.hom (F.map y)) 0
⊢ ∃ j' i, (ModuleCat.Hom.hom (F.map i)) x = 0

Tactic:
exact ⟨j', i, g ▸ by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
U : FormalCoproduct C
T : C
hT : IsTerminal T
n : ℕ
this : HasProduct fun x ↦ U
⊢ HasWidePullback ((incl C).obj T) (fun x ↦ U) fun x ↦ (isTerminalIncl T hT).from U

Tactic:
exact hasWidePullback_of_isTerminal _ (isTerminalIncl _ hT)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Pi

Goal state before:
pp: I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
i : I
⊢ (F.map f ≫ fun i ↦ (c i).ι.app j') i = ((fun i ↦ (c i).ι.app j) ≫ ((Functor.const J).obj fun i ↦ (c i).pt).map f) i

Tactic:
exact (c i).ι.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁵ : Category.{v_1, u_5} K
inst✝⁴ : Category.{v_2, u_6} K'
inst✝³ : Category.{v_3, u_1} J
inst✝² : Category.{v_4, u_2} J'
inst✝¹ : Category.{v_5, u_3} C
inst✝ : Category.{v_6, u_4} D
⊢ (preservesLimitsOfShape K).IsClosedUnderIsomorphisms

Tactic:
preservesLimitsOfShape_eq_iSup

Goal state after:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁵ : Category.{v_1, u_5} K
inst✝⁴ : Category.{v_2, u_6} K'
inst✝³ : Category.{v_3, u_1} J
inst✝² : Category.{v_4, u_2} J'
inst✝¹ : Category.{v_5, u_3} C
inst✝ : Category.{v_6, u_4} D
⊢ (⨅ F, preservesLimit F).IsClosedUnderIsomorphisms
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
j : J
⊢ { pt := Y, ι := hf.incl }.ι.app j ≫ g₁ = { pt := Y, ι := hf.incl }.ι.app j ≫ g₂

pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
⊢ ∃ a, (fun g ↦ f ≫ g) a = g

Tactic:
· dsimp at h ⊢
      induction j using SuccOrder.limitRecOn with
      | isMin j hj =>
        obtain rfl := hj.eq_bot
        simpa [← cancel_epi hf.isoBot.inv]
      | succ j hj hj' => exact (hf.map_mem j hj _ hZ).1 (by simpa)
      | isSuccLimit j hj hj' =>
        exact (hf.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
          (fun ⟨k, hk⟩ ↦ by simpa using! hj' _ hk)

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
⊢ ∃ a, (fun g ↦ f ≫ g) a = g
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case refine_2
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
this✝ : CatCommSq E.functor L₁ L₂ E'.functor
X Y : Discrete J ⥤ C
f : X ⟶ Y
hf : W.functorCategory (Discrete J) f
this : ∀ (j : Discrete J), IsIso ((L₂.map f).app j)
⊢ IsIso (L₂.map f)

Tactic:
apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
⊢ ∀ {X_1 Y : X} (f : X_1 ⟶ Y),
    ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.map f ≫
        (Iso.refl
            (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj Y)).hom =
      (Iso.refl
            (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj X_1)).hom ≫
        ((𝟭 (CatCommSqOver F G X)).obj x✝).fst.map f

Tactic:
intros; simp

Goal state after: