awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
c : ↥S := Subtype.mk (p := fun (x : X) ↦ x ∈ S) (a ⇨ (↑s : X)) ⋯
rw : S.restrictAux b ≤ c ↔ b ≤ (↑c : X)
⊢ (↑(S.restrictAux b) : X) ≤ (↑c : X) ↔ b ≤ (↑c : X)
have rw₁ : b ≤ (↑c : X) ↔ b ≤ (↑c : X)
Tactic: rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
⊢ S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux (a ⊓ b) ≤ s
have _ : S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s
Tactic: calc
      _ ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s := by simp
      _ ↔ S.restrictAux b ≤ a ⇨ s := by rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
      _ ↔ b ≤ a ⇨ s := by
        set c : S := ⟨a ⇨ s, S.himp_mem s.coe_prop⟩
        change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c
        rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]
      _ ↔ S.restrictAux (a ⊓ b) ≤ s := by simp [inf_comm, S.giAux.gc.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
_ : S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s
⊢ S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux (a ⊓ b) ≤ s
have _₁ : S.restrictAux a ≤ S.restrictAux b ⇨ s ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
Tactic: calc
      _ ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s := by simp
      _ ↔ S.restrictAux b ≤ a ⇨ s := by rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
      _ ↔ b ≤ a ⇨ s := by
        set c : S := ⟨a ⇨ s, S.himp_mem s.coe_prop⟩
        change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c
        rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]
      _ ↔ S.restrictAux (a ⊓ b) ≤ s := by simp [inf_comm, S.giAux.gc.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
_ : S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s
_₁ : S.restrictAux a ≤ S.restrictAux b ⇨ s ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
⊢ S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux (a ⊓ b) ≤ s
have _₂ : (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X) ↔ b ≤ a ⇨ (↑s : X)
Tactic: calc
      _ ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s := by simp
      _ ↔ S.restrictAux b ≤ a ⇨ s := by rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
      _ ↔ b ≤ a ⇨ s := by
        set c : S := ⟨a ⇨ s, S.himp_mem s.coe_prop⟩
        change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c
        rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]
      _ ↔ S.restrictAux (a ⊓ b) ≤ s := by simp [inf_comm, S.giAux.gc.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
_ : S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s
_₁ : S.restrictAux a ≤ S.restrictAux b ⇨ s ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
_₂ : (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X) ↔ b ≤ a ⇨ (↑s : X)
⊢ S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux (a ⊓ b) ≤ s
have _₃ : b ≤ a ⇨ (↑s : X) ↔ S.restrictAux (a ⊓ b) ≤ s
Tactic: calc
      _ ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s := by simp
      _ ↔ S.restrictAux b ≤ a ⇨ s := by rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
      _ ↔ b ≤ a ⇨ s := by
        set c : S := ⟨a ⇨ s, S.himp_mem s.coe_prop⟩
        change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c
        rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]
      _ ↔ S.restrictAux (a ⊓ b) ≤ s := by simp [inf_comm, S.giAux.gc.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ Eq.{u_1 + 1} (α := ↥S) (sInf {s : ↥S | ⊤ ≤ (↑s : X)}) ⊤
have refine : LE.le.{u_1} (α := ↥S) ⊤ (sInf {s : ↥S | ⊤ ≤ (↑s : X)})
Tactic: refine le_antisymm le_top ?_
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ LE.le.{u_1} (α := ↥S) ⊤ (sInf {s : ↥S | ⊤ ≤ (↑s : X)})
have change : ⊤ ≤ S.restrictAux ⊤
Tactic: change _ ≤ restrictAux S ⊤
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ ⊤ ≤ S.restrictAux ⊤
have rw : ⊤ ≤ (↑(S.restrictAux ⊤) : X)
Tactic: rw [← Subtype.coe_le_coe, S.giAux.gc.u_top]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
⊢ Eq (α := ↥S) (sInf {s_2 : ↥S | sSup s ≤ (↑s_2 : X)}) (sSup ((fun (x : X) ↦ sInf {s : ↥S | x ≤ (↑s : X)}) '' s))
have change : S.restrictAux (sSup s) = sSup ((fun (x : X) ↦ sInf {s : ↥S | x ≤ (↑s : X)}) '' s)
Tactic: change Sublocale.restrictAux S (sSup s) = _
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a b : X
S : Sublocale X
s : Set X
⊢ S.restrictAux (sSup s) = sSup ((fun (x : X) ↦ sInf {s : ↥S | x ≤ (↑s : X)}) '' s)
have rw : Eq.{u_1 + 1} (α := ↥S) (⨆ a ∈ s, S.restrictAux a) (⨆ a ∈ s, sInf {s : ↥S | a ≤ (↑s : X)})
Tactic: rw [S.giAux.gc.l_sSup, sSup_image]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
⊢ LE.le (α := X) (↑((S.restrict : (a : X) → ↥S) (↑((S.restrict : (a : X) → ↥S) x) : X)) : X)
    (↑((S.restrict : (a : X) → ↥S) x) : X)
have rw : LE.le.{u_1} (α := X) (↑((S.restrict : (a : X) → ↥S) x) : X) (↑((S.restrict : (a : X) → ↥S) x) : X)
Tactic: rw [S.giRestrict.gc.l_u_l_eq_l]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
⊢ range (ι := X) (⇑S.toNucleus : (a : X) → X) = (↑S : Set X)
have h : ∀ (x : X), Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x ↔ x ∈ (↑S : Set X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x ↔ x ∈ (↑S : Set X)
have h : Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x → x ∈ (↑S : Set X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
x : X
h : Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x → x ∈ (↑S : Set X)
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x ↔ x ∈ (↑S : Set X)
have h₁ : x ∈ (↑S : Set X) → Membership.mem (γ := Set X) (range (ι := X) (⇑S.toNucleus : (a : X) → X)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range (ι := X) (⇑n : (a : X) → X)
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) (sInf a)
have rw : (n : (a : X) → X) (sInf a) = sInf a
Tactic: rw [mem_range]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range (ι := X) (⇑n : (a : X) → X)
⊢ (n : (a : X) → X) (sInf a) = sInf a
have refine : ∀ (b : X) (h1 : b ∈ a), (n : (a : X) → X) (sInf a) ≤ b
Tactic: refine le_antisymm (le_sInf_iff.mpr (fun b h1 ↦ ?_)) le_apply
-- Lean 4 proof step from Mathlib.Order.Sublocale (hypothesis)
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range (ι := X) (⇑n : (a : X) → X)
b : X
h1 : b ∈ a
⊢ (n : (a : X) → X) (sInf a) ≤ b
have h₁ : ∀ x ∈ a, (n : (a : X) → X) x = x
Tactic: simp_rw [subset_def, mem_range] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a : Set X
b : X
h1 : b ∈ a
h : ∀ x ∈ a, (n : (a : X) → X) x = x
⊢ (n : (a : X) → X) (sInf a) ≤ b
have rw : LE.le (α := X) ((n : (a : X) → X) (sInf a) : X) ((n : (a : X) → X) b : X)
Tactic: rw [← h b h1]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a b : X
h : Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) b
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) (a ⇨ b)
have rw : ∀ (h : (n : (a : X) → X) b = b), (n : (a : X) → X) (a ⇨ b) = a ⇨ b
Tactic: rw [mem_range, ← h, map_himp_apply] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a b : X
h : Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) b
rw : ∀ (h : (n : (a : X) → X) b = b), (n : (a : X) → X) (a ⇨ b) = a ⇨ b
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) (a ⇨ b)
have rw₁ : ∀ (h : Eq (α := X) ((n : (a : X) → X) ((n : (a : X) → X) b : X) : X) ((n : (a : X) → X) b : X)),
  (n : (a : X) → X) (a ⇨ (n : (a : X) → X) b) = a ⇨ (n : (a : X) → X) b
