awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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₁)
have e_a : ∀ (x : G i₁),
  Eq (α := 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) :
          (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))
    ((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))
Tactic: ext x
-- 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
⊢ 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₂)
have e_a : ∀ (x : G i₂),
  Eq (α := 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) :
          (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))
    ((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))
Tactic: ext x
-- 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]
n : ℕ
z : DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
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 =
      HMul.hMul (α := (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])
        (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X n)
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
⊢ Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
      (HMul.hMul (α := (G i)[X]) ((C : (a : G i) → (G i)[X]) x : (G i)[X]) (HPow.hPow (α := (G i)[X]) X (n + 1))) =
    HMul.hMul (α := (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])
      (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1))
have rw : HMul.hMul (α := (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))
    (Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)) i)
      (HPow.hPow (α := (G i)[X]) X (n + 1))) =
  HMul.hMul (α := (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])
    (HPow.hPow (α := (DirectLimit G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j))[X]) X (n + 1))
Tactic: rw [Polynomial.map_mul, map_C, h, Polynomial.map_pow, map_X]
-- 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
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
⊢ LE.le (α := Ideal (FreeCommRing ((i : ι) × G i)))
    (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})
    (Ideal.comap (F := FreeCommRing ((i : ι) × G i) →+* P)
      ((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
        (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
      ⊥)
have rw : {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} ⊆
  (↑(Ideal.comap (F := FreeCommRing ((i : ι) × G i) →+* P)
        ((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
        ⊥) :
    Set (FreeCommRing ((i : ι) × G i)))
Tactic: rw [Ideal.span_le]
-- 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
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
x : FreeCommRing ((i : ι) × G i)
hx :
  Membership.mem (γ := Set (FreeCommRing ((i : ι) × G i)))
    {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}
    x
⊢ x ∈
    (↑(Ideal.comap (F := FreeCommRing ((i : ι) × G i) →+* P)
          ((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)))
          ⊥) :
      Set (FreeCommRing ((i : ι) × G i)))
have rw : Eq.{u_3 + 1} (α := P)
  (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
          (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
        (a : FreeCommRing ((i : ι) × G i)) → P)
      x :
    P)
  (0 : P)
Tactic: rw [SetLike.mem_coe, Ideal.mem_comap, mem_bot]
-- 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
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
x : FreeCommRing ((i : ι) × G i)
hx :
  Membership.mem (γ := Set (FreeCommRing ((i : ι) × G i)))
    {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}
    x
⊢ Eq.{u_3 + 1} (α := P)
    (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
          (a : FreeCommRing ((i : ι) × G i)) → P)
        x :
      P)
    (0 : P)
have inl : ∀ (i j : ι) (hij : i ≤ j) (x : G i),
  Eq.{u_3 + 1} (α := P)
    (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
          (a : FreeCommRing ((i : ι) × G i)) → P)
        (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j hij x)) -
          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x)) :
      P)
    (0 : P)
Tactic: rcases hx with (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩)
Cleared hypotheses: x, hx
-- 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
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
x : FreeCommRing ((i : ι) × G i)
hx :
  Membership.mem (γ := Set (FreeCommRing ((i : ι) × G i)))
    {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}
    x
inl :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P)
      (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
              (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
            (a : FreeCommRing ((i : ι) × G i)) → P)
          (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) j (f i j hij x)) -
            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x)) :
        P)
      (0 : P)
⊢ Eq.{u_3 + 1} (α := P)
    (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
          (a : FreeCommRing ((i : ι) × G i)) → P)
        x :
      P)
    (0 : P)
have inr : ∀ (i : ι),
  Eq.{u_3 + 1} (α := P)
    (((FreeCommRing.lift : (a : (i : ι) × G i → P) → FreeCommRing ((i : ι) × G i) →+* P) fun (x : (i : ι) × G i) ↦
            (g (x.fst (β := fun (i : ι) ↦ G i)) : (a : G x.fst) → P) (x.snd (β := fun (i : ι) ↦ G i)) :
          (a : FreeCommRing ((i : ι) × G i)) → P)
        (HSub.hSub (α := FreeCommRing ((i : ι) × G i)) (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) 1) :
      P)
    (0 : P)
