awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : CommSemiring R
inst_5 : (i : ι) → Semiring (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_7 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_9 : Nonempty ι
P : Type u_7
inst_10 : Semiring P
inst_11 : Algebra R P
g₁ g₂ : DirectLimit G (T := T) f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
i : ι
x : G i
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)

Tactic:
exact congr($(h i) x)
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : CommSemiring R
inst_6 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_7 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_9 : Nonempty ι
i : ι
m : R
x : G i
rw :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) m : R) x)⟧
rw₁ rw₂ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧ =
    HSMul.hSMul (α := R) (β := DirectLimit G (T := T) f) ((MonoidHom.id R : (a : R) → R) m : R)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧

Tactic:
rw [smul_def, MonoidHom.id_apply]

Premises used: DirectLimit.smul_def, MonoidHom.id_apply
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := DirectLimit G (T := T) f)
    (((of G (T := T) f j : G j →ₙₐ[R] DirectLimit G (T := T) f) : (a : G j) → DirectLimit G f)
        ((f i j hij : (a : G i) → G j) x) :
      DirectLimit G (T := T) f)
    (((of G (T := T) f i : G i →ₙₐ[R] DirectLimit G (T := T) f) : (a : G i) → DirectLimit G f) x :
      DirectLimit G (T := T) f)

Tactic:
.symm <| eq_of_le ..

Premises used: DirectLimit.eq_of_le, Eq.symm
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : CommSemiring R
inst_6 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_7 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_9 : Nonempty ι
P : Type u_7
inst_10 : NonUnitalNonAssocSemiring P
inst_11 : DistribMulAction R P
g : (i : ι) → NonUnitalAlgHom.{u_1, u_1, u_3, u_7} (MonoidHom.id R) (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_7 + 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)
m : R
⊢ ∀ (x : DirectLimit G (T := T) f),
    DirectLimit.lift (F := G) (T := T) f (fun (x1 : ι) (x2 : G x1) ↦ (g x1 : (a : G x1) → P) x2) ⋯ (m • x) =
      HSMul.hSMul (α := R) (β := P) ((MonoidHom.id R : (a : R) → R) m : R)
        (DirectLimit.lift (F := G) (T := T) f (fun (x1 : ι) (x2 : G x1) ↦ (g x1 : (a : G x1) → P) x2) ⋯ x)

Tactic:
apply lift_smul

Premises used: DirectLimit.lift_smul
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : DistribMulAction R P
g : (i : ι) → NonUnitalAlgHom.{u_1, u_1, u_3, u_7} (MonoidHom.id R) (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_7 + 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 : ι
⊢ NonUnitalAlgHom.comp (B := DirectLimit G (T := T) f) (lift G (T := T) f P g Hg : DirectLimit G (T := T) f →ₙₐ[R] P)
      (of G (T := T) f i : G i →ₙₐ[R] DirectLimit G (T := T) f) =
    g i

Tactic:
rfl

Premises used: NonUnitalAlgHom.comp, DirectLimit.lift, rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : DistribMulAction R P
g : (i : ι) → NonUnitalAlgHom.{u_1, u_1, u_3, u_7} (MonoidHom.id R) (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_7 + 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_7 + 1} (α := P)
    (((lift G (T := T) f P g Hg : DirectLimit G (T := T) f →ₙₐ[R] P) : (a : DirectLimit G f) → P)
        (((of G (T := T) f i : G i →ₙₐ[R] DirectLimit G (T := T) f) : (a : G i) → DirectLimit G f) x :
          DirectLimit G (T := T) f) :
      P)
    ((g i : (a : G i) → P) x : P)

Tactic:
rfl

Premises used: DirectLimit.lift, rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : DistribMulAction R P
g₁ g₂ : DirectLimit G (T := T) f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
h₁ :
  ∀ (x : DirectLimit G (T := T) f),
    Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
⊢ g₁ = g₂

Tactic:
ext x
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : DistribMulAction R P
g₁ g₂ : DirectLimit G (T := T) f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
x : DirectLimit G (T := T) f
h₁ :
  ∀ (i : ι) (x : G i),
    Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
      ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)

Tactic:
induction x using DirectLimit.induction with | _ i x
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : DistribMulAction R P
g₁ g₂ : DirectLimit G (T := T) f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
i : ι
x : G i
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)

Tactic:
congr($(h i) x)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : DistribMulAction R P
g₁ g₂ : DirectLimit G (T := T) f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
i : ι
x : G i
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)

Tactic:
exact congr($(h i) x)
-- Module: Mathlib.Algebra.Colimit.Finiteness
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq (Submodule R M)
x : M
⊢ Membership.mem (γ := Set M) {x} x

