awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (hypothesis)
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_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)
have 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)
Tactic: have eq1 := DFunLike.congr_fun (he i j h) ((e i).symm x)
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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)
⊢ 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)
have 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)
Tactic: simp only [RingEquiv.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
        RingEquiv.apply_symm_apply] at eq1 ⊢
Cleared hypotheses: eq1
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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 : ι
⊢ Ne (α := Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) 0 1
have 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)
Tactic: rw [← (Ring.DirectLimit.of _ _ _).map_one]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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)
⊢ False
have 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
Tactic: rcases Ring.DirectLimit.of.zero_exact H.symm with ⟨j, hij, hf⟩
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (hypothesis)
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)
j : ι
hij : i ≤ j
hf : Eq (α := G j) ((f' i j hij : (a : G i) → G j) 1 : G j) (0 : G j)
⊢ False
have hf₁ : Eq.{u_2 + 1} (α := G j) 1 0
Tactic: rw [(f' i j hij).map_one] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
i : ι
x : G i
H :
  Ne (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
h : x = 0
⊢ Eq (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
have rw : Eq (α := Ring.DirectLimit G f) ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) 0) 0
Tactic: rw [h, (Ring.DirectLimit.of _ _ _).map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
i : ι
x : G i
H :
  Ne (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
h : x = 0
rw : Eq (α := Ring.DirectLimit G f) ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) 0) 0
⊢ Eq (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
have rw₁ : Eq (α := Ring.DirectLimit G f) 0 0
Tactic: rw [h, (Ring.DirectLimit.of _ _ _).map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
i : ι
x : G i
H :
  Ne (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
⊢ HMul.hMul (α := Ring.DirectLimit G f) (β := Ring.DirectLimit G f)
      ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f)
      ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x⁻¹ : Ring.DirectLimit G f) =
    1
have rw : Eq (α := Ring.DirectLimit G f)
  ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) (x * x⁻¹) : Ring.DirectLimit G f)
  (1 : Ring.DirectLimit G f)
Tactic: rw [← (Ring.DirectLimit.of _ _ _).map_mul,
        mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
        (Ring.DirectLimit.of _ _ _).map_one]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
i : ι
x : G i
H :
  Ne (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
rw :
  Eq (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) (x * x⁻¹) : Ring.DirectLimit G f)
    (1 : Ring.DirectLimit G f)
⊢ HMul.hMul (α := Ring.DirectLimit G f) (β := Ring.DirectLimit G f)
      ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f)
      ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x⁻¹ : Ring.DirectLimit G f) =
    1
have rw₁ : Eq (α := Ring.DirectLimit G f) ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) 1) 1
Tactic: rw [← (Ring.DirectLimit.of _ _ _).map_mul,
        mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
        (Ring.DirectLimit.of _ _ _).map_one]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
i : ι
x : G i
H :
  Ne (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f) (0 : Ring.DirectLimit G f)
rw :
  Eq (α := Ring.DirectLimit G f)
    ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) (x * x⁻¹) : Ring.DirectLimit G f)
    (1 : Ring.DirectLimit G f)
rw₁ : Eq (α := Ring.DirectLimit G f) ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) 1) 1
⊢ HMul.hMul (α := Ring.DirectLimit G f) (β := Ring.DirectLimit G f)
      ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x : Ring.DirectLimit G f)
      ((Ring.DirectLimit.of G f i : (a : G i) → Ring.DirectLimit G f) x⁻¹ : Ring.DirectLimit G f) =
    1
have rw₂ : Eq (α := Ring.DirectLimit G f) 1 1
Tactic: rw [← (Ring.DirectLimit.of _ _ _).map_mul,
        mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
        (Ring.DirectLimit.of _ _ _).map_one]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ p * inv G f p = 1
