mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1))

Tactic:
← neg_le_neg_iff,

Goal state after:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ -∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1)) ≤ -∫ (x : ℝ) in x₀..x₀ + ↑a, f x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ i ∈ Finset.Ico a b, f ↑(i + 1)

Tactic:
← neg_le_neg_iff,

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ -∑ i ∈ Finset.Ico a b, f ↑(i + 1) ≤ -∫ (x : ℝ) in ↑a..↑b, f x
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_1
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
b : B
X : CostructuredArrow L (R.obj b)
⊢ ∃ c, Nonempty ((fst L R).obj c ⟶ a)

Tactic:
exact ⟨⟨IsCofiltered.min a X.left, b, L.map (IsCofiltered.minToRight a X.left) ≫ X.hom⟩,
      ⟨IsCofiltered.minToLeft a X.left⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
⊢ (ConcreteCategory.hom (limit.π (F.op ⋙ G) i)) ((colimitYonedaHomEquiv F G) η) =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))

Tactic:
simp only [colimitYonedaHomEquiv, Iso.toEquiv, uliftFunctor_obj,
    Iso.trans_def, Iso.trans_assoc, Iso.trans_hom, Iso.trans_inv,
    Category.assoc, Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.coe_fn_mk, comp_apply,
    Equiv.ulift_apply]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
⊢ (ConcreteCategory.hom (limit.π (F.op ⋙ G) i))
      ((ConcreteCategory.hom (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).symm.hom)
          ((ConcreteCategory.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom)
            ((ConcreteCategory.hom (colimitYonedaHomIsoLimitOp F G).hom) η))).down =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : I ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).inv ≫ coyoneda.map (colimit.ι F i).op = limit.π (F.op ⋙ coyoneda) (op i)

Tactic:
by
  rw [← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape WalkingParallelPair C
⊢ HasColimitsOfShape WalkingParallelPair (Ind C)

Tactic:
refine ⟨fun F => ?_⟩
  obtain ⟨P⟩ := nonempty_indParallelPairPresentation (F.obj WalkingParallelPair.zero).2
    (F.obj WalkingParallelPair.one).2 (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.left)
    (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.right)
  exact hasColimit_of_iso (diagramIsoParallelPair _ ≪≫ P.parallelPairIsoParallelPairCompIndYoneda)

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

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
hy₂ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')

Tactic:
← hy,

Goal state after:
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
hy₂ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ I.iso.inv ≫ (injectiveResolutions C).map f ≫ J.iso.hom =
    ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ ≫ J.iso.inv) ≫ J.iso.hom

Tactic:
iso_hom_naturality f I J φ comm,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ I.iso.inv ≫ I.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ =
    ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ ≫ J.iso.inv) ≫ J.iso.hom
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f ≫ J.iso.hom) ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)

Tactic:
iso_hom_naturality f I J φ comm,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map
        (I.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
β : (injectiveResolution X).cocomplex ⟶ P.cocomplex
hβ : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β = P.iso.hom
⊢ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((G.mapHomologicalComplex (ComplexShape.up ℕ)).map β) =
    (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map β) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)

Tactic:
simp only [← Functor.map_comp, NatTrans.mapHomologicalComplex_naturality]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
β : (injectiveResolution X).cocomplex ⟶ P.cocomplex
hβ : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β = P.iso.hom
⊢ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
      ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as ≫
        (G.mapHomologicalComplex (ComplexShape.up ℕ)).map β) =
    (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
      ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app (injectiveResolution X).cocomplex ≫
        (G.mapHomologicalComplex (ComplexShape.up ℕ)).map β)
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ ∀ {X Y Z : C} (i : X ⟶ Y), isomorphisms C i → ∀ (f : Y ⟶ Z), ofObjectProperty P Q f → ofObjectProperty P Q (i ≫ f)