Tactic: rcases hx with (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩)
Cleared hypotheses: x, hx
-- 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
P : Type u_3
inst_2 : CommRing P
F : DirectLimit G f →+* P
⊢ lift G f P (fun (i : ι) ↦ F.comp (of G f i)) ⋯ = F
have h : ∀ (i : ι) (x : G i),
  Eq.{u_3 + 1} (α := P)
    ((RingHom.comp (lift G f P (fun (i : ι) ↦ F.comp (of G f i)) sorry) (of G f i) : (a : G i) → P) x : P)
    ((F.comp (of G f i) : (a : G i) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Colimit.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
⊢ Eq (α := DirectLimit G f →+* DirectLimit G f) (lift G f (DirectLimit G f) (of G f) ⋯) (RingHom.id (DirectLimit G f))
have h : ∀ (i : ι) (x : G i),
  Eq (α := DirectLimit G f)
    ((RingHom.comp (lift G f (DirectLimit G f) (of G f) sorry) (of G f i) : (a : G i) → DirectLimit G f) x :
      DirectLimit G f)
    ((RingHom.comp (RingHom.id (DirectLimit G f)) (of G f i) : (a : G i) → DirectLimit G f) x : DirectLimit G f)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Colimit.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
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective.{u_2 + 1, u_3 + 1} (α := G i) (β := P) (⇑(g i) : (a : G i) → P)
⊢ Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift G f P g Hg) : (a : DirectLimit G f) → P)
have simp_rw : ∀ (injective : ∀ (i : ι) (a : G i), Eq.{u_3 + 1} (α := P) ((g i : (a : G i) → P) a : P) (0 : P) → a = 0)
  (a : DirectLimit G f), Eq.{u_3 + 1} (α := P) ((lift G f P g Hg : (a : DirectLimit G f) → P) a : P) (0 : P) → a = 0
Tactic: simp_rw [injective_iff_map_eq_zero] at injective ⊢
Cleared hypotheses: injective
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (hypothesis)
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
P : Type u_3
inst_2 : CommRing P
g_1 : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g_1 j : (a : G j) → P) (f i j hij x) : P) ((g_1 i : (a : G i) → P) x : P)
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), Eq.{u_3 + 1} (α := P) ((g_1 i : (a : G i) → P) a : P) (0 : P) → a = 0
i : ι
g : G i
hz :
  Eq.{u_3 + 1} (α := P)
    ((lift G f P g_1 Hg : (a : DirectLimit G f) → P) ((of G f i : (a : G i) → DirectLimit G f) g : DirectLimit G f) : P)
    (0 : P)
⊢ Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) g : DirectLimit G f) (0 : DirectLimit G f)
have hz₁ : Eq.{u_3 + 1} (α := P) ((g_1 i : (a : G i) → P) g : P) (0 : P)
Tactic: rw [lift_of] at hz
Cleared hypotheses: hz
-- 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
P : Type u_3
inst_2 : CommRing P
g_1 : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g_1 j : (a : G j) → P) (f i j hij x) : P) ((g_1 i : (a : G i) → P) x : P)
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), Eq.{u_3 + 1} (α := P) ((g_1 i : (a : G i) → P) a : P) (0 : P) → a = 0
i : ι
g : G i
hz : Eq.{u_3 + 1} (α := P) ((g_1 i : (a : G i) → P) g : P) (0 : P)
⊢ Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) g : DirectLimit G f) (0 : DirectLimit G f)
have ih : Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) 0) 0
Tactic: rw [injective _ g hz, map_zero]
-- 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
P : Type u_3
inst_2 : CommRing P
g_1 : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g_1 j : (a : G j) → P) (f i j hij x) : P) ((g_1 i : (a : G i) → P) x : P)
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), Eq.{u_3 + 1} (α := P) ((g_1 i : (a : G i) → P) a : P) (0 : P) → a = 0
i : ι
g : G i
hz : Eq.{u_3 + 1} (α := P) ((g_1 i : (a : G i) → P) g : P) (0 : P)
ih : Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) 0) 0
⊢ Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) g : DirectLimit G f) (0 : DirectLimit G f)
have ih₁ : Eq (α := DirectLimit G f) 0 0
Tactic: rw [injective _ g hz, map_zero]
-- 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
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), Eq.{u_3 + 1} (α := P) ((g i : (a : G i) → P) a : P) (0 : P) → a = 0
z : DirectLimit G f
hz : Eq.{u_3 + 1} (α := P) ((lift G f P g Hg : (a : DirectLimit G f) → P) z : P) (0 : P)
⊢ z = 0
have ih : ∀ (i : ι) (g_1 : G i)
  (hz :
    Eq.{u_3 + 1} (α := P)
      ((lift G f P g Hg : (a : DirectLimit G f) → P) ((of G f i : (a : G i) → DirectLimit G f) g_1 : DirectLimit G f) :
        P)
      (0 : P)),
  Eq (α := DirectLimit G f) ((of G f i : (a : G i) → DirectLimit G f) g_1 : DirectLimit G f) (0 : DirectLimit G f)
Tactic: induction z using DirectLimit.induction_on with
  | ih _ g => rw [lift_of] at hz; rw [injective _ g hz, map_zero]
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (hypothesis)
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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
i : ι
x : G i
hix :
  Eq (α := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
    ((of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) i :
          (a : G i) → DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
        x :
      DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
    (0 : DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
⊢ ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f' i j hij : (a : G i) → G j) x : G j) (0 : G j)
have this : Nonempty ι
Tactic: have := Nonempty.intro i