awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Colimit.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : Preorder ι
G : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (G i)
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)
⊢ Eq (α := DirectLimit G' f' →+ DirectLimit G' f')
    (AddMonoidHom.comp (map (G := G) (G' := G') (fun (x : ι) ↦ (↑(e x) : G x →+ G' x)) he)
      (map (G := G') (G' := G) (fun (i : ι) ↦ (↑(e i).symm : G' i →+ G i)) ⋯))
    (AddMonoidHom.id (DirectLimit G' f'))

Tactic:
simp [map_comp]

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

Tactic:
map_apply_of _ he _

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, AddCommGroup.DirectLimit.map_apply_of, List.foldr, Finset.sum, Trunc.lift
-- Module: Mathlib.Algebra.Colimit.Module
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
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 : ι
g : G' i
⊢ Eq (α := DirectLimit G f)
    ((AddEquiv.symm (congr (G := G) (G' := G') e he) : (a : DirectLimit G' f') → DirectLimit G f)
        ((of G' f' i : (a : G' i) → DirectLimit G' f') g) :
      DirectLimit G f)
    ((of G f i : (a : G i) → DirectLimit G f) (((e i).symm : (a : G' i) → G i) g) : DirectLimit G f)

Tactic:
simp only [congr, AddMonoidHom.toAddEquiv_symm_apply, map_apply_of, AddMonoidHom.coe_coe]

Premises used: AddMonoidHom.toAddEquiv_symm_apply, AddMonoidHom.coe_coe, AddCommGroup.DirectLimit.congr, AddCommGroup.DirectLimit.map_apply_of
-- Module: Mathlib.Algebra.Colimit.Ring
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
i j : ι
hij : i ≤ j
x : G i
⊢ Eq (α := DirectLimit G f) ((of G f j : (a : G j) → DirectLimit G f) (f i j hij x) : DirectLimit G f)
    ((of G f i : (a : G i) → DirectLimit G f) x : DirectLimit G f)

Tactic:
Ideal.Quotient.eq.2 <| subset_span <| Or.inl ⟨i, j, hij, x, rfl⟩

Premises used: Iff.mpr, Submodule.Quotient.mk, Ideal.Quotient.eq, Ring.DirectLimit, Exists.intro, Or.inl, Submodule.subset_span, rfl
-- Module: Mathlib.Algebra.Colimit.Ring
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)
simp : Eq (α := DirectLimit G f) (-1) (-1)
⊢ 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))

Tactic:
simp
-- Module: Mathlib.Algebra.Colimit.Ring
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) (-1) (-1)

Tactic:
rfl
-- Module: Mathlib.Algebra.Colimit.Ring
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])
rw₁ 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])
⊢ 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)

Tactic:
rw [map_C, h]

Premises used: Polynomial.map_C
-- Module: Mathlib.Algebra.Colimit.Ring
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
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₂)
⊢ 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₂

Tactic:
rw [Polynomial.map_add, map_map, map_map, ← ih₁, ← ih₂]

Premises used: Polynomial.map_add, Polynomial.map_map
-- Module: Mathlib.Algebra.Colimit.Ring
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₁)
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₂)
⊢ 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:
congr 2
-- Module: Mathlib.Algebra.Colimit.Ring
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 :
  ∀ (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))
⊢ 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:
ext x
-- Module: Mathlib.Algebra.Colimit.Ring
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 :
  ∀ (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))
⊢ 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:
ext x
-- Module: Mathlib.Algebra.Colimit.Ring
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 ι
C : DirectLimit G f → Prop
z : DirectLimit G f
ih : ∀ (i : ι) (x : G i), C ((of G f i : (a : G i) → DirectLimit G f) x)
⊢ C z

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

Premises used: Eq.rec, _private.0.Ring.DirectLimit.induction_on.match_1, Ring.DirectLimit.exists_of
-- Module: Mathlib.Algebra.Colimit.Ring
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)
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)))
⊢ 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)))
      ⊥)

Tactic:
rw [Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.Algebra.Colimit.Ring
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
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)
⊢ 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)))

Tactic:
rw [SetLike.mem_coe, Ideal.mem_comap, mem_bot]

Premises used: Submodule.mem_bot, SetLike.mem_coe, Ideal.mem_comap
-- Module: Mathlib.Algebra.Colimit.Ring
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)
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:
simp only [map_sub, lift_of, Hg, map_one, map_add, map_mul,
          (g i).map_one, (g i).map_add, (g i).map_mul, sub_self]

Premises used: map_sub, sub_self, FreeCommRing.lift_of, RingHom.map_one, map_add, map_mul, map_one, RingHom.map_mul, RingHom.map_add