awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : Semiring R
inst_5 : (i : ι) → AddCommMonoid (G i)
inst_6 : (i : ι) → Module.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : AddCommMonoid P
inst_10 : Module R P
g₁ g₂ : DirectLimit G (T := T) f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G (T := T) f i = g₂ ∘ₗ of R ι G (T := T) f i
x : DirectLimit G (T := T) f
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
have h₁ : ∀ (i : ι) (x : G i),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
Tactic: induction x using DirectLimit.induction with | _ i x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G (T := T) f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
⊢ g₁ = g₂
have a : ∀ (x : DirectLimit G (T := T) f),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G (T := T) f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
x : DirectLimit G (T := T) f
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
have a : ∀ (i : ι) (x : G i),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
Tactic: induction x using DirectLimit.induction with | _ i x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : (i : ι) → NonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonAssocSemiring P
g₁ g₂ : DirectLimit G (T := T) f →+* P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
⊢ g₁ = g₂
have a : ∀ (x : DirectLimit G (T := T) f),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : (i : ι) → NonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
P : Type u_7
inst_7 : NonAssocSemiring P
g₁ g₂ : DirectLimit G (T := T) f →+* P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
x : DirectLimit G (T := T) f
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
have a : ∀ (i : ι) (x : G i),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
Tactic: induction x using DirectLimit.induction with | _ i x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : (i : ι) → StarRing (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : StarRing P
g₁ g₂ : DirectLimit G (T := T) f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
⊢ g₁ = g₂
have h₁ : ∀ (x : DirectLimit G (T := T) f),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : (i : ι) → StarRing (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : StarRing P
g₁ g₂ : DirectLimit G (T := T) f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
x : DirectLimit G (T := T) f
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
have h₁ : ∀ (i : ι) (x : G i),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
Tactic: induction x using DirectLimit.induction with | _ i x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_6 : (i : ι) → Semiring (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_10 : Nonempty ι
i : ι
r : R
⊢ Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧
    ((algebraMap R (DirectLimit G (T := T) f) : (a : R) → DirectLimit G f) r)
have rw : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) 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: rw [algebraMap_def i]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_6 : (i : ι) → Semiring (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_10 : Nonempty ι
P : Type u_7
inst_11 : Semiring P
inst_12 : Algebra R P
g : (i : ι) → AlgHom.{u_1, u_3, u_7} R (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_7 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
r : R
i : ι := Classical.arbitrary ι
⊢ Eq.{u_7 + 1} (α := P)
    (DirectLimit.lift (F := G) (T := T) f (fun (x1 : ι) (x2 : G x1) ↦ (g x1 : (a : G x1) → P) x2) ⋯
        ((algebraMap R (DirectLimit G (T := T) f) : (a : R) → DirectLimit G f) r) :
      P)
    ((algebraMap R P : (a : R) → P) r : P)
have rw : Eq.{u_7 + 1} (α := P)
  (DirectLimit.lift (F := G) (T := T) f (fun (x1 : ι) (x2 : G x1) ↦ (g x1 : (a : G x1) → P) x2) sorry
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧ :
    P)
  ((algebraMap R P : (a : R) → P) r : P)
Tactic: rw [algebraMap_def i r, lift_def, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_6 : (i : ι) → Semiring (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_10 : Nonempty ι
P : Type u_7
inst_11 : Semiring P
inst_12 : Algebra R P
g : (i : ι) → AlgHom.{u_1, u_3, u_7} R (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_7 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
r : R
i : ι := Classical.arbitrary ι
rw :
  Eq.{u_7 + 1} (α := P)
    (DirectLimit.lift (F := G) (T := T) f (fun (x1 : ι) (x2 : G x1) ↦ (g x1 : (a : G x1) → P) x2) ⋯
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧ :
      P)
    ((algebraMap R P : (a : R) → P) r : P)
⊢ Eq.{u_7 + 1} (α := P)
    (DirectLimit.lift (F := G) (T := T) f (fun (x1 : ι) (x2 : G x1) ↦ (g x1 : (a : G x1) → P) x2) ⋯
        ((algebraMap R (DirectLimit G (T := T) f) : (a : R) → DirectLimit G f) r) :
      P)
    ((algebraMap R P : (a : R) → P) r : P)
have rw₁ : Eq.{u_7 + 1} (α := P)
  ((g
          (Sigma.fst (β := fun (i : ι) ↦ G i)
            (Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r))) :
        (a : G ⟨i, (algebraMap R (G i) : (a : R) → G i) r⟩.fst) → P)
      (Sigma.snd (β := fun (i : ι) ↦ G i)
        (Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r))) :
    P)
  ((algebraMap R P : (a : R) → P) r : P)
Tactic: rw [algebraMap_def i r, lift_def, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_6 : (i : ι) → Semiring (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : (i : ι) → Algebra.{u_1, u_3} R (G i)
inst_9 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_10 : Nonempty ι
P : Type u_7
inst_11 : Semiring P
inst_12 : Algebra R P
g : (i : ι) → AlgHom.{u_1, u_3, u_7} R (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_7 + 1} (α := P) ((g j : (a : G j) → P) ((f i j hij : (a : G i) → G j) x : G j) : P)
      ((g i : (a : G i) → P) x : P)
r : R
i : ι := Classical.arbitrary ι
rw :
  Eq.{u_7 + 1} (α := P)
    (DirectLimit.lift (F := G) (T := T) f (fun (x1 : ι) (x2 : G x1) ↦ (g x1 : (a : G x1) → P) x2) ⋯
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r)⟧ :
      P)
    ((algebraMap R P : (a : R) → P) r : P)
rw₁ :
  Eq.{u_7 + 1} (α := P)
    ((g
            (Sigma.fst (β := fun (i : ι) ↦ G i)
              (Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r))) :
          (a : G ⟨i, (algebraMap R (G i) : (a : R) → G i) r⟩.fst) → P)
        (Sigma.snd (β := fun (i : ι) ↦ G i)
          (Sigma.mk (β := fun (i : ι) ↦ G i) i ((algebraMap R (G i) : (a : R) → G i) r))) :
      P)
    ((algebraMap R P : (a : R) → P) r : P)
⊢ Eq.{u_7 + 1} (α := P)
    (DirectLimit.lift (F := G) (T := T) f (fun (x1 : ι) (x2 : G x1) ↦ (g x1 : (a : G x1) → P) x2) ⋯
        ((algebraMap R (DirectLimit G (T := T) f) : (a : R) → DirectLimit G f) r) :
      P)
    ((algebraMap R P : (a : R) → P) r : P)
have rw₂ : Eq.{u_7 + 1} (α := P) ((algebraMap R P : (a : R) → P) r : P) ((algebraMap R P : (a : R) → P) r : P)
Tactic: rw [algebraMap_def i r, lift_def, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_5 : (i : ι) → Semiring (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
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)
inst_9 : Nonempty ι
P : Type u_7
inst_10 : Semiring P
inst_11 : Algebra R P
g₁ g₂ : DirectLimit G (T := T) f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
⊢ g₁ = g₂
have H : ∀ (x : DirectLimit G (T := T) f),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_5 : (i : ι) → Semiring (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), RingHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
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)
inst_9 : Nonempty ι
P : Type u_7
inst_10 : Semiring P
inst_11 : Algebra R P
g₁ g₂ : DirectLimit G (T := T) f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
x : DirectLimit G (T := T) f
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
have H : ∀ (i : ι) (x : G i),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
Tactic: induction x using DirectLimit.induction with | _ i x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_6 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_7 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_9 : Nonempty ι
i : ι
m : R
x : G i
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧ =
    HSMul.hSMul (α := R) (β := DirectLimit G (T := T) f) ((MonoidHom.id R : (a : R) → R) m : R)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
have rw : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) m : R) x)⟧
Tactic: rw [smul_def, MonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_6 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_7 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_8 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_9 : Nonempty ι
i : ι
m : R
x : G i
rw :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) m : R) x)⟧
⊢ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧ =
    HSMul.hSMul (α := R) (β := DirectLimit G (T := T) f) ((MonoidHom.id R : (a : R) → R) m : R)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
have rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (m • x)⟧
Tactic: rw [smul_def, MonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : DistribMulAction R P
g₁ g₂ : DirectLimit G (T := T) f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
⊢ g₁ = g₂
have h₁ : ∀ (x : DirectLimit G (T := T) f),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : CommSemiring R
inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst_6 : (i : ι) → DistribMulAction.{u_1, u_3} R (G i)
inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass.{u_6, u_1, u_3, u_3} (T h) R (G i) (G j)
inst_8 : Nonempty ι
P : Type u_7
inst_9 : NonUnitalNonAssocSemiring P
inst_10 : DistribMulAction R P
g₁ g₂ : DirectLimit G (T := T) f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G (T := T) f i) = g₂.comp (of G (T := T) f i)
x : DirectLimit G (T := T) f
⊢ Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) x : P) ((g₂ : (a : DirectLimit G f) → P) x : P)
have h₁ : ∀ (i : ι) (x : G i),
  Eq.{u_7 + 1} (α := P) ((g₁ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
    ((g₂ : (a : DirectLimit G f) → P) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ : P)
Tactic: induction x using DirectLimit.induction with | _ i x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Finiteness (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq (Submodule R M)
N : { N : Submodule R M // N.FG }
⊢ (↑(equiv R M) :
        DirectLimit (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M)) (fgSystem R M) →ₗ[R] M) ∘ₗ
      of R { N : Submodule R M // N.FG } (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M))
        (fgSystem R M) N =
    (↑N : Submodule R M).subtype
have h : ∀ (x : ↥(↑N : Submodule R M)),
  Eq (α := M)
    (((↑(equiv R M) :
              DirectLimit (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M)) (fgSystem R M) →ₗ[R] M) ∘ₗ
            of R { N : Submodule R M // N.FG } (fun (i : { N : Submodule R M // N.FG }) ↦ ↥(↑i : Submodule R M))
              (fgSystem R M) N :
          (a : ↥(↑N : Submodule R M)) → M)
        x :
      M)
    (((↑N : Submodule R M).subtype : (a : ↥(↑N : Submodule R M)) → M) x : M)
Tactic: ext