awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Biproducts (goal)
Goal:
R : Type u
inst : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
r : R
x : (↑s.1 : Type (max v w))
⊢ (fun (j : J) ↦
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
            (CC := carrier) (X := Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
            (s.π.app { as := j }) :
          (a : (↑(((Functor.const (Discrete J)).obj s.pt).obj { as := j }) : Type (max v w))) →
            (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
        (r • x)) =
    HSMul.hSMul (α := R) (β := (j : J) → (↑(f j) : Type (max v w))) ((RingHom.id R : (a : R) → R) r : R) fun (j : J) ↦
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
            (CC := carrier) (X := Functor.obj (Functor.obj (Functor.const (Discrete J)) s.pt) { as := j : Discrete J })
            (s.π.app { as := j : Discrete J }) :
          (a : (↑(((Functor.const (Discrete J)).obj s.pt).obj { as := j }) : Type (max v w))) →
            (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
        x
have simp : (fun (j : J) ↦
    HSMul.hSMul (β := (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w))) r
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
              (CC := carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
              (s.π.app { as := j }) :
            (a : (↑s.pt : Type (max v w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
          x :
        (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w)))) =
  HSMul.hSMul (α := R) (β := (j : J) → (↑(f j) : Type (max v w))) ((RingHom.id R : (a : R) → R) r : R) fun (j : J) ↦
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w))) (CC :=
          carrier) (X := s.pt) (Y := Functor.obj (Discrete.functor f) { as := j : Discrete J })
          (s.π.app { as := j : Discrete J }) :
        (a : (↑s.pt : Type (max v w))) → (↑((Discrete.functor f).obj { as := j }) : Type (max v w)))
      x
Tactic: simp only [Functor.const_obj_obj, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Biproducts (goal)
Goal:
R : Type u
A : Type uA
M : Type uM
B : Type uB
inst : Ring R
inst_1 : AddCommGroup A
inst_2 : AddCommGroup B
inst_3 : AddCommGroup M
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective.{uA + 1, uM + 1} (α := A) (β := M) (⇑j : (a : A) → M)
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ ((↑(LinearEquiv.symm ULift.moduleEquiv) : B →ₗ[R] ULift.{max (max uA uB) uM, uB} B) ∘ₗ
        g ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uM} M →ₗ[R] M)) ∘ₗ
      (↑(LinearEquiv.symm ULift.moduleEquiv) : M →ₗ[R] ULift.{max (max uA uB) uM, uM} M) ∘ₗ
        f ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uB} B →ₗ[R] B) =
    LinearMap.id
have h₁ : ∀ (x : ULift.{max uA uM uB, uB} B),
  Eq.{uB + 1} (α := B)
    (ULift.down
      ((((↑(LinearEquiv.symm ULift.moduleEquiv) : B →ₗ[R] ULift.{max (max uA uB) uM, uB} B) ∘ₗ
              g ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uM} M →ₗ[R] M)) ∘ₗ
            (↑(LinearEquiv.symm ULift.moduleEquiv) : M →ₗ[R] ULift.{max (max uA uB) uM, uM} M) ∘ₗ
              f ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uB} B →ₗ[R] B) :
          (a : ULift.{max uA uM uB, uB} B) → ULift.{max uA uM uB, uB} B)
        x))
    (ULift.down ((LinearMap.id : (a : ULift.{max uA uM uB, uB} B) → ULift.{max uA uM uB, uB} B) x))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Biproducts (goal)
Goal:
R : Type u
A : Type uA
M : Type uM
B : Type uB
inst : Ring R
inst_1 : AddCommGroup A
inst_2 : AddCommGroup B
inst_3 : AddCommGroup M
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective.{uM + 1, uB + 1} (α := M) (β := B) (⇑g : (a : M) → B)
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ ((↑(LinearEquiv.symm ULift.moduleEquiv) : A →ₗ[R] ULift.{max (max uA uB) uM, uA} A) ∘ₗ
        f ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uM} M →ₗ[R] M)) ∘ₗ
      (↑(LinearEquiv.symm ULift.moduleEquiv) : M →ₗ[R] ULift.{max (max uA uB) uM, uM} M) ∘ₗ
        j ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uA} A →ₗ[R] A) =
    LinearMap.id
have h₁ : ∀ (x : ULift.{max uA uM uB, uA} A),
  Eq.{uA + 1} (α := A)
    (ULift.down
      ((((↑(LinearEquiv.symm ULift.moduleEquiv) : A →ₗ[R] ULift.{max (max uA uB) uM, uA} A) ∘ₗ
              f ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uM} M →ₗ[R] M)) ∘ₗ
            (↑(LinearEquiv.symm ULift.moduleEquiv) : M →ₗ[R] ULift.{max (max uA uB) uM, uM} M) ∘ₗ
              j ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uA} A →ₗ[R] A) :
          (a : ULift.{max uA uM uB, uA} A) → ULift.{max uA uM uB, uA} A)
        x))
    (ULift.down ((LinearMap.id : (a : ULift.{max uA uM uB, uA} A) → ULift.{max uA uM uB, uA} A) x))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