Tactic:
rfl
-- Module: Mathlib.Algebra.Colimit.Finiteness
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq (Submodule R M)
N : { N : Submodule R M // N.FG }
h :
  ∀ (x : ↥(↑N : Submodule R M)),
    Eq (α := M)
      (((↑(equiv R M) :
                DirectLimit (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M)) (fgSystem R M) →ₗ[R] M) ∘ₗ
              of R { N : Submodule R M // N.FG } (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M))
                (fgSystem R M) N :
            (a : ↥(↑N : Submodule R M)) → M)
          x :
        M)
      (((↑N : Submodule R M).subtype : (a : ↥(↑N : Submodule R M)) → M) x : M)
⊢ (↑(equiv R M) :
        DirectLimit (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M)) (fgSystem R M) →ₗ[R] M) ∘ₗ
      of R { N : Submodule R M // N.FG } (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M))
        (fgSystem R M) N =
    (↑N : Submodule R M).subtype

Tactic:
ext
-- Module: Mathlib.Algebra.Colimit.Finiteness
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq (Submodule R M)
N : { N : Submodule R M // N.FG }
x : ↥(↑N : Submodule R M)
⊢ Eq (α := M)
    (((↑(equiv R M) :
              DirectLimit (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M)) (fgSystem R M) →ₗ[R] M) ∘ₗ
            of R { N : Submodule R M // N.FG } (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M))
              (fgSystem R M) N :
          (a : ↥(↑N : Submodule R M)) → M)
        x :
      M)
    (((↑N : Submodule R M).subtype : (a : ↥(↑N : Submodule R M)) → M) x : M)

Tactic:
simp [equiv]

Premises used: Module.fgSystem.equiv
-- 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 ι
s : R
i j : ι
h : i ≤ j
x : G i
⊢ Eqv (G := G) f
    (HSMul.hSMul (β := DirectSum ι G) s
      ((DirectSum.lof R ι G i : (a : G i) → DirectSum ι fun (i : ι) ↦ G i) x :
        DirectSum.{u_2, u_3} ι fun (i : ι) ↦ G i))
    (HSMul.hSMul (β := DirectSum ι G) s
      ((DirectSum.lof R ι G j : (a : G j) → DirectSum ι fun (i : ι) ↦ G i) ((f i j h : (a : G i) → G j) x) :
        DirectSum.{u_2, u_3} ι fun (i : ι) ↦ G i))

Tactic:
simpa only [← map_smul] using .of_map ..

Premises used: 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 ι
i : ι
x : G i
⊢ Eq (α := Quot (α := DirectSum ι G) (⇑(moduleCon f).toSetoid : DirectSum ι G → DirectSum ι G → Prop))
    (Quot.mk (⇑(moduleCon f).toSetoid : DirectSum ι G → DirectSum ι G → Prop)
        ((DirectSum.of G i : (a : G i) → DirectSum ι fun (i : ι) ↦ G i) x) :
      Quot (α := DirectSum ι G) (⇑(moduleCon f).toSetoid : DirectSum ι G → DirectSum ι G → Prop))
    ((of R ι G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)

Tactic:
rfl

Premises used: 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 ι
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:
(AddCon.eq _).mpr <| .symm <| .of _ _ (.of_map _ _)

Premises used: Iff.mpr, AddCon.eq, Module.DirectLimit.Eqv.of_map, AddConGen.Rel.of, AddConGen.Rel.symm, Module.DirectLimit, AddCon.toQuotient, ModuleCon.Quotient
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
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 : DirectLimit G f
⊢ Nonempty ι

Tactic:
infer_instance
-- 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 ι
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
rw : HAdd.hAdd (α := DirectLimit G f) (Quotient.mk'' p) (Quotient.mk'' q) = Quotient.mk'' (p + q)
⊢ 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)

Tactic:
rw [map_add, of_f, of_f, ihx, ihy]

Premises used: Module.DirectLimit.of_f, map_add
-- 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 ι
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
⊢ HAdd.hAdd (α := DirectLimit G f) (Quotient.mk'' p) (Quotient.mk'' q) = Quotient.mk'' (p + q)

Tactic:
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 : 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
rw₁ rw₂ : z = z
⊢ (of R ι G f k : (a : G k) → DirectLimit G f) ((f i k hik : (a : G i) → G k) x) = z

Tactic:
rw [of_f, hx]

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 ι
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
rw₁ rw₂ : w = w
⊢ (of R ι G f k : (a : G k) → DirectLimit G f) ((f j k hjk : (a : G j) → G k) y) = w

Tactic:
rw [of_f, hy]

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 ι
inst_5 : Nonempty ι
inst_6 : IsDirectedOrder ι
C : DirectLimit G f → Prop
z : DirectLimit G f
ih : ∀ (i : ι) (x : G i), C ((of R ι G f i : (a : G i) → DirectLimit G f) x)
⊢ C z

Tactic:
let ⟨i, x, h⟩ := exists_of z
  h ▸ ih i x

Premises used: _private.0.Module.DirectLimit.exists_of₂.match_1, Eq.rec, 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)
x x_1 : DirectSum ι G
h : Eqv (G := G) f x x_1
i j : ι
h_1 : i ≤ j
x_2 : G i
⊢ (AddCon.ker (F := DirectSum ι G →+ P) (↑(DirectSum.toModule R ι (M := G) P g) : DirectSum ι G →+ P) :
      (a : DirectSum ι G) → DirectSum ι G → Prop)
    ((DirectSum.lof R ι G i : (a : G i) → DirectSum ι fun (i : ι) ↦ G i) x_2 : DirectSum.{u_2, u_3} ι fun (i : ι) ↦ G i)
    ((DirectSum.lof R ι G j : (a : G j) → DirectSum ι fun (i : ι) ↦ G i) ((f i j h_1 : (a : G i) → G j) x_2))

Tactic:
simpa using (Hg _ _ _ _).symm

Premises used: Eq.symm
-- 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:
map_smul (DirectSum.toModule R ι P g) r x

Premises used: Quotient.liftOn', AddCon.liftOn, DirectSum.toModule, map_smul, Trunc.lift