Tactic:
by
    intro X Y Z i hi f ⟨hY, hZ⟩
    rw [isomorphisms.iff] at hi
    exact ⟨(P.prop_iff_of_isIso i).mpr hY, hZ⟩

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
g : G
x : s.pt.V
⊢ (ConcreteCategory.hom (s.pt.ρ g ≫ ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x)).toFun x =
    (ConcreteCategory.hom
          ((↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x) ≫
            { pt := ofMulAction G ((i : ι) → F i),
                    π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt.ρ
              g)).toFun
      x

Tactic:
funext j

Goal state after:
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
g : G
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom (s.pt.ρ g ≫ ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x)).toFun x j =
    (ConcreteCategory.hom
          ((↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x) ≫
            { pt := ofMulAction G ((i : ι) → F i),
                    π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt.ρ
              g)).toFun
      x j
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h :
  ∀ (j : Discrete ι),
    f ≫
        { pt := ofMulAction G ((i : ι) → F i),
                π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.π.app
          j =
      s.π.app j
x : s.pt.V
⊢ (ConcreteCategory.hom f.hom).toFun x =
    (ConcreteCategory.hom { hom := ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x, comm := ⋯ }.hom).toFun
      x

Tactic:
funext j

Goal state after:
ι : Type v
G : Type (max v u)
inst✝¹ : Monoid G
F : ι → Type (max v u)
inst✝ : (i : ι) → MulAction G (F i)
s : Cone (Discrete.functor fun i ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    { pt := ofMulAction G ((i : ι) → F i), π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.pt
h :
  ∀ (j : Discrete ι),
    f ≫
        { pt := ofMulAction G ((i : ι) → F i),
                π := Discrete.natTrans fun i ↦ { hom := ↾fun x ↦ x i.as, comm := ⋯ } }.π.app
          j =
      s.π.app j
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom f.hom).toFun x j =
    (ConcreteCategory.hom { hom := ↾fun x i ↦ (ConcreteCategory.hom (s.π.app { as := i }).hom) x, comm := ⋯ }.hom).toFun
      x j
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ ∀ (x y : N), ⟨x * y, 1⟩ = ⟨x, 1⟩ * ⟨y, 1⟩

Tactic:
by intros; ext <;>
    simp only [mul_left, map_one, MulAut.one_apply, mul_right, mul_one]

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

Goal state before:
pp: case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) = g • Fin.partialProd f

Tactic:
funext x

Goal state after:
case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
x : Fin (n + 1 + 1)
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) x = (g • Fin.partialProd f) x
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case f
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
θ : g ⟶ h
a✝ : Hom₂ f g
⊢ Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝ ≫ θ) = Quot.lift (liftHom₂ F) ⋯ (Quot.mk Rel a✝) ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
induction θ using Quot.rec <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
        F.map (𝟙 { as := { as := () } }) ◁ F.mapId { as := { as := () } } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
F.mapComp_id_right,

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.map₂ (ρ_ (𝟙 { as := { as := () } })).hom ≫ (ρ_ (F.map (𝟙 { as := { as := () } }))).inv =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ 𝟙 (𝟙 a ≫ h) ⊗≫ s.unit ⊗≫ leftZigzag adj.unit adj.counit ▷ s.extension ⊗≫ 𝟙 (f ≫ s.extension) = s.unit

Tactic:
rw [adj.left_triangle]; bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ τ = 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift

Tactic:
rw [adj.left_triangle]; bicategory

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝¹ : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst✝ : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ (fst f' g' ≫ γ₁) ≫ f = (snd f' g' ≫ γ₂) ≫ g

Tactic:
rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]

Goal state after:
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:
rw [leftDistrib_hom, coprod.inl_desc]

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

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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
⊢ ∀ {b'_1 : 𝒳} (φ'_1 : a ⟶ b'_1) [p.IsHomLift f φ'_1], ∃! χ, p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = φ'_1

Tactic:
intro c ψ hψ
    use φ'.inv ≫ IsCocartesian.map p f φ ψ
    refine ⟨⟨inferInstance, by simp⟩, ?_⟩
    rintro τ ⟨hτ₁, hτ₂⟩
    rw [Iso.eq_inv_comp]
    apply map_uniq
    exact ((assoc φ _ _) ▸ hτ₂)

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

Goal state before:
pp: J : Type
inst✝ : SmallCategory J
K : J ⥤ FintypeCat
j : J
⊢ Finite ((K ⋙ FintypeCat.incl).obj j)

Tactic:
simp only [comp_obj, FintypeCat.incl_obj]

Goal state after:
J : Type
inst✝ : SmallCategory J
K : J ⥤ FintypeCat
j : J
⊢ Finite (K.obj j).obj
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A X : C
inst✝ : IsConnected A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ Finite (A ⟶ X)

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A X : C
inst✝ : IsConnected A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Finite (A ⟶ X)
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A : C
inst✝ : IsConnected A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ Finite (Aut A)

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
A : C
inst✝ : IsConnected A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Finite (Aut A)
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: 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
⊢ ∃! τ, f ≫ τ.hom = σ.hom ≫ f

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Goal state after:
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
⊢ ∃! τ, f ≫ τ.hom = σ.hom ≫ f
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃ a, autMap f a = σ

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∃ a, autMap f a = σ
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ X ∈ ⋃ X, Set.range (ff X), IsConnected X

Tactic:
rintro X ⟨A, ⟨Y, rfl⟩, hA2⟩

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : ↥I → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
X : C
Y : ↥I
hA2 : X ∈ (fun X ↦ Set.range (ff X)) Y
⊢ IsConnected X