X Y : ModuleCat.{v, u₂} S
a₁ a₂ : X ⟶ Y
h : (restrictScalars f).map a₁ = (restrictScalars f).map a₂
⊢ a₁ = a₂
have hf : ∀ (x : (↑X : Type v)),
  Eq (α := (↑Y : Type v)) ((Hom.hom a₁ : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v))
    ((Hom.hom a₂ : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
X Y : ModuleCat.{v, u₂} S
x : X ⟶ Y
h : Mono x
⊢ Mono ((restrictScalars f).map x)
have rwa : ∀
  (h :
    Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u₂} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v)) (CC :=
            carrier) x) :
        (a : (↑X : Type v)) → (↑Y : Type v))),
  Function.Injective (α := (↑((restrictScalars f).obj X) : Type v)) (β := (↑((restrictScalars f).obj Y) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u₁} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) ((restrictScalars f).map x)) :
      (a : (↑((restrictScalars f).obj X) : Type v)) → (↑((restrictScalars f).obj Y) : Type v))
Tactic: rwa [mono_iff_injective] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f g : R →+* S
e : f = g
X : ModuleCat.{u_1, u₂} S
x : R
x_1 : (↑((restrictScalars f).obj X) : Type u_1)
⊢ Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) x_1)
have subst : Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) (x • x_1) =
  HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
    (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) x_1)
Tactic: subst e
Cleared hypotheses: g, e
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f g : R →+* S
e : f = g
X Y : ModuleCat.{u_1, u₂} S
x : X ⟶ Y
⊢ (restrictScalars f).map x ≫
      Iso.hom
        ((fun (X : ModuleCat.{u_1, u₂} S) ↦
            (LinearEquiv.toModuleIso
                (let __spread.0 :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                  AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
                { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ }) :
              Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
                (of R (↑((restrictScalars g).obj X) : Type u_1))))
          Y) =
    Iso.hom
        ((fun (X : ModuleCat.{u_1, u₂} S) ↦
            (LinearEquiv.toModuleIso
                (let __spread.0 :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                  AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
                { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃ₗ[R] (↑((restrictScalars g).obj X) : Type u_1) }) :
              Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
                (of R (↑((restrictScalars g).obj X) : Type u_1))))
          X) ≫
      (restrictScalars g).map x
