mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst✝³] (Ioo (z x) (y x))

Tactic:
;

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst✝³] (Ioo (z x) (y x))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : MonCat
z x y : ↑A
⊢ (hom (MonoidalCategoryStruct.whiskerRight (↾fun p ↦ p.1 * p.2) ↑A ≫ ↾fun p ↦ p.1 * p.2)).toFun ((x, y), z) =
    (hom
          ((MonoidalCategoryStruct.associator ↑A ↑A ↑A).hom ≫
            MonoidalCategoryStruct.whiskerLeft (↑A) (↾fun p ↦ p.1 * p.2) ≫ ↾fun p ↦ p.1 * p.2)).toFun
      ((x, y), z)

Tactic:
;

Goal state after:
A : MonCat
z x y : ↑A
⊢ (hom (MonoidalCategoryStruct.whiskerRight (↾fun p ↦ p.1 * p.2) ↑A ≫ ↾fun p ↦ p.1 * p.2)).toFun ((x, y), z) =
    (hom
          ((MonoidalCategoryStruct.associator ↑A ↑A ↑A).hom ≫
            MonoidalCategoryStruct.whiskerLeft (↑A) (↾fun p ↦ p.1 * p.2) ≫ ↾fun p ↦ p.1 * p.2)).toFun
      ((x, y), z)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : Type u
inst✝¹ : MonObj A
inst✝ : IsCommMonObj A
x y : A
⊢ x * y = y * x

Tactic:
by
      convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x)

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1.h
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ n = addOrderOf ↑(↑m / ↑n * p) * ?refine_1.w

pp: case refine_1.w
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ ℕ

Tactic:
;

Goal state after:
case refine_1.h
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ n = addOrderOf ↑(↑m / ↑n * p) * ?refine_1.w

case refine_1.w
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ ℕ
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_

Goal state before:
pp: A : Type u
inst✝¹ : GrpObj A
inst✝ : IsCommMonObj A
x y : A
⊢ x * y = y * x

