mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ { pt := s.pt, π := Discrete.natTrans fun x ↦ s.π.app { as := x.as.succ } }.π.app { as := i } =
    s.π.app { as := i.succ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i ↦ F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i ↦ f i.succ)
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ᶜ fun i ↦ f i.succ))
j : Fin (n + 1)
i : Fin n
a✝ :
  (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
            (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π.app
      { as := i.castSucc } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
              F.map
                (Fin.cases (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)))
                  (fun i ↦
                    BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)) ≫
                      (limit.cone (Discrete.functor fun i ↦ f i.succ)).π.app { as := i })
                  j)).π.app
        { as := i.castSucc }
⊢ F.map (prod.snd ≫ Pi.π (fun i ↦ f i.succ) i) =
    F.map
      (BinaryFan.snd (limit.cone (pair (f 0) (limit (Discrete.functor fun i ↦ f i.succ)))) ≫
        limit.π (Discrete.functor fun i ↦ f i.succ) { as := i })

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }.ι.app { as := i } =
    s.ι.app { as := i.succ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P.retractClosure X ↔ ∃ Y, ∃ (_ : P Y), Nonempty (Retract X Y)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
J : Type u_2
inst✝¹ : Preorder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : ∀ (j : J), W (F.map (homOfLE ⋯))
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ F.map (homOfLE ⋯) = F.map (homOfLE ⋯ ≫ x✝)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
let c₁ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₁)) h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i ↦ F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i ↦ f i.succ)
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i ↦ f i.succ))
j : Fin (n + 1)
i : Fin n
a✝ :
  (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι.app
        { as := i.castSucc } ≫
      (Iso.refl
          (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
            F.map
              (Fin.cases
                (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                (fun i ↦
                  (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).ι.app { as := i } ≫
                    BinaryCofan.inr
                      (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                j)).ι.app
      { as := i.castSucc }
⊢ F.map (Sigma.ι (fun i ↦ f i.succ) i ≫ coprod.inr) =
    F.map
      (colimit.ι (Discrete.functor fun i ↦ f i.succ) { as := i } ≫
        BinaryCofan.inr (colimit.cocone (pair (f 0) (colimit (Discrete.functor fun i ↦ f i.succ)))))

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z X Y : C
f : X ⟶ Y
inst✝¹ : HasPushout f f
inst✝ : Epi f
⊢ IsIso (codiagonal f)

Tactic:
rw [(IsIso.inv_eq_of_hom_inv_id (inl_codiagonal f)).symm]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z X Y : C
f : X ⟶ Y
inst✝¹ : HasPushout f f
inst✝ : Epi f
⊢ IsIso (inv (inl f f))
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape Jᵒᵖ ≤ P ↔ (P.colimitsOfShape Jᵒᵖ).op ≤ P.op

Tactic:
op_monotone_iff

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.colimitsOfShape Jᵒᵖ ≤ P ↔ P.colimitsOfShape Jᵒᵖ ≤ P
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.limitsOfShape Jᵒᵖ ≤ P ↔ (P.limitsOfShape Jᵒᵖ).op ≤ P.op

Tactic:
op_monotone_iff

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.limitsOfShape Jᵒᵖ ≤ P ↔ P.limitsOfShape Jᵒᵖ ≤ P
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
    ∀ (x x_1 : C) (x_2 : x ⟶ X) (x_3 : x_1 ⟶ Y) (x_4 : x ⟶ x_1), IsPullback x_4 x_2 x_3 f → P x_4 ∧ Q x_4

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ∀ (j : Discrete WalkingPair),
    ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
          tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) ≫
        (ℬ X Y).cone.π.app j =
      tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y) ≫ (ℬ X Y).cone.π.app j

Tactic:
by rintro ⟨_ | _⟩ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝

Tactic:
ext; change lift (fst M M) (snd M M) ≫ μ = μ; rw [lift_fst_snd, Category.id_comp]

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case ha
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ (((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
            (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝))).comp
        includeLeft)
      x✝ =
    (((Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
            (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom)).comp
        includeLeft)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case hb
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
x✝ : ↑Y✝
⊢ ((AlgHom.restrictScalars R
            ((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
              (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝)))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom))).comp
        includeRight)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case ha
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
x✝ : ↑X✝
⊢ (((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
            (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝))).comp
        includeLeft)
      x✝ =
    (((Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
            (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom)).comp
        includeLeft)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case hb
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
x✝ : ↑Z✝
⊢ ((AlgHom.restrictScalars R
            ((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
              (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝)))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom))).comp
        includeRight)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case ha.ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑S
⊢ (((((↑(assoc R R R ↑T ↑U ↑S)).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
                ↑(assoc R R R ↑S ↑T ↑U)).comp
            includeLeft).comp
        includeLeft)
      x✝ =
    (((((Algebra.TensorProduct.map (AlgHom.id R ↑T) (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
                    ↑(assoc R R R ↑T ↑S ↑U)).comp
                (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom)
                  (AlgHom.id R ↑U))).comp
            includeLeft).comp
        includeLeft)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case ha.hb
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑T
⊢ ((AlgHom.restrictScalars R
            ((((↑(assoc R R R ↑T ↑U ↑S)).comp
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
                  ↑(assoc R R R ↑S ↑T ↑U)).comp
              includeLeft)).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((((Algebra.TensorProduct.map (AlgHom.id R ↑T)
                          (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
                      ↑(assoc R R R ↑T ↑S ↑U)).comp
                  (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom)
                    (AlgHom.id R ↑U))).comp
              includeLeft)).comp
        includeRight)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case hb
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑U
⊢ ((AlgHom.restrictScalars R
            (((↑(assoc R R R ↑T ↑U ↑S)).comp
                  (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
              ↑(assoc R R R ↑S ↑T ↑U))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (((Algebra.TensorProduct.map (AlgHom.id R ↑T)
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
                  ↑(assoc R R R ↑T ↑S ↑U)).comp
              (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom)
                (AlgHom.id R ↑U)))).comp
        includeRight)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑S
⊢ ((((↑(assoc R R R ↑U ↑S ↑T).symm).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
            ↑(assoc R R R ↑S ↑T ↑U).symm).comp
        includeLeft)
      x✝ =
    ((((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom) (AlgHom.id R ↑T)).comp
                ↑(assoc R R R ↑S ↑U ↑T).symm).comp
            (Algebra.TensorProduct.map (AlgHom.id R ↑S)
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom))).comp
        includeLeft)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case hb.ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑T
⊢ (((AlgHom.restrictScalars R
                (((↑(assoc R R R ↑U ↑S ↑T).symm).comp
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
                  ↑(assoc R R R ↑S ↑T ↑U).symm)).comp
            includeRight).comp
        includeLeft)
      x✝ =
    (((AlgHom.restrictScalars R
                (((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
                          (AlgHom.id R ↑T)).comp
                      ↑(assoc R R R ↑S ↑U ↑T).symm).comp
                  (Algebra.TensorProduct.map (AlgHom.id R ↑S)
                    (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom)))).comp
            includeRight).comp
        includeLeft)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case hb.hb
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑U
⊢ ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars R
                  (((↑(assoc R R R ↑U ↑S ↑T).symm).comp
                        (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
                    ↑(assoc R R R ↑S ↑T ↑U).symm)).comp
              includeRight)).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars R
                  (((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
                            (AlgHom.id R ↑T)).comp
                        ↑(assoc R R R ↑S ↑U ↑T).symm).comp
                    (Algebra.TensorProduct.map (AlgHom.id R ↑S)
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom)))).comp
              includeRight)).comp
        includeRight)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: case hba
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ((AlgebraTensorModule.curry
          (toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
              toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A))).ofConv)
        a)
      b =
    ((AlgebraTensorModule.curry (ofConv 1)) a) b