have subst : (restrictScalars f).map x ≫
    Iso.hom
      ((fun (X : ModuleCat.{u_1, u₂} S) ↦
          (LinearEquiv.toModuleIso
              (let __spread.0 :
                (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
              { toFun := __spread.0.toFun, map_add' := sorry, map_smul' := sorry, invFun := __spread.0.invFun, left_inv := sorry,
                right_inv := sorry }) :
            Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
              (of R (↑((restrictScalars f).obj X) : Type u_1))))
        Y) =
  Iso.hom
      ((fun (X : ModuleCat.{u_1, u₂} S) ↦
          (LinearEquiv.toModuleIso
              (let __spread.0 :
                (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
              { toFun := __spread.0.toFun, map_add' := sorry, map_smul' := sorry, invFun := __spread.0.invFun, left_inv := sorry,
                right_inv := sorry :
                (↑((restrictScalars f).obj X) : Type u_1) ≃ₗ[R] (↑((restrictScalars f).obj X) : Type u_1) }) :
            Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
              (of R (↑((restrictScalars f).obj X) : Type u_1))))
        X) ≫
    (restrictScalars f).map x
Tactic: subst e
Cleared hypotheses: g, e
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
inst : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat.{u_1, u₁} R
r : R
x : (↑((restrictScalars f).obj M) : Type u_1)
⊢ (AddEquiv.refl (↑((restrictScalars f).obj M) : Type u_1) :
        (a : (↑((restrictScalars f).obj M) : Type u_1)) → (↑M : Type u_1))
      (r • x) =
    HSMul.hSMul (β := (↑M : Type u_1)) r
      ((AddEquiv.refl (↑((restrictScalars f).obj M) : Type u_1) :
            (a : (↑((restrictScalars f).obj M) : Type u_1)) → (↑M : Type u_1))
          x :
        (↑M : Type u_1))
have subst : ∀ (x : (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1)),
  (AddEquiv.refl (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1) :
        (a : (↑((restrictScalars (RingHom.id R)).obj M) : Type u_1)) → (↑M : Type u_1))
      (r • x) =
    HSMul.hSMul (β := (↑M : Type u_1)) r
      ((AddEquiv.refl (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1) :
            (a : (↑((restrictScalars (RingHom.id R)).obj M) : Type u_1)) → (↑M : Type u_1))
          x :
        (↑M : Type u_1))
Tactic: subst hf
Cleared hypotheses: f, hf, x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst : Ring R₁
inst_1 : Ring R₂
inst_2 : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M : ModuleCat.{u_1, u₃} R₃
r : R₁
x : (↑((restrictScalars gf).obj M) : Type u_1)
⊢ (AddEquiv.refl (↑((restrictScalars gf).obj M) : Type u_1) :
        (a : (↑((restrictScalars gf).obj M) : Type u_1)) →
          (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
      (r • x) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1)) r
      ((AddEquiv.refl (↑((restrictScalars gf).obj M) : Type u_1) :
            (a : (↑((restrictScalars gf).obj M) : Type u_1)) →
              (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
          x :
        (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
have subst : ∀ (x : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)),
  (AddEquiv.refl (↑((restrictScalars (g.comp f)).obj M) : Type u_1) :
        (a : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)) →
          (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
      (r • x) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1)) r
      ((AddEquiv.refl (↑((restrictScalars (g.comp f)).obj M) : Type u_1) :
            (a : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)) →
              (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
          x :
        (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
Tactic: subst hgf
Cleared hypotheses: gf, hgf, x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R₀ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Ring S
inst_3 : Algebra R₀ R
inst_4 : Algebra R₀ S
f : R →ₐ[R₀] S
M N : ModuleCat.{u_4, u_3} S
g : M ⟶ N
r₀ : R₀
⊢ (restrictScalars f.toRingHom).map (r₀ • g) = r₀ • (restrictScalars f.toRingHom).map g
have hf : ∀ (m : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)),
  Eq (α := (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
    ((Hom.hom ((restrictScalars f.toRingHom).map (r₀ • g)) :
          (a : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)) →
            (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
        m :
      (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
    ((Hom.hom (r₀ • (restrictScalars f.toRingHom).map g) :
          (a : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)) →
            (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
        m :
      (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
⊢ map' f (l₁₂ ≫ l₂₃) = map' f l₁₂ ≫ map' f l₂₃
have hf : ∀ (x : (↑(obj' f M₁) : Type (max u₂ v))),
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x y : TensorProduct.{u₁, u₂, v} R (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M₁ : Type v)
ihx :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
ihy :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
      (↑(obj' f M₃) : Type (max u₂ v)))
⊢ Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x + y) :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x + y) :
      (↑(obj' f M₃) : Type (max u₂ v)))
have hf : HAdd.hAdd (α := (↑(obj' f M₃) : Type (max u₂ v))) (β := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
      (↑(obj' f M₃) : Type (max u₂ v))) =
  HAdd.hAdd (α := (↑(obj' f M₃) : Type (max u₂ v))) (β := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
      (↑(obj' f M₃) : Type (max u₂ v)))
Tactic: erw [LinearMap.map_add, LinearMap.map_add]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x : (↑(obj' f M₁) : Type (max u₂ v))
⊢ Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
have hf : Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
  ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
  ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
Tactic: induction x using TensorProduct.induction_on with
  | zero => rfl
  | tmul => rfl
  | add _ _ ihx ihy => erw [LinearMap.map_add, LinearMap.map_add]; grind
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x : (↑(obj' f M₁) : Type (max u₂ v))
hf :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
⊢ Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
have hf₁ : ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑M₁ : Type v)),
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑(obj' f M₃) : Type (max u₂ v)))
Tactic: induction x using TensorProduct.induction_on with
  | zero => rfl
  | tmul => rfl
  | add _ _ ihx ihy => erw [LinearMap.map_add, LinearMap.map_add]; grind
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat.{v, u₁} R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x : (↑(obj' f M₁) : Type (max u₂ v))
hf :
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) 0)
hf₁ :
  ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑M₁ : Type v)),
    Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          (x ⊗ₜ[R] y) :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          (x ⊗ₜ[R] y) :
        (↑(obj' f M₃) : Type (max u₂ v)))
⊢ Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
      (↑(obj' f M₃) : Type (max u₂ v)))
have hf₂ : ∀ (x y : TensorProduct.{u₁, u₂, v} R (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M₁ : Type v))
  (ihx :
    Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) x :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          x :
        (↑(obj' f M₃) : Type (max u₂ v))))
  (ihy :
    Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v))) y :
        (↑(obj' f M₃) : Type (max u₂ v)))
      ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
          y :
        (↑(obj' f M₃) : Type (max u₂ v)))),
  Eq (α := (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f (l₁₂ ≫ l₂₃)) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x + y) :
      (↑(obj' f M₃) : Type (max u₂ v)))
    ((Hom.hom (map' f l₁₂ ≫ map' f l₂₃) : (a : (↑(obj' f M₁) : Type (max u₂ v))) → (↑(obj' f M₃) : Type (max u₂ v)))
        (x + y) :
      (↑(obj' f M₃) : Type (max u₂ v)))
Tactic: induction x using TensorProduct.induction_on with
  | zero => rfl
  | tmul => rfl
  | add _ _ ihx ihy => erw [LinearMap.map_add, LinearMap.map_add]; grind
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
⊢ α = β
have a : (restrictScalars f).map α = (restrictScalars f).map β
Tactic: apply (restrictScalars f).map_injective