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)
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
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 j : ι
h : i ≤ j
rw : f' i j h = (↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h ∘ₗ (fun (i : ι) ↦ (↑(e i).symm : G' i →ₗ[R] G i)) i
rw₁ : f' i j h = ((↑(e j) : G j →ₗ[R] G' j) ∘ₗ f i j h) ∘ₗ (fun (i : ι) ↦ (↑(e i).symm : G' i →ₗ[R] G i)) i
rw₂ : f' i j h = (f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i)) ∘ₗ (fun (i : ι) ↦ (↑(e i).symm : G' i →ₗ[R] G i)) i
rw₃ : f' i j h = f' i j h ∘ₗ (↑(e i) : G i →ₗ[R] G' i) ∘ₗ (fun (i : ι) ↦ (↑(e i).symm : G' i →ₗ[R] G i)) 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
rw₇ rw₈ : f' i j h = f' i j h
⊢ (fun (i : ι) ↦ (↑(e i).symm : G' i →ₗ[R] G i)) j ∘ₗ f' i j h =
    f i j h ∘ₗ (fun (i : ι) ↦ (↑(e i).symm : G' i →ₗ[R] G i)) i

Tactic:
rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
        refl_toLinearMap, comp_id]

Premises used: LinearMap.comp_assoc, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_trans_self, LinearEquiv.toLinearMap_symm_comp_eq, LinearEquiv.comp_coe, LinearMap.comp_id
-- 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
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)
⊢ Eq (α := DirectLimit G' f' →ₗ[R] DirectLimit G' f')
    (map (G := G) (G' := G') (fun (x : ι) ↦ (↑(e x) : G x →ₗ[R] G' x)) he ∘ₗ
      map (G := G') (G' := G) (fun (i : ι) ↦ (↑(e i).symm : G' i →ₗ[R] G i)) ⋯)
    LinearMap.id

Tactic:
simp [map_comp]

Premises used: Module.DirectLimit.map_comp
-- 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
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)
⊢ Eq (α := DirectLimit G f →ₗ[R] DirectLimit G f)
    (map (G := G') (G' := G) (fun (i : ι) ↦ (↑(e i).symm : G' i →ₗ[R] G i)) ⋯ ∘ₗ
      map (G := G) (G' := G') (fun (x : ι) ↦ (↑(e x) : G x →ₗ[R] G' x)) he)
    LinearMap.id

Tactic:
simp [map_comp]

Premises used: Module.DirectLimit.map_comp
-- 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
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 : ι
g : G i
⊢ Eq (α := DirectLimit G' f')
    ((congr (G := G) (G' := G') e he : (a : DirectLimit G f) → DirectLimit G' f')
        ((of R ι G f i : (a : G i) → DirectLimit G f) g) :
      DirectLimit G' f')
    ((of R ι G' f' i : (a : G' i) → DirectLimit G' f') ((e i : (a : G i) → G' i) g) : DirectLimit G' f')

Tactic:
map_apply_of _ he _

Premises used: Module.DirectLimit.map_apply_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 ι
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
rw₇ rw₈ : f' i j h = f' i j h
⊢ (↑(e j).symm : G' j →ₗ[R] G j) ∘ₗ f' i j h = f i j h ∘ₗ (↑(e i).symm : 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]

Premises used: LinearMap.comp_assoc, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_trans_self, LinearEquiv.toLinearMap_symm_comp_eq, LinearEquiv.comp_coe, LinearMap.comp_id
-- 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 ι
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)
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) ⋯ ∘ₗ
                Module.lift R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f (of R ι G f) ⋯) ∘ₗ
              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)
⊢ 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

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 ι
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)
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) ⋯ ∘ₗ
              Module.lift R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f (of R ι G f) ⋯) ∘ₗ
            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:
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 ι
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)
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) ⋯ ∘ₗ
                lift R ι G f (Module.of R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) 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)
    (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

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 ι
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)
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) ⋯ ∘ₗ
              lift R ι G f (Module.of R ι G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) 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 ι
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)
i : ι
g : G i
⊢ 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) g) :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f)
    (⟦Sigma.mk (β := fun (i : ι) ↦ G i) i g⟧ :
      Quotient (α := (i : ι) × G i) (setoid (F := G) (T := fun (i j : ι) (h : i ≤ j) ↦ G i →ₗ[R] G j) f))

Tactic:
simp [linearEquiv]

Premises used: Module.DirectLimit.linearEquiv
-- 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 ι
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)
g : (i : ι) × G i
⊢ Eq (α := DirectLimit G f)
    ((LinearEquiv.symm (linearEquiv G f) : (a : _root_.DirectLimit G f) → DirectLimit G f) ⟦g⟧ : DirectLimit G f)
    ((of R ι G f (g.fst (β := fun (i : ι) ↦ G i)) : (a : G g.fst) → DirectLimit G f) (g.snd (β := fun (i : ι) ↦ G i)) :
      DirectLimit G f)

Tactic:
rfl

Premises used: DirectLimit.lift, AddCon.toQuotient, rfl
-- 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 ι
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)
⊢ Nonempty ι

Tactic:
have := Nonempty.intro i
-- 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 ι
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 ι
⊢ 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

Premises used: Module.DirectLimit.linearEquiv
-- 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 ι
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)
⊢ 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

Premises used: Module.DirectLimit.linearEquiv_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 ι
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⟧
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)
⊢ ∃ (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
-- 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 ι
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_1 :
  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 : ι
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:
⟨j, h.1, h.2.2⟩

Premises used: Exists.intro
-- 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 ι
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_1 :
  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 : ι
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:
exact ⟨j, h.1, h.2.2⟩
-- 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 ι
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) ((f i j hij : (a : G i) → G j) 0 : G j)

Tactic:
exists_eq_of_of_eq (H.trans (map_zero <| _).symm)

Premises used: map_zero, Module.DirectLimit.exists_eq_of_of_eq, Eq.symm, Eq.trans
-- 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 ι
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)
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)
⊢ ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f i j hij : (a : G i) → G j) x : G j) (0 : G j)

Tactic:
convert! exists_eq_of_of_eq (H.trans (map_zero <| _).symm)

Premises used: map_zero, Module.DirectLimit.exists_eq_of_of_eq, Eq.symm, Eq.trans
-- 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 ι
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_1 : i ≤ x_1
h h₁ : Eq.{u_3 + 1} (α := G x_1) 0 0
⊢ Eq (α := G x_1) (0 : G x_1) ((f i x_1 h_1 : (a : G i) → G x_1) 0 : G x_1)

Tactic:
rw [map_zero]

Premises used: map_zero
-- 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
h : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
⊢ DirectedSystem G fun (i j : ι) (hij : i ≤ j) ↦ (⇑(f i j hij).toNatLinearMap : (a : G i) → G j)

Tactic:
h