awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
⊢ f (f^[n] a) ≤ ⨆ (i : ℕ), f (f^[i] a)
have apply : Subset.{u_1} (α := Set α) (range fun (n : ℕ) ↦ f (f^[n] a)) (range fun (n : ℕ) ↦ f^[n] a)
Tactic: apply (le_ciSup (hf'.mono _) n)
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
⊢ Subset.{u_1} (α := Set α) (range fun (n : ℕ) ↦ f (f^[n] a)) (range fun (n : ℕ) ↦ f^[n] a)
have simp_rw : Subset.{u_1} (α := Set α) (range fun (n : ℕ) ↦ f^[n.succ] a) (range fun (n : ℕ) ↦ f^[n] a)
Tactic: simp_rw [← f.iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ f ⁻¹' Iic x = Iic (sSup (f ⁻¹' Iic x))
have refine : ∀ (y : α) (hy : y ∈ Iic (sSup (f ⁻¹' Iic x))), y ∈ f ⁻¹' Iic x
Tactic: refine le_antisymm (fun _ ↦ le_csSup h₂) (fun y hy ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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))
⊢ y ∈ f ⁻¹' Iic x
have inl : ∀ (hy : y < sSup (f ⁻¹' Iic x)), y ∈ f ⁻¹' Iic x
Tactic: obtain hy | rfl := hy.lt_or_eq
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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
⊢ y ∈ f ⁻¹' Iic x
have inr : ∀ (hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))), sSup (f ⁻¹' Iic x) ∈ f ⁻¹' Iic x
Tactic: obtain hy | rfl := hy.lt_or_eq
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
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)
⊢ y ∈ f ⁻¹' Iic x
have hy₁ : ∃ b ∈ f ⁻¹' Iic x, y < b
Tactic: rw [lt_csSup_iff h₂ h₁] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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
⊢ y ∈ f ⁻¹' Iic x
have inl : ∀ (z : α) (hz : z ∈ f ⁻¹' Iic x) (hyz : y < z), y ∈ f ⁻¹' Iic x
Tactic: obtain ⟨z, hz, hyz⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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))
⊢ sSup (f ⁻¹' Iic x) ∈ f ⁻¹' Iic x
have inr : sSup (f '' f ⁻¹' Iic x) ∈ Iic x
Tactic: rw [mem_preimage, hf.map_sSup h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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))
⊢ sSup (f '' f ⁻¹' Iic x) ∈ Iic x
have inr : sSup (Iic x) ≤ x
Tactic: apply (csSup_le_csSup bddAbove_Iic _ (image_preimage_subset ..)).trans
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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
⊢ sSup (f '' f ⁻¹' Iic x) ∈ Iic x
have apply : (f '' f ⁻¹' Iic x).Nonempty
Tactic: apply (csSup_le_csSup bddAbove_Iic _ (image_preimage_subset ..)).trans
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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))
⊢ sSup (Iic x) ≤ x
have inr : x ≤ x
Tactic: rw [csSup_Iic]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ f a = ⨆ (b : (↑(Iio a) : Type u_1)), f (↑b : α)
have h : a = ⨆ (i : (↑(Iio a) : Type u_1)), (↑i : α)
Tactic: convert! map_iSup hf _
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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 : α)
⊢ f a = ⨆ (b : (↑(Iio a) : Type u_1)), f (↑b : α)
have convert_2 : Nonempty.{u_1 + 1} (↑(Iio a) : Type u_1)
Tactic: convert! map_iSup hf _
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ f a = ⨆ (b : (↑(Iio a) : Type u_1)), f (↑b : α)
have convert_4 : BddAbove.{u_1} (α := α) (range (ι := (↑(Iio a) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iio a)))
Tactic: convert! map_iSup hf _
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ BddAbove.{u_1} (α := α) (range (ι := (↑(Iio a) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iio a)))
have h : Membership.mem (γ := Set α)
  (upperBounds (range (ι := (↑(Iio a) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iio a)))) a
Tactic: use a
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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
have refine : ∀ (a b : α), a < b → f a < f b
Tactic: refine ⟨fun a b ↦ ?_, fun ha ↦ (hl ha).2⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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
⊢ f a < f (succ b)
have succ : ∀ (hb : ¬IsMax a) (IH : a < a → f a < f a) (hab : a < succ a), f a < f (succ a)
Tactic: obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
Cleared hypotheses: b, hb, IH, hab
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ f a < f (Order.succ b)
have succ₁ : ∀ (h : a < b), f a < f (Order.succ b)
Tactic: obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
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
⊢ f a < f b
have hab' : succ a < b
Tactic: have hab' := hb.succ_lt hab
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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 : α
⊢ a < b → f a < f b
have isMin : ∀ (b : α) (hb : IsMin 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'))
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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 : α
isMin : ∀ (b : α) (hb : IsMin b), a < b → f a < f b
⊢ a < b → f a < f b
have succ : ∀ (b : α) (hb : ¬IsMax b) (IH : a < b → f a < f b), a < succ b → f a < f (succ 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'))
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ a < b → f a < f b
have isSuccLimit : ∀ (b : α) (hb : IsSuccLimit b) (IH : ∀ b_1 < b, a < b_1 → f a < f b_1), 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'))
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
have mp : f = g → f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ f = g ↔ f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)
have mpr : (f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)) → f = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ f = g
have mpr : ∀ (a : α), f a = g a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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 ⊥
⊢ f a = g a
have mpr₁ : g ⊥ = g ⊥
Tactic: rw [ha.eq_bot, H₁]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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 a = g a
have mpr : IsLUB (f '' Iio a) (g a)
Tactic: apply (hf.isLUB_image_Iio_of_isSuccLimit ha).unique
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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 (f '' Iio a) (g a)
have h : f '' Iio a = g '' Iio a
Tactic: convert! hg.isLUB_image_Iio_of_isSuccLimit ha using 1
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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 : α
⊢ f a = g a
have mpr : ∀ (a : α) (ha : IsMin 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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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
⊢ f a = g a
have mpr₁ : ∀ (a : α) (ha : ¬IsMax a) (IH : f a = g a), f (succ a) = g (succ 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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ f a = g a
have mpr₂ : ∀ (a : α) (ha : IsSuccLimit a) (IH : ∀ b < a, f b = g b), 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
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
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
⊢ ∃ (a : α), f a ≤ x ∧ x < f (succ a)
have this : Nonempty β
Tactic: have : Nonempty β := ⟨x⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
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 β
⊢ ∃ (a : α), f a ≤ x ∧ x < f (succ a)
have H : 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⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
have refine_1 : f (sSup (f ⁻¹' Iic x)) ≤ x
Tactic: refine ⟨sSup (f ⁻¹' Set.Iic x), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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
⊢ ∃ (a : α), f a ≤ x ∧ x < f (succ a)
have refine_2 : x < f (succ (sSup (f ⁻¹' Iic x)))
Tactic: refine ⟨sSup (f ⁻¹' Set.Iic x), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ f (sSup (f ⁻¹' Iic x)) ≤ x
have refine_1 : sSup (f ⁻¹' Iic x) ≤ sSup (f ⁻¹' Iic x)
Tactic: rw [hf.le_iff_le_sSup ⟨⊥, hx⟩ H]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))
have refine_2 : ¬f (succ (sSup (f ⁻¹' Iic x))) ≤ x
Tactic: rw [← not_le, hf.le_iff_le_sSup ⟨⊥, hx⟩ H, not_le, lt_succ_iff]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))
have refine_2₁ : ¬succ (sSup (f ⁻¹' Iic x)) ≤ sSup (f ⁻¹' Iic x)
Tactic: rw [← not_le, hf.le_iff_le_sSup ⟨⊥, hx⟩ H, not_le, lt_succ_iff]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))
have refine_2₂ : sSup (f ⁻¹' Iic x) < succ (sSup (f ⁻¹' Iic x))
Tactic: rw [← not_le, hf.le_iff_le_sSup ⟨⊥, hx⟩ H, not_le, lt_succ_iff]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
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))
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))
have refine_2₃ : sSup (f ⁻¹' Iic x) ≤ sSup (f ⁻¹' Iic x)
Tactic: rw [← not_le, hf.le_iff_le_sSup ⟨⊥, hx⟩ H, not_le, lt_succ_iff]
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ (f ⁻¹' s).Nonempty
have obtain : ∀ (b : α) (hb : b ∈ s), (f ⁻¹' s).Nonempty
Tactic: obtain ⟨b, hb⟩ := hs₀
Cleared hypotheses: hs₀
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
b : α
hb : b ∈ s
⊢ (f ⁻¹' s).Nonempty
have obtain : ∀ (c : α) (hb : f c ∈ s), (f ⁻¹' s).Nonempty
Tactic: obtain ⟨c, rfl⟩ := hs hb
Cleared hypotheses: b, hb