awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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)
r : R
x_1 : DirectLimit G f
x : DirectSum ι G
⊢ ZeroHom.toFun
      (↑(AddCon.lift (addConGen (Eqv (G := G) f)) (↑(DirectSum.toModule R ι (M := G) P g) : DirectSum ι G →+ P) ⋯) :
        ZeroHom (addConGen (Eqv f)).Quotient P)
      (HSMul.hSMul (β := DirectLimit G f) r
        (Quot.mk (⇑(moduleCon f).toSetoid : DirectSum ι G → DirectSum ι G → Prop) x)) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (ZeroHom.toFun (M := AddCon.Quotient (addConGen (Eqv (G := G) f)))
        (↑(AddCon.lift (addConGen (Eqv (G := G) f)) (↑(DirectSum.toModule R ι (M := G) P g) : DirectSum ι G →+ P) ⋯) :
          ZeroHom (addConGen (Eqv f)).Quotient P)
        (Quot.mk (⇑(moduleCon f).toSetoid : DirectSum ι G → DirectSum ι G → Prop) x))

Tactic:
exact map_smul (DirectSum.toModule R ι P g) r x

Premises used: DirectSum.toModule, map_smul
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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 R ι G f g Hg : (a : DirectLimit G f) → P)
        ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) :
      P)
    ((g i : (a : G i) → P) x : P)

Tactic:
DirectSum.toModule_lof R _ _

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, DirectSum.toModule_lof, List.foldr, Finset.sum, Trunc.lift
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g₁ g₂ : DirectLimit G f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i
⊢ g₁ = g₂

Tactic:
LinearMap.toAddMonoidHom_injective <| AddCon.hom_ext <| DirectSum.addHom_ext' fun i =>
    congr($(h i).toAddMonoidHom)

