awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
x y : (↑s.1 : Type (max v w))
⊢ (fun (j : J) ↦
      HAdd.hAdd (α := (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w))) (β :=
        (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w)))
        ((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)))
        ((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)))
            y :
          (↑(Functor.obj (Discrete.functor f) { as := j : Discrete J }) : Type (max v w)))) =
    HAdd.hAdd (α := (j : J) → (↑(f j) : 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 := 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)
      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)))
        y

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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))
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
⊢ (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

Tactic:
simp only [Functor.const_obj_obj, map_smul]

Premises used: CategoryTheory.Functor.const_obj_obj, map_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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) ↦
      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:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    Cone.pt (J := Discrete J) (F := Discrete.functor f)
      { pt := of R ((j : J) → (↑(f j) : Type (max v w))),
        π :=
          Discrete.natTrans fun (j : Discrete J) ↦
            ↟(LinearMap.proj (φ := fun (j : J) ↦ (↑(f j) : Type (max v w))) j.as) }
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := of R ((j : J) → (↑(f j) : Type (max v w))),
              π :=
                Discrete.natTrans fun (j : Discrete J) ↦
                  ↟(LinearMap.proj (φ := fun (j : J) ↦ (↑(f j) : Type (max v w))) j.as) })
          j =
      s.π.app j
x : (↑s.pt : Type (max v w))
j : J
⊢ Eq (α := (↑(f j) : Type (max v w)))
    ((Hom.hom m :
          (a : (↑s.pt : Type (max v w))) →
            (↑{ pt := of R ((j : J) → (↑(f j) : Type (max v w))),
                    π := Discrete.natTrans fun (j : Discrete J) ↦ ↟(LinearMap.proj j.as) }.pt :
              Type (max v w)))
        x j :
      (↑(f j) : Type (max v w)))
    ((Hom.hom (lift.{w, v, u} f s) :
          (a : (↑s.pt : Type (max v w))) →
            (↑{ pt := of R ((j : J) → (↑(f j) : Type (max v w))),
                    π := Discrete.natTrans fun (j : Discrete J) ↦ ↟(LinearMap.proj j.as) }.pt :
              Type (max v w)))
        x j :
      (↑(f j) : Type (max v w)))

Tactic:
congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Discrete.mk, congr_arg, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    Cone.pt (J := Discrete J) (F := Discrete.functor f)
      { pt := of R ((j : J) → (↑(f j) : Type (max v w))),
        π :=
          Discrete.natTrans fun (j : Discrete J) ↦
            ↟(LinearMap.proj (φ := fun (j : J) ↦ (↑(f j) : Type (max v w))) j.as) }
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := of R ((j : J) → (↑(f j) : Type (max v w))),
              π :=
                Discrete.natTrans fun (j : Discrete J) ↦
                  ↟(LinearMap.proj (φ := fun (j : J) ↦ (↑(f j) : Type (max v w))) j.as) })
          j =
      s.π.app j
x : (↑s.pt : Type (max v w))
j : J
⊢ Eq (α := (↑(f j) : Type (max v w)))
    ((Hom.hom m :
          (a : (↑s.pt : Type (max v w))) →
            (↑{ pt := of R ((j : J) → (↑(f j) : Type (max v w))),
                    π := Discrete.natTrans fun (j : Discrete J) ↦ ↟(LinearMap.proj j.as) }.pt :
              Type (max v w)))
        x j :
      (↑(f j) : Type (max v w)))
    ((Hom.hom (lift.{w, v, u} f s) :
          (a : (↑s.pt : Type (max v w))) →
            (↑{ pt := of R ((j : J) → (↑(f j) : Type (max v w))),
                    π := Discrete.natTrans fun (j : Discrete J) ↦ ↟(LinearMap.proj j.as) }.pt :
              Type (max v w)))
        x j :
      (↑(f j) : Type (max v w)))

Tactic:
exact congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Discrete.mk, congr_arg, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
J : Type
inst_1 : Finite J
f : J → ModuleCat.{v, u} R
j : J
⊢ CategoryStruct.comp (Y := ⨁ f) (Iso.inv (biproductIsoPi f) : of R ((j : J) → (↑(f j) : Type v)) ⟶ ⨁ f)
      (biproduct.π f j : ⨁ f ⟶ f j) =
    ↟(LinearMap.proj (φ := fun (j : J) ↦ (↑(f j) : Type v)) j)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk j)

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
A M B : Type v
inst : Ring R
inst_1 : AddCommGroup A
inst_2 : Module R A
inst_3 : AddCommGroup B
inst_4 : Module R B
inst_5 : AddCommGroup M
inst_6 : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : B →ₗ[R] M
hj : Function.Injective (α := A) (β := M) (⇑j : (a : A) → M)
exac : j.range = g.ker
h : g ∘ₗ f = LinearMap.id
⊢ Mono (ShortComplex.moduleCatMkOfKerLERange (↟j) (↟g) ⋯).f

Tactic:
simpa only [ModuleCat.mono_iff_injective]

