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 : ι) → Mul (G i)
inst_7 : (i : ι) → SMul.{u_1, u_3} R (G i)
inst_8 : ∀ (i : ι), SMulCommClass.{u_3, u_1, u_3} (G i) R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_10 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
⊢ SMulCommClass (DirectLimit G (T := T) f) R (DirectLimit G (T := T) f)

Tactic:
have _ (i) : SMulCommClass R (G i) (G i) := SMulCommClass.symm _ _ _
  SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm, DirectLimit
-- 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 : ι) → DivisionSemiring (G i)
inst_7 : DivisionSemiring C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{u_4, u_3, u_5} (H i) (G i) C
q : ℚ≥0
simp_rw :
  Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (↑q : G (Classical.arbitrary ι))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HDiv.hDiv (α := G (Classical.arbitrary ι)) (↑q.num : G (Classical.arbitrary ι))
          (↑q.den : G (Classical.arbitrary ι)))⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        ((fun (x : ι) ↦ ((↑q : G x) : G x)) (Classical.arbitrary ι))⟧ =
    HDiv.hDiv (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
          ((fun (x : ι) ↦ ((↑q.num : G x) : G x)) (Classical.arbitrary ι))⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
          ((fun (x : ι) ↦ ((↑q.den : G x) : G x)) (Classical.arbitrary ι))⟧

Tactic:
simp_rw [div₀_def]

Premises used: DirectLimit.div₀_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 : ι) → DivisionSemiring (G i)
inst_7 : DivisionSemiring C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{u_4, u_3, u_5} (H i) (G i) C
q : ℚ≥0
rw rw₁ :
  Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HDiv.hDiv (α := G (Classical.arbitrary ι)) (↑q.num : G (Classical.arbitrary ι))
          (↑q.den : G (Classical.arbitrary ι)))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HDiv.hDiv (α := G (Classical.arbitrary ι)) (↑q.num : G (Classical.arbitrary ι))
          (↑q.den : G (Classical.arbitrary ι)))⟧
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (↑q : G (Classical.arbitrary ι))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HDiv.hDiv (α := G (Classical.arbitrary ι)) (↑q.num : G (Classical.arbitrary ι))
          (↑q.den : G (Classical.arbitrary ι)))⟧

Tactic:
rw [NNRat.cast_def]

Premises used: NNRat.cast_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_3 : ι) → (h : x ≤ x_3) → 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 : ι) → DivisionSemiring (G i)
inst_7 : DivisionSemiring C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{u_4, u_3, u_5} (H i) (G i) C
q : ℚ≥0
x_1 x_2 : ι
h : x_1 ≤ x_2
x : G x_1
simp_rw simp_rw₁ :
  (f x_1 x_2 h : (a : G x_1) → G x_2) (q • x) =
    HSMul.hSMul (β := G x_2) q ((f x_1 x_2 h : (a : G x_1) → G x_2) x : G x_2)
simp_rw₂ :
  (f x_1 x_2 h : (a : G x_1) → G x_2) ((↑q : G x_1) * x) =
    HMul.hMul (α := G x_2) (β := G x_2) ((↑q : G x_2) : G x_2) ((f x_1 x_2 h : (a : G x_1) → G x_2) x : G x_2)
simp_rw₃ :
  HMul.hMul (α := G x_2) (β := G x_2) ((f x_1 x_2 h : (a : G x_1) → G x_2) (↑q : G x_1) : G x_2)
      ((f x_1 x_2 h : (a : G x_1) → G x_2) x : G x_2) =
    HMul.hMul (α := G x_2) (β := G x_2) ((↑q : G x_2) : G x_2) ((f x_1 x_2 h : (a : G x_1) → G x_2) x : G x_2)
⊢ Eq.{u_3 + 1} (α := G x_2) ((f x_1 x_2 h : (a : G x_1) → G x_2) ((fun (x : ι) (x_3 : G x) ↦ q • x_3) x_1 x) : G x_2)
    ((fun (x : ι) (x_3 : G x) ↦ q • x_3) x_2 ((f x_1 x_2 h : (a : G x_1) → G x_2) x) : G x_2)

Tactic:
simp_rw [NNRat.smul_def, map_mul, map_nnratCast]

Premises used: map_nnratCast, map_mul, NNRat.smul_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_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 : ι) → DivisionSemiring (G i)
inst_7 : DivisionSemiring C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{u_4, u_3, u_5} (H i) (G i) C
x_1 : ℚ≥0
i : ι
x : G i
simp_rw simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 • x)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f fun (x : ι) ↦ (↑x_1 : G x))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
simp_rw₂ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 • x)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (↑x_1 : G i)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
simp_rw₃ :
  Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f)) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 • x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((↑x_1 : G i) * x)⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).fst (β := fun (i : ι) ↦ G i))
        ((fun (x : ι) (x_2 : G x) ↦ x_1 • x_2) ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).fst (β := fun (i : ι) ↦ G i))
          ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).snd (β := fun (i : ι) ↦ G i)))⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f fun (x : ι) ↦ (↑x_1 : G x))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧

Tactic:
simp_rw [map₀_def _ _ (fun _ _ _ ↦ map_nnratCast _ _) i, mul_def, NNRat.smul_def]

Premises used: DirectLimit.mul_def, map_nnratCast, NNRat.smul_def, 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 : ι) → DivisionSemiring (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
q : ℚ≥0
i : ι
⊢ Eq (α := DirectLimit G (T := T) f) (↑q : DirectLimit G f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (↑q : G i)⟧

Tactic:
map₀_def _ _ (fun _ _ _ ↦ map_nnratCast _ _) _

Premises used: map_nnratCast, DirectLimit.map₀_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_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 : ι) → DivisionSemiring (G i)
inst_7 : DivisionSemiring C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{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))
q : ℚ≥0
let :
  ∀ (i : ι),
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h (↑q : DirectLimit G f) = (↑q : C)
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h (↑q : DirectLimit G f) = (↑q : C)

Tactic:
let ⟨i⟩ := ‹Nonempty ι›
-- 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_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 : ι) → DivisionSemiring (G i)
inst_7 : DivisionSemiring C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{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))
q : ℚ≥0
i : ι
rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (↑q : G i)⟧ =
    (↑q : C)
i₁ : ι
rw₁ :
  Eq.{u_5 + 1} (α := C)
    ((g (Sigma.fst (β := fun (i : ι) ↦ G i) (Sigma.mk (β := fun (i : ι) ↦ G i) i (↑q : G i))) :
          (a : G ⟨i, (↑q : G i)⟩.fst) → C)
        (Sigma.snd (β := fun (i : ι) ↦ G i) (Sigma.mk (β := fun (i : ι) ↦ G i) i (↑q : G i))) :
      C)
    ((↑q : C) : C)
i₂ : ι
rw₂ rw₃ : Eq.{u_5 + 1} (α := C) (↑q : C) (↑q : C)
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h (↑q : DirectLimit G f) = (↑q : C)

Tactic:
rw [nnratCast_def, lift_def, map_nnratCast (g i)]

Premises used: DirectLimit.lift_def, map_nnratCast, DirectLimit.nnratCast_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 : ι) → DivisionRing (G i)
inst_7 : DivisionRing C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{u_4, u_3, u_5} (H i) (G i) C
q : ℚ
simp_rw :
  Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (↑q : G (Classical.arbitrary ι))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HDiv.hDiv (α := G (Classical.arbitrary ι)) (↑q.num : G (Classical.arbitrary ι))
          (↑q.den : G (Classical.arbitrary ι)))⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        ((fun (x : ι) ↦ ((↑q : G x) : G x)) (Classical.arbitrary ι))⟧ =
    HDiv.hDiv (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
          ((fun (x : ι) ↦ ((↑q.num : G x) : G x)) (Classical.arbitrary ι))⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
          ((fun (x : ι) ↦ ((↑q.den : G x) : G x)) (Classical.arbitrary ι))⟧

Tactic:
simp_rw [div₀_def]

Premises used: DirectLimit.div₀_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 : ι) → DivisionRing (G i)
inst_7 : DivisionRing C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{u_4, u_3, u_5} (H i) (G i) C
q : ℚ
rw rw₁ :
  Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HDiv.hDiv (α := G (Classical.arbitrary ι)) (↑q.num : G (Classical.arbitrary ι))
          (↑q.den : G (Classical.arbitrary ι)))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HDiv.hDiv (α := G (Classical.arbitrary ι)) (↑q.num : G (Classical.arbitrary ι))
          (↑q.den : G (Classical.arbitrary ι)))⟧
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (↑q : G (Classical.arbitrary ι))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HDiv.hDiv (α := G (Classical.arbitrary ι)) (↑q.num : G (Classical.arbitrary ι))
          (↑q.den : G (Classical.arbitrary ι)))⟧

Tactic:
rw [Rat.cast_def]

Premises used: Rat.cast_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_3 : ι) → (h : x ≤ x_3) → 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 : ι) → DivisionRing (G i)
inst_7 : DivisionRing C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{u_4, u_3, u_5} (H i) (G i) C
q : ℚ
x_1 x_2 : ι
h : x_1 ≤ x_2
x : G x_1
simp_rw simp_rw₁ :
  (f x_1 x_2 h : (a : G x_1) → G x_2) (q • x) =
    HSMul.hSMul (β := G x_2) q ((f x_1 x_2 h : (a : G x_1) → G x_2) x : G x_2)