Premises used: LinearMap.toAddMonoidHom, congrArg, LinearMap.toAddMonoidHom_injective, id, AddCon.hom_ext, DirectSum.addHom_ext'
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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 →ₗ[R] P
i j : ι
hij : i ≤ j
x : G i
⊢ Eq.{u_4 + 1} (α := P)
    (((fun (i : ι) ↦ F ∘ₗ of R ι G f i) j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
    (((fun (i : ι) ↦ F ∘ₗ of R ι G f i) 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
F : DirectLimit G f →ₗ[R] P
h :
  ∀ (i : ι) (x : G i),
    Eq.{u_4 + 1} (α := P) ((lift R ι G f (fun (i : ι) ↦ F ∘ₗ of R ι G f i) ⋯ ∘ₗ of R ι G f i : (a : G i) → P) x : P)
      ((F ∘ₗ of R ι G f i : (a : G i) → P) x : P)
⊢ lift R ι G f (fun (i : ι) ↦ F ∘ₗ of R ι G f i) ⋯ = F

Tactic:
ext
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
F : DirectLimit G f →ₗ[R] P
i : ι
x : G i
⊢ Eq.{u_4 + 1} (α := P) ((lift R ι G f (fun (i : ι) ↦ F ∘ₗ of R ι G f i) ⋯ ∘ₗ of R ι G f i : (a : G i) → P) x : P)
    ((F ∘ₗ of R ι 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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 R ι G f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G f)
    ((of R ι 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G f)
      ((lift R ι G f (of R ι G f) ⋯ ∘ₗ of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
      ((LinearMap.id ∘ₗ of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
⊢ Eq (α := DirectLimit G f →ₗ[R] DirectLimit G f) (lift R ι G f (of R ι G f) ⋯) LinearMap.id

Tactic:
ext
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
i : ι
x : G i
⊢ Eq (α := DirectLimit G f)
    ((lift R ι G f (of R ι G f) ⋯ ∘ₗ of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
    ((LinearMap.id ∘ₗ of R ι 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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_7 : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective.{u_3 + 1, u_4 + 1} (α := G i) (β := P) (⇑(g i) : (a : G i) → P)
inl : IsEmpty ι → Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift R ι G f g Hg) : (a : DirectLimit G f) → P)
inr : Nonempty ι → Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift R ι G f g Hg) : (a : DirectLimit G f) → P)
⊢ Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift R ι G f g Hg) : (a : DirectLimit G f) → P)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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_7 : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective.{u_3 + 1, u_4 + 1} (α := G i) (β := P) (⇑(g i) : (a : G i) → P)
h : IsEmpty ι
⊢ Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift R ι G f g Hg) : (a : DirectLimit G f) → P)

Tactic:
apply Function.injective_of_subsingleton

Premises used: Function.injective_of_subsingleton
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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_7 : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective.{u_3 + 1, u_4 + 1} (α := G i) (β := P) (⇑(g i) : (a : G i) → P)
h : Nonempty ι
z w : DirectLimit G f
eq :
  Eq.{u_4 + 1} (α := P) ((lift R ι G f g Hg : (a : DirectLimit G f) → P) z : P)
    ((lift R ι G f g Hg : (a : DirectLimit G f) → P) w : P)
inr :
  ∀ (i : ι) (x y : G i)
    (eq :
      Eq.{u_4 + 1} (α := P)
        ((lift R ι G f g Hg : (a : DirectLimit G f) → P)
            ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) :
          P)
        ((lift R ι G f g Hg : (a : DirectLimit G f) → P)
            ((of R ι G f i : (a : G i) → DirectLimit G f) y : DirectLimit G f) :
          P)),
    Eq (α := DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
      ((of R ι G f i : (a : G i) → DirectLimit G f) y : DirectLimit G f)
⊢ z = w

Tactic:
obtain ⟨i, x, y, rfl, rfl⟩ := exists_of₂ z w

Premises used: rfl, Module.DirectLimit.exists_of₂
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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_7 : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective.{u_3 + 1, u_4 + 1} (α := G i) (β := P) (⇑(g i) : (a : G i) → P)
h : Nonempty ι
i : ι
x y : G i
eq :
  Eq.{u_4 + 1} (α := P)
    ((lift R ι G f g Hg : (a : DirectLimit G f) → P)
        ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) :
      P)
    ((lift R ι G f g Hg : (a : DirectLimit G f) → P)
        ((of R ι G f i : (a : G i) → DirectLimit G f) y : DirectLimit G f) :
      P)
⊢ Eq.{u_4 + 1} (α := P) ((g i : (a : G i) → P) x : P) ((g i : (a : G i) → P) y : P)

Tactic:
simp_rw [lift_of] at eq

Premises used: Module.DirectLimit.lift_of
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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_7 : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective.{u_3 + 1, u_4 + 1} (α := G i) (β := P) (⇑(g i) : (a : G i) → P)
h : Nonempty ι
i : ι
x y : G i
eq : Eq.{u_4 + 1} (α := P) ((g i : (a : G i) → P) x : P) ((g i : (a : G i) → P) y : P)
inr inr₁ :
  Eq (α := DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) y : DirectLimit G f)
    ((of R ι G f i : (a : G i) → DirectLimit G f) y : DirectLimit G f)
⊢ Eq (α := DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
    ((of R ι G f i : (a : G i) → DirectLimit G f) y : DirectLimit G f)

Tactic:
rw [injective _ eq]
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g_1 : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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_7 : (i : ι) → AddCommMonoid (G' i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst_9 : (i : ι) → AddCommMonoid (G'' i)
inst_10 : (i : ι) → Module.{u_1, u_6} R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g_2 : (i : ι) → LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), g_2 j ∘ₗ f i j h = f' i j h ∘ₗ g_2 i
i j : ι
h : i ≤ j
g : G i
⊢ Eq.{u_5 + 1} (α := G' j) ((g_2 j ∘ₗ f i j h : (a : G i) → G' j) g : G' j)
    ((f' i j h ∘ₗ g_2 i : (a : G i) → G' j) g : G' j)

Tactic:
have eq1 := LinearMap.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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g_1 : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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_7 : (i : ι) → AddCommMonoid (G' i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst_9 : (i : ι) → AddCommMonoid (G'' i)
inst_10 : (i : ι) → Module.{u_1, u_6} R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g_2 : (i : ι) → LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), g_2 j ∘ₗ f i j h = f' i j h ∘ₗ 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 R ι 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 R ι 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 R ι G' f' i : (a : G' i) → DirectLimit G' f') ((g_2 i : (a : G i) → G' i) g) : DirectLimit G' f')
    ((of R ι 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 R ι 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 R ι 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: Module.DirectLimit.of_f
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), g j ∘ₗ f i j h = f' i j h ∘ₗ 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 R ι G f i : (a : G i) → DirectLimit G f) x) :
      DirectLimit G' f')
    ((of R ι 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: Module.DirectLimit.lift_of, AddCon.toQuotient
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G f)
      ((map (G := G) (G' := G) (fun (x : ι) ↦ LinearMap.id) ⋯ ∘ₗ of R ι G f i : (a : G i) → DirectLimit G f) x :
        DirectLimit G f)
      ((LinearMap.id ∘ₗ of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
⊢ Eq (α := DirectLimit G f →ₗ[R] DirectLimit G f) (map (G := G) (G' := G) (fun (x : ι) ↦ LinearMap.id) ⋯) LinearMap.id

Tactic:
ext
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
i : ι
x : G i
⊢ Eq (α := DirectLimit G f)
    ((map (G := G) (G' := G) (fun (x : ι) ↦ LinearMap.id) ⋯ ∘ₗ of R ι G f i : (a : G i) → DirectLimit G f) x :
      DirectLimit G f)
    ((LinearMap.id ∘ₗ of R ι 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (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_7 : (i : ι) → AddCommMonoid (G' i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst_9 : (i : ι) → AddCommMonoid (G'' i)
inst_10 : (i : ι) → Module.{u_1, u_6} R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
g₂ : (i : ι) → LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (G' i) (G'' i)
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i j : ι
h : i ≤ j
rw : g₂ j ∘ₗ g₁ j ∘ₗ f i j h = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
rw₁ : g₂ j ∘ₗ f' i j h ∘ₗ g₁ i = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
rw₂ : (g₂ j ∘ₗ f' i j h) ∘ₗ g₁ i = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
rw₃ : (f'' i j h ∘ₗ g₂ i) ∘ₗ g₁ i = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
rw₄ rw₅ : f'' i j h ∘ₗ g₂ i ∘ₗ g₁ i = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
⊢ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) j ∘ₗ f i j h = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i

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

Premises used: LinearMap.comp_assoc
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst_7 : (i : ι) → AddCommMonoid (G'' i)
inst_8 : (i : ι) → Module.{u_1, u_6} R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
g₂ : (i : ι) → LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (G' i) (G'' i)
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G'' f'')
      (((map (G := G') (G' := G'') g₂ hg₂ ∘ₗ map (G := G) (G' := G') g₁ hg₁) ∘ₗ of R ι G f i :
            (a : G i) → DirectLimit G'' f'')
          x :
        DirectLimit G'' f'')
      ((map (G := G) (G' := G'') (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) ⋯ ∘ₗ of R ι G f i : (a : G i) → DirectLimit G'' f'') x :
        DirectLimit G'' f'')
⊢ Eq (α := DirectLimit G f →ₗ[R] DirectLimit G'' f'')
    (map (G := G') (G' := G'') g₂ hg₂ ∘ₗ map (G := G) (G' := G') g₁ hg₁)
    (map (G := G) (G' := G'') (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) ⋯)

Tactic:
ext
-- 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)
inst_3 : (i : ι) → Module.{u_1, u_3} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_4 : DecidableEq ι
G' : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (G' i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst_7 : (i : ι) → AddCommMonoid (G'' i)
inst_8 : (i : ι) → Module.{u_1, u_6} R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
g₂ : (i : ι) → LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (G' i) (G'' i)
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i : ι
x : G i
⊢ Eq (α := DirectLimit G'' f'')
    (((map (G := G') (G' := G'') g₂ hg₂ ∘ₗ map (G := G) (G' := G') g₁ hg₁) ∘ₗ of R ι G f i :
          (a : G i) → DirectLimit G'' f'')
        x :
      DirectLimit G'' f'')
    ((map (G := G) (G' := G'') (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) ⋯ ∘ₗ of R ι G f i : (a : G i) → DirectLimit G'' f'') x :
      DirectLimit G'' f'')

Tactic:
simp