awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
change : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
⊢ motive ((↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M).toFun y)

Tactic:
change motive (TensorProduct.lift f y)

Premises used: TensorProduct.lift, DFunLike.coe
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
zero₁ zero₂ zero₃ zero₄ : motive 0
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) 0)

Tactic:
rwa [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x : M₁
y : M₂
tmul₁ : motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y))

Tactic:
rw [TensorProduct.lift.tmul]

Premises used: TensorProduct.lift.tmul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x : M₁
y : M₂
⊢ motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)

Tactic:
apply tmul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x y : M₁ ⊗[R] M₂
h_1 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x)
h_2 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
add₁ :
  motive
    (HAdd.hAdd (α := M) (β := M) ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x : M)
      ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y : M))
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x + y))

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x y : M₁ ⊗[R] M₂
h_1 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x)
h_2 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
add₁ : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x)
add₂ : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
⊢ motive
    (HAdd.hAdd (α := M) (β := M) ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x : M)
      ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y : M))

Tactic:
apply add
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x y : M₁ ⊗[R] M₂
h_1 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x)
h_2 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x)

Tactic:
assumption
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x y : M₁ ⊗[R] M₂
h_1 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x)
h_2 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)

Tactic:
assumption
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
zero₁ : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) 0)
tmul₁ : ∀ (x : M₁) (y : M₂), motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y))
add₁ :
  ∀ (x y : M₁ ⊗[R] M₂),
    motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x) →
      motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y) →
        motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x + y))
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)

Tactic:
induction y with
  | zero => rwa [map_zero]
  | tmul _ _ =>
    rw [TensorProduct.lift.tmul]
    apply tmul
  | add _ _ _ _ =>
    rw [map_add]
    apply add <;> assumption

Premises used: map_zero, map_add, TensorProduct.lift.tmul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he :
  ∀ (x : M₁) (y : M₂),
    Eq.{u_4 + 1} (α := M) ((e : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y) : M)
      ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
a :
  ∀ (x : M₁) (y : M₂),
    Eq.{u_4 + 1} (α := M)
      (((((AlgebraTensorModule.curry (TensorProduct.lift f) : M₁ →ₗ[R] M₂ →ₗ[R] M) : (a : M₁) → M₂ →ₗ[R] M) x :
              M₂ →ₗ[R] M) :
            (a : M₂) → M)
          y :
        M)
      (((((AlgebraTensorModule.curry (↑e : M₁ ⊗[R] M₂ →ₗ[R] M) : M₁ →ₗ[R] M₂ →ₗ[R] M) : (a : M₁) → M₂ →ₗ[R] M) x :
              M₂ →ₗ[R] M) :
            (a : M₂) → M)
          y :
        M)
⊢ TensorProduct.lift f = (↑e : M₁ ⊗[R] M₂ →ₗ[R] M)

Tactic:
ext x y
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he :
  ∀ (x : M₁) (y : M₂),
    Eq.{u_4 + 1} (α := M) ((e : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y) : M)
      ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
x : M₁
y : M₂
⊢ Eq.{u_4 + 1} (α := M)
    (((((AlgebraTensorModule.curry (TensorProduct.lift f) : M₁ →ₗ[R] M₂ →ₗ[R] M) : (a : M₁) → M₂ →ₗ[R] M) x :
            M₂ →ₗ[R] M) :
          (a : M₂) → M)
        y :
      M)
    (((((AlgebraTensorModule.curry (↑e : M₁ ⊗[R] M₂ →ₗ[R] M) : M₁ →ₗ[R] M₂ →ₗ[R] M) : (a : M₁) → M₂ →ₗ[R] M) x :
            M₂ →ₗ[R] M) :
          (a : M₂) → M)
        y :
      M)

Tactic:
simp [he]
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he :
  ∀ (x : M₁) (y : M₂),
    Eq.{u_4 + 1} (α := M) ((e : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y) : M)
      ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
⊢ TensorProduct.lift f = (↑e : M₁ ⊗[R] M₂ →ₗ[R] M)

Tactic:
have : TensorProduct.lift f = e := by
    ext x y
    simp [he]
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he :
  ∀ (x : M₁) (y : M₂),
    Eq.{u_4 + 1} (α := M) ((e : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y) : M)
      ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