have rw : (p * if H : p = 0 then 0 else Classical.choose (p := fun (x : Ring.DirectLimit G f) ↦ p * x = 1) sorry) = 1
Tactic: rw [inv, dif_neg hp, Classical.choose_spec (DirectLimit.exists_inv G f hp)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
hp : p ≠ 0
rw : (p * if H : p = 0 then 0 else Classical.choose (p := fun (x : Ring.DirectLimit G f) ↦ p * x = 1) ⋯) = 1
⊢ p * inv G f p = 1
have rw₁ : p * Classical.choose (p := fun (x : Ring.DirectLimit G f) ↦ p * x = 1) sorry = 1
Tactic: rw [inv, dif_neg hp, Classical.choose_spec (DirectLimit.exists_inv G f hp)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
hp : p ≠ 0
rw : (p * if H : p = 0 then 0 else Classical.choose (p := fun (x : Ring.DirectLimit G f) ↦ p * x = 1) ⋯) = 1
rw₁ : p * Classical.choose (p := fun (x : Ring.DirectLimit G f) ↦ p * x = 1) ⋯ = 1
⊢ p * inv G f p = 1
have rw₂ : Eq (α := Ring.DirectLimit G f) 1 1
Tactic: rw [inv, dif_neg hp, Classical.choose_spec (DirectLimit.exists_inv G f hp)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ inv G f p * p = 1
have rw : p * inv G f p = 1
Tactic: rw [_root_.mul_comm, DirectLimit.mul_inv_cancel G f hp]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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
p : Ring.DirectLimit G f
hp : p ≠ 0
rw : p * inv G f p = 1
⊢ inv G f p * p = 1
have rw₁ : Eq (α := Ring.DirectLimit G f) 1 1
Tactic: rw [_root_.mul_comm, DirectLimit.mul_inv_cancel G f hp]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.TensorProduct (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : Submodule R P
hN : N.FG
x y : TensorProduct.{u_1, u_3, u_2} R (↥N) M
eq :
  Eq (α := P ⊗[R] M) ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
⊢ ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : N ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
have lift : ∀ (N : { x : Submodule R P // x.FG }) {x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M}
  (eq :
    Eq (α := P ⊗[R] M)
      ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
      ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y :
        P ⊗[R] M)),
  ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : (↑N : Submodule R P) ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
Tactic: lift N to {N : Submodule R P // N.FG} using hN
Cleared hypotheses: N, hN, x, y, eq
-- Lean 4 proof step from Mathlib.Algebra.Colimit.TensorProduct (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : { x : Submodule R P // x.FG }
x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M
eq :
  Eq (α := P ⊗[R] M)
    ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
⊢ ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : (↑N : Submodule R P) ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
have eq₁ : Eq (α :=
  TensorProduct.{u_1, u_3, u_2} R
    (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)
  ((LinearMap.rTensor M
          (↑(LinearEquiv.symm (Module.fgSystem.equiv R P)) :
            P →ₗ[R]
              Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                (Module.fgSystem R P)) :
        (a : P ⊗[R] M) →
          Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
              (Module.fgSystem R P) ⊗[R]
            M)
      ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x) :
    TensorProduct.{u_1, u_3, u_2} R
      (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)
  ((LinearMap.rTensor M
          (↑(LinearEquiv.symm (Module.fgSystem.equiv R P)) :
            P →ₗ[R]
              Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
                (Module.fgSystem R P)) :
        (a : P ⊗[R] M) →
          Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P))
              (Module.fgSystem R P) ⊗[R]
            M)
      ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y) :
    TensorProduct.{u_1, u_3, u_2} R
      (Module.DirectLimit (fun (i : { N : Submodule R P // N.FG }) ↦ ↥(↑i : Submodule R P)) (Module.fgSystem R P)) M)
Tactic: apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Colimit.TensorProduct (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : Submodule R P
hN : N.FG
x y : TensorProduct.{u_1, u_3, u_2} R (↥N) M
eq :
  Eq (α := P ⊗[R] M) ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
⊢ ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : N ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
have lift : ∀ (N : { x : Submodule R P // x.FG }) (hN : (↑N : Submodule R P).FG)
  {x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M}
  (eq :
    Eq (α := P ⊗[R] M)
      ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
      ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y :
        P ⊗[R] M)),
  ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : (↑N : Submodule R P) ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
Tactic: classical
  lift N to {N : Submodule R P // N.FG} using hN
  apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
  apply_fun directLimitLeft _ _ at eq
  simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
    (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
  have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
  exact ⟨_, N'.2, le, eq⟩
Cleared hypotheses: N, hN, x, y, eq
-- Lean 4 proof step from Mathlib.Algebra.Colimit.TensorProduct (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : Submodule R P
hN : N.FG
x y : TensorProduct.{u_1, u_3, u_2} R (↥N) M
eq :
  Eq (α := P ⊗[R] M) ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
    ((LinearMap.rTensor M N.subtype : (a : ↥N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
lift :
  ∀ (N : { x : Submodule R P // x.FG }) (hN : (↑N : Submodule R P).FG)
    {x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M}
    (eq :
      Eq (α := P ⊗[R] M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x :
          P ⊗[R] M)
        ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y :
          P ⊗[R] M)),
    ∃ (N' : Submodule R P),
      N'.FG ∧
        ∃ (h : (↑N : Submodule R P) ≤ N'),
          Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
            ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) x :
              TensorProduct.{u_1, u_3, u_2} R (↥N') M)
            ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) y :
              TensorProduct.{u_1, u_3, u_2} R (↥N') M)
⊢ ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : N ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥N ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
have lift₁ : ∀ (N : { x : Submodule R P // x.FG }) {x y : TensorProduct.{u_1, u_3, u_2} R (↥(↑N : Submodule R P)) M}
  (eq :
    Eq (α := P ⊗[R] M)
      ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) x : P ⊗[R] M)
      ((LinearMap.rTensor M (↑N : Submodule R P).subtype : (a : ↥(↑N : Submodule R P) ⊗[R] M) → P ⊗[R] M) y :
        P ⊗[R] M)),
  ∃ (N' : Submodule R P),
    N'.FG ∧
      ∃ (h : (↑N : Submodule R P) ≤ N'),
        Eq (α := TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) x :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
          ((LinearMap.rTensor M (inclusion h) : (a : ↥(↑N : Submodule R P) ⊗[R] M) → ↥N' ⊗[R] M) y :
            TensorProduct.{u_1, u_3, u_2} R (↥N') M)
Tactic: classical
  lift N to {N : Submodule R P // N.FG} using hN
  apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
  apply_fun directLimitLeft _ _ at eq
  simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
    (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
  have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
  exact ⟨_, N'.2, le, eq⟩
Cleared hypotheses: N, hN, x, y, eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
⊢ (of v).convs (n + 1) = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
have rw : (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
Tactic: rw [of_convs_eq_convs', convs'_succ, of_convs_eq_convs']