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)
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)
rw₁ : (g₂ j).comp ((f' i j h).comp (g₁ i)) = (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]
-- 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)
rw₁ : (g₂ j).comp ((f' i j h).comp (g₁ i)) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
rw₂ : ((g₂ j).comp (f' i j h)).comp (g₁ i) = (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₃ : ((f'' i j h).comp (g₂ i)).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]
-- 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)
rw₁ : (g₂ j).comp ((f' i j h).comp (g₁ i)) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
rw₂ : ((g₂ j).comp (f' i j h)).comp (g₁ i) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
rw₃ : ((f'' i j h).comp (g₂ i)).comp (g₁ i) = (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₄ : (f'' i j h).comp ((g₂ i).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]
-- 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 ι
G' : ι → Type u_5
inst_3 : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst_4 : (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)
⊢ Eq (α := DirectLimit G f →+ DirectLimit G'' f'')
    (AddMonoidHom.comp (map (G := G') (G' := G'') g₂ hg₂) (map (G := G) (G' := G') g₁ hg₁))
    (map (G := G) (G' := G'') (fun (i : ι) ↦ (g₂ i).comp (g₁ i)) ⋯)
have h : ∀ (i : ι) (x : G i),
  Eq (α := DirectLimit G'' f'')
    ((AddMonoidHom.comp (AddMonoidHom.comp (map (G := G') (G' := G'') g₂ hg₂) (map (G := G) (G' := G') g₁ hg₁))
            (of G f i) :
          (a : G i) → DirectLimit G'' f'')
        x :
      DirectLimit G'' f'')
    ((AddMonoidHom.comp (map (G := G) (G' := G'') (fun (i : ι) ↦ (g₂ i).comp (g₁ i)) sorry) (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 : (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
e : (i : ι) → AddEquiv.{u_3, u_5} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) = (f' i j h).comp (↑(e i) : G i →+ G' i)
i j : ι
h : i ≤ j
x : G' i
⊢ Eq.{u_3 + 1} (α := G j)
    ((AddMonoidHom.comp
            ((fun (i : ι) ↦
                ((↑(e i).symm : AddMonoidHom.{u_5, u_3} (G' i) (G i)) : AddMonoidHom.{u_5, u_3} (G' i) (G i)))
              j)
            (f' i j h) :
          (a : G' i) → G j)
        x :
      G j)
    (((f i j h).comp
            ((fun (i : ι) ↦
                ((↑(e i).symm : AddMonoidHom.{u_5, u_3} (G' i) (G i)) : AddMonoidHom.{u_5, u_3} (G' i) (G i)))
              i) :
          (a : G' i) → G j)
        x :
      G j)
have eq1 : Eq.{u_5 + 1} (α := G' j)
  ((AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) : (a : G i) → G' j) (((e i).symm : (a : G' i) → G i) x) : G' j)
  ((((f' i j h).comp (↑(e i) : G i →+ G' i) : AddMonoidHom.{u_3, u_5} (G i) (G' j)) : (a : G i) → G' j)
      (((e i).symm : (a : G' i) → G i) x) :
    G' j)
Tactic: have eq1 := DFunLike.congr_fun (he i j h) ((e i).symm x)
-- 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
e : (i : ι) → AddEquiv.{u_3, u_5} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) = (f' i j h).comp (↑(e i) : G i →+ G' i)
i j : ι
h : i ≤ j
x : G' i
eq1 :
  Eq.{u_5 + 1} (α := G' j)
    ((AddMonoidHom.comp (e j).toAddMonoidHom (f i j h) : (a : G i) → G' j) (((e i).symm : (a : G' i) → G i) x) : G' j)
    ((((f' i j h).comp (↑(e i) : G i →+ G' i) : AddMonoidHom.{u_3, u_5} (G i) (G' j)) : (a : G i) → G' j)
        (((e i).symm : (a : G' i) → G i) x) :
      G' j)
⊢ Eq.{u_3 + 1} (α := G j)
    ((AddMonoidHom.comp
            ((fun (i : ι) ↦
                ((↑(e i).symm : AddMonoidHom.{u_5, u_3} (G' i) (G i)) : AddMonoidHom.{u_5, u_3} (G' i) (G i)))
              j)
            (f' i j h) :
          (a : G' i) → G j)
        x :
      G j)
    (((f i j h).comp
            ((fun (i : ι) ↦
                ((↑(e i).symm : AddMonoidHom.{u_5, u_3} (G' i) (G i)) : AddMonoidHom.{u_5, u_3} (G' i) (G i)))
              i) :
          (a : G' i) → G j)
        x :
      G j)
have simp : ∀
  (eq1 :
    Eq.{u_5 + 1} (α := G' j)
      ((e j : (a : G j) → G' j) ((f i j h : (a : G i) → G j) (((e i).symm : (a : G' i) → G i) x : G i)) : G' j)
      ((f' i j h : (a : G' i) → G' j) x : G' j)),
  Eq.{u_3 + 1} (α := G j) (((e j).symm : (a : G' j) → G j) ((f' i j h : (a : G' i) → G' j) x) : G j)
    ((f i j h : (a : G i) → G j) (((e i).symm : (a : G' i) → G i) x : G i) : G j)
Tactic: simp only [AddMonoidHom.coe_comp, AddEquiv.coe_toAddMonoidHom, Function.comp_apply,
        AddMonoidHom.coe_coe, AddEquiv.apply_symm_apply] at eq1 ⊢
Cleared hypotheses: eq1
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
⊢ Eq (α := DirectLimit G f) ((of G f (Classical.arbitrary ι) : (a : G (Classical.arbitrary ι)) → DirectLimit G f) (-1))
    ((Ideal.Quotient.mk
          (Ideal.span
            {a : FreeCommRing ((i : ι) × G i) |
              (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
                  FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j H x)) -
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) =
                    a) ∨
                (∃ (i : ι),
                    HSub.hSub (α := FreeCommRing ((i : ι) × G i))
                        (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1 =
                      a) ∨
                  (∃ (i : ι) (x : G i) (y : G i),
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x + y)) -
                          (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
                            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) =
                        a) ∨
                    ∃ (i : ι) (x : G i) (y : G i),
                      FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)) -
                          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
                            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y) =
                        a}) :
        (a : FreeCommRing ((i : ι) × G i)) →
          FreeCommRing ((i : ι) × G i) ⧸
            Ideal.span
              {a : FreeCommRing ((i : ι) × G i) |
                (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i), FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                  (∃ (i : ι), FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                    (∃ (i : ι) (x : G i) (y : G i),
                        FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                      ∃ (i : ι) (x : G i) (y : G i),
                        FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})
      (-1))
have simp : Eq (α := DirectLimit G f) (-1) (-1)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
q : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
z : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
i : ι
x : G i
h :
  (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i :
        (a : G i) → DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
      x =
    z
⊢ Eq (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
      ((C : (a : G i) → (G i)[X]) x))
    ((C :
        (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
          (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      z)
have rw : Eq (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
  ((C :
        (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
          (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      ((of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i :
          (a : G i) → DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
        x) :
    (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
  ((C :
        (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
          (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      z :
    (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
Tactic: rw [map_C, h]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
q : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
z : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
i : ι
x : G i
h :
  (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i :
        (a : G i) → DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
      x =
    z
rw :
  Eq (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    ((C :
          (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
            (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
        ((of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i :
            (a : G i) → DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
          x) :
      (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    ((C :
          (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
            (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
        z :
      (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
⊢ Eq (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
      ((C : (a : G i) → (G i)[X]) x))
    ((C :
        (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
          (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      z)
have rw₁ : Eq (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
  ((C :
        (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
          (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      z :
    (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
  ((C :
        (a : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) →
          (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      z :
    (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
Tactic: rw [map_C, h]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
q : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
q₁ q₂ : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
h :
  ∃ (i : ι) (p : (G i)[X]), Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) p = q₁
h_1 :
  ∃ (i : ι) (p : (G i)[X]), Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
      (Polynomial.map (f' i₁ i h1) p₁ + Polynomial.map (f' i₂ i h2) p₂) =
    q₁ + q₂
have rw : HAdd.hAdd (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    (Polynomial.map (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₁ i h1))
      p₁)
    (Polynomial.map (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₂ i h2))
      p₂) =
  HAdd.hAdd (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
    (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₁) p₁)
    (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₂) p₂)
Tactic: rw [Polynomial.map_add, map_map, map_map, ← ih₁, ← ih₂]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
q : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
q₁ q₂ : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
h :
  ∃ (i : ι) (p : (G i)[X]), Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) p = q₁
h_1 :
  ∃ (i : ι) (p : (G i)[X]), Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ HAdd.hAdd (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (Polynomial.map (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₁ i h1))
        p₁)
      (Polynomial.map (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₂ i h2))
        p₂) =
    HAdd.hAdd (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₁) p₁)
      (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₂) p₂)
have e_a : Eq (α := G i₁ →+* DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
  (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₁ i h1))
  (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₁)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
q : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
q₁ q₂ : (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]
h :
  ∃ (i : ι) (p : (G i)[X]), Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) p = q₁
h_1 :
  ∃ (i : ι) (p : (G i)[X]), Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
e_a :
  Eq (α := G i₁ →+* DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
    (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₁ i h1))
    (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₁)
⊢ HAdd.hAdd (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (Polynomial.map (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₁ i h1))
        p₁)
      (Polynomial.map (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₂ i h2))
        p₂) =
    HAdd.hAdd (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X])
      (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₁) p₁)
      (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₂) p₂)
have e_a₁ : Eq (α := G i₂ →+* DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))
  (RingHom.comp (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i) (f' i₂ i h2))
  (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i₂)
Tactic: congr 2