awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := DirectLimit G f)
    ((of G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f)
    ((of G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)

Tactic:
Module.DirectLimit.of_f

Premises used: AddCommGroup.DirectLimit, Module.DirectLimit.of_f, AddCon.toQuotient
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
C : DirectLimit G f → Prop
z : DirectLimit G f
ih : ∀ (i : ι) (x : G i), C ((of G f i : (a : G i) → DirectLimit G f) x)
⊢ C z

Tactic:
Module.DirectLimit.induction_on z ih

Premises used: Module.DirectLimit.induction_on
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
inst_3 : IsDirectedOrder ι
inst_4 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
i : ι
x : G i
h : Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) (0 : DirectLimit G f)
⊢ ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j) (0 : G j)

Tactic:
Module.DirectLimit.of.zero_exact h

Premises used: Module.DirectLimit.of.zero_exact
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
P : Type u_4
inst_3 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
i : ι
x : G i
⊢ Eq.{u_4 + 1} (α := P)
    ((lift G f P g Hg : (a : DirectLimit G f) → P) ((of G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) : P)
    ((g i : (a : G i) → P) x : P)

Tactic:
Module.DirectLimit.lift_of
    -- Note: had to make these arguments explicit https://github.com/leanprover-community/mathlib4/pull/8386
    (f := fun i j hij ↦ (f i j hij).toNatLinearMap)
    (fun i ↦ (g i).toNatLinearMap)
    Hg
    x

Premises used: Multiset.sum, Multiset.foldr, Module.DirectLimit.lift_of, Quotient.liftOn', AddCon.liftOn, AddMonoidHom.toNatLinearMap, List.foldr, Finset.sum, Trunc.lift
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
P : Type u_4
inst_3 : AddCommMonoid P
g₁ g₂ : DirectLimit G f →+ P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
AddCon.hom_ext <| DirectSum.addHom_ext' h

Premises used: AddCommGroup.DirectLimit, AddCon.hom_ext, Module.DirectLimit, DirectSum.addHom_ext', ModuleCon.Quotient
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
F : DirectLimit G f →+ P
i j : ι
hij : i ≤ j
x : G i
⊢ Eq.{u_4 + 1} (α := P)
    (((fun (i : ι) ↦ F.comp (of G f i)) j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
    (((fun (i : ι) ↦ F.comp (of G f i)) i : (a : G i) → P) x : P)

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
P : Type u_4
inst_3 : AddCommMonoid P
F : DirectLimit G f →+ P
h :
  ∀ (i : ι) (x : G i),
    Eq.{u_4 + 1} (α := P)
      ((AddMonoidHom.comp (N := DirectLimit G f) (lift G f P (fun (i : ι) ↦ F.comp (of G f i)) ⋯) (of G f i) :
            (a : G i) → P)
          x :
        P)
      ((F.comp (of G f i) : (a : G i) → P) x : P)
⊢ lift G f P (fun (i : ι) ↦ F.comp (of G f i)) ⋯ = F

Tactic:
ext
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
P : Type u_4
inst_3 : AddCommMonoid P
F : DirectLimit G f →+ P
i : ι
x : G i
⊢ Eq.{u_4 + 1} (α := P)
    ((AddMonoidHom.comp (N := DirectLimit G f) (lift G f P (fun (i : ι) ↦ F.comp (of G f i)) ⋯) (of G f i) :
          (a : G i) → P)
        x :
      P)
    ((F.comp (of G f i) : (a : G i) → P) x : P)

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := DirectLimit G f)
    ((of G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f)
    ((of G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G f)
      ((AddMonoidHom.comp (N := DirectLimit G f) (lift G f (DirectLimit G f) (of G f) ⋯) (of G f i) :
            (a : G i) → DirectLimit G f)
          x :
        DirectLimit G f)
      ((AddMonoidHom.comp (AddMonoidHom.id (DirectLimit G f)) (of G f i) : (a : G i) → DirectLimit G f) x :
        DirectLimit G f)
⊢ Eq (α := DirectLimit G f →+ DirectLimit G f) (lift G f (DirectLimit G f) (of G f) ⋯)
    (AddMonoidHom.id (DirectLimit G f))

Tactic:
ext
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
i : ι
x : G i
⊢ Eq (α := DirectLimit G f)
    ((AddMonoidHom.comp (N := DirectLimit G f) (lift G f (DirectLimit G f) (of G f) ⋯) (of G f i) :
          (a : G i) → DirectLimit G f)
        x :
      DirectLimit G f)
    ((AddMonoidHom.comp (AddMonoidHom.id (DirectLimit G f)) (of G f i) : (a : G i) → DirectLimit G f) x :
      DirectLimit G f)

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
P : Type u_4
inst_3 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
inst_4 : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective.{u_3 + 1, u_4 + 1} (α := G i) (β := P) (⇑(g i) : (a : G i) → P)
⊢ Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift G f P g Hg) : (a : DirectLimit G f) → P)

Tactic:
Module.DirectLimit.lift_injective (f := fun i j hij ↦ (f i j hij).toNatLinearMap) _ Hg injective

Premises used: Module.DirectLimit.lift_injective, AddCommGroup.DirectLimit, Quotient.liftOn', AddCon.liftOn, Module.DirectLimit, AddCon.Quotient
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g_1 : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_6 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g_2 : (i : ι) → AddMonoidHom.{u_3, u_5} (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), (g_2 j).comp (f i j h) = (f' i j h).comp (g_2 i)
i j : ι
h : i ≤ j
g : G i
⊢ Eq.{u_5 + 1} (α := G' j) (((g_2 j).comp (f i j h) : (a : G i) → G' j) g : G' j)
    (((f' i j h).comp (g_2 i) : (a : G i) → G' j) g : G' j)

Tactic:
have eq1 := DFunLike.congr_fun (hg i j h) g
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g_1 : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g_1 j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g_1 i : (a : G i) → P) x : P)
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_6 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g_2 : (i : ι) → AddMonoidHom.{u_3, u_5} (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), (g_2 j).comp (f i j h) = (f' i j h).comp (g_2 i)
i j : ι
h : i ≤ j
g : G i
eq1 :
  Eq.{u_5 + 1} (α := G' j) ((g_2 j : (a : G j) → G' j) ((f i j h : (a : G i) → G j) g) : G' j)
    ((f' i j h : (a : G' i) → G' j) ((g_2 i : (a : G i) → G' i) g : G' i) : G' j)
rw :
  Eq (α := DirectLimit G' f')
    ((of G' f' j : (a : G' j) → DirectLimit G' f')
        ((f' i j h : (a : G' i) → G' j) ((g_2 i : (a : G i) → G' i) g : G' i)) :
      DirectLimit G' f')
    ((of G' f' i : (a : G' i) → DirectLimit G' f') ((g_2 i : (a : G i) → G' i) g) : DirectLimit G' f')
rw₁ rw₂ :
  Eq (α := DirectLimit G' f')
    ((of G' f' i : (a : G' i) → DirectLimit G' f') ((g_2 i : (a : G i) → G' i) g) : DirectLimit G' f')
    ((of G' f' i : (a : G' i) → DirectLimit G' f') ((g_2 i : (a : G i) → G' i) g) : DirectLimit G' f')
⊢ Eq (α := DirectLimit G' f')
    ((of G' f' j : (a : G' j) → DirectLimit G' f') ((g_2 j : (a : G j) → G' j) ((f i j h : (a : G i) → G j) g)) :
      DirectLimit G' f')
    ((of G' f' i : (a : G' i) → DirectLimit G' f') ((g_2 i : (a : G i) → G' i) g) : DirectLimit G' f')

Tactic:
rw [eq1, of_f]

Premises used: AddCommGroup.DirectLimit.of_f
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
G' : ι → Type u_5
inst_3 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
g : (i : ι) → AddMonoidHom.{u_3, u_5} (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)
i : ι
x : G i
⊢ Eq (α := DirectLimit G' f')
    ((map (G := G) (G' := G') g hg : (a : DirectLimit G f) → DirectLimit G' f')
        ((of G f i : (a : G i) → DirectLimit G f) x) :
      DirectLimit G' f')
    ((of G' f' i : (a : G' i) → DirectLimit G' f') ((g i : (a : G i) → G' i) x) : DirectLimit G' f')

Tactic:
lift_of _ _ _ _ _

Premises used: AddCommGroup.DirectLimit.lift_of, AddCon.toQuotient
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G f)
      ((AddMonoidHom.comp (map (G := G) (G' := G) (fun (x : ι) ↦ AddMonoidHom.id (G x)) ⋯) (of G f i) :
            (a : G i) → DirectLimit G f)
          x :
        DirectLimit G f)
      ((AddMonoidHom.comp (AddMonoidHom.id (DirectLimit G f)) (of G f i) : (a : G i) → DirectLimit G f) x :
        DirectLimit G f)
⊢ Eq (α := DirectLimit G f →+ DirectLimit G f) (map (G := G) (G' := G) (fun (x : ι) ↦ AddMonoidHom.id (G x)) ⋯)
    (AddMonoidHom.id (DirectLimit G f))

Tactic:
ext
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
i : ι
x : G i
⊢ Eq (α := DirectLimit G f)
    ((AddMonoidHom.comp (map (G := G) (G' := G) (fun (x : ι) ↦ AddMonoidHom.id (G x)) ⋯) (of G f i) :
          (a : G i) → DirectLimit G f)
        x :
      DirectLimit G f)
    ((AddMonoidHom.comp (AddMonoidHom.id (DirectLimit G f)) (of G f i) : (a : G i) → DirectLimit G f) x :
      DirectLimit G f)

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_6 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g₁ : (i : ι) → AddMonoidHom.{u_3, u_5} (G i) (G' i)
g₂ : (i : ι) → AddMonoidHom.{u_5, u_6} (G' i) (G'' i)
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
rw : (g₂ j).comp ((g₁ j).comp (f i j h)) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
rw₁ : (g₂ j).comp ((f' i j h).comp (g₁ i)) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
rw₂ : ((g₂ j).comp (f' i j h)).comp (g₁ i) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
rw₃ : ((f'' i j h).comp (g₂ i)).comp (g₁ i) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
rw₄ rw₅ : (f'' i j h).comp ((g₂ i).comp (g₁ i)) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
⊢ AddMonoidHom.comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) j) (f i j h) =
    (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)

Tactic:
rw [AddMonoidHom.comp_assoc, hg₁ i, ← AddMonoidHom.comp_assoc, hg₂ i,
        AddMonoidHom.comp_assoc]

Premises used: AddMonoidHom.comp_assoc
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
G' : ι → Type u_5
inst_3 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_4 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g₁ : (i : ι) → AddMonoidHom.{u_3, u_5} (G i) (G' i)
g₂ : (i : ι) → AddMonoidHom.{u_5, u_6} (G' i) (G'' i)
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G'' f'')
      ((AddMonoidHom.comp (AddMonoidHom.comp (map (G := G') (G' := G'') g₂ hg₂) (map (G := G) (G' := G') g₁ hg₁))
              (of G f i) :
            (a : G i) → DirectLimit G'' f'')
          x :
        DirectLimit G'' f'')
      ((AddMonoidHom.comp (map (G := G) (G' := G'') (fun (i : ι) ↦ (g₂ i).comp (g₁ i)) ⋯) (of G f i) :
            (a : G i) → DirectLimit G'' f'')
          x :
        DirectLimit G'' f'')
⊢ Eq (α := DirectLimit G f →+ DirectLimit G'' f'')
    (AddMonoidHom.comp (map (G := G') (G' := G'') g₂ hg₂) (map (G := G) (G' := G') g₁ hg₁))
    (map (G := G) (G' := G'') (fun (i : ι) ↦ (g₂ i).comp (g₁ i)) ⋯)

Tactic:
ext
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_2 : DecidableEq ι
G' : ι → Type u_5
inst_3 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_4 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g₁ : (i : ι) → AddMonoidHom.{u_3, u_5} (G i) (G' i)
g₂ : (i : ι) → AddMonoidHom.{u_5, u_6} (G' i) (G'' i)
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i : ι
x : G i
⊢ Eq (α := DirectLimit G'' f'')
    ((AddMonoidHom.comp (AddMonoidHom.comp (map (G := G') (G' := G'') g₂ hg₂) (map (G := G) (G' := G') g₁ hg₁))
            (of G f i) :
          (a : G i) → DirectLimit G'' f'')
        x :
      DirectLimit G'' f'')
    ((AddMonoidHom.comp (map (G := G) (G' := G'') (fun (i : ι) ↦ (g₂ i).comp (g₁ i)) ⋯) (of G f i) :
          (a : G i) → DirectLimit G'' f'')
        x :
      DirectLimit G'' f'')

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_6 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
e : (i : ι) → AddEquiv.{u_3, u_5} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) = (f' i j h).comp (↑(e i) : G i →+ G' i)
i j : ι
h : i ≤ j
x : G' i
⊢ Eq.{u_5 + 1} (α := G' j)
    ((AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) : (a : G i) → G' j) (((e i).symm : (a : G' i) → G i) x) : G' j)
    ((((f' i j h).comp (↑(e i) : G i →+ G' i) : AddMonoidHom.{u_3, u_5} (G i) (G' j)) : (a : G i) → G' j)
        (((e i).symm : (a : G' i) → G i) x) :
      G' j)

Tactic:
have eq1 := DFunLike.congr_fun (he i j h) ((e i).symm x)
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_6 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
e : (i : ι) → AddEquiv.{u_3, u_5} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) = (f' i j h).comp (↑(e i) : G i →+ G' i)
i j : ι
h : i ≤ j
x : G' i
eq1 :
  Eq.{u_5 + 1} (α := G' j)
    ((AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) : (a : G i) → G' j) (((e i).symm : (a : G' i) → G i) x) : G' j)
    ((((f' i j h).comp (↑(e i) : G i →+ G' i) : AddMonoidHom.{u_3, u_5} (G i) (G' j)) : (a : G i) → G' j)
        (((e i).symm : (a : G' i) → G i) x) :
      G' j)
simp :
  ∀
    (eq1 :
      Eq.{u_5 + 1} (α := G' j)
        ((e j : (a : G j) → G' j) ((f i j h : (a : G i) → G j) (((e i).symm : (a : G' i) → G i) x : G i)) : G' j)
        ((f' i j h : (a : G' i) → G' j) x : G' j)),
    Eq.{u_3 + 1} (α := G j) (((e j).symm : (a : G' j) → G j) ((f' i j h : (a : G' i) → G' j) x) : G j)
      ((f i j h : (a : G i) → G j) (((e i).symm : (a : G' i) → G i) x : G i) : G j)
⊢ Eq.{u_3 + 1} (α := G j)
    ((AddMonoidHom.comp
            ((fun (i : ι) ↦
                ((↑(e i).symm : AddMonoidHom.{u_5, u_3} (G' i) (G i)) : AddMonoidHom.{u_5, u_3} (G' i) (G i)))
              j)
            (f' i j h) :
          (a : G' i) → G j)
        x :
      G j)
    (((f i j h).comp
            ((fun (i : ι) ↦
                ((↑(e i).symm : AddMonoidHom.{u_5, u_3} (G' i) (G i)) : AddMonoidHom.{u_5, u_3} (G' i) (G i)))
              i) :
          (a : G' i) → G j)
        x :
      G j)

Tactic:
simp only [AddMonoidHom.coe_comp, AddEquiv.coe_toAddMonoidHom, Function.comp_apply,
        AddMonoidHom.coe_coe, AddEquiv.apply_symm_apply] at eq1 ⊢

Premises used: AddMonoidHom.coe_coe, AddEquiv.apply_symm_apply, AddMonoidHom.coe_comp, Function.comp_apply, AddEquiv.coe_toAddMonoidHom
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_6 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
e : (i : ι) → AddEquiv.{u_3, u_5} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) = (f' i j h).comp (↑(e i) : G i →+ G' i)
i j : ι
h : i ≤ j
x : G' i
eq1 :
  Eq.{u_5 + 1} (α := G' j)
    ((e j : (a : G j) → G' j) ((f i j h : (a : G i) → G j) (((e i).symm : (a : G' i) → G i) x : G i)) : G' j)
    ((f' i j h : (a : G' i) → G' j) x : G' j)
⊢ Eq.{u_3 + 1} (α := G j) (((e j).symm : (a : G' j) → G j) ((f' i j h : (a : G' i) → G' j) x) : G j)
    ((f i j h : (a : G i) → G j) (((e i).symm : (a : G' i) → G i) x : G i) : G j)

Tactic:
simp [← eq1]
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst_3 : DecidableEq ι
P : Type u_4
inst_4 : AddCommMonoid P
g : (i : ι) → AddMonoidHom.{u_3, u_4} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_4 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_6 : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
e : (i : ι) → AddEquiv.{u_3, u_5} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) = (f' i j h).comp (↑(e i) : G i →+ G' i)
⊢ Eq (α := DirectLimit G f →+ DirectLimit G f)
    (AddMonoidHom.comp (map (G := G') (G' := G) (fun (i : ι) ↦ (↑(e i).symm : G' i →+ G i)) ⋯)
      (map (G := G) (G' := G') (fun (x : ι) ↦ (↑(e x) : G x →+ G' x)) he))
    (AddMonoidHom.id (DirectLimit G f))

Tactic:
simp [map_comp]

Premises used: AddCommGroup.DirectLimit.map_comp