this : TensorProduct.lift f = (↑e : M₁ ⊗[R] M₂ →ₗ[R] M)
⊢ IsTensorProduct f

Tactic:
simpa [IsTensorProduct, this] using e.bijective

Premises used: LinearEquiv.bijective, IsTensorProduct
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_7 : AddCommMonoid N₁
inst_8 : AddCommMonoid N₂
inst_9 : AddCommMonoid N
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
P₁ : Type u_9
P₂ : Type u_10
P : Type u_11
inst_13 : AddCommMonoid P₁
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid P
inst_16 : Module R P₁
inst_17 : Module R P₂
inst_18 : Module R P
p : P₁ →ₗ[R] P₂ →ₗ[R] P
hf : IsTensorProduct f
hg : IsTensorProduct g
hp : IsTensorProduct p
i₁ : N₁ →ₗ[R] P₁
j₁ : M₁ →ₗ[R] N₁
i₂ : N₂ →ₗ[R] P₂
j₂ : M₂ →ₗ[R] N₂
x : M
⊢ Eq.{u_11 + 1} (α := P) ((hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) : (a : M) → P) 0 : P)
    ((hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂ : (a : M) → P) 0 : P)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_7 : AddCommMonoid N₁
inst_8 : AddCommMonoid N₂
inst_9 : AddCommMonoid N
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
P₁ : Type u_9
P₂ : Type u_10
P : Type u_11
inst_13 : AddCommMonoid P₁
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid P
inst_16 : Module R P₁
inst_17 : Module R P₂
inst_18 : Module R P
p : P₁ →ₗ[R] P₂ →ₗ[R] P
hf : IsTensorProduct f
hg : IsTensorProduct g
hp : IsTensorProduct p
i₁ : N₁ →ₗ[R] P₁
j₁ : M₁ →ₗ[R] N₁
i₂ : N₂ →ₗ[R] P₂
j₂ : M₂ →ₗ[R] N₂
x : M
⊢ ∀ (x : M₁) (y : M₂),
    Eq.{u_11 + 1} (α := P)
      ((hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) : (a : M) → P)
          ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        P)
      ((hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂ : (a : M) → P)
          ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        P)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_7 : AddCommMonoid N₁
inst_8 : AddCommMonoid N₂
inst_9 : AddCommMonoid N
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
P₁ : Type u_9
P₂ : Type u_10
P : Type u_11
inst_13 : AddCommMonoid P₁
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid P
inst_16 : Module R P₁
inst_17 : Module R P₂
inst_18 : Module R P
p : P₁ →ₗ[R] P₂ →ₗ[R] P
hf : IsTensorProduct f
hg : IsTensorProduct g
hp : IsTensorProduct p
i₁ : N₁ →ₗ[R] P₁
j₁ : M₁ →ₗ[R] N₁
i₂ : N₂ →ₗ[R] P₂
j₂ : M₂ →ₗ[R] N₂
x x_1 x_2 : M
h₁ :
  Eq.{u_11 + 1} (α := P) ((hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) : (a : M) → P) x_1 : P)
    ((hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂ : (a : M) → P) x_1 : P)
h₂ :
  Eq.{u_11 + 1} (α := P) ((hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) : (a : M) → P) x_2 : P)
    ((hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂ : (a : M) → P) x_2 : P)
⊢ Eq.{u_11 + 1} (α := P) ((hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) : (a : M) → P) (x_1 + x_2) : P)
    ((hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂ : (a : M) → P) (x_1 + x_2) : P)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_7 : AddCommMonoid N₁
inst_8 : AddCommMonoid N₂
inst_9 : AddCommMonoid N
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
P₁ : Type u_9
P₂ : Type u_10
P : Type u_11
inst_13 : AddCommMonoid P₁
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid P
inst_16 : Module R P₁
inst_17 : Module R P₂
inst_18 : Module R P
p : P₁ →ₗ[R] P₂ →ₗ[R] P
hf : IsTensorProduct f
hg : IsTensorProduct g
hp : IsTensorProduct p
i₁ : N₁ →ₗ[R] P₁
j₁ : M₁ →ₗ[R] N₁
i₂ : N₂ →ₗ[R] P₂
j₂ : M₂ →ₗ[R] N₂
x : M
⊢ Eq.{u_11 + 1} (α := P) ((hg.map hp i₁ i₂ : (a : N) → P) ((hf.map hg j₁ j₂ : (a : M) → N) x : N) : P)
    ((hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) : (a : M) → P) x : P)

