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
inst_2 : IsDirectedOrder ι
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective (α := G i) (β := G j) (⇑(f' i j hij) : (a : G i) → G j)
i : ι
this : Nonempty ι
x x_1 : G i
eq :
  Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    (Function.comp (β := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      (⇑(RingEquiv.toEquiv (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 (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)
    (Function.comp (β := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      (⇑(RingEquiv.toEquiv (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 (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_1)
⊢ Eq (α :=
    Quotient (α := (i : ι) × G i) (DirectLimit.setoid (F := G) (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f'))
    ((fun (x : G i) ↦
        (⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ :
          Quotient (α := (i : ι) × G i)
            (DirectLimit.setoid (F := G) (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')))
      x)
    ((fun (x : G i) ↦
        (⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ :
          Quotient (α := (i : ι) × G i)
            (DirectLimit.setoid (F := G) (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')))
      x_1)

Tactic:
simpa only [← ringEquiv_of]

Premises used: Ring.DirectLimit.ringEquiv_of
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f_1 : (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_1 i j hij x) : P) ((g_1 i : (a : G i) → P) x : P)
f'_1 f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst_3 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_4 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g_2 : (i : ι) → RingHom.{u_2, u_4} (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), (g_2 j).comp (f i j h) = (f' i j h).comp (g_2 i)
i j : ι
h : i ≤ j
g : G i
⊢ Eq.{u_4 + 1} (α := G' j) (((g_2 j).comp (f i j h) : (a : G i) → G' j) g : G' j)
    (((f' i j h).comp (g_2 i) : (a : G i) → G' j) g : G' j)

Tactic:
have eq1 := DFunLike.congr_fun (hg i j h) g
-- 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
G' : ι → Type u_4
inst_2 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
g : (i : ι) → RingHom.{u_2, u_4} (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)
i : ι
x : G i
⊢ Eq (α := DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
    ((map (G := G) (G' := G') g hg :
          (a : DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) →
            DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
        ((of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i :
            (a : G i) → DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
          x) :
      DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
    ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) i :
          (a : G' i) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
        ((g i : (a : G i) → G' i) x) :
      DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))

Tactic:
lift_of _ _ _ _ _

Premises used: Submodule.Quotient.mk, 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
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
      ((RingHom.comp (β := DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
              (map (G := G) (G' := G) (fun (x : ι) ↦ RingHom.id (G x)) ⋯)
              (of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i) :
            (a : G i) → DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
          x :
        DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
      ((RingHom.comp (RingHom.id (DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)))
              (of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i) :
            (a : G i) → DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
          x :
        DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
⊢ Eq (α :=
    (DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) →+*
      DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
    (map (G := G) (G' := G) (fun (x : ι) ↦ RingHom.id (G x)) ⋯)
    (RingHom.id (DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)))

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 fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
    ((RingHom.comp (β := DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
            (map (G := G) (G' := G) (fun (x : ι) ↦ RingHom.id (G x)) ⋯)
            (of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i) :
          (a : G i) → DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
        x :
      DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
    ((RingHom.comp (RingHom.id (DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)))
            (of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i) :
          (a : G i) → DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
        x :
      DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_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_1 : (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_1 i j hij x) : P) ((g i : (a : G i) → P) x : P)
f'_1 f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst_3 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_4 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → RingHom.{u_2, u_4} (G i) (G' i)
g₂ : (i : ι) → RingHom.{u_4, u_5} (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)
rw₄ rw₅ : (f'' i j h).comp ((g₂ i).comp (g₁ i)) = (f'' i j h).comp ((fun (i : ι) ↦ (g₂ i).comp (g₁ i)) i)
⊢ RingHom.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)

Tactic:
rw [RingHom.comp_assoc, hg₁ i, ← RingHom.comp_assoc, hg₂ i, RingHom.comp_assoc]

Premises used: RingHom.comp_assoc
-- 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
G' : ι → Type u_4
inst_2 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_3 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → RingHom.{u_2, u_4} (G i) (G' i)
g₂ : (i : ι) → RingHom.{u_4, u_5} (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)
h :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
      ((((map (G := G') (G' := G'') g₂ hg₂).comp (map (G := G) (G' := G') g₁ hg₁)).comp
              (of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i) :
            (a : G i) → DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
          x :
        DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
      ((RingHom.comp (β := DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
              (map (G := G) (G' := G'') (fun (i : ι) ↦ (g₂ i).comp (g₁ i)) ⋯)
              (of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i) :
            (a : G i) → DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
          x :
        DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
⊢ (map (G := G') (G' := G'') g₂ hg₂).comp (map (G := G) (G' := G') g₁ hg₁) =
    map (G := G) (G' := G'') (fun (i : ι) ↦ (g₂ i).comp (g₁ i)) ⋯

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
G' : ι → Type u_4
inst_2 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_3 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → RingHom.{u_2, u_4} (G i) (G' i)
g₂ : (i : ι) → RingHom.{u_4, u_5} (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 : ι
x : G i
⊢ Eq (α := DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
    ((((map (G := G') (G' := G'') g₂ hg₂).comp (map (G := G) (G' := G') g₁ hg₁)).comp
            (of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i) :
          (a : G i) → DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
        x :
      DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
    ((RingHom.comp (β := DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
            (map (G := G) (G' := G'') (fun (i : ι) ↦ (g₂ i).comp (g₁ i)) ⋯)
            (of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i) :
          (a : G i) → DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_1))
        x :
      DirectLimit G'' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f'' x x_1 h) : (a : G'' x) → G'' x_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_1 : (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_1 i j hij x) : P) ((g i : (a : G i) → P) x : P)
f'_1 f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst_3 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_4 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
e : (i : ι) → RingEquiv.{u_2, u_4} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (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_4 + 1} (α := G' j)
    (((e j).toRingHom.comp (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) : RingHom.{u_2, u_4} (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)
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f_1 : (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_1 i j hij x) : P) ((g i : (a : G i) → P) x : P)
f'_1 f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst_3 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_4 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
e : (i : ι) → RingEquiv.{u_2, u_4} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (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_4 + 1} (α := G' j)
    (((e j).toRingHom.comp (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) : RingHom.{u_2, u_4} (G i) (G' j)) : (a : G i) → G' j)
        (((e i).symm : (a : G' i) → G i) x) :
      G' j)
simp :
  ∀
    (eq1 :
      Eq.{u_4 + 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_2 + 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)
⊢ Eq.{u_2 + 1} (α := G j)
    ((RingHom.comp
            ((fun (i : ι) ↦ ((↑(e i).symm : RingHom.{u_4, u_2} (G' i) (G i)) : RingHom.{u_4, u_2} (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 : RingHom.{u_4, u_2} (G' i) (G i)) : RingHom.{u_4, u_2} (G' i) (G i))) i) :
          (a : G' i) → G j)
        x :
      G j)

Tactic:
simp only [RingEquiv.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
        RingEquiv.apply_symm_apply] at eq1 ⊢

Premises used: RingEquiv.apply_symm_apply, RingHom.coe_coe, RingHom.coe_comp, RingEquiv.toRingHom_eq_coe, Function.comp_apply
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f_1 : (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_1 i j hij x) : P) ((g i : (a : G i) → P) x : P)
f'_1 f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst_3 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_4 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
e : (i : ι) → RingEquiv.{u_2, u_4} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (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_4 + 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_2 + 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 [← eq1]
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f_1 : (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_1 i j hij x) : P) ((g i : (a : G i) → P) x : P)
f'_1 f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst_3 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_4 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
e : (i : ι) → RingEquiv.{u_2, u_4} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp (↑(e i) : G i →+* G' i)
⊢ (map (G := G) (G' := G') (fun (x : ι) ↦ (↑(e x) : G x →+* G' x)) he).comp
      (map (G := G') (G' := G) (fun (i : ι) ↦ (↑(e i).symm : G' i →+* G i)) ⋯) =
    RingHom.id (DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))

Tactic:
simp [map_comp]

Premises used: Ring.DirectLimit.map_comp
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f_1 : (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_1 i j hij x) : P) ((g i : (a : G i) → P) x : P)
f'_1 f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst_3 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_4 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
e : (i : ι) → RingEquiv.{u_2, u_4} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp (↑(e i) : G i →+* G' i)
⊢ RingHom.comp (map (G := G') (G' := G) (fun (i : ι) ↦ (↑(e i).symm : G' i →+* G i)) ⋯)
      (map (G := G) (G' := G') (fun (x : ι) ↦ (↑(e x) : G x →+* G' x)) he) =
    RingHom.id (DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))

Tactic:
simp [map_comp]

Premises used: Ring.DirectLimit.map_comp
-- 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
G' : ι → Type u_4
inst_2 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
e : (i : ι) → RingEquiv.{u_2, u_4} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp (↑(e i) : G i →+* G' i)
i : ι
g : G i
⊢ Eq (α := DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
    ((congr (G := G) (G' := G') e he :
          (a : DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) →
            DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
        ((of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i :
            (a : G i) → DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
          g) :
      DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
    ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) i :
          (a : G' i) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
        ((e i : (a : G i) → G' i) g) :
      DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))

Tactic:
map_apply_of _ he _

Premises used: Quotient.liftOn', AddCon.liftOn, FreeGroup.Lift.aux, Quotient.map₂, Con.liftOn, List.foldr, Ring.DirectLimit.map_apply_of, 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
G' : ι → Type u_4
inst_2 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
e : (i : ι) → RingEquiv.{u_2, u_4} (G i) (G' i)
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp (↑(e i) : G i →+* G' i)
i : ι
g : G' i
⊢ Eq (α := DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
    (((congr (G := G) (G' := G') e he).symm :
          (a : DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) →
            DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
        ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) i :
            (a : G' i) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
          g) :
      DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
    ((of G (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1)) i :
          (a : G i) → DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))
        (((e i).symm : (a : G' i) → G i) g) :
      DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f x x_1 h) : (a : G x) → G x_1))

Tactic:
simp only [congr, RingEquiv.ofRingHom_symm_apply, map_apply_of, RingHom.coe_coe]

Premises used: RingHom.coe_coe, RingEquiv.ofRingHom_symm_apply, Ring.DirectLimit.congr, Ring.DirectLimit.map_apply_of
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_4 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)
⊢ Nonempty ι

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_4 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)
i : ι
rw :
  Ne (α := Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) 0
    ((Ring.DirectLimit.of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) i :
        (a : G i) → Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      1)
rw₁ : ι
⊢ Ne (α := Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) 0 1

Tactic:
rw [← (Ring.DirectLimit.of _ _ _).map_one]

Premises used: Ring.DirectLimit.of, RingHom.map_one
-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
inst_3 : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_4 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)
i : ι
H :
  Eq (α := Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) 0
    ((Ring.DirectLimit.of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) i :
        (a : G i) → Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      1)
rcases : ∀ (j : ι) (hij : i ≤ j) (hf : Eq (α := G j) ((f' i j hij : (a : G i) → G j) 1 : G j) (0 : G j)), False
⊢ False

Tactic:
rcases Ring.DirectLimit.of.zero_exact H.symm with ⟨j, hij, hf⟩

Premises used: Ring.DirectLimit.of.zero_exact, Eq.symm