awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (fst G G) (snd G G)) μ) μ
have H : 𝟙 (tensorObj.{v, u} (𝒞 := inst) G G) ≫ μ = μ
Tactic: rw [lift_fst_snd, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
H : 𝟙 (tensorObj.{v, u} (𝒞 := inst) G G) ≫ μ = μ
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (fst G G) (snd G G)) μ) μ
have H₁ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G) μ μ
Tactic: rw [lift_fst_snd, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G_1 H_1 X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G_1
inst_4 : GrpObj H_1
G H : Grp.{v, u} C
α : Functor.obj yonedaGrp G ⟶ Functor.obj yonedaGrp H
⊢ Functor.map yonedaGrp
      (Grp.homMk'
        (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
          (Functor.whiskerRight α
            (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
              MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier))))) =
    α
have w : ∀ (X : Cᵒᵖ),
  GrpCat.Hom.hom
      (NatTrans.app
        (Functor.map yonedaGrp
          (Grp.homMk'
            (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
              (Functor.whiskerRight α
                (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                  GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                  MonCat.carrier))))))
        X) =
    GrpCat.Hom.hom (α.app X)
Tactic: ext X : 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
X_1 Y_1 : Grp.{v, u} C
f : X_1 ⟶ Y_1
⊢ Grp.homMk'
      (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
        (Functor.whiskerRight (Functor.map yonedaGrp f)
          (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
            MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier)))) =
    f
have h : Mon.Hom.hom
    (InducedCategory.Hom.hom
      (Grp.homMk'
        (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
          (Functor.whiskerRight (Functor.map yonedaGrp f)
            (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
              MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier)))))) =
  f.hom.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
X_1 Y_1 : Grp.{v, u} C
f : X_1 ⟶ Y_1
⊢ Mon.Hom.hom
      (InducedCategory.Hom.hom
        (Grp.homMk'
          (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
            (Functor.whiskerRight (Functor.map yonedaGrp f)
              (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
                MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier)))))) =
    f.hom.hom
