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
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 : Nonempty ι
inst_6 : CommSemiring R
inst_7 : (i : ι) → Semiring (G i)
inst_8 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
i : ι
x : G i
dsimp :
  HMul.hMul (α := DirectLimit G (T := T) f)
      (map₀ (F := G) (T := T) f fun (i : ι) ↦ (algebraMap R (G i) : (a : R) → G i) r)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      (map₀ (F := G) (T := T) f fun (i : ι) ↦ (algebraMap R (G i) : (a : R) → G i) r)
⊢ HMul.hMul (α := DirectLimit G (T := T) f) (β := DirectLimit G (T := T) f)
      (((RingHom.comp (map₀RingHom (G := G) (T := T) f) (algebraMap R ((i : ι) → G i)) :
              R →+* DirectLimit G (T := T) f) :
            (a : R) → DirectLimit G f)
          r :
        DirectLimit G (T := T) f)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) (β := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      (((RingHom.comp (map₀RingHom (G := G) (T := T) f) (algebraMap R ((i : ι) → G i)) :
              R →+* DirectLimit G (T := T) f) :
            (a : R) → DirectLimit G f)
          r :
        DirectLimit G (T := T) f)

Tactic:
dsimp [Pi.algebraMap_def]

Premises used: Pi.algebraMap_def
-- 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 : Nonempty ι
inst_6 : CommSemiring R
inst_7 : (i : ι) → Semiring (G i)
inst_8 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
i : ι
x : G i
rw :
  HMul.hMul (α := DirectLimit G (T := T) f)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧
rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) ((algebraMap R (G i) : (a : R) → G i) r : G i) x)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧
rw₂ :
  Eq (α := DirectLimit G (T := T) f)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) ((algebraMap R (G i) : (a : R) → G i) r : G i) x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (β := G i) x ((algebraMap R (G i) : (a : R) → G i) r : G i))⟧
rw₃ rw₄ :
  Eq (α := DirectLimit G (T := T) f)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (β := G i) x ((algebraMap R (G i) : (a : R) → G i) r : G i))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (β := G i) x ((algebraMap R (G i) : (a : R) → G i) r : G i))⟧
⊢ HMul.hMul (α := DirectLimit G (T := T) f)
      (map₀ (F := G) (T := T) f fun (i : ι) ↦ (algebraMap R (G i) : (a : R) → G i) r)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      (map₀ (F := G) (T := T) f fun (i : ι) ↦ (algebraMap R (G i) : (a : R) → G i) r)

Tactic:
rw [map₀_algebraMap i, mul_def, mul_def, Algebra.commutes]

Premises used: DirectLimit.mul_def, DirectLimit.map₀_algebraMap, Algebra.commutes
-- 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 : Nonempty ι
inst_6 : CommSemiring R
inst_7 : (i : ι) → Semiring (G i)
inst_8 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
i : ι
x : G i
dsimp :
  HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f)
      (map₀ (F := G) (T := T) f fun (i : ι) ↦ (algebraMap R (G i) : (a : R) → G i) r)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
⊢ HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) (β := DirectLimit G (T := T) f)
      (((RingHom.comp (map₀RingHom (G := G) (T := T) f) (algebraMap R ((i : ι) → G i)) :
              R →+* DirectLimit G (T := T) f) :
            (a : R) → DirectLimit G f)
          r :
        DirectLimit G (T := T) f)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧

Tactic:
dsimp [Pi.algebraMap_def]

Premises used: Pi.algebraMap_def
-- 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 : Nonempty ι
inst_6 : CommSemiring R
inst_7 : (i : ι) → Semiring (G i)
inst_8 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
r : R
i : ι
x : G i
rw :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f)
      (map₀ (F := G) (T := T) f fun (i : ι) ↦ (algebraMap R (G i) : (a : R) → G i) r)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
rw₂ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (r • x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) ((algebraMap R (G i) : (a : R) → G i) r : G i) x)⟧
rw₃ rw₄ :
  Eq (α := DirectLimit G (T := T) f)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) ((algebraMap R (G i) : (a : R) → G i) r : G i) x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HMul.hMul (α := G i) ((algebraMap R (G i) : (a : R) → G i) r : G i) x)⟧
