awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → InvolutiveStar (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
⊢ Eq (α := DirectLimit G (T := T) f) (star (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
have ih : Eq (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧)
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
Tactic: rw [star_def, star_def, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → InvolutiveStar (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
ih :
  Eq (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
⊢ Eq (α := DirectLimit G (T := T) f) (star (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
have ih₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star (star x))⟧
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
Tactic: rw [star_def, star_def, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → InvolutiveStar (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
ih :
  Eq (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
ih₁ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star (star x))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
⊢ Eq (α := DirectLimit G (T := T) f) (star (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
have ih₂ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
Tactic: rw [star_def, star_def, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Mul (G i)
inst_6 : Mul C
inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : ∀ (i : ι), MulHomClass.{u_4, u_3, u_5} (H i) (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
x_1 y_1 : DirectLimit G (T := T) f
i : ι
x y : G i
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧) =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧
have simp_rw : DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)⟧ =
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧
Tactic: simp_rw [mul_def, lift_def, map_mul (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Mul (G i)
inst_6 : Mul C
inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : ∀ (i : ι), MulHomClass.{u_4, u_3, u_5} (H i) (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
x_1 y_1 : DirectLimit G (T := T) f
i : ι
x y : G i
simp_rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)⟧ =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧) =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧
have simp_rw₁ : (g i : (a : G i) → C) (x * y) = HMul.hMul (α := C) (β := C) ((g i : (a : G i) → C) x : C) ((g i : (a : G i) → C) y : C)
Tactic: simp_rw [mul_def, lift_def, map_mul (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : (i : ι) → Mul (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
r s : (i : ι) → G i
⊢ map₀ (F := G) (T := T) f (r * s) =
    HMul.hMul (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f r) (map₀ (F := G) (T := T) f s)
have simp_rw : ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) ((r * s) (Classical.arbitrary ι))⟧ =
  HMul.hMul (α := DirectLimit G (T := T) f)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (r (Classical.arbitrary ι))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (s (Classical.arbitrary ι))⟧
Tactic: simp_rw [map₀, Pi.mul_apply, mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : (i : ι) → Mul (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
r s : (i : ι) → G i
simp_rw :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) ((r * s) (Classical.arbitrary ι))⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (r (Classical.arbitrary ι))⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (s (Classical.arbitrary ι))⟧
⊢ map₀ (F := G) (T := T) f (r * s) =
    HMul.hMul (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f r) (map₀ (F := G) (T := T) f s)
have simp_rw₁ : ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
      (HMul.hMul (α := G (Classical.arbitrary ι)) (r (Classical.arbitrary ι)) (s (Classical.arbitrary ι)))⟧ =
  HMul.hMul (α := DirectLimit G (T := T) f)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (r (Classical.arbitrary ι))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (s (Classical.arbitrary ι))⟧
Tactic: simp_rw [map₀, Pi.mul_apply, mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → CommMagma (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 : G i
⊢ HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
have simp_rw : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 * x)⟧
Tactic: simp_rw [mul_def, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_3 : ι) → (h : x ≤ x_3) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Semigroup (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 x_2 : G i
⊢ HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ *
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ =
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧
have simp_rw : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1 * x_2)⟧
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * (x_1 * x_2))⟧
Tactic: simp_rw [mul_def, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Mul (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_7 : (i : ι) → StarMul (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 : G i
⊢ star
      (HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧) =
    HMul.hMul (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)
      (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
have simp_rw : star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧ =
  HMul.hMul (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)
    (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
Tactic: simp_rw [mul_def, star_def, star_mul, mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Mul (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_7 : (i : ι) → StarMul (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 : G i
simp_rw :
  star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)
      (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
⊢ star
      (HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧) =
    HMul.hMul (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)
      (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
have simp_rw₁ : ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star (x * x_1))⟧ =
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x_1)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧
Tactic: simp_rw [mul_def, star_def, star_mul, mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Mul (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_7 : (i : ι) → StarMul (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 : G i
simp_rw :
  star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)
      (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star (x * x_1))⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x_1)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧
⊢ star
      (HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧) =
    HMul.hMul (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)
      (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
have simp_rw₂ : ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x_1 * star x)⟧ =
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x_1)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧
Tactic: simp_rw [mul_def, star_def, star_mul, mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → SMul.{u_1, u_3} R (G i)
inst_6 : SMul R C
inst_7 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : ∀ (i : ι), MulActionHomClass.{u_4, u_1, u_3, u_5} (H i) R (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
r : R
x_1 : DirectLimit G (T := T) f
i : ι
x : G i
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
    r •
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
have simp_rw : DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧ =
  r •
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
Tactic: simp_rw [smul_def, lift_def, map_smul (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → SMul.{u_1, u_3} R (G i)
inst_6 : SMul R C
inst_7 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : ∀ (i : ι), MulActionHomClass.{u_4, u_1, u_3, u_5} (H i) R (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
r : R
x_1 : DirectLimit G (T := T) f
i : ι
x : G i
simp_rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧ =
    r •
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
    r •
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
have simp_rw₁ : (g i : (a : G i) → C) (r • x) = HSMul.hSMul (β := C) r ((g i : (a : G i) → C) x : C)
Tactic: simp_rw [smul_def, lift_def, map_smul (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Star R
inst_6 : (i : ι) → Star (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : (i : ι) → SMul.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_10 : ∀ (i : ι), StarModule.{u_1, u_3} R (G i)
r : R
i : ι
x : G i
⊢ star (HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
    HSMul.hSMul (β := DirectLimit G (T := T) f) (star r) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
have simp_rw : star (HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
  HSMul.hSMul (β := DirectLimit G (T := T) f) (star r) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧
Tactic: simp_rw [star_def, smul_def, ← star_smul, star_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Star R
inst_6 : (i : ι) → Star (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : (i : ι) → SMul.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_10 : ∀ (i : ι), StarModule.{u_1, u_3} R (G i)
r : R
i : ι
x : G i
simp_rw :
  star (HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
    HSMul.hSMul (β := DirectLimit G (T := T) f) (star r) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧
⊢ star (HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
    HSMul.hSMul (β := DirectLimit G (T := T) f) (star r) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
have simp_rw₁ : Eq (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧)
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star r • star x)⟧
Tactic: simp_rw [star_def, smul_def, ← star_smul, star_def]