awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : ι) → AddGroupWithOne (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
n : ℕ
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        ((fun (x : ι) ↦ ((↑(Int.negSucc n) : G x) : G x)) (Classical.arbitrary ι))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i)
        (Sigma.fst (β := fun (i : ι) ↦ G i)
          (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
            ((fun (x : ι) ↦ ((↑(n + 1) : G x) : G x)) (Classical.arbitrary ι))))
        ((fun (x : ι) (x_1 : G x) ↦ -x_1)
          (Sigma.fst (β := fun (i : ι) ↦ G i)
            (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
              ((fun (x : ι) ↦ ((↑(n + 1) : G x) : G x)) (Classical.arbitrary ι))))
          (Sigma.snd (β := fun (i : ι) ↦ G i)
            (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
              ((fun (x : ι) ↦ ((↑(n + 1) : G x) : G x)) (Classical.arbitrary ι)))))⟧

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Nonempty ι
inst_5 : (i : ι) → AddGroupWithOne (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_7 : ∀ (i j : ι) (h : i ≤ j), OneHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
n : ℤ
i : ι
⊢ Eq (α := DirectLimit G (T := T) f) (↑n : DirectLimit G f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (↑n : G i)⟧

Tactic:
map₀_def _ _ (fun _ _ _ ↦ map_intCast' _ (map_one _) _) _

Premises used: map_one, map_intCast', DirectLimit.map₀_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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)⟧
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)⟧
⊢ ⟦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⟧

Tactic:
simp_rw [add_def, mul_def, left_distrib, add_def]

Premises used: DirectLimit.mul_def, DirectLimit.add_def, left_distrib
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 + 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⟧
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_2)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 * x_2)⟧
simp_rw₂ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_2 + x_1 * x_2)⟧ =
    HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_2)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 * x_2)⟧
⊢ 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⟧

Tactic:
simp_rw [add_def, mul_def, right_distrib, add_def]

Premises used: DirectLimit.mul_def, DirectLimit.add_def, right_distrib
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : ι) → Zero (G i)
inst_7 : (i : ι) → SMulZeroClass.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
rw :
  Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 0⟧ 0
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HSMul.hSMul (β := G (Classical.arbitrary ι)) r ((fun (x : ι) ↦ (0 : G x)) (Classical.arbitrary ι)))⟧
    0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : ι) → Zero (G i)
inst_7 : (i : ι) → SMulZeroClass.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 0⟧ 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Zero R
inst_7 : (i : ι) → Zero (G i)
inst_8 : (i : ι) → SMulWithZero.{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 j : ι) (h : i ≤ j), ZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
simp_rw :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x)⟧ 0
simp_rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 0⟧ 0
⊢ HSMul.hSMul (α := R) (β := DirectLimit G (T := T) f) 0 ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ = 0

Tactic:
simp_rw [smul_def, zero_smul, zero_def i]

Premises used: DirectLimit.smul_def, zero_smul, DirectLimit.zero_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Nonempty ι
inst_6 : (i : ι) → AddZeroClass (G i)
inst_7 : (i : ι) → DistribSMul.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
i : ι
x x_1 : G i
simp_rw :
  HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x + x_1)⟧ =
    HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ +
      HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • (x + x_1))⟧ =
    HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x_1)⟧
simp_rw₂ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x + r • x_1)⟧ =
    HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x_1)⟧
⊢ r •
      HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ +
      HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧

Tactic:
simp_rw [add_def, smul_def, smul_add, add_def]

Premises used: DirectLimit.add_def, DirectLimit.smul_def, smul_add
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Monoid R
inst_7 : (i : ι) → Monoid (G i)
inst_8 : (i : ι) → MulDistribMulAction.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_10 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
rw :
  Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧ 1
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HSMul.hSMul (β := G (Classical.arbitrary ι)) r ((fun (x : ι) ↦ (1 : G x)) (Classical.arbitrary ι)))⟧
    1

Tactic:
rw [smul_one]

