case refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : Module.rank R M = 0
⊢ ∀ (x : M), x = 0

case refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∀ (x : M), x = 0
⊢ Module.rank R M = 0
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∃ x, x ≠ 0
⊢ Module.rank R M ≠ 0
case refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : Module.rank R M = 0
⊢ ∀ (x : M), x = 0
contrapose! h
case refine'_1.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
x : M
hx : x ≠ 0
⊢ Module.rank R M ≠ 0
case refine'_1
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∃ x, x ≠ 0
⊢ Module.rank R M ≠ 0
obtain ⟨x, hx⟩ := h
case refine'_1.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
x : M
hx : x ≠ 0
this : Nontrivial M := nontrivial_of_ne x 0 hx
⊢ Module.rank R M ≠ 0
case refine'_1.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
x : M
hx : x ≠ 0
⊢ Module.rank R M ≠ 0
letI : Nontrivial M := nontrivial_of_ne _ _ hx
no goals
case refine'_1.intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
x : M
hx : x ≠ 0
this : Nontrivial M := nontrivial_of_ne x 0 hx
⊢ Module.rank R M ≠ 0
exact rank_pos.ne'
case refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∀ (x : M), x = 0
this : ⊤ = ⊥
⊢ Module.rank R M = 0
case refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∀ (x : M), x = 0
⊢ Module.rank R M = 0
have : (⊤ : Submodule R M) = ⊥ := by
  ext x
  simp [h x]
no goals
case refine'_2
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∀ (x : M), x = 0
this : ⊤ = ⊥
⊢ Module.rank R M = 0
rw [← rank_top, this, rank_bot]
case h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∀ (x : M), x = 0
x : M
⊢ x ∈ ⊤ ↔ x ∈ ⊥
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∀ (x : M), x = 0
⊢ ⊤ = ⊥
ext x
no goals
case h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.245408
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Nontrivial R
h : ∀ (x : M), x = 0
x : M
⊢ x ∈ ⊤ ↔ x ∈ ⊥
simp [h x]