awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
m : Submodule R M
n : Submodule R N
x : M ⧸ m
x_1 : N
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    ((((AlgebraTensorModule.curry
                    ((LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).liftQ
                        (map m.mkQ n.mkQ) ⋯ ∘ₗ
                      lift
                        (m.liftQ
                          (LinearMap.flip
                            (n.liftQ
                              (LinearMap.compr₂ (LinearMap.flip (mk R M N))
                                (LinearMap.range (map m.subtype LinearMap.id) ⊔
                                    LinearMap.range (map LinearMap.id n.subtype)).mkQ)
                              ⋯))
                          ⋯)) :
                  M ⧸ m →ₗ[R] N ⧸ n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                (a : M ⧸ m) → N ⧸ n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
              x ∘ₗ
            n.mkQ :
          (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
        x_1 :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    ((((AlgebraTensorModule.curry LinearMap.id :
                  M ⧸ m →ₗ[R] N ⧸ n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                (a : M ⧸ m) → N ⧸ n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
              x ∘ₗ
            n.mkQ :
          (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
        x_1 :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
have a : Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
  (((LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).liftQ
          (map m.mkQ n.mkQ) sorry :
        (a : M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range) → (M ⧸ m) ⊗[R] (N ⧸ n))
      ((((m.liftQ
                  (LinearMap.flip
                    (n.liftQ
                      (LinearMap.compr₂ (LinearMap.flip (mk R M N))
                        (LinearMap.range (map m.subtype LinearMap.id) ⊔
                            LinearMap.range (map LinearMap.id n.subtype)).mkQ)
                      sorry))
                  sorry :
                (a : M ⧸ m) →
                  N ⧸ n →ₗ[R] M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
              x :
            N ⧸ n →ₗ[R]
              M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
          (a : N ⧸ n) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
        (Submodule.Quotient.mk x_1)) :
    TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
  (x ⊗ₜ[R] Submodule.Quotient.mk x_1 : TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
I : Ideal R
⊢ Submodule.map (M := R ⊗[R] M) (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M)
      (LinearMap.range (map (Submodule.subtype I) LinearMap.id)) =
    HSMul.hSMul (β := Submodule R M) I ⊤
have rw : Eq (α := Submodule R M)
  (LinearMap.range (M := TensorProduct.{u_1, u_1, u_2} R ↥I ↥⊤)
    (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
      (↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv) : ↥I ⊗[R] ↥⊤ →ₗ[R] ↥I ⊗[R] M)))
  (LinearMap.range (M := TensorProduct.{u_1, u_1, u_2} R ↥I ↥⊤) (lift (LinearMap.lsmul R M) ∘ₗ mapIncl I ⊤))
Tactic: rw [← LinearMap.range_comp, ← (Submodule.topEquiv.lTensor I).range_comp, Submodule.smul_eq_map₂,
      map₂_eq_range_lift_comp_mapIncl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
x : M
⊢ Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    ((quotTensorEquivQuotSMul M I : (a : (R ⧸ I) ⊗[R] M) → M ⧸ I • ⊤) (1 ⊗ₜ[R] x) :
      M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    (Submodule.Quotient.mk x : M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
have rw : Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) (Submodule.Quotient.mk (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x))
  (Submodule.Quotient.mk x)
Tactic: rw [← RingHom.map_one (Ideal.Quotient.mk I), TensorProduct.quotTensorEquivQuotSMul_mk_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
⊢ Eq (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (Submodule.span A
      {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x})
have refine_1 : {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x} ⊆
  (↑(LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N)) : Set (M ⊗[R] N))
Tactic: refine (Submodule.span_eq_of_le (mapOfCompatibleSMul A R A M N).ker ?_ ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
refine_1 :
  {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x} ⊆
    (↑(LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N)) : Set (M ⊗[R] N))
⊢ Eq (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (Submodule.span A
      {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x})
have refine_2 : LE.le (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
  (Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x})
Tactic: refine (Submodule.span_eq_of_le (mapOfCompatibleSMul A R A M N).ker ?_ ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
m : M
a : A
n : N
⊢ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] (a • n)) =
    HSMul.hSMul (α := A) (β := M ⊗[R] N ⧸ S) ((RingHom.id A : (a : A) → A) a : A)
      ((S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n) : M ⊗[R] N ⧸ S)
have rw : HSMul.hSMul (β := M ⊗[R] N) a (m ⊗ₜ[R] n) - m ⊗ₜ[R] (a • n) ∈ S
Tactic: rw [Submodule.mkQ_apply, Submodule.mkQ_apply, ← Submodule.Quotient.mk_smul, eq_comm,
            Submodule.Quotient.eq, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
x x_1 : M
⊢ { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) ((x + x_1) ⊗ₜ[R] n), map_add' := ⋯,
      map_smul' := ⋯ } =
    HAdd.hAdd (α := N →ₗ[A] M ⊗[R] N ⧸ S)
      { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ :
        N →ₗ[A] M ⊗[R] N ⧸ S }
      { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x_1 ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ :
        N →ₗ[A] M ⊗[R] N ⧸ S }
have h : ∀ (x_2 : N),
  Eq (α := M ⊗[R] N ⧸ S)
    (({ toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) ((x + x_1) ⊗ₜ[R] n), map_add' := sorry,
            map_smul' := sorry } :
          (a : N) → M ⊗[R] N ⧸ S)
        x_2 :
      M ⊗[R] N ⧸ S)
    ((HAdd.hAdd (α := N →ₗ[A] M ⊗[R] N ⧸ S)
            { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x ⊗ₜ[R] n), map_add' := sorry,
              map_smul' := sorry : N →ₗ[A] M ⊗[R] N ⧸ S }
            { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x_1 ⊗ₜ[R] n), map_add' := sorry,
              map_smul' := sorry : N →ₗ[A] M ⊗[R] N ⧸ S } :
          (a : N) → M ⊗[R] N ⧸ S)
        x_2 :
      M ⊗[R] N ⧸ S)
Tactic: ext _
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
x : A
x_1 : M
⊢ { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) ((x • x_1) ⊗ₜ[R] n), map_add' := ⋯,
      map_smul' := ⋯ } =
    HSMul.hSMul (α := A) (β := N →ₗ[A] M ⊗[R] N ⧸ S) ((RingHom.id A : (a : A) → A) x : A)
      { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (x_1 ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ :
        N →ₗ[A] M ⊗[R] N ⧸ S }
have simp : { toFun := fun (n : N) ↦ Submodule.Quotient.mk ((x • x_1) ⊗ₜ[R] n), map_add' := sorry, map_smul' := sorry } =
  HSMul.hSMul (β := N →ₗ[A] M ⊗[R] N ⧸ S) x
    { toFun := fun (n : N) ↦ Submodule.Quotient.mk (x_1 ⊗ₜ[R] n), map_add' := sorry, map_smul' := sorry : N →ₗ[A] M ⊗[R] N ⧸ S }
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
⊢ F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
have a : ∀ (x : M) (x_1 : N),
  Eq (α := M ⊗[R] N ⧸ S)
    (((((curry (F ∘ₗ mapOfCompatibleSMul A R A M N) : M →ₗ[A] N →ₗ[R] M ⊗[R] N ⧸ S) : (a : M) → N →ₗ[R] M ⊗[R] N ⧸ S)
              x :
            N →ₗ[R] M ⊗[R] N ⧸ S) :
          (a : N) → M ⊗[R] N ⧸ S)
        x_1 :
      M ⊗[R] N ⧸ S)
    (((((curry S.mkQ : M →ₗ[A] N →ₗ[R] M ⊗[R] N ⧸ S) : (a : M) → N →ₗ[R] M ⊗[R] N ⧸ S) x : N →ₗ[R] M ⊗[R] N ⧸ S) :
          (a : N) → M ⊗[R] N ⧸ S)
        x_1 :
      M ⊗[R] N ⧸ S)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
⊢ LE.le (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (Submodule.span A
      {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x})
have h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
Tactic: have h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ := by ext; simp [S, F]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    {
      toFun := fun (m : M) ↦
        { toFun := fun (n : N) ↦ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N) ≤ S
have refine_2 : LE.le (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
  (LinearMap.ker (F ∘ₗ mapOfCompatibleSMul A R A M N))
Tactic: rw [← Submodule.ker_mkQ S, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q g)) (range (lTensor Q g.range.subtype))
have this : g = g.range.subtype ∘ₗ g.rangeRestrict
Tactic: have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q g)) (range (lTensor Q g.range.subtype))
have nth_rewrite : Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q (g.range.subtype ∘ₗ g.rangeRestrict)))
  (range (lTensor Q g.range.subtype))
Tactic: nth_rewrite 1 [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q (g.range.subtype ∘ₗ g.rangeRestrict)))
    (range (lTensor Q g.range.subtype))
have rw : Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q g.range.subtype ∘ₗ lTensor Q g.rangeRestrict))
  (range (lTensor Q g.range.subtype))
Tactic: rw [lTensor_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Eq (α := Submodule R (Q ⊗[R] P)) (range (lTensor Q g.range.subtype ∘ₗ lTensor Q g.rangeRestrict))
    (range (lTensor Q g.range.subtype))
have hf : Eq (α := Submodule R (TensorProduct.{u_1, u_5, u_4} R Q ↥g.range)) (range (lTensor Q g.rangeRestrict)) ⊤
Tactic: apply range_comp_of_range_eq_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Eq (α := Submodule R (TensorProduct.{u_1, u_5, u_4} R Q ↥g.range)) (range (lTensor Q g.rangeRestrict)) ⊤
have hf : Function.Surjective (α := Q ⊗[R] N) (β := TensorProduct.{u_1, u_5, u_4} R Q ↥g.range)
  (⇑(lTensor Q g.rangeRestrict) : (a : Q ⊗[R] N) → Q ⊗[R] ↥g.range)
Tactic: rw [range_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective (α := Q ⊗[R] N) (β := TensorProduct.{u_1, u_5, u_4} R Q ↥g.range)
    (⇑(lTensor Q g.rangeRestrict) : (a : Q ⊗[R] N) → Q ⊗[R] ↥g.range)
have hf : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := ↥g.range) (⇑g.rangeRestrict : (a : N) → ↥g.range)
Tactic: apply lTensor_surjective
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := ↥g.range) (⇑g.rangeRestrict : (a : N) → ↥g.range)
have hf : Eq (α := Submodule R ↥g.range) (range g.rangeRestrict) ⊤
Tactic: rw [← range_eq_top, range_rangeRestrict]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
this : g = g.range.subtype ∘ₗ g.rangeRestrict
hf : Eq (α := Submodule R ↥g.range) (range g.rangeRestrict) ⊤
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := ↥g.range) (⇑g.rangeRestrict : (a : N) → ↥g.range)
have hf₁ : Eq.{u_4 + 1} (α := Submodule R ↥g.range) ⊤ ⊤
Tactic: rw [← range_eq_top, range_rangeRestrict]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
A : Type u_6
inst_5 : Semiring A
inst_6 : Algebra R A
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ Function.Surjective (α := A ⊗[R] N) (β := A ⊗[R] P) (⇑(baseChange A g) : (a : A ⊗[R] N) → A ⊗[R] P)
have rw : Function.Surjective (α := A ⊗[R] N) (β := A ⊗[R] P) (⇑(lTensor A g) : (a : A ⊗[R] N) → A ⊗[R] P)
Tactic: rw [LinearMap.baseChange_eq_ltensor]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
p : P
q : Q
⊢ ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (p ⊗ₜ[R] q : P ⊗[R] Q)
have tmul : ∀ (n : N),
  ∃ (a : N ⊗[R] Q),
    Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) ((g : (a : N) → P) n ⊗ₜ[R] q : P ⊗[R] Q)
Tactic: obtain ⟨n, rfl⟩ := hg p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x y : P ⊗[R] Q
hx : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = x
hy : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = y
⊢ ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = x + y
have add : ∀ (x : N ⊗[R] Q),
  ∃ (a : N ⊗[R] Q),
    (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a =
      HAdd.hAdd (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) x : P ⊗[R] Q) y
Tactic: obtain ⟨x, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
y : P ⊗[R] Q
hy : ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = y
x : N ⊗[R] Q
⊢ ∃ (a : N ⊗[R] Q),
    (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a =
      HAdd.hAdd (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) x : P ⊗[R] Q) y
have add : ∀ (y : N ⊗[R] Q),
  ∃ (a : N ⊗[R] Q),
    (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a =
      HAdd.hAdd (α := P ⊗[R] Q) (β := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) x : P ⊗[R] Q)
        ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) y : P ⊗[R] Q)
Tactic: obtain ⟨y, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
z : P ⊗[R] Q
⊢ ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = z
have zero : ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (0 : P ⊗[R] Q)
Tactic: induction z with
  | zero => exact ⟨0, map_zero _⟩
  | tmul p q =>
    obtain ⟨n, rfl⟩ := hg p
    exact ⟨n ⊗ₜ[R] q, rfl⟩
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.RightExactness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R N
inst_5 : Module R P
inst_6 : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
z : P ⊗[R] Q
zero : ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (0 : P ⊗[R] Q)
⊢ ∃ (a : N ⊗[R] Q), (rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a = z
have tmul : ∀ (p : P) (q : Q),
  ∃ (a : N ⊗[R] Q), Eq (α := P ⊗[R] Q) ((rTensor Q g : (a : N ⊗[R] Q) → P ⊗[R] Q) a : P ⊗[R] Q) (p ⊗ₜ[R] q : P ⊗[R] Q)
Tactic: induction z with
  | zero => exact ⟨0, map_zero _⟩
  | tmul p q =>
    obtain ⟨n, rfl⟩ := hg p
    exact ⟨n ⊗ₜ[R] q, rfl⟩
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩
Cleared hypotheses: z