Premises used: ModuleCat.mono_iff_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
A M B : Type v
inst : Ring R
inst_1 : AddCommGroup A
inst_2 : Module R A
inst_3 : AddCommGroup B
inst_4 : Module R B
inst_5 : AddCommGroup M
inst_6 : Module R M
j : A →ₗ[R] M
g : M →ₗ[R] B
f : M →ₗ[R] A
hg : Function.Surjective (α := M) (β := B) (⇑g : (a : M) → B)
exac : j.range = g.ker
h : f ∘ₗ j = LinearMap.id
⊢ Epi (ShortComplex.moduleCatMkOfKerLERange (↟j) (↟g) ⋯).g

Tactic:
simpa only [ModuleCat.epi_iff_surjective] using hg

Premises used: ModuleCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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
⊢ Function.Injective (α := ULift.{max uA uM uB, uA} A) (β := ULift.{max uA uM uB, uM} 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, uM} M)

Tactic:
simpa using hj
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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) : M →ₗ[R] ULift.{max (max uA uB) uM, uM} M) ∘ₗ
        j ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uA} A →ₗ[R] A)).range =
    ((↑(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)).ker

Tactic:
simp [LinearMap.range_comp, LinearMap.ker_comp, exac, Submodule.comap_equiv_eq_map_symm]

Premises used: Submodule.comap_equiv_eq_map_symm, LinearMap.range_comp, LinearMap.ker_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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
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))
⊢ ((↑(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

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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
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:
simpa using congr($h x.down)
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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
⊢ Function.Surjective (α := ULift.{max uA uM uB, uM} M) (β := ULift.{max uA uM uB, uB} B)
    (⇑((↑(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)) :
      (a : ULift.{max uA uM uB, uM} M) → ULift.{max uA uM uB, uB} B)

Tactic:
simpa using hg
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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) : M →ₗ[R] ULift.{max (max uA uB) uM, uM} M) ∘ₗ
        j ∘ₗ (↑ULift.moduleEquiv : ULift.{max (max uA uB) uM, uA} A →ₗ[R] A)).range =
    ((↑(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)).ker

Tactic:
simp [LinearMap.range_comp, LinearMap.ker_comp, exac, Submodule.comap_equiv_eq_map_symm]

Premises used: Submodule.comap_equiv_eq_map_symm, LinearMap.range_comp, LinearMap.ker_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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
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))
⊢ ((↑(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

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
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
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:
simpa using congr($h x.down)
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
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₂
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))
⊢ a₁ = a₂

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
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₂
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:
simpa only using DFunLike.congr_fun (ModuleCat.hom_ext_iff.mp h) x

Premises used: DFunLike.congr_fun, ModuleCat.hom_ext_iff, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
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
rwa rwa₁ rwa₂ 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))
⊢ Mono ((restrictScalars f).map x)

Tactic:
rwa [mono_iff_injective] at h ⊢

Premises used: ModuleCat.mono_iff_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
⊢ (restrictScalars f).ReflectsIsomorphisms

Tactic:
have : (restrictScalars f ⋙ CategoryTheory.forget (ModuleCat R)).ReflectsIsomorphisms :=
    inferInstanceAs (CategoryTheory.forget (ModuleCat S)).ReflectsIsomorphisms
  reflectsIsomorphisms_of_comp _ (CategoryTheory.forget _)

Premises used: ModuleCat, _private.0.ModuleCat.instReflectsIsomorphismsRestrictScalars._proof_1, ModuleCat.restrictScalars, CategoryTheory.forget, CategoryTheory.reflectsIsomorphisms_of_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M M' : ModuleCat.{v, u₂} S
g : M ⟶ M'
x : (↑((restrictScalars f).obj M) : Type v)
⊢ Eq (α := (↑((restrictScalars f).obj M') : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u₁} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) ((restrictScalars f).map g) :
          (a : (↑((restrictScalars f).obj M) : Type v)) → (↑((restrictScalars f).obj M') : Type v))
        x :
      (↑((restrictScalars f).obj M') : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u₂} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v)) (CC :=
            carrier) g :
          (a : (↑M : Type v)) → (↑M' : Type v))
        x :
      (↑M' : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M : ModuleCat.{v, u₂} S
r : R
m : (↑((restrictScalars f).obj M) : Type v)
⊢ r • m =
    HSMul.hSMul.{u₂, v, v} (α := S) (β := (↑M : Type v)) ((f : (a : R) → S) r : S)
      (have this := m;
      this)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M : ModuleCat.{v, u₂} S
r : R
m : (↑M : Type v)
⊢ HSMul.hSMul (β := (↑((restrictScalars f).obj M) : Type v)) r
      (have this := m;
      this) =
    HSMul.hSMul.{u₂, v, v} (α := S) ((f : (a : R) → S) r : S) m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : CommRing S
f : R →+* S
M : Type v
I : AddCommGroup M
inst_2 : Module S M
r : R
s : S
m : M
⊢ HSMul.hSMul.{u₂, v, v} (α := S) ((f : (a : R) → S) r : S) (s • m) =
    s • HSMul.hSMul.{u₂, v, v} (α := S) ((f : (a : R) → S) r : S) m

Tactic:
simp [← mul_smul, mul_comm]

Premises used: mul_comm, SemigroupAction.mul_smul