R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C (AddHom.toFun (↑(equiv h)).toAddHom (LinearEquiv.invFun (equiv h) m))
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C m
rw [← h.equiv.right_inv m]
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
y : M₁ ⊗[R] M₂
⊢ C (AddHom.toFun (↑(equiv h)).toAddHom y)
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C (AddHom.toFun (↑(equiv h)).toAddHom (LinearEquiv.invFun (equiv h) m))
generalize h.equiv.invFun m = y
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
y : M₁ ⊗[R] M₂
⊢ C (↑(TensorProduct.lift f) y)
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
y : M₁ ⊗[R] M₂
⊢ C (AddHom.toFun (↑(equiv h)).toAddHom y)
change C (TensorProduct.lift f y)
case C0
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C (↑(TensorProduct.lift f) 0)

case C1
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
x✝ : M₁
y✝ : M₂
⊢ C (↑(TensorProduct.lift f) (x✝ ⊗ₜ[R] y✝))

case Cp
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : C (↑(TensorProduct.lift f) x✝)
a✝ : C (↑(TensorProduct.lift f) y✝)
⊢ C (↑(TensorProduct.lift f) (x✝ + y✝))
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
y : M₁ ⊗[R] M₂
⊢ C (↑(TensorProduct.lift f) y)
induction y using TensorProduct.induction_on
no goals
case C0
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
⊢ C (↑(TensorProduct.lift f) 0)
rwa [map_zero]
case C1
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
x✝ : M₁
y✝ : M₂
⊢ C (↑(↑f x✝) y✝)
case C1
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
x✝ : M₁
y✝ : M₂
⊢ C (↑(TensorProduct.lift f) (x✝ ⊗ₜ[R] y✝))
rw [TensorProduct.lift.tmul]
no goals
case C1
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
x✝ : M₁
y✝ : M₂
⊢ C (↑(↑f x✝) y✝)
apply htmul
case Cp
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : C (↑(TensorProduct.lift f) x✝)
a✝ : C (↑(TensorProduct.lift f) y✝)
⊢ C (↑(TensorProduct.lift f) x✝ + ↑(TensorProduct.lift f) y✝)
case Cp
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : C (↑(TensorProduct.lift f) x✝)
a✝ : C (↑(TensorProduct.lift f) y✝)
⊢ C (↑(TensorProduct.lift f) (x✝ + y✝))
rw [map_add]
no goals
case Cp
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.113149
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type ?u.115388
N₂ : Type ?u.115391
N : Type ?u.115394
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
h : IsTensorProduct f
C : M → Prop
m : M
h0 : C 0
htmul : ∀ (x : M₁) (y : M₂), C (↑(↑f x) y)
hadd : ∀ (x y : M), C x → C y → C (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : C (↑(TensorProduct.lift f) x✝)
a✝ : C (↑(TensorProduct.lift f) y✝)
⊢ C (↑(TensorProduct.lift f) x✝ + ↑(TensorProduct.lift f) y✝)
apply hadd <;> assumption