awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
C : Type ?u.445607
inst_10 : Ring C
inst_11 : Algebra R C
x y : 𝒜 ᵍ⊗[R] ℬ
dsimp :
  (LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
      ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
          (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) (x * y))) =
    HMul.hMul (α := ℬ ᵍ⊗[R] 𝒜) (β := ℬ ᵍ⊗[R] 𝒜)
      ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
          ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
              (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
            ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x)) :
        ℬ ᵍ⊗[R] 𝒜)
      ((LinearEquiv.symm (auxEquiv R ℬ 𝒜) : (a : (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) → ℬ ᵍ⊗[R] 𝒜)
          ((gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i) :
              (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
            ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) y)) :
        ℬ ᵍ⊗[R] 𝒜)
⊢ ((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i)) ≪≫ₗ LinearEquiv.symm (auxEquiv R ℬ 𝒜) :
        (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜)
      (x * y) =
    HMul.hMul (α := ℬ ᵍ⊗[R] 𝒜) (β := ℬ ᵍ⊗[R] 𝒜)
      (((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i)) ≪≫ₗ
              LinearEquiv.symm (auxEquiv R ℬ 𝒜) :
            (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜)
          x :
        ℬ ᵍ⊗[R] 𝒜)
      (((auxEquiv R 𝒜 ℬ ≪≫ₗ gradedComm R (fun (i : ι) ↦ ↥(𝒜 i)) fun (i : ι) ↦ ↥(ℬ i)) ≪≫ₗ
              LinearEquiv.symm (auxEquiv R ℬ 𝒜) :
            (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜)
          y :
        ℬ ᵍ⊗[R] 𝒜)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
⊢ Eq (α := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    ((auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        ((comm 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜) x) :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    ((gradedComm R (fun (x : ι) ↦ ↥(𝒜 x)) fun (x : ι) ↦ ↥(ℬ x) :
          (a : (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        ((auxEquiv R 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → (⨁ (i : ι), ↥(𝒜 i)) ⊗[R] ⨁ (i : ι), ↥(ℬ i)) x) :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))

Tactic:
LinearEquiv.eq_symm_apply _ |>.mp rfl

Premises used: LinearEquiv.eq_symm_apply, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
simp_rw :
  HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
              (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
            b ⊗ₜ[R]
          ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            a :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
    (auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (HSMul.hSMul (α := R) (β := ℬ ᵍ⊗[R] 𝒜) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
        ((↑b : B) ᵍ⊗ₜ[R] (↑a : A)))
⊢ Eq (α := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    ((auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        ((comm 𝒜 ℬ : (a : 𝒜 ᵍ⊗[R] ℬ) → ℬ ᵍ⊗[R] 𝒜) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B))) :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
    ((auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
        (HSMul.hSMul (β := ℬ ᵍ⊗[R] 𝒜) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((↑b : B) ᵍ⊗ₜ[R] (↑a : A))) :
      (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))

Tactic:
simp_rw [auxEquiv_comm, auxEquiv_tmul, decompose_coe, ← lof_eq_of R, gradedComm_of_tmul_of,
      @Units.smul_def _ _ (_) (_), ← Int.cast_smul_eq_zsmul R]

Premises used: GradedTensorProduct.auxEquiv_comm, DirectSum.lof_eq_of, GradedTensorProduct.auxEquiv_tmul, Units.smul_def, DirectSum.decompose_coe, TensorProduct.gradedComm_of_tmul_of, Int.cast_smul_eq_zsmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
rw :
  HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
              (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
            b ⊗ₜ[R]
          ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            a :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
    HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) (↑b : B) ⊗ₜ[R] (decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
⊢ HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
              (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
            b ⊗ₜ[R]
          ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            a :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
    (auxEquiv R ℬ 𝒜 : (a : ℬ ᵍ⊗[R] 𝒜) → (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (HSMul.hSMul (α := R) (β := ℬ ᵍ⊗[R] 𝒜) (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
        ((↑b : B) ᵍ⊗ₜ[R] (↑a : A)))

Tactic:
rw [LinearEquiv.map_smul, auxEquiv_tmul]

Premises used: GradedTensorProduct.auxEquiv_tmul, LinearEquiv.map_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
simp_rw :
  HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
              (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
            b ⊗ₜ[R]
          ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            a :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
    HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((DirectSum.of.{u_2, u_4} (fun (i : ι) ↦ ↥(ℬ i)) j : ↥(ℬ j) →+ ⨁ (i : ι), ↥(ℬ i)) :
              (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
            b ⊗ₜ[R]
          ((DirectSum.of.{u_2, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            a :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
⊢ HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      (((lof.{u_1, u_2, u_4} R ι (fun (x : ι) ↦ ↥(ℬ x)) j : ↥(ℬ j) →ₗ[R] ⨁ (i : ι), ↥(ℬ i)) :
              (a : ↥(ℬ j)) → ⨁ (i : ι), ↥(ℬ i))
            b ⊗ₜ[R]
          ((lof.{u_1, u_2, u_3} R ι (fun (x : ι) ↦ ↥(𝒜 x)) i : ↥(𝒜 i) →ₗ[R] ⨁ (i : ι), ↥(𝒜 i)) :
              (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            a :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i)) =
    HSMul.hSMul (α := R) (β := (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))
      (↑(↑(HPow.hPow (α := ℤˣ) (-1) (j * i)) : ℤ) : R)
      ((decompose ℬ : (a : B) → ⨁ (i : ι), ↥(ℬ i)) (↑b : B) ⊗ₜ[R] (decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) :
        (⨁ (i : ι), ↥(ℬ i)) ⊗[R] ⨁ (i : ι), ↥(𝒜 i))

Tactic:
simp_rw [decompose_coe, lof_eq_of]

Premises used: DirectSum.lof_eq_of, DirectSum.decompose_coe
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
m : M
n : N
⊢ Eq (α := M₂ ⊗[R₂] N₂) ((map f g : (a : M ⊗[R] N) → M₂ ⊗[R₂] N₂) (m ⊗ₜ[R] n) : M₂ ⊗[R₂] N₂)
    ((f : (a : M) → M₂) m ⊗ₜ[R₂] (g : (a : N) → N₂) n : M₂ ⊗[R₂] N₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ map f g ∘ₛₗ (↑(TensorProduct.comm R N M) : N ⊗[R] M →ₗ[R] M ⊗[R] N) =
    (↑(TensorProduct.comm R₂ N₂ M₂) : N₂ ⊗[R₂] M₂ →ₗ[R₂] M₂ ⊗[R₂] N₂) ∘ₛₗ map g f

Tactic:
ext rfl

Premises used: TensorProduct.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
R₂ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid N₂
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R₂ M₂
inst_9 : Module R₂ N₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
x : N ⊗[R] M
⊢ Eq (α := M₂ ⊗[R₂] N₂)
    ((map f g : (a : M ⊗[R] N) → M₂ ⊗[R₂] N₂) ((TensorProduct.comm R N M : (a : N ⊗[R] M) → M ⊗[R] N) x) : M₂ ⊗[R₂] N₂)
    ((TensorProduct.comm R₂ N₂ M₂ : (a : N₂ ⊗[R₂] M₂) → M₂ ⊗[R₂] N₂) ((map g f : (a : N ⊗[R] M) → N₂ ⊗[R₂] M₂) x) :
      M₂ ⊗[R₂] N₂)

Tactic:
DFunLike.congr_fun (map_comp_comm_eq _ _) _

Premises used: DFunLike.congr_fun, TensorProduct.map_comp_comm_eq, Quotient.liftOn', AddCon.liftOn
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
simp_rw : Submodule.map₂ (compr₂ (mk R M N) (map f g)) ⊤ ⊤ = Submodule.map₂ (compl₁₂ (mk R P Q) f g) ⊤ ⊤
⊢ (map f g).range = Submodule.map₂ (mk R P Q) f.range g.range

Tactic:
simp_rw [← Submodule.map_top, Submodule.map₂_map_map, ← map₂_mk_top_top_eq_top,
    Submodule.map_map₂]

Premises used: Submodule.map_top, TensorProduct.map₂_mk_top_top_eq_top, Submodule.map_map₂, Submodule.map₂_map_map
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ Submodule.map₂ (compr₂ (mk R M N) (map f g)) ⊤ ⊤ = Submodule.map₂ (compl₁₂ (mk R P Q) f g) ⊤ ⊤

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
simp :
  Eq (α := Submodule R (P ⊗[R] Q))
    (Submodule.span R
      (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
        {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}))
    (Submodule.span R {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t})
⊢ (map f g).range =
    Submodule.span R {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t}

Tactic:
simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span]

Premises used: TensorProduct.span_tmul_eq_top, Submodule.map_top, Submodule.map_span
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
e_s :
  Eq (α := Set (P ⊗[R] Q))
    (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
      {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t}
⊢ Eq (α := Submodule R (P ⊗[R] Q))
    (Submodule.span R
      (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
        {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t}))
    (Submodule.span R {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t})

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
e_s :
  ∀ (t : P ⊗[R] Q),
    Membership.mem (γ := Set (P ⊗[R] Q))
        (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
          {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
        t ↔
      Membership.mem (γ := Set (P ⊗[R] Q))
        {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t} t
⊢ Eq (α := Set (P ⊗[R] Q))
    (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
      {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
    {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t}

Tactic:
ext t
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
t : P ⊗[R] Q
⊢ Membership.mem (γ := Set (P ⊗[R] Q))
      (Set.image (α := M ⊗[R] N) (⇑(map f g) : (a : M ⊗[R] N) → P ⊗[R] Q)
        {t : M ⊗[R] N | ∃ (m : M) (n : N), m ⊗ₜ[R] n = t})
      t ↔
    Membership.mem (γ := Set (P ⊗[R] Q))
      {t : P ⊗[R] Q | ∃ (m : M) (n : N), (f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n = t} t

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid P
inst_2 : AddCommMonoid Q
inst_3 : Module R P
inst_4 : Module R Q
p : Submodule R P
q : Submodule R Q
simp_rw : (map p.subtype q.subtype).range = Submodule.map₂ (mk R P Q) p q
simp_rw₁ : Submodule.map₂ (mk R P Q) p.subtype.range q.subtype.range = Submodule.map₂ (mk R P Q) p q
⊢ (mapIncl p q).range = Submodule.map₂ (mk R P Q) p q

Tactic:
simp_rw [mapIncl, range_map, Submodule.range_subtype]

Premises used: TensorProduct.range_map, TensorProduct.mapIncl, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
f : P →ₗ[R] Q →ₗ[R] M
p : Submodule R P
q : Submodule R Q
simp_rw : Submodule.map₂ f p q = Submodule.map₂ (compr₂ (mk R P Q) (lift f)) p q
⊢ Submodule.map₂ f p q = (lift f ∘ₗ mapIncl p q).range

Tactic:
simp_rw [LinearMap.range_comp, range_mapIncl, Submodule.map_map₂]

Premises used: TensorProduct.range_mapIncl, LinearMap.range_comp, Submodule.map_map₂
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
f : P →ₗ[R] Q →ₗ[R] M
p : Submodule R P
q : Submodule R Q
⊢ Submodule.map₂ f p q = Submodule.map₂ (compr₂ (mk R P Q) (lift f)) p q

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
M : Type u_7
N : Type u_8
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₃
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R₂ M₂
inst_12 : Module R₂ N₂
inst_13 : Module R₃ M₃
inst_14 : Module R₃ N₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f₂ : M₂ →ₛₗ[σ₂₃] M₃
g₂ : N₂ →ₛₗ[σ₂₃] N₃
f₁ : M →ₛₗ[σ₁₂] M₂
g₁ : N →ₛₗ[σ₁₂] N₂
⊢ map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) = map f₂ g₂ ∘ₛₗ map f₁ g₁

Tactic:
ext' fun _ _ => rfl

Premises used: TensorProduct.ext', rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
M : Type u_7
N : Type u_8
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₃
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R₂ M₂
inst_12 : Module R₂ N₂
inst_13 : Module R₃ M₃
inst_14 : Module R₃ N₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f₂ : M₂ →ₛₗ[σ₂₃] M₃
g₂ : N₂ →ₛₗ[σ₂₃] N₃
f₁ : M →ₛₗ[σ₁₂] M₂
g₁ : N →ₛₗ[σ₁₂] N₂
x : M ⊗[R] N
⊢ Eq (α := M₃ ⊗[R₃] N₃)
    ((map f₂ g₂ : (a : M₂ ⊗[R₂] N₂) → M₃ ⊗[R₃] N₃) ((map f₁ g₁ : (a : M ⊗[R] N) → M₂ ⊗[R₂] N₂) x) : M₃ ⊗[R₃] N₃)
    ((map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) : (a : M ⊗[R] N) → M₃ ⊗[R₃] N₃) x : M₃ ⊗[R₃] N₃)

Tactic:
DFunLike.congr_fun (map_comp ..).symm x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, TensorProduct.map_comp, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₃
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R N₂
inst_12 : Module R N₃
a : M →ₗ[R] M₂
b : M₃ →ₗ[R] M₂
c : N →ₗ[R] N₂
d : N₃ →ₗ[R] N₂
hab : a.range ≤ b.range
hcd : c.range ≤ d.range
simp_rw : Submodule.map₂ (mk R M₂ N₂) a.range c.range ≤ Submodule.map₂ (mk R M₂ N₂) b.range d.range
⊢ (map a c).range ≤ (map b d).range

Tactic:
simp_rw [range_map]

Premises used: TensorProduct.range_map
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₃
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R N₂
inst_12 : Module R N₃
a : M →ₗ[R] M₂
b : M₃ →ₗ[R] M₂
c : N →ₗ[R] N₂
d : N₃ →ₗ[R] N₂
hab : a.range ≤ b.range
hcd : c.range ≤ d.range
⊢ Submodule.map₂ (mk R M₂ N₂) a.range c.range ≤ Submodule.map₂ (mk R M₂ N₂) b.range d.range

Tactic:
Submodule.map₂_le_map₂ hab hcd

Premises used: Submodule.map₂_le_map₂, Set.Mem, setOf
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_7
N : Type u_8
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid N₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₃
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R N₂
inst_12 : Module R N₃
a : M →ₗ[R] M₂
b : M₃ →ₗ[R] M₂
c : N →ₗ[R] N₂
d : N₃ →ₗ[R] N₂
hab : a.range ≤ b.range
hcd : c.range ≤ d.range
⊢ Submodule.map₂ (mk R M₂ N₂) a.range c.range ≤ Submodule.map₂ (mk R M₂ N₂) b.range d.range

Tactic:
exact Submodule.map₂_le_map₂ hab hcd

Premises used: Submodule.map₂_le_map₂
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid P
inst_2 : AddCommMonoid Q
inst_3 : Module R P
inst_4 : Module R Q
p p' : Submodule R P
q q' : Submodule R Q
hp : p ≤ p'
hq : q ≤ q'
⊢ p.subtype.range ≤ p'.subtype.range

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_9
Q : Type u_10
inst_1 : AddCommMonoid P
inst_2 : AddCommMonoid Q
inst_3 : Module R P
inst_4 : Module R Q
p p' : Submodule R P
q q' : Submodule R Q
hp : p ≤ p'
hq : q ≤ q'
⊢ q.subtype.range ≤ q'.subtype.range

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.TensorProduct.Map
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
P₃ : Type u_18
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid N₂
inst_7 : AddCommMonoid P₃
inst_8 : Module R M
inst_9 : Module R N
inst_10 : Module R₂ M₂
inst_11 : Module R₂ N₂
inst_12 : Module R₃ P₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
i : M₂ →ₛₗ[σ₂₃] N₂ →ₛₗ[σ₂₃] P₃
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ lift i ∘ₛₗ map f g = lift ((i ∘ₛₗ f).compl₂ g)

Tactic:
ext' fun _ _ => rfl

Premises used: TensorProduct.ext', rfl