no goals
α : Type ?u.208151
β : Type ?u.208154
γ : Type ?u.208157
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
h : IsLimit b
H : ∀ (b' : Ordinal), b' < b → a * b' ≤ c
⊢ ¬c < a * b
induction a using inductionOn with
| H α r =>
  induction b using inductionOn with
  | H β s =>
    exact mul_le_of_limit_aux h H
no goals
case H
α✝ : Type ?u.208151
β : Type ?u.208154
γ : Type ?u.208157
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
b c : Ordinal
h : IsLimit b
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
H : ∀ (b' : Ordinal), b' < b → type r * b' ≤ c
⊢ ¬c < type r * b
induction b using inductionOn with
| H β s =>
  exact mul_le_of_limit_aux h H
no goals
case H.H
α✝ : Type ?u.208151
β✝ : Type ?u.208154
γ : Type ?u.208157
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Ordinal
α : Type u_1
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
inst✝ : IsWellOrder β s
h : IsLimit (type s)
H : ∀ (b' : Ordinal), b' < type s → type r * b' ≤ c
⊢ ¬c < type r * type s
exact mul_le_of_limit_aux h H