Tactic:
simp [((ℛ R a).tmul (ℛ R b)).convMul_apply, ← Bialgebra.counit_mul,
      ← sum_antipode_mul_eq_algebraMap_counit ((ℛ R b).mul (ℛ R a)),
      ← Finset.map_swap_product (ℛ R b).index (ℛ R a).index]

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ 1 = 1 ⊗ₜ[R] 1

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ f⁻¹ * f =
    toConv
      ((lmul' R).comp
        ((Algebra.TensorProduct.map (f.ofConv.comp (antipodeAlgHom R A)) (f.ofConv.comp (AlgHom.id R A))).comp
          (comulAlgHom R A)))

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X Y : C
inst✝ : Closed A
g : Y ⟶ (ihom A).obj X
⊢ uncurry g = A ◁ g ≫ (ihom.ev A).app X

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ Preadditive.preadditiveHasZeroMorphisms = Limits.hasZeroMorphismsOpposite

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((fun x x_1 ↦
          ((fun x x_2 ↦
                  (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                    ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                (F.obj x) x_1).trans
            (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
        Y Z)
      ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      ((fun x x_1 ↦
              ((fun x x_2 ↦
                      (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                        ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                    (F.obj x) x_1).trans
                (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
            Y Z).symm
        f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))).symm f))

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : Closed X
⊢ curry (ρ_ X).hom = id X

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
m : ↑M
n : ↑X'✝
⊢ (Hom.hom ((M.monoidalClosedHomEquiv X'✝ Y✝).symm (f✝ ≫ g✝))) (m ⊗ₜ[R] n) =
    (Hom.hom ((MonoidalCategory.tensorLeft M).map f✝ ≫ (M.monoidalClosedHomEquiv X✝ Y✝).symm g✝)) (m ⊗ₜ[R] n)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
n : ℕ
x✝ : Encodable (WType' β n)
a✝ : α
f✝ : β a✝ → WType β
property✝ : (mk a✝ f✝).depth ≤ n + 1
⊢ finv n (f n ⟨mk a✝ f✝, property✝⟩) = ⟨mk a✝ f✝, property✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (↥(closure s)) (operate s) (WType.mk (Sum.inl 1) fun t ↦ Bool.rec x y t) =
    WType.elim (↥(closure s)) (operate s) x * WType.elim (↥(closure s)) (operate s) y

Tactic:
rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x y : WType (Operands s)
⊢ WType.elim (↥(closure s)) (operate s) (WType.mk (Sum.inl 0) fun t ↦ Bool.rec x y t) =
    WType.elim (↥(closure s)) (operate s) x + WType.elim (↥(closure s)) (operate s) y

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
⊢ Submodule.map (Submodule.map f p).mkQ f.range = Submodule.map (Submodule.map f p).mkQ (comap id f.range)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : lift.{v, u} (max ℵ₀ #K) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
rw [lift_max, lift_aleph0, max_le_iff] at key

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)