awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → Group (G i)
inst_7 : Group C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidHomClass.{u_4, u_3, u_5} (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ HPow.hPow (β := ℤ) x (↑n.succ : ℤ) = HPow.hPow (β := ℤ) x (↑n : ℤ) * x

Tactic:
apply DivInvMonoid.zpow_succ'

Premises used: DivInvMonoid.zpow_succ'
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → Group (G i)
inst_7 : Group C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidHomClass.{u_4, u_3, u_5} (H i) (G i) C
n : ℕ
i : ι
x : G i
simp_rw :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x ^ Int.negSucc n)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹⟧
⊢ Eq (α := DirectLimit G (T := T) f)
    (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ x_1 ^ Int.negSucc n) ⋯
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
    (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ x_1⁻¹) ⋯
      (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ HPow.hPow (β := ℤ) x_1 (↑n.succ : ℤ))
        ⋯ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧))

Tactic:
simp_rw +instances [map_def]

Premises used: DirectLimit.map_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → Group (G i)
inst_7 : Group C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidHomClass.{u_4, u_3, u_5} (H i) (G i) C
n : ℕ
i : ι
x : G i
e_a : x ^ Int.negSucc n = (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹
⊢ Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x ^ Int.negSucc n)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹⟧

Tactic:
congr
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → Group (G i)
inst_7 : Group C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidHomClass.{u_4, u_3, u_5} (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ x ^ Int.negSucc n = (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⁻¹

Tactic:
apply DivInvMonoid.zpow_neg'

Premises used: DivInvMonoid.zpow_neg'
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → Group (G i)
inst_7 : Group C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidHomClass.{u_4, u_3, u_5} (H i) (G i) C
i : ι
x : G i
simp_rw :
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⁻¹⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    1
simp_rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x⁻¹ * x)⟧ 1
simp_rw₂ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 1⟧ 1
⊢ HMul.hMul (α := DirectLimit G (T := T) f)
      (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ x_1⁻¹) ⋯
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    1

Tactic:
simp_rw [map_def, mul_def, inv_mul_cancel, one_def i]

Premises used: inv_mul_cancel, DirectLimit.map_def, DirectLimit.mul_def, DirectLimit.one_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
inst_5 : (i : ι) → Group (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f)) (⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)⁻¹
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⁻¹⟧

Tactic:
rfl

Premises used: DirectLimit.map, DirectLimit.lift, rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
inst_5 : (i : ι) → Group (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x y : G i
⊢ HDiv.hDiv (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f)) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧ =
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x / y)⟧

Tactic:
map₂_def ..

Premises used: DirectLimit.map₂_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
inst_5 : (i : ι) → Group (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
n : ℤ
⊢ HPow.hPow (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f)) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      n =
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x ^ n)⟧

Tactic:
rfl

Premises used: DirectLimit.map, DirectLimit.lift, rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → Group (G i)
inst_7 : Group C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidHomClass.{u_4, u_3, u_5} (H i) (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
x_1 : DirectLimit G (T := T) f
i : ι
x : G i
simp_rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⁻¹⟧ =
    (DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)⁻¹
simp_rw₁ : Eq.{u_5 + 1} (α := C) ((g i : (a : G i) → C) x⁻¹ : C) (((g i : (a : G i) → C) x)⁻¹ : C)
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)⁻¹ =
    (DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)⁻¹

Tactic:
simp_rw [inv_def, lift_def, map_inv (g i)]

Premises used: map_inv, DirectLimit.lift_def, DirectLimit.inv_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → Group (G i)
inst_7 : Group C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidHomClass.{u_4, u_3, u_5} (H i) (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
x_1 y_1 : DirectLimit G (T := T) f
i : ι
x y : G i
simp_rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x / y)⟧ =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ /
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧
simp_rw₁ :
  (g i : (a : G i) → C) (x / y) =
    HDiv.hDiv (α := C) (β := C) ((g i : (a : G i) → C) x : C) ((g i : (a : G i) → C) y : C)
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HDiv.hDiv (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧) =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ /
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧

Tactic:
simp_rw [div_def, lift_def, map_div (g i)]

Premises used: DirectLimit.lift_def, map_div, DirectLimit.div_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → Group (G i)
inst_7 : Group C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidHomClass.{u_4, u_3, u_5} (H i) (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
x_1 : DirectLimit G (T := T) f
z : ℤ
i : ι
x : G i
simp_rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x ^ z)⟧ =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ^
      z
simp_rw₁ : (g i : (a : G i) → C) (x ^ z) = HPow.hPow (α := C) ((g i : (a : G i) → C) x : C) z
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HPow.hPow (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ z) =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ^
      z

Tactic:
simp_rw [zpow_def, lift_def, map_zpow (g i)]