Tactic:
by
      convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x)

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
inst✝¹¹ : BraidedCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
inst✝⁸ : BraidedCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
inst✝⁵ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁴ : F.LaxBraided
inst✝³ : F'.LaxBraided
inst✝² : G.LaxBraided
M : C
inst✝¹ : MonObj M
inst✝ : IsCommMonObj M
⊢ (β_ (F.obj M) (F.obj M)).hom ≫ LaxMonoidal.μ F M M ≫ F.map μ = LaxMonoidal.μ F M M ≫ F.map μ

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
inst✝¹¹ : BraidedCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
inst✝⁸ : BraidedCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
inst✝⁵ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁴ : F.LaxBraided
inst✝³ : F'.LaxBraided
inst✝² : G.LaxBraided
M : C
inst✝¹ : MonObj M
inst✝ : IsCommMonObj M
⊢ (β_ (F.obj M) (F.obj M)).hom ≫ LaxMonoidal.μ F M M ≫ F.map μ = LaxMonoidal.μ F M M ≫ F.map μ
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
f : X✝ ⟶ Y✝
⊢ ((𝟭 (LaxBraidedFunctor (Discrete PUnit.{u + 1}) C)).map f ≫
              (isoOfComponents (fun x ↦ Y✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom).hom.hom.app
      { as := PUnit.unit } =
    ((isoOfComponents (fun x ↦ X✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom ≫
              (laxBraidedToCommMon C ⋙ commMonToLaxBraided C).map f).hom.hom.app
      { as := PUnit.unit }

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
f : X✝ ⟶ Y✝
⊢ ((𝟭 (LaxBraidedFunctor (Discrete PUnit.{u + 1}) C)).map f ≫
              (isoOfComponents (fun x ↦ Y✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom).hom.hom.app
      { as := PUnit.unit } =
    ((isoOfComponents (fun x ↦ X✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom ≫
              (laxBraidedToCommMon C ⋙ commMonToLaxBraided C).map f).hom.hom.app
      { as := PUnit.unit }
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
f : X✝ ⟶ Y✝
⊢ f.hom.hom.app { as := PUnit.unit } ≫ Y✝.map (𝟙 { as := PUnit.unit }) =
    X✝.map (𝟙 { as := PUnit.unit }) ≫ f.hom.hom.app (𝟙_ (Discrete PUnit.{u + 1}))

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
f : X✝ ⟶ Y✝
⊢ f.hom.hom.app { as := PUnit.unit } ≫ Y✝.map (𝟙 { as := PUnit.unit }) =
    X✝.map (𝟙 { as := PUnit.unit }) ≫ f.hom.hom.app (𝟙_ (Discrete PUnit.{u + 1}))
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
⊢ ∀ (X : C ⥤ₗ Type v), PreservesFiniteLimits (inverseAux.obj X)

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
⊢ ∀ (X : C ⥤ₗ Type v), PreservesFiniteLimits (inverseAux.obj X)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
have : IsEmpty { u : AddCircle p // ¬IsOfFinAddOrder u } := by simpa [isEmpty_subtype] using h

Goal state after:
case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
this : IsEmpty { u // ¬IsOfFinAddOrder u }
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
rw [equivIccQuot_comp_mk_eq_toIcoMod]
  funext x
  by_cases h : a ≡ x [PMOD p]
  · simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]
    exact Quot.sound EndpointIdent.mk
  · simp_rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x ∧
    ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x

Tactic:
;

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x ∧
    ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.one ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom = MonObj.one

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.mul ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom =
    ((Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom ⊗ₘ
        (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom) ≫
      MonObj.mul

pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ {X Y : CommGrp C} (f : X ⟶ Y),
    (CommGrp.forget C ⋙ toCommGrp C).map f ≫
        (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj Y).X) ⋯ ⋯).hom =
      (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj X).X) ⋯ ⋯).hom ≫ (𝟭 (CommGrp C)).map f

Tactic:
· exact ((IsZero.iff_id_eq_zero _).2 (Subsingleton.elim _ _)).eq_of_src _ _

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.mul ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom =
    ((Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom ⊗ₘ
        (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom) ≫
      MonObj.mul

case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ {X Y : CommGrp C} (f : X ⟶ Y),
    (CommGrp.forget C ⋙ toCommGrp C).map f ≫
        (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj Y).X) ⋯ ⋯).hom =
      (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj X).X) ⋯ ⋯).hom ≫ (𝟭 (CommGrp C)).map f
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝⁴ x✝³ x✝² : HopfAlgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝⁴ ⊗ x✝³)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝⁴ ◁ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³)).inv ≫
          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ◁ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝⁴ x✝³ x✝² : HopfAlgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝⁴ ⊗ x✝³)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝⁴ ◁ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³)).inv ≫
          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ◁ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²)).hom))
      x✝
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : HopfAlgCat R
x✝² : X₁✝ ⟶ X₂✝
x✝¹ : HopfAlgCat R
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁✝ ⊗ x✝¹)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝² ▷ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).inv ≫
          (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝² ▷ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : HopfAlgCat R
x✝² : X₁✝ ⟶ X₂✝
x✝¹ : HopfAlgCat R
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁✝ ⊗ x✝¹)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝² ▷ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).inv ≫
          (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝² ▷ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom))
      x✝
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : HopfAlgCat R
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁✝ ⊗ X₂✝)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝² ⊗ₘ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝)).inv ≫
          ((forget₂ (HopfAlgCat R) (BialgCat R)).map x✝² ⊗ₘ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹) ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₂✝)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : HopfAlgCat R
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁✝ ⊗ X₂✝)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝² ⊗ₘ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝)).inv ≫
          ((forget₂ (HopfAlgCat R) (BialgCat R)).map x✝² ⊗ₘ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹) ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₂✝)).hom))
      x✝
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : HopfAlgCat R
x✝ : x✝¹.carrier
⊢ (((TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝¹.carrier).compr₂ₛₗ
          ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (λ_ x✝¹).hom).toBialgHom'))
        1)
      x✝ =
    (((TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝¹.carrier).compr₂ₛₗ
          ((fun x ↦ ↑x)
            (((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)) ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl (𝟙_ (BialgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹))) ≪≫
                  λ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom.toBialgHom'))
        1)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝¹ : HopfAlgCat R
x✝ : x✝¹.carrier
⊢ (((TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝¹.carrier).compr₂ₛₗ
          ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (λ_ x✝¹).hom).toBialgHom'))
        1)
      x✝ =
    (((TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝¹.carrier).compr₂ₛₗ
          ((fun x ↦ ↑x)
            (((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)) ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl (𝟙_ (BialgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹))) ≪≫
                  λ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom.toBialgHom'))
        1)
      x✝
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : HopfAlgCat R
x✝ : x✝¹.carrier
⊢ (((TensorProduct.mk R x✝¹.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
          ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (ρ_ x✝¹).hom).toBialgHom'))
        x✝)
      1 =
    (((TensorProduct.mk R x✝¹.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
          ((fun x ↦ ↑x)
            (((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)))).symm ≪≫
                    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹) ⊗ᵢ (Iso.refl (𝟙_ (BialgCat R))).symm)) ≪≫
                  ρ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom.toBialgHom'))
        x✝)
      1

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝¹ : HopfAlgCat R
x✝ : x✝¹.carrier
⊢ (((TensorProduct.mk R x✝¹.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
          ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (ρ_ x✝¹).hom).toBialgHom'))
        x✝)
      1 =
    (((TensorProduct.mk R x✝¹.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
          ((fun x ↦ ↑x)
            (((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)))).symm ≪≫
                    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹) ⊗ᵢ (Iso.refl (𝟙_ (BialgCat R))).symm)) ≪≫
                  ρ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom.toBialgHom'))
        x✝)
      1
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝¹ : (free R).obj X ⟶ M
x✝ : X
⊢ (ConcreteCategory.hom
        ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x)) x✝¹)))
      (freeMk x✝) =
    (ConcreteCategory.hom x✝¹) (freeMk x✝)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝¹ : (free R).obj X ⟶ M
