awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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 ι
inst_5 : Nonempty ι
inst_6 : IsDirectedOrder ι
z_1 : DirectLimit G f
ind : ι
z : DirectSum ι G
p q : DirectSum.{u_2, u_3} ι fun (i : ι) ↦ G i
h :
  ∃ (i : ι) (x : G i),
    Eq (α := DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
      (Quotient.mk'' p : Quotient (moduleCon (G := G) f).toSetoid)
h_1 :
  ∃ (i : ι) (x : G i),
    Eq (α := DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
      (Quotient.mk'' q : Quotient (moduleCon (G := G) f).toSetoid)
i : ι
x : G i
ihx :
  Eq (α := DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)
    (Quotient.mk'' p : Quotient (moduleCon (G := G) f).toSetoid)
j : ι
y : G j
ihy :
  Eq (α := DirectLimit G f) ((of R ι G f j : (a : G j) → DirectLimit G f) y : DirectLimit G f)
    (Quotient.mk'' q : Quotient (moduleCon (G := G) f).toSetoid)
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ Eq (α := DirectLimit G f)
    ((of R ι G f k : (a : G k) → DirectLimit G f)
        (HAdd.hAdd (α := G k) (β := G k) ((f i k hik : (a : G i) → G k) x : G k)
          ((f j k hjk : (a : G j) → G k) y : G k)) :
      DirectLimit G f)
    (Quotient.mk'' (p + q) : Quotient (moduleCon (G := G) f).toSetoid)
have rw : HAdd.hAdd (α := DirectLimit G f) (Quotient.mk'' p) (Quotient.mk'' q) = Quotient.mk'' (p + q)
Tactic: rw [map_add, of_f, of_f, ihx, ihy]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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 ι
inst_5 : Nonempty ι
inst_6 : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i : (a : G i) → DirectLimit G f) x = z
j : ι
y : G j
hy : (of R ι G f j : (a : G j) → DirectLimit G f) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
rw : (of R ι G f i : (a : G i) → DirectLimit G f) x = z
⊢ (of R ι G f k : (a : G k) → DirectLimit G f) ((f i k hik : (a : G i) → G k) x) = z
have rw₁ : z = z
Tactic: rw [of_f, hx]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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 ι
inst_5 : Nonempty ι
inst_6 : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i : (a : G i) → DirectLimit G f) x = z
j : ι
y : G j
hy : (of R ι G f j : (a : G j) → DirectLimit G f) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
rw : (of R ι G f j : (a : G j) → DirectLimit G f) y = w
⊢ (of R ι G f k : (a : G k) → DirectLimit G f) ((f j k hjk : (a : G j) → G k) y) = w
have rw₁ : w = w
Tactic: rw [of_f, hy]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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
⊢ lift R ι G f (fun (i : ι) ↦ F ∘ₗ of R ι G f i) ⋯ = F
have h : ∀ (i : ι) (x : G i),
  Eq.{u_4 + 1} (α := P) ((lift R ι G f (fun (i : ι) ↦ F ∘ₗ of R ι G f i) sorry ∘ₗ of R ι G f i : (a : G i) → P) x : P)
    ((F ∘ₗ of R ι G f i : (a : G i) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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 ι
⊢ Eq (α := DirectLimit G f →ₗ[R] DirectLimit G f) (lift R ι G f (of R ι G f) ⋯) LinearMap.id
have h : ∀ (i : ι) (x : G i),
  Eq (α := DirectLimit G f)
    ((lift R ι G f (of R ι G f) sorry ∘ₗ 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: ext
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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)
⊢ Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift R ι G f g Hg) : (a : DirectLimit G f) → P)
have inl : IsEmpty ι → Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift R ι G f g Hg) : (a : DirectLimit G f) → P)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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)
⊢ Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift R ι G f g Hg) : (a : DirectLimit G f) → P)
have inr : Nonempty ι → Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift R ι G f g Hg) : (a : DirectLimit G f) → P)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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)
⊢ z = w
have 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)
Tactic: obtain ⟨i, x, y, rfl, rfl⟩ := exists_of₂ z w
Cleared hypotheses: z, w, eq
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (hypothesis)
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 (α := 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)
have eq₁ : 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
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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)
⊢ 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)
have 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)
Tactic: rw [injective _ eq]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (hypothesis)
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 (α := DirectLimit G' f')
    (((fun (i : ι) ↦ (of R ι G' f' i ∘ₗ g_2 i : G i →ₗ[R] DirectLimit G' f')) j : (a : G j) → DirectLimit G' f')
        ((f i j h : (a : G i) → G j) g) :
      DirectLimit G' f')
    (((fun (i : ι) ↦ (of R ι G' f' i ∘ₗ g_2 i : G i →ₗ[R] DirectLimit G' f')) i : (a : G i) → DirectLimit G' f') g :
      DirectLimit G' f')
have eq1 : 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
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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)
⊢ 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')
have 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')
Tactic: rw [eq1, of_f]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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')
⊢ 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')
have 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')
Tactic: rw [eq1, of_f]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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 ι
⊢ Eq (α := DirectLimit G f →ₗ[R] DirectLimit G f) (map (G := G) (G' := G) (fun (x : ι) ↦ LinearMap.id) ⋯) LinearMap.id
have h : ∀ (i : ι) (x : G i),
  Eq (α := DirectLimit G f)
    ((map (G := G) (G' := G) (fun (x : ι) ↦ LinearMap.id) sorry ∘ₗ 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: ext
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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
⊢ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) j ∘ₗ f i j h = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
have rw : g₂ j ∘ₗ g₁ 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]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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
⊢ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) j ∘ₗ f i j h = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
have rw₁ : g₂ j ∘ₗ f' i j h ∘ₗ g₁ i = 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]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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
⊢ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) j ∘ₗ f i j h = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
have rw₂ : (g₂ j ∘ₗ f' i j h) ∘ₗ g₁ i = 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]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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
⊢ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) j ∘ₗ f i j h = f'' i j h ∘ₗ (fun (i : ι) ↦ g₂ i ∘ₗ g₁ i) i
have rw₃ : (f'' i j h ∘ₗ g₂ i) ∘ₗ g₁ i = 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]