case mp
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : SeparatingLeft B
x : M₁
hB : ↑B x = 0
⊢ x = 0

case mpr
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
⊢ x = 0
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
⊢ SeparatingLeft B ↔ ∀ (x : M₁), ↑B x = 0 → x = 0
constructor <;> intro h x hB
case mpr
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
h' : ↑B x = 0
⊢ x = 0
case mpr
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
⊢ x = 0
have h' : B x = 0 := by
  ext
  rw [zero_apply]
  exact hB _
no goals
case mpr
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
h' : ↑B x = 0
⊢ x = 0
exact h x h'
no goals
case mp
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : SeparatingLeft B
x : M₁
hB : ↑B x = 0
⊢ x = 0
simpa only [hB, zero_apply, eq_self_iff_true, forall_const] using h x
case h
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
x✝ : M₂
⊢ ↑(↑B x) x✝ = ↑0 x✝
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
⊢ ↑B x = 0
ext
case h
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
x✝ : M₂
⊢ ↑(↑B x) x✝ = 0
case h
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
x✝ : M₂
⊢ ↑(↑B x) x✝ = ↑0 x✝
rw [zero_apply]
no goals
case h
R : Type u_2
R₁ : Type u_1
R₂ : Type u_5
R₃ : Type ?u.550523
M : Type ?u.550526
M₁ : Type u_3
M₂ : Type u_4
Mₗ₁ : Type ?u.550535
Mₗ₁' : Type ?u.550538
Mₗ₂ : Type ?u.550541
Mₗ₂' : Type ?u.550544
K : Type ?u.550547
K₁ : Type ?u.550550
K₂ : Type ?u.550553
V : Type ?u.550556
V₁ : Type ?u.550559
V₂ : Type ?u.550562
n : Type ?u.550565
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R
h : ∀ (x : M₁), ↑B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), ↑(↑B x) y = 0
x✝ : M₂
⊢ ↑(↑B x) x✝ = 0
exact hB _