Tactic: rw [mem_range, ← h, map_himp_apply] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
a b : X
h : Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) b
rw : ∀ (h : (n : (a : X) → X) b = b), (n : (a : X) → X) (a ⇨ b) = a ⇨ b
rw₁ :
  ∀ (h : Eq (α := X) ((n : (a : X) → X) ((n : (a : X) → X) b : X) : X) ((n : (a : X) → X) b : X)),
    (n : (a : X) → X) (a ⇨ (n : (a : X) → X) b) = a ⇨ (n : (a : X) → X) b
⊢ Membership.mem (γ := Set X) (range (ι := X) (⇑n : (a : X) → X)) (a ⇨ b)
have rw₂ : ∀ (h : Eq (α := X) ((n : (a : X) → X) ((n : (a : X) → X) b : X) : X) ((n : (a : X) → X) b : X)),
  a ⇨ (n : (a : X) → X) b = a ⇨ (n : (a : X) → X) b
Tactic: rw [mem_range, ← h, map_himp_apply] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
n : Nucleus X
x : X
⊢ Eq (α := ↥n.toSublocale) ((n.toSublocale.restrict : (a : X) → ↥n.toSublocale) x : ↥n.toSublocale)
    (Subtype.mk (p := fun (x : X) ↦ x ∈ n.toSublocale) ((n : (a : X) → X) x) ⋯ : ↥n.toSublocale)