⊢ HSMul.hSMul (β := DirectLimit G (T := T) f) r ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f)
      (map₀ (F := G) (T := T) f fun (i : ι) ↦ (algebraMap R (G i) : (a : R) → G i) r)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧

Tactic:
rw [smul_def, map₀_algebraMap i, mul_def, Algebra.smul_def']

Premises used: Algebra.smul_def', DirectLimit.mul_def, DirectLimit.map₀_algebraMap, DirectLimit.smul_def
-- 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 : Nonempty ι
inst_5 : CommSemiring R
inst_6 : (i : ι) → Semiring (G i)
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)
i : ι
r : R
⊢ Eq (α := DirectLimit G (T := T) f)
    ((algebraMap R (DirectLimit G (T := T) f) : (a : R) → DirectLimit G f) r : DirectLimit G (T := T) f)
    (⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧ :
      Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))

Tactic:
map₀_algebraMap i r

Premises used: DirectLimit.map₀_algebraMap, DirectLimit.map₀
-- 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 : Semiring R
inst_5 : (i : ι) → AddCommMonoid (G i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{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 R ι G (T := T) f j : (a : G j) → DirectLimit G f) ((f i j hij : (a : G i) → G j) x) : DirectLimit G (T := T) f)
    ((of R ι G (T := T) f i : (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
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 : Semiring R
inst_5 : (i : ι) → AddCommMonoid (G i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : AddCommMonoid P
inst_10 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.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 : ι
⊢ lift R ι G (T := T) f g Hg ∘ₗ of R ι G (T := T) f i = g i

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 : Semiring R
inst_5 : (i : ι) → AddCommMonoid (G i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : AddCommMonoid P
inst_10 : Module R P
g : (i : ι) → LinearMap.{u_1, u_1, u_3, u_7} (RingHom.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 R ι G (T := T) f g Hg : (a : DirectLimit G f) → P)
        ((of R ι G (T := T) f i : (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 : Semiring R
inst_5 : (i : ι) → AddCommMonoid (G i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : AddCommMonoid P
inst_10 : Module R P
g₁ g₂ : DirectLimit G (T := T) f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G (T := T) f i = g₂ ∘ₗ of R ι 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 : Semiring R
inst_5 : (i : ι) → AddCommMonoid (G i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : AddCommMonoid P
inst_10 : Module R P
g₁ g₂ : DirectLimit G (T := T) f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G (T := T) f i = g₂ ∘ₗ of R ι 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 : Semiring R
inst_5 : (i : ι) → AddCommMonoid (G i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : AddCommMonoid P
inst_10 : Module R P
g₁ g₂ : DirectLimit G (T := T) f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G (T := T) f i = g₂ ∘ₗ of R ι 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 : Semiring R
inst_5 : (i : ι) → AddCommMonoid (G i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : AddCommMonoid P
inst_10 : Module R P
g₁ g₂ : DirectLimit G (T := T) f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G (T := T) f i = g₂ ∘ₗ of R ι 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:
ι : 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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := DirectLimit G (T := T) f)
    ((of G (T := T) f j : (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 : (a : G i) → DirectLimit G f) x : DirectLimit G (T := T) f)

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : 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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonUnitalNonAssocSemiring P
g : (i : ι) → NonUnitalRingHom.{u_3, u_7} (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 : ι
⊢ NonUnitalRingHom.comp (β := DirectLimit G (T := T) f) (lift G (T := T) f P g Hg) (of G (T := T) f i) = g i

Tactic:
rfl

Premises used: DirectLimit.lift, rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : 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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonUnitalNonAssocSemiring P
g : (i : ι) → NonUnitalRingHom.{u_3, u_7} (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 : (a : DirectLimit G f) → P)
        ((of G (T := T) f i : (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:
ι : 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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G (T := T) f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
a :
  ∀ (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:
ι : 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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G (T := T) f →ₙ+* 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
a :
  ∀ (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:
ι : 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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G (T := T) f →ₙ+* 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:
ι : 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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G (T := T) f →ₙ+* 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:
ι : 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 : (i : ι) → NonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := DirectLimit G (T := T) f)
    ((of G (T := T) f j : (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 : (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