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 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{u_4, u_3, u_5} (H i) (G i) C
i : ι
x : G i
ne : Ne (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ 0
this : x ≠ 0
simp_rw :
  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⟧
      (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ x_1⁻¹) ⋯
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
    1
have simp_rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x⁻¹)⟧ 1
Tactic: simp_rw [map_def, mul_def, mul_inv_cancel₀ this, one_def 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 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{u_4, u_3, u_5} (H i) (G i) C
i : ι
x : G i
ne : Ne (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ 0
this : x ≠ 0
simp_rw :
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⁻¹⟧ =
    1
simp_rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x⁻¹)⟧ 1
⊢ HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ x_1⁻¹) ⋯
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
    1
have simp_rw₂ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 1⟧ 1
Tactic: simp_rw [map_def, mul_def, mul_inv_cancel₀ this, one_def 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 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{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 : 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
      (⟦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 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 x⁻¹⟧ =
  (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 [inv₀_def, lift_def, map_inv₀ (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 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{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 : 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 x⁻¹⟧ =
    (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 x⟧)⁻¹ =
    (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₁ : Eq.{u_5 + 1} (α := C) ((g i : (a : G i) → C) x⁻¹ : C) (((g i : (a : G i) → C) x)⁻¹ : C)
Tactic: simp_rw [inv₀_def, lift_def, map_inv₀ (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 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{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
      (HDiv.hDiv (α := 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 [div₀_def, lift_def, map_div₀ (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 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{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
      (HDiv.hDiv (α := 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) = HDiv.hDiv (α := C) (β := C) ((g i : (a : G i) → C) x : C) ((g i : (a : G i) → C) y : C)
Tactic: simp_rw [div₀_def, lift_def, map_div₀ (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 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{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 : DirectLimit G (T := T) f
z : ℤ
i : ι
x : G i
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HPow.hPow (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ z) =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ^
      z
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 ^ z)⟧ =
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ^
    z
Tactic: simp_rw [zpow₀_def, lift_def, map_zpow₀ (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 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{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 : DirectLimit G (T := T) f
z : ℤ
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 (x ^ z)⟧ =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ^
      z
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HPow.hPow (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ z) =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ^
      z
have simp_rw₁ : (g i : (a : G i) → C) (x ^ z) = HPow.hPow (α := C) ((g i : (a : G i) → C) x : C) z
Tactic: simp_rw [zpow₀_def, lift_def, map_zpow₀ (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 : Nonempty ι
inst_6 : (i : ι) → AddMonoidWithOne (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
n : ℕ
simp_rw simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (↑(n + 1) : G (Classical.arbitrary ι))⟧ =
    HAdd.hAdd (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (↑n : G (Classical.arbitrary ι))⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        ((fun (x : ι) ↦ ((↑(n + 1) : G x) : G x)) (Classical.arbitrary ι))⟧ =
    HAdd.hAdd (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
          ((fun (x : ι) ↦ ((↑n : G x) : G x)) (Classical.arbitrary ι))⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) ((fun (x : ι) ↦ (1 : G x)) (Classical.arbitrary ι))⟧
have simp_rw₂ : ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
      (HAdd.hAdd (α := G (Classical.arbitrary ι)) (↑n : G (Classical.arbitrary ι)) 1)⟧ =
  HAdd.hAdd (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (↑n : G (Classical.arbitrary ι))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧
Tactic: simp_rw [Nat.cast_succ, add_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_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 : Nonempty ι
inst_6 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 x_2 : G i
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ =
    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⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧
have simp_rw : HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 + x_2)⟧ =
  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⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧
Tactic: simp_rw [add_def, mul_def, left_distrib, add_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_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 : Nonempty ι
inst_6 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 x_2 : G i
simp_rw :
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 + x_2)⟧ =
    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⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ =
    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⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧
have simp_rw₁ : ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * (x_1 + x_2))⟧ =
  HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_2)⟧
Tactic: simp_rw [add_def, mul_def, left_distrib, add_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_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 : Nonempty ι
inst_6 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 x_2 : G i
simp_rw :
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 + x_2)⟧ =
    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⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧
simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * (x_1 + x_2))⟧ =
    HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_2)⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ =
    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⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧
have simp_rw₂ : ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1 + x * x_2)⟧ =
  HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_2)⟧
Tactic: simp_rw [add_def, mul_def, left_distrib, add_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_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 : Nonempty ι
inst_6 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 x_2 : G i
⊢ HAdd.hAdd (α := 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⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ +
      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 : HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x + x_1)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ =
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ +
    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⟧
Tactic: simp_rw [add_def, mul_def, right_distrib, add_def]