have a : Eq (α := X) ((↑((n.toSublocale.restrict : (a : X) → ↥n.toSublocale) x) : X) : X)
  ((↑(Subtype.mk (p := fun (x : X) ↦ x ∈ n.toSublocale) ((n : (a : X) → X) x) sorry) : X) : X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
⊢ (fun (n : (Nucleus X)ᵒᵈ) ↦
        (Nucleus.toSublocale ((OrderDual.ofDual : (a : (Nucleus X)ᵒᵈ) → Nucleus X) n) : Sublocale X))
      ((fun (s : Sublocale X) ↦ ((OrderDual.toDual : (a : Nucleus X) → (Nucleus X)ᵒᵈ) s.toNucleus : (Nucleus X)ᵒᵈ)) S) =
    S
have h : ∀ (x : X),
  Membership.mem (γ := Sublocale X)
      ((fun (n : (Nucleus X)ᵒᵈ) ↦
          (Nucleus.toSublocale ((OrderDual.ofDual : (a : (Nucleus X)ᵒᵈ) → Nucleus X) n) : Sublocale X))
        ((fun (s : Sublocale X) ↦ ((OrderDual.toDual : (a : Nucleus X) → (Nucleus X)ᵒᵈ) s.toNucleus : (Nucleus X)ᵒᵈ))
          S))
      x ↔
    x ∈ S
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
a b : α
⊢ (∃ (n : ℕ), succ^[n] a = b) ↔ a ≤ b
have refine : (∃ (n : ℕ), succ^[n] a = b) → a ≤ b
Tactic: refine ⟨?_, exists_succ_iterate_of_le⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : α
hmn : m ≤ n
⊢ P n hmn
have obtain : ∀ (n : ℕ) (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
Tactic: obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ^[n + 1] m) hmn
have succ₁ : P (Order.succ (Order.succ^[n] m)) sorry
Tactic: simp_rw [Function.iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
hmn : m ≤ Order.succ^[n] m
⊢ P (Order.succ^[n] m) hmn
have zero : ∀ (hmn : m ≤ Order.succ^[0] m), P (Order.succ^[0] m) hmn
Tactic: induction n with
  | zero => exact rfl
  | succ n ih =>
    simp_rw [Function.iterate_succ_apply']
    exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
hmn : m ≤ Order.succ^[n] m
zero : ∀ (hmn : m ≤ Order.succ^[0] m), P (Order.succ^[0] m) hmn
⊢ P (Order.succ^[n] m) hmn
have succ₁ : ∀ (n : ℕ) (ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn) (hmn : m ≤ Order.succ^[n + 1] m),
  P (Order.succ^[n + 1] m) hmn
Tactic: induction n with
  | zero => exact rfl
  | succ n ih =>
    simp_rw [Function.iterate_succ_apply']
    exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
p : α → Prop
hsucc : ∀ (a : α), p a ↔ p (succ a)
a b : α
h : a ≤ b
⊢ p a ↔ p b
have obtain : ∀ (n : ℕ) (h : a ≤ succ^[n] a), p a ↔ p (succ^[n] a)
Tactic: obtain ⟨n, rfl⟩ := h.exists_succ_iterate
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ ≤ v₂ ∨ v₂ ≤ v₁
have obtain : ∀ (n : ℕ) (h₁ : r ≤ succ^[n] r), succ^[n] r ≤ v₂ ∨ v₂ ≤ succ^[n] r
Tactic: obtain ⟨n, rfl⟩ := h₁.exists_succ_iterate
Cleared hypotheses: v₁, h₁
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₂ : α
h₂ : r ≤ v₂
n : ℕ
h₁ : r ≤ succ^[n] r
⊢ succ^[n] r ≤ v₂ ∨ v₂ ≤ succ^[n] r
have obtain : ∀ (m : ℕ) (h₂ : r ≤ succ^[m] r), succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
Tactic: obtain ⟨m, rfl⟩ := h₂.exists_succ_iterate
Cleared hypotheses: v₂, h₂
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
have inr : ∀
  (this :
    ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
      succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r)
  (h : ¬n ≤ m), succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
Tactic: wlog h : n ≤ m
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
inr :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
        succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r)
    (h : ¬n ≤ m), succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
have wlog : ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
  succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
Tactic: wlog h : n ≤ m
Cleared hypotheses: inst_1, inst_2, r, n, m
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
    succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
have inr : succ^[m] r ≤ succ^[n] r ∨ succ^[n] r ≤ succ^[m] r
Tactic: rw [Or.comm]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_3 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ) (h : n ≤ m),
    succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[m] r ≤ succ^[n] r ∨ succ^[n] r ≤ succ^[m] r
have inr : m ≤ n
Tactic: apply this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
have h₁ : succ^[n] r ≤ succ^[m] r
Tactic: left
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r
have h₁ : ∀ (k : ℕ) (h : n ≤ n + k), succ^[n] r ≤ succ^[n + k] r
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α_1 : Type u_1
inst : Preorder α_1
α : Type u_1
inst_1 : Preorder α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[n + k] r
have h₁ : succ^[n] r ≤ succ^[k] (succ^[n] r)
Tactic: rw [Nat.add_comm, Function.iterate_add, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ < v₂ ∨ v₂ ≤ v₁
have rw : ¬v₂ ≤ v₁ → v₁ < v₂
Tactic: rw [Classical.or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
⊢ v₁ < v₂
have inl : ∀ (h : v₁ ≤ v₂), v₁ < v₂
Tactic: rcases le_total_of_codirected h₁ h₂ with h | h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
inl : ∀ (h : v₁ ≤ v₂), v₁ < v₂
⊢ v₁ < v₂
have inr : ∀ (h : v₂ ≤ v₁), v₁ < v₂
Tactic: rcases le_total_of_codirected h₁ h₂ with h | h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
⊢ False
have hm' : ∀ (a : α), f a ≤ m
Tactic: have hm' : ∀ a, f a ≤ m := fun a ↦ hm <| Set.mem_range_self _
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
⊢ False
have obtain : ∀ (a₀ : α), False
Tactic: obtain ⟨a₀⟩ := ‹Nonempty α›
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
this : ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
⊢ False
have obtain : ∀ (a : α) (ha : m < f a), False
Tactic: obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
⊢ False
have suffices : ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
Tactic: suffices ∀ b, f a₀ ≤ b → ∃ a, b < f a by
    obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
    exact ha.not_ge (hm' a)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
⊢ ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
have h : ∀ (a : α), ∃ (a' : α), f a < f a'
Tactic: have h : ∀ a, ∃ a', f a < f a' := fun a ↦ (exists_gt a).imp (fun a' h ↦ hf h)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ (a' : α), f a < f a'
⊢ ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
have rfl : ∃ (a : α), f a₀ < f a
Tactic: apply Succ.rec
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : Preorder β
f : α → β
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
inst_5 : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ (a' : α), f a < f a'
rfl : ∃ (a : α), f a₀ < f a
⊢ ∀ (b : β), f a₀ ≤ b → ∃ (a : α), b < f a
have succ : ∀ (n : β) (hmn : f a₀ ≤ n), (∃ (a : α), n < f a) → ∃ (a : α), succ n < f a
Tactic: apply Succ.rec
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b : α
⊢ ∀ (h : a ≤ b), ∃ (n : ℕ), pred^[n] b = a
have refine : ∀ (x : α),
  (∀ y < x, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y) → (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) x
Tactic: refine WellFounded.fix (C := fun b => a ≤ b → ∃ n, Nat.iterate pred n b = a)
      h.wf ?_ b
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y
hab : a ≤ b
⊢ ∃ (n : ℕ), pred^[n] b = a
have hab₁ : a = b ∨ a < b
Tactic: replace hab := eq_or_lt_of_le hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h : WellFoundedLT α
inst_1 : PredOrder α
a b_1 b : α
ih : ∀ y < b, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y
hab : a = b ∨ a < b
⊢ ∃ (n : ℕ), pred^[n] b = a
have inl : ∀ (ih : ∀ y < a, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y), ∃ (n : ℕ), pred^[n] a = a
Tactic: rcases hab with (rfl | hab)
Cleared hypotheses: b, ih, hab