-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.le_set {f o} (H : IsNormal f) (p : Set Ordinal) (p0 : p.Nonempty) (b)
    (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f a ≤ o :=
  ⟨fun h _ pa => (H.le_iff.2 ((H₂ _).1 le_rfl _ pa)).trans h, fun h => by
    -- Porting note: `refine'` didn't work well so `induction` is used
    induction b using limitRecOn with
    | H₁ =>
      obtain ⟨x, px⟩ := p0
      have := Ordinal.le_zero.1 ((H₂ _).1 (Ordinal.zero_le _) _ px)
      rw [this] at px
      exact h _ px
    | H₂ S _ =>
      rcases not_forall₂.1 (mt (H₂ S).2 <| (lt_succ S).not_le) with ⟨a, h₁, h₂⟩
      exact (H.le_iff.2 <| succ_le_of_lt <| not_le.1 h₂).trans (h _ h₁)
    | H₃ S L _ =>
      refine (H.2 _ L _).2 fun a h' => ?_
      rcases not_forall₂.1 (mt (H₂ a).2 h'.not_le) with ⟨b, h₁, h₂⟩
      exact (H.le_iff.2 <| (not_le.1 h₂).le).trans (h _ h₁)⟩

Proof state:
case H₁.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
h : ∀ a ∈ p, f a ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), 0 ≤ o ↔ ∀ a ∈ p, a ≤ o
x : Ordinal.{u_4}
px : x ∈ p
⊢ f 0 ≤ o

Tactic:
have := Ordinal.le_zero.1 ((H₂ _).1 (Ordinal.zero_le _) _ px)

Result:
case H₁.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
h : ∀ a ∈ p, f a ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), 0 ≤ o ↔ ∀ a ∈ p, a ≤ o
x : Ordinal.{u_4}
px : x ∈ p
this : x = 0
⊢ f 0 ≤ o

Proof state:
case H₁.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
h : ∀ a ∈ p, f a ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), 0 ≤ o ↔ ∀ a ∈ p, a ≤ o
x : Ordinal.{u_4}
px : 0 ∈ p
this : x = 0
⊢ f 0 ≤ o

Tactic:
exact h _ px

Result:
no goals

Proof state:
case H₃
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
S : Ordinal.{u_4}
L : S.IsLimit
a✝ : ∀ o' < S, (∀ (o : Ordinal.{u_4}), o' ≤ o ↔ ∀ a ∈ p, a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), S ≤ o ↔ ∀ a ∈ p, a ≤ o
a : Ordinal.{u_4}
h' : a < S
⊢ f a ≤ o

Tactic:
rcases not_forall₂.1 (mt (H₂ a).2 h'.not_le) with ⟨b, h₁, h₂⟩

Result:
case H₃.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
S : Ordinal.{u_4}
L : S.IsLimit
a✝ : ∀ o' < S, (∀ (o : Ordinal.{u_4}), o' ≤ o ↔ ∀ a ∈ p, a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), S ≤ o ↔ ∀ a ∈ p, a ≤ o
a : Ordinal.{u_4}
h' : a < S
b : Ordinal.{u_4}
h₁ : b ∈ p
h₂ : ¬b ≤ a
⊢ f a ≤ o

Proof state:
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o
h : ∀ a ∈ p, f a ≤ o
⊢ f b ≤ o

Tactic:
induction b using limitRecOn with
| H₁ =>
  obtain ⟨x, px⟩ := p0
  have := Ordinal.le_zero.1 ((H₂ _).1 (Ordinal.zero_le _) _ px)
  rw [this] at px
  exact h _ px
| H₂ S _ =>
  rcases not_forall₂.1 (mt (H₂ S).2 <| (lt_succ S).not_le) with ⟨a, h₁, h₂⟩
  exact (H.le_iff.2 <| succ_le_of_lt <| not_le.1 h₂).trans (h _ h₁)
| H₃ S L _ =>
  refine (H.2 _ L _).2 fun a h' => ?_
  rcases not_forall₂.1 (mt (H₂ a).2 h'.not_le) with ⟨b, h₁, h₂⟩
  exact (H.le_iff.2 <| (not_le.1 h₂).le).trans (h _ h₁)

Result:
no goals

Proof state:
case H₃.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
S : Ordinal.{u_4}
L : S.IsLimit
a✝ : ∀ o' < S, (∀ (o : Ordinal.{u_4}), o' ≤ o ↔ ∀ a ∈ p, a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), S ≤ o ↔ ∀ a ∈ p, a ≤ o
a : Ordinal.{u_4}
h' : a < S
b : Ordinal.{u_4}
h₁ : b ∈ p
h₂ : ¬b ≤ a
⊢ f a ≤ o

Tactic:
exact (H.le_iff.2 <| (not_le.1 h₂).le).trans (h _ h₁)

Result:
no goals

Proof state:
case H₁.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
h : ∀ a ∈ p, f a ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), 0 ≤ o ↔ ∀ a ∈ p, a ≤ o
x : Ordinal.{u_4}
px : x ∈ p
this : x = 0
⊢ f 0 ≤ o

Tactic:
rw [this] at px

Result:
case H₁.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
h : ∀ a ∈ p, f a ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), 0 ≤ o ↔ ∀ a ∈ p, a ≤ o
x : Ordinal.{u_4}
px : 0 ∈ p
this : x = 0
⊢ f 0 ≤ o

Proof state:
case H₃
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
S : Ordinal.{u_4}
L : S.IsLimit
a✝ : ∀ o' < S, (∀ (o : Ordinal.{u_4}), o' ≤ o ↔ ∀ a ∈ p, a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), S ≤ o ↔ ∀ a ∈ p, a ≤ o
⊢ f S ≤ o

Tactic:
refine (H.2 _ L _).2 fun a h' => ?_

Result:
case H₃
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
S : Ordinal.{u_4}
L : S.IsLimit
a✝ : ∀ o' < S, (∀ (o : Ordinal.{u_4}), o' ≤ o ↔ ∀ a ∈ p, a ≤ o) → f o' ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), S ≤ o ↔ ∀ a ∈ p, a ≤ o
a : Ordinal.{u_4}
h' : a < S
⊢ f a ≤ o

Proof state:
case H₂
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
S : Ordinal.{u_4}
a✝ : (∀ (o : Ordinal.{u_4}), S ≤ o ↔ ∀ a ∈ p, a ≤ o) → f S ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), succ S ≤ o ↔ ∀ a ∈ p, a ≤ o
⊢ f (succ S) ≤ o

Tactic:
rcases not_forall₂.1 (mt (H₂ S).2 <| (lt_succ S).not_le) with ⟨a, h₁, h₂⟩

Result:
case H₂.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
S : Ordinal.{u_4}
a✝ : (∀ (o : Ordinal.{u_4}), S ≤ o ↔ ∀ a ∈ p, a ≤ o) → f S ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), succ S ≤ o ↔ ∀ a ∈ p, a ≤ o
a : Ordinal.{u_4}
h₁ : a ∈ p
h₂ : ¬a ≤ S
⊢ f (succ S) ≤ o

Proof state:
case H₂.intro.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
S : Ordinal.{u_4}
a✝ : (∀ (o : Ordinal.{u_4}), S ≤ o ↔ ∀ a ∈ p, a ≤ o) → f S ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), succ S ≤ o ↔ ∀ a ∈ p, a ≤ o
a : Ordinal.{u_4}
h₁ : a ∈ p
h₂ : ¬a ≤ S
⊢ f (succ S) ≤ o

Tactic:
exact (H.le_iff.2 <| succ_le_of_lt <| not_le.1 h₂).trans (h _ h₁)

Result:
no goals

Proof state:
case H₁
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
p0 : p.Nonempty
h : ∀ a ∈ p, f a ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), 0 ≤ o ↔ ∀ a ∈ p, a ≤ o
⊢ f 0 ≤ o

Tactic:
obtain ⟨x, px⟩ := p0

Result:
case H₁.intro
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set Ordinal.{u_4}
h : ∀ a ∈ p, f a ≤ o
H₂ : ∀ (o : Ordinal.{u_4}), 0 ≤ o ↔ ∀ a ∈ p, a ≤ o
x : Ordinal.{u_4}
px : x ∈ p
⊢ f 0 ≤ o