awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
⊢ 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:
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
-- 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 : ι
x y : 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) i (x + y)) -
          (FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) +
            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y))) :
      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
-- 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 : ι
x y : 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) i (x * y)) -
          FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i x) *
            FreeCommRing.of (Sigma.mk (β := fun (i : ι) ↦ G i) i y)) :
      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
-- 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 : ι
x : G i
⊢ 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) x : DirectLimit G f) : P)
    ((g i : (a : G i) → P) x : P)

Tactic:
FreeCommRing.lift_of _ _

Premises used: Quotient.liftOn', AddCon.liftOn, FreeCommRing.lift_of, FreeGroup.Lift.aux, Con.liftOn, List.foldr, List.prod
-- 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₁ g₂ : DirectLimit G f →+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
Ideal.Quotient.ringHom_ext <| FreeCommRing.hom_ext fun ⟨i, x⟩ => congr($(h i) x)

Premises used: HMul.hMul, Ideal.Quotient.ringHom_ext, FreeCommRing.hom_ext, congrArg, Ideal.Quotient.mk, setOf, HSub.hSub, FreeCommRing.of, Exists, id, RingHom.comp, HAdd.hAdd, Ring.DirectLimit, Ideal.span, Or, Sigma.mk, _private.0.Ring.DirectLimit.exists_of.match_1, OfNat.ofNat, Eq, DFunLike.coe
-- 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)
F : DirectLimit G f →+* P
i j : ι
hij : i ≤ j
x : G i
⊢ Eq.{u_3 + 1} (α := P) (((fun (i : ι) ↦ F.comp (of G f i)) j : (a : G j) → P) (f i j hij x) : P)
    (((fun (i : ι) ↦ F.comp (of G f i)) i : (a : G i) → P) x : P)

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
P : Type u_3
inst_2 : CommRing P
F : DirectLimit G f →+* P
h :
  ∀ (i : ι) (x : G i),
    Eq.{u_3 + 1} (α := P)
      ((RingHom.comp (lift G f P (fun (i : ι) ↦ F.comp (of G f i)) ⋯) (of G f i) : (a : G i) → P) x : P)
      ((F.comp (of G f i) : (a : G i) → P) x : P)
⊢ lift G f P (fun (i : ι) ↦ F.comp (of G f i)) ⋯ = F

