a b : Cardinal
n m : ℕ
h : IsUnit a
⊢ a = 1
a b : Cardinal
n m : ℕ
⊢ IsUnit a ↔ a = 1
refine'
  ⟨fun h => _, by
    rintro rfl
    exact isUnit_one⟩
case inl
b : Cardinal
n m : ℕ
h : IsUnit 0
⊢ 0 = 1

case inr
a b : Cardinal
n m : ℕ
h : IsUnit a
ha : a ≠ 0
⊢ a = 1
a b : Cardinal
n m : ℕ
h : IsUnit a
⊢ a = 1
rcases eq_or_ne a 0 with (rfl | ha)
case inr
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
⊢ a = 1
case inr
a b : Cardinal
n m : ℕ
h : IsUnit a
ha : a ≠ 0
⊢ a = 1
rw [isUnit_iff_forall_dvd] at h
case inr.intro
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : 1 = a * t
⊢ a = 1
case inr
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
⊢ a = 1
cases' h 1 with t ht
case inr.intro
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a = 1 ∧ t = 1
⊢ a = 1

case inr.intro.ha
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a * t = 1
⊢ 1 ≤ a

case inr.intro.hb
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a * t = 1
⊢ 1 ≤ t
case inr.intro
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : 1 = a * t
⊢ a = 1
rw [eq_comm, mul_eq_one_iff'] at ht
b : Cardinal
n m : ℕ
⊢ IsUnit 1
a b : Cardinal
n m : ℕ
⊢ a = 1 → IsUnit a
rintro rfl
no goals
b : Cardinal
n m : ℕ
⊢ IsUnit 1
exact isUnit_one
no goals
case inl
b : Cardinal
n m : ℕ
h : IsUnit 0
⊢ 0 = 1
exact (not_isUnit_zero h).elim
no goals
case inr.intro
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a = 1 ∧ t = 1
⊢ a = 1
exact ht.1
no goals
case inr.intro.ha
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a * t = 1
⊢ 1 ≤ a
exact one_le_iff_ne_zero.mpr ha
case inr.intro.hb
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a * t = 1
⊢ t ≠ 0
case inr.intro.hb
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a * t = 1
⊢ 1 ≤ t
apply one_le_iff_ne_zero.mpr
case inr.intro.hb
a b : Cardinal
n m : ℕ
h✝ : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a * t = 1
h : t = 0
⊢ False
case inr.intro.hb
a b : Cardinal
n m : ℕ
h : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a * t = 1
⊢ t ≠ 0
intro h
case inr.intro.hb
a b : Cardinal
n m : ℕ
h✝ : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : 0 = 1
h : t = 0
⊢ False
case inr.intro.hb
a b : Cardinal
n m : ℕ
h✝ : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : a * t = 1
h : t = 0
⊢ False
rw [h, mul_zero] at ht
no goals
case inr.intro.hb
a b : Cardinal
n m : ℕ
h✝ : ∀ (y : Cardinal), a ∣ y
ha : a ≠ 0
t : Cardinal
ht : 0 = 1
h : t = 0
⊢ False
exact zero_ne_one ht