case H₁
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
⊢ 0 ≤ b / c ↔ c * 0 ≤ b

case H₂
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
⊢ ∀ (o : Ordinal), (o ≤ b / c ↔ c * o ≤ b) → (succ o ≤ b / c ↔ c * succ o ≤ b)

case H₃
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → (o' ≤ b / c ↔ c * o' ≤ b)) → (o ≤ b / c ↔ c * o ≤ b)
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
⊢ a ≤ b / c ↔ c * a ≤ b
apply limitRecOn a
no goals
case H₁
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
⊢ 0 ≤ b / c ↔ c * 0 ≤ b
simp only [mul_zero, Ordinal.zero_le]
case H₂
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
o✝ : Ordinal
a✝ : o✝ ≤ b / c ↔ c * o✝ ≤ b
⊢ succ o✝ ≤ b / c ↔ c * succ o✝ ≤ b
case H₂
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
⊢ ∀ (o : Ordinal), (o ≤ b / c ↔ c * o ≤ b) → (succ o ≤ b / c ↔ c * succ o ≤ b)
intros
no goals
case H₂
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
o✝ : Ordinal
a✝ : o✝ ≤ b / c ↔ c * o✝ ≤ b
⊢ succ o✝ ≤ b / c ↔ c * succ o✝ ≤ b
rw [succ_le_iff, lt_div c0]
no goals
case H₃
α : Type ?u.234535
β : Type ?u.234538
γ : Type ?u.234541
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
c0 : c ≠ 0
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → (o' ≤ b / c ↔ c * o' ≤ b)) → (o ≤ b / c ↔ c * o ≤ b)
simp (config := { contextual := true }) only [mul_le_of_limit, limit_le, iff_self_iff,
  forall_true_iff]