Tactic:
ext
-- 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
F : DirectLimit G f →+* P
i : ι
x : G i
⊢ Eq.{u_3 + 1} (α := P)
    ((RingHom.comp (lift G f P (fun (i : ι) ↦ F.comp (of G f i)) ⋯) (of G f i) : (a : G i) → P) x : P)
    ((F.comp (of G f i) : (a : G i) → P) x : P)

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
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 (α := 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:
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
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G f)
      ((RingHom.comp (lift G f (DirectLimit G f) (of G f) ⋯) (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)
⊢ Eq (α := DirectLimit G f →+* DirectLimit G f) (lift G f (DirectLimit G f) (of G f) ⋯) (RingHom.id (DirectLimit G f))

Tactic:
ext
-- 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 : ι
x : G i
⊢ Eq (α := DirectLimit G f)
    ((RingHom.comp (lift G f (DirectLimit G f) (of G f) ⋯) (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:
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
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)
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
⊢ Function.Injective (α := DirectLimit G f) (β := P) (⇑(lift G f P g Hg) : (a : DirectLimit G f) → P)

Tactic:
simp_rw [injective_iff_map_eq_zero] at injective ⊢

Premises used: injective_iff_map_eq_zero
-- 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_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.{u_3 + 1} (α := P) ((g_1 i : (a : G i) → P) g : P) (0 : P)

Tactic:
rw [lift_of] at hz

Premises used: Ring.DirectLimit.lift_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_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
ih₁ ih₂ : Eq (α := 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)

Tactic:
rw [injective _ g hz, map_zero]

Premises used: map_zero
-- 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)
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)
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)
⊢ z = 0

Tactic:
induction z using DirectLimit.induction_on with
  | ih _ g => rw [lift_of] at hz; rw [injective _ g hz, map_zero]

Premises used: map_zero, Ring.DirectLimit.lift_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)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
i : ι
x : G i
⊢ Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    (((@RingHom.comp _ (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') _ _
              (instNonAssocSemiringOfRingHomClass (G := G) (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j)) _
              (RingHom.comp (β := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
                (lift G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
                  (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
                  (Ring.of G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') ⋯)
                (Ring.lift G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f'
                  (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)) ⋯))
              (Ring.of G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f' i) :
            G i →+* _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') :
          (a : G i) → _root_.DirectLimit G f')
        x :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    (((RingHom.comp (RingHom.id (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f'))
              (Ring.of G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f' i) :
            G i →+* _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') :
          (a : G i) → _root_.DirectLimit G f')
        x :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')

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
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)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
i : ι
x : G i
⊢ Eq (α := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
    ((RingHom.comp (β := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
            (@RingHom.comp _ (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') _ _
              (instNonAssocSemiringOfRingHomClass (G := G) (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j)) _
              (Ring.lift G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f'
                (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)) ⋯)
              (lift G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
                (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
                (Ring.of G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') ⋯))
            (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))
    ((RingHom.comp (RingHom.id (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))

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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
i : ι
g : G i
⊢ Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    ((ringEquiv G f' :
          (a : DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) →
            _root_.DirectLimit G f')
        ((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))
          g) :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    (⟦Sigma.mk (β := fun (i : ι) ↦ G i) i g⟧ :
      Quotient (α := (i : ι) × G i) (DirectLimit.setoid (F := G) (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f'))

Tactic:
simp [ringEquiv]

Premises used: Ring.DirectLimit.ringEquiv
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
g : (i : ι) × G i
⊢ Eq (α := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
    ((RingEquiv.symm (ringEquiv G f') :
          (a : _root_.DirectLimit G f') →
            DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
        ⟦g⟧ :
      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)) (g.fst (β := fun (i : ι) ↦ G i)) :
          (a : G g.fst) → DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
        (g.snd (β := fun (i : ι) ↦ G i)) :
      DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))

Tactic:
rfl

Premises used: Submodule.Quotient.mk, DirectLimit.lift, 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 : 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))
⊢ Nonempty ι

Tactic:
have := Nonempty.intro i
-- 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 : 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))
this : Nonempty ι
⊢ Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    ((ringEquiv G f' :
          (a : DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) →
            _root_.DirectLimit G f')
        ((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) :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    ((ringEquiv G f' :
          (a : DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) →
            _root_.DirectLimit G f')
        0 :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')

Tactic:
apply_fun ringEquiv _ _ at hix

Premises used: Ring.DirectLimit.ringEquiv
-- 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 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
inst_3 : IsDirectedOrder ι
i : ι
x : G i
this : Nonempty ι
hix :
  Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    ((ringEquiv G f' :
          (a : DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) →
            _root_.DirectLimit G f')
        ((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) :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    ((ringEquiv G f' :
          (a : DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) →
            _root_.DirectLimit G f')
        0 :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
rwa :
  ∀
    (hix :
      Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
        ((ringEquiv G f' :
              (a : DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) →
                _root_.DirectLimit G f')
            ((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) :
          _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
        (0 : _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')),
    ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f' i j hij : (a : G i) → G j) x : G j) (0 : G j)
rwa₁ :
  ∀
    (hix :
      Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ 0),
    ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f' i j hij : (a : G i) → G j) x : G j) (0 : G j)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (hix :
      ∃ (i_1 : ι) (h : (Sigma.mk (β := fun (i : ι) ↦ G i) i x).fst (β := fun (i : ι) ↦ G i) ≤ i_1),
        Eq (α := G i_1)
          ((f' ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).fst (β := fun (i : ι) ↦ G i)) i_1 h :
                (a : G ⟨i, x⟩.fst) → G i_1)
              ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).snd (β := fun (i : ι) ↦ G i)) :
            G i_1)
          (0 : G i_1)),
    ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f' i j hij : (a : G i) → G j) x : G j) (0 : G j)
⊢ ∃ (j : ι) (hij : i ≤ j), Eq (α := G j) ((f' i j hij : (a : G i) → G j) x : G j) (0 : G j)

Tactic:
rwa [map_zero, ringEquiv_of, DirectLimit.exists_eq_zero] at hix

Premises used: map_zero, Ring.DirectLimit.ringEquiv_of, DirectLimit.exists_eq_zero