a b : Cardinal
n m : ℕ
⊢ ↑n ∣ ↑m → n ∣ m
a b : Cardinal
n m : ℕ
⊢ ↑n ∣ ↑m ↔ n ∣ m
refine' ⟨_, fun ⟨h, ht⟩ => ⟨h, by exact_mod_cast ht⟩⟩
case intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
⊢ n ∣ m
a b : Cardinal
n m : ℕ
⊢ ↑n ∣ ↑m → n ∣ m
rintro ⟨k, hk⟩
case intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
this : ↑m < ℵ₀
⊢ n ∣ m
case intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
⊢ n ∣ m
have : ↑m < ℵ₀ := nat_lt_aleph0 m
case intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m
case intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
this : ↑m < ℵ₀
⊢ n ∣ m
rw [hk, mul_lt_aleph0_iff] at this
case intro.inl
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m

case intro.inr.inl
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m

case intro.inr.inr.intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
case intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m
rcases this with (h | h | ⟨-, hk'⟩)
case intro.inr.inr.intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
case intro.inl
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m

case intro.inr.inl
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m

case intro.inr.inr.intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
iterate 2 simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk; simp [hk]
case intro.inr.inr.intro.intro
a b : Cardinal
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ n ∣ m
case intro.inr.inr.intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
lift k to ℕ using hk'
no goals
case intro.inr.inr.intro.intro
a b : Cardinal
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ n ∣ m
exact ⟨k, by exact_mod_cast hk⟩
no goals
a b : Cardinal
n m : ℕ
x✝ : n ∣ m
h : ℕ
ht : m = n * h
⊢ ↑m = ↑n * ↑h
exact_mod_cast ht
case intro.inr.inl
a b : Cardinal
n m : ℕ
k : Cardinal
h : k = 0
hk : m = 0
⊢ n ∣ m

case intro.inr.inr.intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
case intro.inr.inl
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m

case intro.inr.inr.intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk
case intro.inr.inr.intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
case intro.inr.inl
a b : Cardinal
n m : ℕ
k : Cardinal
h : k = 0
hk : m = 0
⊢ n ∣ m

case intro.inr.inr.intro
a b : Cardinal
n m : ℕ
k : Cardinal
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m
simp [hk]
no goals
a b : Cardinal
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ m = n * k
exact_mod_cast hk