simp_rw₂ :
  (f x_1 x_2 h : (a : G x_1) → G x_2) ((↑q : G x_1) * x) =
    HMul.hMul (α := G x_2) (β := G x_2) ((↑q : G x_2) : G x_2) ((f x_1 x_2 h : (a : G x_1) → G x_2) x : G x_2)
simp_rw₃ :
  HMul.hMul (α := G x_2) (β := G x_2) ((f x_1 x_2 h : (a : G x_1) → G x_2) (↑q : G x_1) : G x_2)
      ((f x_1 x_2 h : (a : G x_1) → G x_2) x : G x_2) =
    HMul.hMul (α := G x_2) (β := G x_2) ((↑q : G x_2) : G x_2) ((f x_1 x_2 h : (a : G x_1) → G x_2) x : G x_2)
⊢ Eq.{u_3 + 1} (α := G x_2) ((f x_1 x_2 h : (a : G x_1) → G x_2) ((fun (x : ι) (x_3 : G x) ↦ q • x_3) x_1 x) : G x_2)
    ((fun (x : ι) (x_3 : G x) ↦ q • x_3) x_2 ((f x_1 x_2 h : (a : G x_1) → G x_2) x) : G x_2)

Tactic:
simp_rw [Rat.smul_def, map_mul, map_ratCast]

Premises used: map_ratCast, map_mul, Rat.smul_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_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 : ι) → DivisionRing (G i)
inst_7 : DivisionRing C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{u_4, u_3, u_5} (H i) (G i) C
x_1 : ℚ
i : ι
x : G i
simp_rw simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 • x)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f fun (x : ι) ↦ (↑x_1 : G x))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
simp_rw₂ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 • x)⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (↑x_1 : G i)⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
simp_rw₃ :
  Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f)) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 • x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((↑x_1 : G i) * x)⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).fst (β := fun (i : ι) ↦ G i))
        ((fun (x : ι) (x_2 : G x) ↦ x_1 • x_2) ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).fst (β := fun (i : ι) ↦ G i))
          ((Sigma.mk (β := fun (i : ι) ↦ G i) i x).snd (β := fun (i : ι) ↦ G i)))⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f fun (x : ι) ↦ (↑x_1 : G x))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧

Tactic:
simp_rw [map₀_def _ _ (fun _ _ _ ↦ map_ratCast _ _) i, mul_def, Rat.smul_def]

Premises used: map_ratCast, DirectLimit.mul_def, Rat.smul_def, 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 : ι) → DivisionRing (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
q : ℚ
i : ι
⊢ Eq (α := DirectLimit G (T := T) f) (↑q : DirectLimit G f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (↑q : G i)⟧

Tactic:
map₀_def _ _ (fun _ _ _ ↦ map_ratCast _ _) _

Premises used: map_ratCast, DirectLimit.map₀_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_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 : ι) → DivisionRing (G i)
inst_7 : DivisionRing C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{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))
q : ℚ
let :
  ∀ (i : ι),
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h (↑q : DirectLimit G f) = (↑q : C)
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h (↑q : DirectLimit G f) = (↑q : C)

Tactic:
let ⟨i⟩ := ‹Nonempty ι›
-- 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_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 : ι) → DivisionRing (G i)
inst_7 : DivisionRing C
inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_9 : ∀ (i : ι), RingHomClass.{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))
q : ℚ
i : ι
rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (↑q : G i)⟧ =
    (↑q : C)
i₁ : ι
rw₁ :
  Eq.{u_5 + 1} (α := C)
    ((g (Sigma.fst (β := fun (i : ι) ↦ G i) (Sigma.mk (β := fun (i : ι) ↦ G i) i (↑q : G i))) :
          (a : G ⟨i, (↑q : G i)⟩.fst) → C)
        (Sigma.snd (β := fun (i : ι) ↦ G i) (Sigma.mk (β := fun (i : ι) ↦ G i) i (↑q : G i))) :
      C)
    ((↑q : C) : C)
i₂ : ι
rw₂ rw₃ : Eq.{u_5 + 1} (α := C) (↑q : C) (↑q : C)
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h (↑q : DirectLimit G f) = (↑q : C)

Tactic:
rw [ratCast_def, lift_def, map_ratCast (g i)]

Premises used: map_ratCast, DirectLimit.ratCast_def, DirectLimit.lift_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : 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 : CommSemiring R
inst_6 : (i : ι) → Semiring (G i)
inst_7 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
i : ι
r : R
⊢ Eq (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f fun (i : ι) ↦ (algebraMap R (G i) : (a : R) → G i) r)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧

Tactic:
map₀_def _ _ (fun _ _ _ => AlgHomClass.commutes _ _) i

Premises used: AlgHomClass.commutes, DirectLimit.map₀_def