Premises used: DirectLimit.lift_def, DirectLimit.zpow_def, map_zpow
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → MulZeroClass (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
simp_rw :
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 0⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 0⟧
simp_rw₁ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (0 * x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 0⟧
⊢ HMul.hMul (α := DirectLimit G (T := T) f) 0 ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ = 0

Tactic:
simp_rw [zero_def i, mul_def, zero_mul]

Premises used: MulZeroClass.zero_mul, DirectLimit.mul_def, DirectLimit.zero_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → MulZeroClass (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
simp_rw :
  HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 0⟧ =
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 0⟧
simp_rw₁ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * 0)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 0⟧
⊢ HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ 0 = 0

Tactic:
simp_rw [zero_def i, mul_def, mul_zero]

Premises used: DirectLimit.mul_def, MulZeroClass.mul_zero, DirectLimit.zero_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → MulZeroOneClass (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : ∀ (i : ι), Nontrivial.{u_3} (G i)
h : Eq (α := DirectLimit G (T := T) f) 0 1
i : ι
w :
  Sigma.fst (β := fun (i : ι) ↦ G i)
      (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) ((fun (x : ι) ↦ (0 : G x)) (Classical.arbitrary ι))) ≤
    i
w_1 :
  Sigma.fst (β := fun (i : ι) ↦ G i)
      (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) ((fun (x : ι) ↦ (1 : G x)) (Classical.arbitrary ι))) ≤
    i
eq :
  Eq.{u_3 + 1} (α := G i)
    ((f
            (Sigma.fst (β := fun (i : ι) ↦ G i)
              (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
                ((fun (x : ι) ↦ (0 : G x)) (Classical.arbitrary ι))))
            i w :
          (a : G ⟨Classical.arbitrary ι, (fun (x : ι) ↦ 0) (Classical.arbitrary ι)⟩.fst) → G i)
        (Sigma.snd (β := fun (i : ι) ↦ G i)
          (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
            ((fun (x : ι) ↦ (0 : G x)) (Classical.arbitrary ι)))) :
      G i)
    ((f
            (Sigma.fst (β := fun (i : ι) ↦ G i)
              (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
                ((fun (x : ι) ↦ (1 : G x)) (Classical.arbitrary ι))))
            i w_1 :
          (a : G ⟨Classical.arbitrary ι, (fun (x : ι) ↦ 1) (Classical.arbitrary ι)⟩.fst) → G i)
        (Sigma.snd (β := fun (i : ι) ↦ G i)
          (Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
            ((fun (x : ι) ↦ (1 : G x)) (Classical.arbitrary ι)))) :
      G i)
⊢ False

Tactic:
simp at eq
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{u_4, u_3, u_5} (H i) (G i) C
i : ι
x x_1 : G i
simp_rw :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x / x_1)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_2 : G x) ↦ x_2⁻¹) ⋯
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)
simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x / x_1)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⁻¹⟧
simp_rw₂ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1⁻¹)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⁻¹⟧
⊢ map₂ (F₁ := G) (F₂ := G) (F := G) (T₁ := T) f (T₂ := T) f (T := T) f (fun (x : ι) (x1 x2 : G x) ↦ x1 / x2) ⋯
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_2 : G x) ↦ x_2⁻¹) ⋯
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧)

Tactic:
simp_rw [map₂_def, map_def, div_eq_mul_inv, mul_def]

Premises used: DirectLimit.map_def, DirectLimit.mul_def, div_eq_mul_inv, DirectLimit.map₂_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{u_4, u_3, u_5} (H i) (G i) C
i : ι
x : G i
simp_rw : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HPow.hPow (β := ℤ) x 0)⟧ 1
simp_rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 1⟧ 1
⊢ Eq (α := DirectLimit G (T := T) f)
    (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ HPow.hPow (β := ℤ) x_1 0) ⋯
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
    1

Tactic:
simp_rw [map_def, zpow_zero, one_def i]

Premises used: DirectLimit.map_def, zpow_zero, DirectLimit.one_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{u_4, u_3, u_5} (H i) (G i) C
n : ℕ
i : ι
x : G i
simp_rw :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)⟧
⊢ map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ HPow.hPow (β := ℤ) x_1 (↑n.succ : ℤ)) ⋯
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f)
      (map (F₁ := G) (F₂ := G) (T₁ := T) f (T₂ := T) f (fun (x : ι) (x_1 : G x) ↦ HPow.hPow (β := ℤ) x_1 (↑n : ℤ)) ⋯
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧

Tactic:
simp_rw [map_def, mul_def]

Premises used: DirectLimit.map_def, DirectLimit.mul_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → GroupWithZero (G i)
inst_7 : GroupWithZero C
inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), MonoidWithZeroHomClass.{u_4, u_3, u_5} (H i) (G i) C
n : ℕ
i : ι
x : G i
e_a : HPow.hPow (β := ℤ) x (↑n.succ : ℤ) = HPow.hPow (β := ℤ) x (↑n : ℤ) * x
⊢ Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HPow.hPow (β := ℤ) x (↑n.succ : ℤ))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)⟧

Tactic:
congr