Premises used: MulDistribMulAction.smul_one
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Monoid R
inst_7 : (i : ι) → Monoid (G i)
inst_8 : (i : ι) → MulDistribMulAction.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_10 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧ 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Nonempty ι
inst_6 : Monoid R
inst_7 : (i : ι) → Monoid (G i)
inst_8 : (i : ι) → MulDistribMulAction.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_10 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
i : ι
x x_1 : G i
simp_rw :
  HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧ =
    HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • (x * x_1))⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x_1)⟧
simp_rw₂ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x * r • x_1)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x_1)⟧
⊢ r •
      HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧

Tactic:
simp_rw [mul_def, smul_def, MulDistribMulAction.smul_mul, mul_def]

Premises used: DirectLimit.mul_def, DirectLimit.smul_def, MulDistribMulAction.smul_mul
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Semiring R
inst_7 : (i : ι) → AddCommMonoid (G i)
inst_8 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
h : ∀ (i j : ι) (h : i ≤ j), DistribMulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
x x_1 : R
i : ι
x_2 : G i
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_2)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 • x_2)⟧
simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x • x_2 + x_1 • x_2)⟧ =
    HAdd.hAdd (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x • x_2)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 • x_2)⟧
⊢ HSMul.hSMul (β := DirectLimit G (T := T) f) (x + x_1) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ =
    HSMul.hSMul (β := DirectLimit G (T := T) f) x ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ +
      HSMul.hSMul (β := DirectLimit G (T := T) f) x_1 ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧

Tactic:
simp_rw [smul_def, add_smul, add_def]

Premises used: DirectLimit.add_def, DirectLimit.smul_def, add_smul
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Semiring R
inst_7 : (i : ι) → AddCommMonoid (G i)
inst_8 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
h : ∀ (i j : ι) (h : i ≤ j), DistribMulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
i : ι
x : G i
simp_rw :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 x)⟧ 0
simp_rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 0⟧ 0
⊢ HSMul.hSMul (α := R) (β := DirectLimit G (T := T) f) 0 ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ = 0

Tactic:
simp_rw [smul_def, zero_smul, zero_def i]

Premises used: DirectLimit.smul_def, zero_smul, DirectLimit.zero_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Nonempty ι
inst_6 : (i : ι) → Mul (G i)
inst_7 : (i : ι) → SMul.{u_1, u_3} R (G i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_3, u_3} R (G i) (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_10 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
i : ι
x x_1 : G i
simp_rw :
  HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    r •
      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₁ :
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    r •
      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₂ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x * x_1)⟧ =
    HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧
simp_rw₃ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x * x_1)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • (x * x_1))⟧
⊢ HSMul.hSMul (β := DirectLimit G (T := T) f)
      (HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    r •
      HSMul.hSMul (α := DirectLimit G (T := T) f) (β := DirectLimit G (T := T) f)
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧

Tactic:
simp_rw [smul_eq_mul, smul_def, mul_def, smul_def, smul_mul_assoc]

Premises used: DirectLimit.mul_def, smul_mul_assoc, DirectLimit.smul_def, smul_eq_mul
-- Module: Mathlib.Algebra.Colimit.DirectLimit
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 : Nonempty ι
inst_6 : (i : ι) → Mul (G i)
inst_7 : (i : ι) → SMul.{u_1, u_3} R (G i)
inst_8 : ∀ (i : ι), SMulCommClass.{u_1, u_3, u_3} R (G i) (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_10 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
i : ι
x x_1 : G i
simp_rw :
  r •
      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⟧ *
      HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
simp_rw₁ :
  r •
      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 (r • x_1)⟧
simp_rw₂ :
  HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧ =
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * r • x_1)⟧
simp_rw₃ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • (x * x_1))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * r • x_1)⟧
⊢ r •
      HSMul.hSMul (α := DirectLimit G (T := T) f) (β := DirectLimit G (T := T) f)
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    HSMul.hSMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      (HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)

Tactic:
simp_rw [smul_eq_mul, smul_def, mul_def, smul_def, mul_smul_comm]

Premises used: DirectLimit.mul_def, DirectLimit.smul_def, mul_smul_comm, smul_eq_mul