have h : Functor.FullyFaithful.preimage yonedaMonFullyFaithful
    (Functor.whiskerRight (Functor.map yonedaGrp f)
      (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier) MonCat
        (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier))) =
  f.hom
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
⊢ Eq (α := ObjectProperty (Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat)) (Functor.essImage (C := Grp.{v, u} C) yonedaGrp)
    fun (F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat) ↦
    (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable
have h : ∀ (F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat),
  Functor.essImage (C := Grp.{v, u} C) yonedaGrp F ↔
    (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable
Tactic: ext F
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat
⊢ Functor.essImage (C := Grp.{v, u} C) yonedaGrp F ↔
    (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable
have h : Functor.essImage (C := Grp.{v, u} C) yonedaGrp F →
  (F ⋙
      forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
        GrpCat.carrier)).IsRepresentable
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat
h :
  Functor.essImage (C := Grp.{v, u} C) yonedaGrp F →
    (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable
⊢ Functor.essImage (C := Grp.{v, u} C) yonedaGrp F ↔
    (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable
have h₁ : (F ⋙
      forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
        GrpCat.carrier)).IsRepresentable →
  Functor.essImage (C := Grp.{v, u} C) yonedaGrp F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : CartesianMonoidalCategory.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_4 : F.Monoidal
X G : C
f : X ⟶ G
inst_5 : GrpObj G
⊢ F.map f⁻¹ = (F.map f)⁻¹
have rw : F.map f⁻¹ * F.map f = 1
Tactic: rw [eq_inv_iff_mul_eq_one, ← Functor.map_mul, inv_mul_cancel, Functor.map_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : CartesianMonoidalCategory.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_4 : F.Monoidal
X G : C
f : X ⟶ G
inst_5 : GrpObj G
rw : F.map f⁻¹ * F.map f = 1
⊢ F.map f⁻¹ = (F.map f)⁻¹
have rw₁ : F.map (f⁻¹ * f) = 1
Tactic: rw [eq_inv_iff_mul_eq_one, ← Functor.map_mul, inv_mul_cancel, Functor.map_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : CartesianMonoidalCategory.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_4 : F.Monoidal
X G : C
f : X ⟶ G
inst_5 : GrpObj G
rw : F.map f⁻¹ * F.map f = 1
rw₁ : F.map (f⁻¹ * f) = 1
⊢ F.map f⁻¹ = (F.map f)⁻¹
have rw₂ : Eq (α := F.obj X ⟶ F.obj G) (F.map 1) 1
Tactic: rw [eq_inv_iff_mul_eq_one, ← Functor.map_mul, inv_mul_cancel, Functor.map_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : CartesianMonoidalCategory.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_4 : F.Monoidal
X G : C
f : X ⟶ G
inst_5 : GrpObj G
rw : F.map f⁻¹ * F.map f = 1
rw₁ : F.map (f⁻¹ * f) = 1
rw₂ : Eq (α := F.obj X ⟶ F.obj G) (F.map 1) 1
⊢ F.map f⁻¹ = (F.map f)⁻¹
have rw₃ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj G) 1 1
Tactic: rw [eq_inv_iff_mul_eq_one, ← Functor.map_mul, inv_mul_cancel, Functor.map_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
n : ℕ
⊢ (f ^ n).hom = f.hom ^ n
have zero : (HPow.hPow (β := ℕ) f 0).hom = HPow.hPow (β := ℕ) f.hom 0
Tactic: induction n with
  | zero => simp
  | succ n hn => simp [pow_succ, hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
n : ℕ
zero : (HPow.hPow (β := ℕ) f 0).hom = HPow.hPow (β := ℕ) f.hom 0
⊢ (f ^ n).hom = f.hom ^ n
have succ : ∀ (n : ℕ) (hn : (f ^ n).hom = f.hom ^ n), (f ^ (n + 1)).hom = f.hom ^ (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n hn => simp [pow_succ, hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
n : ℤ
⊢ (f ^ n).hom.hom = f.hom.hom ^ n
have ofNat : ∀ (a : ℕ), (f ^ Int.ofNat a).hom.hom = f.hom.hom ^ Int.ofNat a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
n : ℤ
ofNat : ∀ (a : ℕ), (f ^ Int.ofNat a).hom.hom = f.hom.hom ^ Int.ofNat a
⊢ (f ^ n).hom.hom = f.hom.hom ^ n
have negSucc : ∀ (a : ℕ), (f ^ Int.negSucc a).hom.hom = f.hom.hom ^ Int.negSucc a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
⊢ IsCommMonObj.{v, u} G ↔
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
have rw : (∀ (X : C), IsMulCommutative.{v} (X ⟶ G)) ↔
  GrpObj.commutator G =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
Tactic: rw [isCommMonObj_iff_isMulCommutative]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
⊢ (∀ (X : C), IsMulCommutative.{v} (X ⟶ G)) ↔
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
have refine_1 : ∀ (h : ∀ (X : C), IsMulCommutative.{v} (X ⟶ G)),
  GrpObj.commutator G =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
Tactic: refine ⟨fun h ↦ ?_, fun heq X ↦ ⟨⟨fun f g ↦ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
refine_1 :
  ∀ (h : ∀ (X : C), IsMulCommutative.{v} (X ⟶ G)),
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
⊢ (∀ (X : C), IsMulCommutative.{v} (X ⟶ G)) ↔
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
have refine_2 : ∀
  (heq :
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η)
  (X : C) (f g : X ⟶ G), f * g = g * f
Tactic: refine ⟨fun h ↦ ?_, fun heq X ↦ ⟨⟨fun f g ↦ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
Z Z' : C
g : Z' ⟶ Z
m : Z ⟶ M
x : Z ⟶ X
⊢ g ≫ (m • x) = g ≫ m • g ≫ x
have rw : g ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) =
  g ≫ m • g ≫ x
Tactic: rw [Hom.smul_def, Hom.smul_def, comp_lift_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
Z Z' : C
g : Z' ⟶ Z
m : Z ⟶ M
x : Z ⟶ X
rw :
  g ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) =
    g ≫ m • g ≫ x
⊢ g ≫ (m • x) = g ≫ m • g ≫ x
have rw₁ : Eq (α := Z' ⟶ X)
  (g ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _))
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift (g ≫ m) (g ≫ x)) (@smul _ _ _ _ _ _ _ inst_2 _ _))
Tactic: rw [Hom.smul_def, Hom.smul_def, comp_lift_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
Z Z' : C
g : Z' ⟶ Z
m : Z ⟶ M
x : Z ⟶ X
rw :
  g ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) =
    g ≫ m • g ≫ x
rw₁ :
  Eq (α := Z' ⟶ X)
    (g ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift (g ≫ m) (g ≫ x))
      (@smul _ _ _ _ _ _ _ inst_2 _ _))
⊢ g ≫ (m • x) = g ≫ m • g ≫ x
have rw₂ : Eq (α := Z' ⟶ X)
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift (g ≫ m) (g ≫ x)) (@smul _ _ _ _ _ _ _ inst_2 _ _))
  (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift (g ≫ m) (g ≫ x)) (@smul _ _ _ _ _ _ _ inst_2 _ _))
Tactic: rw [Hom.smul_def, Hom.smul_def, comp_lift_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
Z : C
x : Z ⟶ X
m : Z ⟶ M
⊢ Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
have h_fst : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (fst X X) =
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift (m • x) x) (fst X X)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
Z : C
x : Z ⟶ X
m : Z ⟶ M
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (fst X X) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift (m • x) x) (fst X X)
⊢ Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
have h_snd : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (snd X X) =
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift (m • x) x) (snd X X)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
⊢ IsIso.{v, u} (X := tensorObj.{v, u} (𝒞 := inst) M X) (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
have H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
  Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
Tactic: have H (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) :
      lift m x ≫ leftSMul M X = lift (m • x) x := by
    ext <;> simp [Hom.smul_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
Z : C
f g : Z ⟶ X
m : Z ⟶ M
x : Z ⟶ X
⊢ Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
have simp : CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) = f ∧ x = g ↔
  x = g ∧ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) = f
Tactic: simp [← lift_leftSMul_eq_lift_iff, CartesianMonoidalCategory.hom_ext_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
⊢ IsIso.{v, u} (X := tensorObj.{v, u} (𝒞 := inst) M X) (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
have h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
  Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
Tactic: have h (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X) :
      lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f := by
    simp [← lift_leftSMul_eq_lift_iff, CartesianMonoidalCategory.hom_ext_iff]
    grind
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
⊢ IsIso.{v, u} (X := tensorObj.{v, u} (𝒞 := inst) M X) (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
have rw : (∀ (T : C),
    Function.Bijective (β := T ⟶ tensorObj.{v, u} (𝒞 := inst) X X) fun (x : T ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦
      x ≫ leftSMul M X) ↔
  ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
Tactic: rw [isIso_iff_yoneda_map_bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
⊢ (∀ (T : C),
      Function.Bijective (β := T ⟶ tensorObj.{v, u} (𝒞 := inst) X X) fun (x : T ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦
        x ≫ leftSMul M X) ↔
    ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
have a : ∀ (Z : C),
  (Function.Bijective (β := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) fun (x : Z ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦
      x ≫ leftSMul M X) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
Tactic: congr! with Z
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
Z : C
⊢ (Function.Bijective (β := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) fun (x : Z ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦
      x ≫ leftSMul M X) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
have a : (∀ (b : Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X),
    ∃! a : (Z ⟶ M) × (Z ⟶ X),
      ((fun (x : Z ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦ x ≫ leftSMul M X) ∘
            (⇑liftEquiv : (a : (Z ⟶ M) × (Z ⟶ X)) → Z ⟶ M ⊗ X))
          a =
        b) ↔
  ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
Tactic: rw [← Function.Bijective.of_comp_iff _ liftEquiv.bijective, Function.bijective_iff_existsUnique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
Z : C
⊢ (∀ (b : Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X),
      ∃! a : (Z ⟶ M) × (Z ⟶ X),
        ((fun (x : Z ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦ x ≫ leftSMul M X) ∘
              (⇑liftEquiv : (a : (Z ⟶ M) × (Z ⟶ X)) → Z ⟶ M ⊗ X))
            a =
          b) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
have a : (∀ (a b : Z ⟶ X), ∃! a_1 : (Z ⟶ M) × (Z ⟶ X), a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔ ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
Tactic: simp only [liftEquiv.surjective.forall, liftEquiv_apply, Prod.forall, Function.comp_apply, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
Z : C
⊢ (∀ (a b : Z ⟶ X), ∃! a_1 : (Z ⟶ M) × (Z ⟶ X), a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
have a : (∀ (b a : Z ⟶ X), ∃! a_1 : (Z ⟶ M) × (Z ⟶ X), a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔ ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
Tactic: rw [forall_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mod (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
Z : C
⊢ (∀ (b a : Z ⟶ X), ∃! a_1 : (Z ⟶ M) × (Z ⟶ X), a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
have a : ∀ (f g : Z ⟶ X), (∃! a : (Z ⟶ M) × (Z ⟶ X), a.2 = f ∧ a.1 • a.2 = g) ↔ ∃! m : Z ⟶ M, m • f = g
Tactic: congr! 2 with f g