x✝ : X
⊢ (ConcreteCategory.hom
        ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x)) x✝¹)))
      (freeMk x✝) =
    (ConcreteCategory.hom x✝¹) (freeMk x✝)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝¹ : X ⟶ ↑M
x✝ : X
⊢ (ConcreteCategory.hom
          ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x))
            ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) x✝¹))).toFun
      x✝ =
    (ConcreteCategory.hom x✝¹).toFun x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝¹ : X ⟶ ↑M
x✝ : X
⊢ (ConcreteCategory.hom
          ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x))
            ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) x✝¹))).toFun
      x✝ =
    (ConcreteCategory.hom x✝¹).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g : Y ⟶ (forget (ModuleCat R)).obj M
x✝ : X
⊢ (ConcreteCategory.hom (freeHomEquiv.symm (f ≫ g))) (freeMk x✝) =
    (ConcreteCategory.hom ((free R).map f ≫ freeHomEquiv.symm g)) (freeMk x✝)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g : Y ⟶ (forget (ModuleCat R)).obj M
x✝ : X
⊢ (ConcreteCategory.hom (freeHomEquiv.symm (f ≫ g))) (freeMk x✝) =
    (ConcreteCategory.hom ((free R).map f ≫ freeHomEquiv.symm g)) (freeMk x✝)
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 1
i : ℕ
hi : i + 2 ≤ 1
⊢ False

Tactic:
;

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 1
i : ℕ
hi : i + 2 ≤ 1
⊢ False
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).sc' ?mp.left.hS 0 1 2
      exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

pp: case mp.left.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).IsComplex

Tactic:
;

Goal state after:
case mp.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).sc' ?mp.left.hS 0 1 2
      exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

case mp.left.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).IsComplex
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact → (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
intro h
    constructor
    · rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero 0
      exact h.exact 0 (by lia)
    · exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero (i + 1)))
        (fun i hi => h.exact (i + 1))

Goal state after: