awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy : y ∈ Iic (sSup (f ⁻¹' Iic x))
inl : ∀ (hy : y < sSup (f ⁻¹' Iic x)), y ∈ f ⁻¹' Iic x
inr : ∀ (hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))), sSup (f ⁻¹' Iic x) ∈ f ⁻¹' Iic x
⊢ y ∈ f ⁻¹' Iic x

Tactic:
obtain hy | rfl := hy.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy_1 : y ∈ Iic (sSup (f ⁻¹' Iic x))
hy : y < sSup (f ⁻¹' Iic x)
⊢ ∃ b ∈ f ⁻¹' Iic x, y < b

Tactic:
rw [lt_csSup_iff h₂ h₁] at hy

Premises used: lt_csSup_iff
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy_1 : y ∈ Iic (sSup (f ⁻¹' Iic x))
hy : ∃ b ∈ f ⁻¹' Iic x, y < b
inl : ∀ (z : α) (hz : z ∈ f ⁻¹' Iic x) (hyz : y < z), y ∈ f ⁻¹' Iic x
⊢ y ∈ f ⁻¹' Iic x

Tactic:
obtain ⟨z, hz, hyz⟩ := hy
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy : y ∈ Iic (sSup (f ⁻¹' Iic x))
z : α
hz : z ∈ f ⁻¹' Iic x
hyz : y < z
⊢ y ∈ f ⁻¹' Iic x

Tactic:
(hf.strictMono hyz).le.trans hz

Premises used: Set.Mem, setOf, LT.lt.le, Set.preimage, Set.Iic, LE.le.trans, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy : y ∈ Iic (sSup (f ⁻¹' Iic x))
z : α
hz : z ∈ f ⁻¹' Iic x
hyz : y < z
⊢ y ∈ f ⁻¹' Iic x

Tactic:
exact (hf.strictMono hyz).le.trans hz

Premises used: LT.lt.le, LE.le.trans, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
inr : sSup (f '' f ⁻¹' Iic x) ∈ Iic x
⊢ sSup (f ⁻¹' Iic x) ∈ f ⁻¹' Iic x

Tactic:
rw [mem_preimage, hf.map_sSup h₁ h₂]

Premises used: Order.IsNormal.map_sSup, Set.mem_preimage
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
inr : sSup (Iic x) ≤ x
apply : (f '' f ⁻¹' Iic x).Nonempty
⊢ sSup (f '' f ⁻¹' Iic x) ∈ Iic x

Tactic:
apply (csSup_le_csSup bddAbove_Iic _ (image_preimage_subset ..)).trans

Premises used: Set.image_preimage_subset, LE.le.trans, csSup_le_csSup, bddAbove_Iic
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
inr inr₁ : x ≤ x
⊢ sSup (Iic x) ≤ x

Tactic:
rw [csSup_Iic]

Premises used: csSup_Iic
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ (f '' f ⁻¹' Iic x).Nonempty

Tactic:
simpa
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : α
y : β
h₁ : (f ⁻¹' Iic y).Nonempty
h₂ : BddAbove (f ⁻¹' Iic y)
⊢ f x ≤ y ↔ x ≤ sSup (f ⁻¹' Iic y)

Tactic:
Set.ext_iff.1 (preimage_Iic hf h₁ h₂) x

Premises used: Set.Mem, setOf, Set.preimage, Order.IsNormal.preimage_Iic, Iff.mp, Set.Iic, Set.ext_iff
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
x y : α
h : (f ⁻¹' Iic y).Nonempty
⊢ f x ≤ y ↔ x ≤ sSup (f ⁻¹' Iic y)

Tactic:
hf.le_iff_le_sSup h ⟨y, fun _ ↦ hf.strictMono.le_apply.trans⟩

Premises used: StrictMono.le_apply, Order.IsNormal.le_iff_le_sSup, Exists.intro, LE.le.trans, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ f (⨆ (i : (↑(Iio a) : Type u_1)), (↑i : α)) = ⨆ (i : (↑(Iio a) : Type u_1)), f (↑i : α)

Tactic:
map_iSup hf _

Premises used: Order.IsNormal.map_iSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
h : a = ⨆ (i : (↑(Iio a) : Type u_1)), (↑i : α)
convert_2 : Nonempty.{u_1 + 1} (↑(Iio a) : Type u_1)
convert_4 : BddAbove.{u_1} (α := α) (range (ι := (↑(Iio a) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iio a)))
⊢ f a = ⨆ (b : (↑(Iio a) : Type u_1)), f (↑b : α)

Tactic:
convert! map_iSup hf _

Premises used: Order.IsNormal.map_iSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ a = ⨆ (i : (↑(Iio a) : Type u_1)), (↑i : α)

Tactic:
ha.iSup_Iio.symm

Premises used: Order.IsSuccLimit.iSup_Iio, Eq.symm
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ a = ⨆ (i : (↑(Iio a) : Type u_1)), (↑i : α)

Tactic:
exact ha.iSup_Iio.symm

Premises used: Order.IsSuccLimit.iSup_Iio, Eq.symm
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ Nonempty.{u_1 + 1} (↑(Iio a) : Type u_1)

Tactic:
⟨⊥, ha.bot_lt⟩

Premises used: Bot.bot, Nonempty.intro, Subtype.mk, Order.IsSuccLimit.bot_lt
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ Nonempty.{u_1 + 1} (↑(Iio a) : Type u_1)

Tactic:
exact ⟨⊥, ha.bot_lt⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
h :
  Membership.mem (γ := Set α)
    (upperBounds (range (ι := (↑(Iio a) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iio a)))) a
⊢ BddAbove.{u_1} (α := α) (range (ι := (↑(Iio a) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iio a)))

Tactic:
use a
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
x : α
hx : x ∈ Iio a
⊢ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) x hx) : α) ≤ a

Tactic:
hx.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
x : α
hx : x ∈ Iio a
⊢ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) x hx) : α) ≤ a

Tactic:
exact hx.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
⊢ IsNormal f

Tactic:
⟨fun a b ↦ ?_, fun ha ↦ (hl ha).2⟩

Premises used: Order.IsNormal.mk, And.right
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
refine : ∀ (a b : α), a < b → f a < f b
⊢ IsNormal f

Tactic:
refine ⟨fun a b ↦ ?_, fun ha ↦ (hl ha).2⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : IsMin b
⊢ a < b → f a < f b

Tactic:
hb.not_lt.elim

Premises used: IsMin.not_lt, Not.elim
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : IsMin b
⊢ a < b → f a < f b

Tactic:
exact hb.not_lt.elim

Premises used: IsMin.not_lt, Not.elim
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (Order.succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : ¬IsMax b
IH : a < b → f a < f b
hab : a < Order.succ b
succ : ∀ (hb : ¬IsMax a) (IH : a < a → f a < f a) (hab : a < Order.succ a), f a < f (Order.succ a)
succ₁ : ∀ (h : a < b), f a < f (Order.succ b)
⊢ f a < f (Order.succ b)

Tactic:
obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab

Premises used: Order.lt_succ_iff_eq_or_lt_of_not_isMax, Iff.mp, rfl
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a : α
hb : ¬IsMax a
IH : a < a → f a < f a
hab : a < succ a
⊢ f a < f (succ a)

Tactic:
hs a
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a : α
hb : ¬IsMax a
IH : a < a → f a < f a
hab : a < succ a
⊢ f a < f (succ a)

Tactic:
exact hs a
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : ¬IsMax b
IH : a < b → f a < f b
hab : a < succ b
h : a < b
⊢ f a < f (succ b)

Tactic:
(IH h).trans (hs b)

Premises used: LT.lt.trans
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : ¬IsMax b
IH : a < b → f a < f b
hab : a < succ b
h : a < b
⊢ f a < f (succ b)

Tactic:
exact (IH h).trans (hs b)

Premises used: LT.lt.trans
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : IsSuccLimit b
IH : ∀ b_1 < b, a < b_1 → f a < f b_1
hab : a < b
⊢ succ a < b

Tactic:
have hab' := hb.succ_lt hab
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : IsSuccLimit b
IH : ∀ b_1 < b, a < b_1 → f a < f b_1
hab : a < b
hab' : succ a < b
⊢ f a < f b

Tactic:
(IH _ hab' (lt_succ_of_not_isMax hab.not_isMax)).trans_le
      ((hl hb).1 (mem_image_of_mem _ hab'))

Premises used: Order.lt_succ_of_not_isMax, And.left, Set.mem_image_of_mem, LT.lt.trans_le, LT.lt.not_isMax
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : IsSuccLimit b
IH : ∀ b_1 < b, a < b_1 → f a < f b_1
hab : a < b
hab' : succ a < b
⊢ f a < f b

Tactic:
exact (IH _ hab' (lt_succ_of_not_isMax hab.not_isMax)).trans_le
      ((hl hb).1 (mem_image_of_mem _ hab'))

Premises used: Order.lt_succ_of_not_isMax, And.left, Set.mem_image_of_mem, LT.lt.trans_le, LT.lt.not_isMax
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
hs : ∀ (a : α), f a < f (Order.succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
isMin : ∀ (b : α) (hb : IsMin b), a < b → f a < f b
succ : ∀ (b : α) (hb : ¬IsMax b) (IH : a < b → f a < f b), a < Order.succ b → f a < f (Order.succ b)
isSuccLimit : ∀ (b : α) (hb : IsSuccLimit b) (IH : ∀ b_1 < b, a < b_1 → f a < f b_1), a < b → f a < f b
⊢ a < b → f a < f b

Tactic:
induction b using SuccOrder.limitRecOn with
  | isMin b hb => exact hb.not_lt.elim
  | succ b hb IH =>
    intro hab
    obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
    · exact hs a
    · exact (IH h).trans (hs b)
  | isSuccLimit b hb IH =>
    intro hab
    have hab' := hb.succ_lt hab
    exact (IH _ hab' (lt_succ_of_not_isMax hab.not_isMax)).trans_le
      ((hl hb).1 (mem_image_of_mem _ hab'))

Premises used: Order.succ, rfl
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
mp : f = g → f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)
mpr : (f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)) → f = g
⊢ f = g ↔ f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)

Tactic:
constructor
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
⊢ f = g → f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)

Tactic:
simp_all
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
mpr : ∀ (a : α), f a = g a
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsMin a
mpr : f ⊥ = g ⊥
mpr₁ mpr₂ : g ⊥ = g ⊥
⊢ f a = g a

Tactic:
rw [ha.eq_bot, H₁]

Premises used: IsMin.eq_bot
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : ¬IsMax a
IH : f a = g a
⊢ f (succ a) = g (succ a)

Tactic:
H₂ a IH
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : ¬IsMax a
IH : f a = g a
⊢ f (succ a) = g (succ a)

Tactic:
exact H₂ a IH
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsSuccLimit a
IH : ∀ b < a, f b = g b
mpr : IsLUB (f '' Iio a) (g a)
⊢ f a = g a

Tactic:
apply (hf.isLUB_image_Iio_of_isSuccLimit ha).unique

Premises used: Order.IsNormal.isLUB_image_Iio_of_isSuccLimit, IsLUB.unique
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsSuccLimit a
IH : ∀ b < a, f b = g b
⊢ IsLUB (g '' Iio a) (g a)

Tactic:
hg.isLUB_image_Iio_of_isSuccLimit ha

Premises used: Order.IsNormal.isLUB_image_Iio_of_isSuccLimit
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsSuccLimit a
IH : ∀ b < a, f b = g b
h : f '' Iio a = g '' Iio a
⊢ IsLUB (f '' Iio a) (g a)

Tactic:
convert! hg.isLUB_image_Iio_of_isSuccLimit ha using 1

Premises used: Order.IsNormal.isLUB_image_Iio_of_isSuccLimit
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsSuccLimit a
IH : ∀ b < a, f b = g b
⊢ f '' Iio a = g '' Iio a

Tactic:
aesop
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
mpr : ∀ (a : α) (ha : IsMin a), f a = g a
mpr₁ : ∀ (a : α) (ha : ¬IsMax a) (IH : f a = g a), f (succ a) = g (succ a)
mpr₂ : ∀ (a : α) (ha : IsSuccLimit a) (IH : ∀ b < a, f b = g b), f a = g a
⊢ f a = g a

Tactic:
induction a using SuccOrder.limitRecOn with
  | isMin a ha => rw [ha.eq_bot, H₁]
  | succ a ha IH => exact H₂ a IH
  | isSuccLimit a ha IH =>
    apply (hf.isLUB_image_Iio_of_isSuccLimit ha).unique
    convert! hg.isLUB_image_Iio_of_isSuccLimit ha using 1
    aesop

Premises used: Order.succ
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
inst_6 : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ (y : α), x ≤ f y
hx : f ⊥ ≤ x
⊢ Nonempty β

Tactic:
have : Nonempty β := ⟨x⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
inst_6 : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ (y : α), x ≤ f y
hx : f ⊥ ≤ x
this_1 : Nonempty β
this_2 : OrderBot β := WellFoundedLT.toOrderBot β
this_3 : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
⊢ BddAbove (f ⁻¹' Iic x)

Tactic:
have H : BddAbove (f ⁻¹' Iic x) :=
    have ⟨y, hy⟩ := hf'
    ⟨y, fun z hz ↦ hf.strictMono.le_iff_le.1 <| hz.trans hy⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
inst_6 : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ (y : α), x ≤ f y
hx : f ⊥ ≤ x
this_1 : Nonempty β
this_2 : OrderBot β := WellFoundedLT.toOrderBot β
this_3 : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ ∃ (a : α), f a ≤ x ∧ x < f (succ a)

Tactic:
⟨sSup (f ⁻¹' Set.Iic x), ?_, ?_⟩

Premises used: Set.preimage, And.intro, Exists.intro, Set.Iic, SupSet.sSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
inst_6 : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ (y : α), x ≤ f y
hx : f ⊥ ≤ x
this_1 : Nonempty β
this_2 : OrderBot β := WellFoundedLT.toOrderBot β
this_3 : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
refine_1 : f (sSup (f ⁻¹' Iic x)) ≤ x
refine_2 : x < f (succ (sSup (f ⁻¹' Iic x)))
⊢ ∃ (a : α), f a ≤ x ∧ x < f (succ a)

Tactic:
refine ⟨sSup (f ⁻¹' Set.Iic x), ?_, ?_⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
inst_6 : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ (y : α), x ≤ f y
hx : f ⊥ ≤ x
this_1 : Nonempty β
this_2 : OrderBot β := WellFoundedLT.toOrderBot β
this_3 : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
refine_1 refine_1₁ : sSup (f ⁻¹' Iic x) ≤ sSup (f ⁻¹' Iic x)
⊢ f (sSup (f ⁻¹' Iic x)) ≤ x

Tactic:
rw [hf.le_iff_le_sSup ⟨⊥, hx⟩ H]

Premises used: Order.IsNormal.le_iff_le_sSup, Bot.bot, Exists.intro
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : LinearOrder β
inst_4 : NoMaxOrder α
inst_5 : OrderBot α
inst_6 : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ (y : α), x ≤ f y
hx : f ⊥ ≤ x
this_1 : Nonempty β
this_2 : OrderBot β := WellFoundedLT.toOrderBot β
this_3 : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
refine_2 : ¬f (succ (sSup (f ⁻¹' Iic x))) ≤ x
refine_2₁ : ¬succ (sSup (f ⁻¹' Iic x)) ≤ sSup (f ⁻¹' Iic x)
refine_2₂ : sSup (f ⁻¹' Iic x) < succ (sSup (f ⁻¹' Iic x))
refine_2₃ refine_2₄ : sSup (f ⁻¹' Iic x) ≤ sSup (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))

Tactic:
rw [← not_le, hf.le_iff_le_sSup ⟨⊥, hx⟩ H, not_le, lt_succ_iff]

Premises used: not_le, Order.IsNormal.le_iff_le_sSup, Bot.bot, Order.lt_succ_iff, Exists.intro
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
inst_4 : OrderBot α
f : α → α
x : α
hf : IsNormal f
hx : f ⊥ ≤ x
⊢ ∃ (a : α), f a ≤ x ∧ x < f (succ a)

Tactic:
exists_map_le_lt_map_succ_of_exists_ge hf ⟨x, hf.strictMono.le_apply⟩ hx

Premises used: StrictMono.le_apply, Order.IsNormal.exists_map_le_lt_map_succ_of_exists_ge, Exists.intro, Order.IsNormal.strictMono