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 ι
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
e : (i : ι) → LinearEquiv.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h = f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i)
i_1 : ι
g : G' i_1
i j : ι
h : i ≤ j
rw : f' i j h = (↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₁ : f' i j h = ((↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₂ : f' i j h = (f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i)) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₃ : f' i j h = f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₄ : f' i j h = f' i j h ∘ₗ (↑((e i).symm ≪≫ₗ e i) : G' i →ₗ[R] G' i)
⊢ (↑(e j).symm : G' j →ₗ[R] G j) ∘ₗ f' i j h = f i j h ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
have rw₅ : f' i j h = f' i j h ∘ₗ (↑(LinearEquiv.refl R (G' i)) : G' i →ₗ[R] G' i)
Tactic: rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
      refl_toLinearMap, comp_id]
-- 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 ι
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
e : (i : ι) → LinearEquiv.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h = f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i)
i_1 : ι
g : G' i_1
i j : ι
h : i ≤ j
rw : f' i j h = (↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₁ : f' i j h = ((↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₂ : f' i j h = (f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i)) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₃ : f' i j h = f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₄ : f' i j h = f' i j h ∘ₗ (↑((e i).symm ≪≫ₗ e i) : G' i →ₗ[R] G' i)
rw₅ : f' i j h = f' i j h ∘ₗ (↑(LinearEquiv.refl R (G' i)) : G' i →ₗ[R] G' i)
⊢ (↑(e j).symm : G' j →ₗ[R] G j) ∘ₗ f' i j h = f i j h ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
have rw₆ : f' i j h = f' i j h ∘ₗ LinearMap.id
Tactic: rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
      refl_toLinearMap, comp_id]
-- 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 ι
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
e : (i : ι) → LinearEquiv.{u_1, u_1, u_3, u_5} (RingHom.id R) (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h = f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i)
i_1 : ι
g : G' i_1
i j : ι
h : i ≤ j
rw : f' i j h = (↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₁ : f' i j h = ((↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₂ : f' i j h = (f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i)) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₃ : f' i j h = f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i) ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
rw₄ : f' i j h = f' i j h ∘ₗ (↑((e i).symm ≪≫ₗ e i) : G' i →ₗ[R] G' i)
rw₅ : f' i j h = f' i j h ∘ₗ (↑(LinearEquiv.refl R (G' i)) : G' i →ₗ[R] G' i)
rw₆ : f' i j h = f' i j h ∘ₗ LinearMap.id
⊢ (↑(e j).symm : G' j →ₗ[R] G j) ∘ₗ f' i j h = f i j h ∘ₗ (↑(e i).symm : G' i →ₗ[R] G i)
have rw₇ : f' i j h = f' i j h
Tactic: rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
      refl_toLinearMap, comp_id]
-- 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 ι
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
⊢ Eq (α :=
    _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f →ₗ[R]
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
    (lift R ι G f (Module.of R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f) ⋯ ∘ₗ
      Module.lift R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f (of R ι G f) ⋯)
    LinearMap.id
have h : ∀ (i : ι) (x : G i),
  Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
    (((lift R ι G f (Module.of R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f) sorry ∘ₗ
              Module.lift R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f (of R ι G f) sorry) ∘ₗ
            Module.of R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f i :
          (a : G i) → _root_.DirectLimit G f)
        x :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
    ((LinearMap.id ∘ₗ Module.of R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f i :
          (a : G i) → _root_.DirectLimit G f)
        x :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) 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 ι
inst_5 : Nonempty ι
inst_6 : IsDirectedOrder ι
inst_7 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
⊢ Eq (α := DirectLimit G f →ₗ[R] DirectLimit G f)
    (Module.lift R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f (of R ι G f) ⋯ ∘ₗ
      lift R ι G f (Module.of R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f) ⋯)
    LinearMap.id
have h : ∀ (i : ι) (x : G i),
  Eq (α := DirectLimit G f)
    (((Module.lift R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f (of R ι G f) sorry ∘ₗ
              lift R ι G f (Module.of R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) 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 (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 ι
inst_5 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_6 : IsDirectedOrder ι
i : ι
x y : G i
h :
  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)
⊢ ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j) ((f i j hij : (a : G i) → G j) y : G j)
have this : Nonempty ι
Tactic: have := Nonempty.intro i
-- 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 ι
inst_5 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_6 : IsDirectedOrder ι
i : ι
x y : G i
h :
  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)
this : Nonempty ι
⊢ ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j) ((f i j hij : (a : G i) → G j) y : G j)
have h₁ : Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
  ((linearEquiv G f : (a : DirectLimit G f) → _root_.DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) x) :
    _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
  ((linearEquiv G f : (a : DirectLimit G f) → _root_.DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) y) :
    _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
Tactic: apply_fun linearEquiv _ _ at h
Cleared hypotheses: h
-- 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 ι
inst_5 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_6 : IsDirectedOrder ι
i : ι
x y : G i
this : Nonempty ι
h :
  Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
    ((linearEquiv G f : (a : DirectLimit G f) → _root_.DirectLimit G f)
        ((of R ι G f i : (a : G i) → DirectLimit G f) x) :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
    ((linearEquiv G f : (a : DirectLimit G f) → _root_.DirectLimit G f)
        ((of R ι G f i : (a : G i) → DirectLimit G f) y) :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
⊢ ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j) ((f i j hij : (a : G i) → G j) y : G j)
have h₁ : Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧
Tactic: simp_rw [linearEquiv_of] at h
Cleared hypotheses: h
-- 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 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_6 : IsDirectedOrder ι
i : ι
x y : G i
this : Nonempty ι
h :
  Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧
⊢ ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j) ((f i j hij : (a : G i) → G j) y : G j)
have have : ∀ (j : ι)
  (h :
    ∃ (hx : (Sigma.mk (β := fun (i : ι) ↦ G i) i x).fst (β := fun (i : ι) ↦ G i) ≤ j) (hy :
      (Sigma.mk (β := fun (i : ι) ↦ G i) i y).fst (β := fun (i : ι) ↦ G i) ≤ j),
      Eq (α := G j)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).fst (β := fun (i : ι) ↦ G i)) j hx : (a : G ⟨i, x⟩.fst) → G j)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).snd (β := fun (i : ι) ↦ G i)) :
          G j)
        ((f ((Sigma.mk (β := fun (i : ι) ↦ G i) i y).fst (β := fun (i : ι) ↦ G i)) j hy : (a : G ⟨i, y⟩.fst) → G j)
            ((Sigma.mk (β := fun (i : ι) ↦ G i) i y).snd (β := fun (i : ι) ↦ G i)) :
          G j)),
  ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j) ((f i j hij : (a : G i) → G j) y : G j)
Tactic: have ⟨j, h⟩ := Quotient.exact h
-- 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 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_6 : IsDirectedOrder ι
i : ι
x : G i
H : Eq (α := DirectLimit G f) ((of R ι 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)
have h : ∀ (x : ι) (x_1 : i ≤ x), Eq (α := G x) (0 : G x) ((f i x x_1 : (a : G i) → G x) 0 : G x)
Tactic: convert! exists_eq_of_of_eq (H.trans (map_zero <| _).symm)
-- 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 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_6 : IsDirectedOrder ι
i : ι
x : G i
H : Eq (α := DirectLimit G f) ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f) (0 : DirectLimit G f)
x_1 : ι
h : i ≤ x_1
⊢ Eq (α := G x_1) (0 : G x_1) ((f i x_1 h : (a : G i) → G x_1) 0 : G x_1)
have h : Eq.{u_3 + 1} (α := G x_1) 0 0
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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
⊢ lift G f P (fun (i : ι) ↦ F.comp (of G f i)) ⋯ = F
have 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)) sorry) (of G f i) :
          (a : G i) → P)
        x :
      P)
    ((F.comp (of G f i) : (a : G i) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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 ι
⊢ Eq (α := DirectLimit G f →+ DirectLimit G f) (lift G f (DirectLimit G f) (of G f) ⋯)
    (AddMonoidHom.id (DirectLimit G f))
have h : ∀ (i : ι) (x : G i),
  Eq (α := DirectLimit G f)
    ((AddMonoidHom.comp (N := DirectLimit G f) (lift G f (DirectLimit G f) (of G f) sorry) (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: ext
-- 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)
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 (α := DirectLimit G' f')
    (((fun (i : ι) ↦ (AddMonoidHom.comp (of G' f' i) (g_2 i) : G i →+ 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 : ι) ↦ (AddMonoidHom.comp (of G' f' i) (g_2 i) : G i →+ 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).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
-- 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)
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)
⊢ 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')
have 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')
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)
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')
⊢ 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')
have 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')
Tactic: rw [eq1, of_f]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Module (goal)
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 ι
⊢ Eq (α := DirectLimit G f →+ DirectLimit G f) (map (G := G) (G' := G) (fun (x : ι) ↦ AddMonoidHom.id (G x)) ⋯)
    (AddMonoidHom.id (DirectLimit G f))
have h : ∀ (i : ι) (x : G i),
  Eq (α := DirectLimit G f)
    ((AddMonoidHom.comp (map (G := G) (G' := G) (fun (x : ι) ↦ AddMonoidHom.id (G x)) sorry) (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: 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)
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
⊢ 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)
have rw : (g₂ j).comp ((g₁ j).comp (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]
-- 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)
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)
⊢ 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)
have rw₁ : (g₂ j).comp ((f' i j h).comp (g₁ i)) = (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]