Tactic:
DFunLike.congr_fun (hf.map_comp hg hp i₁ j₁ i₂ j₂).symm x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, Eq.symm, IsTensorProduct.map_comp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
x : M
⊢ Eq (α := M) ((hf.map hf LinearMap.id LinearMap.id : (a : M) → M) 0 : M) ((LinearMap.id : (a : M) → M) 0 : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
x : M
⊢ ∀ (x : M₁) (y : M₂),
    Eq (α := M)
      ((hf.map hf LinearMap.id LinearMap.id : (a : M) → M)
          ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) :
        M)
      ((LinearMap.id : (a : M) → M) ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M) : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
x x_1 x_2 : M
h₁ : Eq (α := M) ((hf.map hf LinearMap.id LinearMap.id : (a : M) → M) x_1 : M) ((LinearMap.id : (a : M) → M) x_1 : M)
h₂ : Eq (α := M) ((hf.map hf LinearMap.id LinearMap.id : (a : M) → M) x_2 : M) ((LinearMap.id : (a : M) → M) x_2 : M)
⊢ Eq (α := M) ((hf.map hf LinearMap.id LinearMap.id : (a : M) → M) (x_1 + x_2) : M)
    ((LinearMap.id : (a : M) → M) (x_1 + x_2) : M)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i₁ i₂ : M₁ →ₗ[R] M₁
j₁ j₂ : M₂ →ₗ[R] M₂
⊢ hf.map hf (i₁ * i₂) (j₁ * j₂) = hf.map hf i₁ j₁ * hf.map hf i₂ j₂

Tactic:
hf.map_comp hf hf i₁ i₂ j₁ j₂

Premises used: IsTensorProduct.map_comp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
⊢ HPow.hPow (β := ℕ) (hf.map hf i j) 0 = hf.map hf (HPow.hPow (β := ℕ) i 0) (HPow.hPow (β := ℕ) j 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
n : ℕ
ih : hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)
⊢ hf.map hf i j ^ (n + 1) = hf.map hf (i ^ (n + 1)) (j ^ (n + 1))

Tactic:
simp only [pow_succ, ih, hf.map_mul]

Premises used: pow_succ, IsTensorProduct.map_mul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
n : ℕ
zero : HPow.hPow (β := ℕ) (hf.map hf i j) 0 = hf.map hf (HPow.hPow (β := ℕ) i 0) (HPow.hPow (β := ℕ) j 0)
succ :
  ∀ (n : ℕ) (ih : hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)),
    hf.map hf i j ^ (n + 1) = hf.map hf (i ^ (n + 1)) (j ^ (n + 1))
⊢ hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp only [pow_succ, ih, hf.map_mul]

Premises used: pow_succ, IsTensorProduct.map_mul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
change :
  Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        (HSMul.hSMul (β := M₁₂) s ((hf.equiv.toAddEquiv.toEquiv : (a : M₁ ⊗[R] M₂) → M₁₂) (y ⊗ₜ[R] x) : M₁₂)) :
      M₁ ⊗[R] M₂)
    (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)
⊢ HSMul.hSMul (β := M₁ ⊗[R] M₂) s (y ⊗ₜ[R] x) = y ⊗ₜ[R] (s • x)

Tactic:
change hf.equiv.symm (s • _) = _

Premises used: LinearEquiv.symm, IsTensorProduct.equiv, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
dsimp :
  Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        (HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) y : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x : M₁₂)) :
      M₁ ⊗[R] M₂)
    (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)
⊢ Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        (HSMul.hSMul (β := M₁₂) s ((hf.equiv.toAddEquiv.toEquiv : (a : M₁ ⊗[R] M₂) → M₁₂) (y ⊗ₜ[R] x) : M₁₂)) :
      M₁ ⊗[R] M₂)
    (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)

Tactic:
dsimp