awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : OrderBot ι
i j : ι
⊢ toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j
have rw : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ toZ ⊥ i ≤ toZ ⊥ j
Tactic: rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : NoMaxOrder ι
inst_5 : OrderBot ι
i j : ι
rw : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ toZ ⊥ i ≤ toZ ⊥ j
⊢ toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j
have rw₁ : toZ ⊥ i ≤ toZ ⊥ j ↔ toZ ⊥ i ≤ toZ ⊥ j
Tactic: rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
⊢ (fun (i : ι) ↦
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat ⋯ :
          ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))))
      ((fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ (succ^[(↑n : ℕ)] ⊥ : ι)) n) =
    n
have a : (↑((fun (i : ι) ↦
          (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat sorry :
            ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))))
        ((fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ (succ^[(↑n : ℕ)] ⊥ : ι)) n)) :
    ℕ) =
  (↑n : ℕ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
⊢ (↑((fun (i : ι) ↦
            (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat ⋯ :
              ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))))
          ((fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ (succ^[(↑n : ℕ)] ⊥ : ι)) n)) :
      ℕ) =
    (↑n : ℕ)
have a : (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat = (↑n : ℕ)
Tactic: simp only
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
⊢ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat = (↑n : ℕ)
have a : (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat ≤ (↑n : ℕ)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
a : (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat ≤ (↑n : ℕ)
⊢ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat = (↑n : ℕ)
have a₁ : (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
⊢ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat ≤ (↑n : ℕ)
have a : toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥) ≤ (↑(↑n : ℕ) : ℤ)
Tactic: rw [Int.toNat_le]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
have pos : ∀ (hn_max : IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)), (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
Tactic: by_cases hn_max : IsMax (succ^[↑n] (⊥ : ι))
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
pos : ∀ (hn_max : IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)), (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
have neg : ∀ (hn_max : ¬IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)), (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
Tactic: by_cases hn_max : IsMax (succ^[↑n] (⊥ : ι))
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
have hn_max₁ : Eq.{u_1 + 1} (α := ι) (succ^[(↑n : ℕ)] ⊥) ⊤
Tactic: rw [← isTop_iff_isMax, isTop_iff_eq_top] at hn_max
Cleared hypotheses: hn_max
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : Eq.{u_1 + 1} (α := ι) (succ^[(↑n : ℕ)] ⊥) ⊤
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
have pos : (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ ⊤).toNat
Tactic: rw [hn_max]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax.{u_1} (α := ι) (succ^[(↑n : ℕ)] ⊥)
⊢ (↑n : ℕ) ≤ (toZ.{u_1} (ι := ι) ⊥ (succ^[(↑n : ℕ)] ⊥)).toNat
have neg : (↑n : ℕ) ≤ Int.toNat (↑(↑n : ℕ) : ℤ)
Tactic: rw [toZ_iterate_succ_of_not_isMax _ hn_max]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
i j : ι
⊢ LE.le (α := ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)))
      ((({
                toFun := fun (i : ι) ↦
                  Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat
                    ⋯,
                invFun := fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ succ^[(↑n : ℕ)] ⊥,
                left_inv := ⋯, right_inv := ⋯ } :
              ι ≃ ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) :
            (a : ι) → ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1)))
          i :
        ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)))
      ((({
                toFun := fun (i : ι) ↦
                  Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1)) (toZ ⊥ i).toNat
                    ⋯,
                invFun := fun (n : ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↦ succ^[(↑n : ℕ)] ⊥,
                left_inv := ⋯, right_inv := ⋯ } :
              ι ≃ ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) :
            (a : ι) → ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1)))
          j :
        ↥(Finset.range ((toZ.{u_1} (ι := ι) ⊥ ⊤).toNat + 1))) ↔
    i ≤ j
have simp : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j
Tactic: simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Int.toNat_le]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
i j : ι
⊢ toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j
have rw : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ toZ ⊥ i ≤ toZ ⊥ j
Tactic: rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
inst_4 : OrderBot ι
inst_5 : OrderTop ι
i j : ι
rw : toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ toZ ⊥ i ≤ toZ ⊥ j
⊢ toZ ⊥ i ≤ (↑(toZ ⊥ j).toNat : ℤ) ↔ i ≤ j
have rw₁ : toZ ⊥ i ≤ toZ ⊥ j ↔ toZ ⊥ i ≤ toZ ⊥ j
Tactic: rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico n m, r i (succ i)
hnm : n ≤ m
⊢ ReflTransGen r n m
have revert : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
have refine_1 : ∀ (h : ∀ i ∈ Ico n n, r i (succ i)), ReflTransGen r n n
Tactic: refine Succ.rec ?_ ?_ hnm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
refine_1 : ∀ (h : ∀ i ∈ Ico n n, r i (succ i)), ReflTransGen r n n
⊢ ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
have refine_2 : ∀ (n_1 : α) (hmn : n ≤ n_1),
  (∀ (h : ∀ i ∈ Ico n n_1, r i (succ i)), ReflTransGen r n n_1) →
    ∀ (h : ∀ i ∈ Ico n (succ n_1), r i (succ i)), ReflTransGen r n (succ n_1)
Tactic: refine Succ.rec ?_ ?_ hnm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m_1 : α
hnm_1 : n ≤ m_1
m : α
hnm : n ≤ m
ih : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
⊢ ReflTransGen r n (succ m)
have this : ReflTransGen r n m
Tactic: have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m_1 : α
hnm_1 : n ≤ m_1
m : α
hnm : n ≤ m
ih : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
⊢ ReflTransGen r n (succ m)
have refine_2 : ∀ (hm : m = succ m), ReflTransGen r n (succ m)
Tactic: rcases (le_succ m).eq_or_lt with hm | hm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m_1 : α
hnm_1 : n ≤ m_1
m : α
hnm : n ≤ m
ih : ∀ (h : ∀ i ∈ Ico n m, r i (succ i)), ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
refine_2 : ∀ (hm : m = succ m), ReflTransGen r n (succ m)
⊢ ReflTransGen r n (succ m)
have refine_2₁ : ∀ (hm : m < succ m), ReflTransGen r n (succ m)
Tactic: rcases (le_succ m).eq_or_lt with hm | hm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≤ n
⊢ ReflTransGen r n m
have rw : ReflTransGen (swap (φ := fun (a a_1 : α) ↦ Prop) r) m n
Tactic: rw [← reflTransGen_swap]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
inst_3 : Std.Refl r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
⊢ TransGen r n m
have inl : ∀ (h1 : ∀ i ∈ Ico m m, r i (succ i)) (h2 : ∀ i ∈ Ico m m, r (succ i) i), TransGen r m m
Tactic: rcases eq_or_ne m n with (rfl | hmn)
Cleared hypotheses: n, h1, h2
-- Lean 4 proof step from Mathlib.Order.SuccPred.Relation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
r : α → α → Prop
n m : α
inst_3 : Std.Refl r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
inl : ∀ (h1 : ∀ i ∈ Ico m m, r i (succ i)) (h2 : ∀ i ∈ Ico m m, r (succ i) i), TransGen r m m
⊢ TransGen r n m
have inr : ∀ (hmn : m ≠ n), TransGen r n m
Tactic: rcases eq_or_ne m n with (rfl | hmn)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
⊢ Eq.{u_1 + 1} (α := α) (findAtom ⊥) ⊥
have h : Eq.{u_1 + 1} (α := α) (Order.pred ⊥) ⊥
Tactic: apply Function.iterate_fixed
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
⊢ Order.pred (Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1] r) = ⊥
have generalize : ∀ (n : ℕ) (h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) sorry = n), Order.pred (Order.pred^[n - 1] r) = ⊥
Tactic: generalize h : Nat.find (bot_le (a := r)).exists_pred_iterate = n
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
n : ℕ
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n
⊢ Order.pred (Order.pred^[n - 1] r) = ⊥
have zero : ∀ (h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) sorry = 0), Order.pred (Order.pred^[HSub.hSub (α := ℕ) 0 1] r) = ⊥
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
n : ℕ
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n
zero :
  ∀ (h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0),
    Order.pred (Order.pred^[HSub.hSub (α := ℕ) 0 1] r) = ⊥
⊢ Order.pred (Order.pred^[n - 1] r) = ⊥
have succ : ∀ (n : ℕ) (h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) sorry = n + 1), Order.pred (Order.pred^[n + 1 - 1] r) = ⊥
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0
⊢ Order.pred^[0] r = ⊥
have rw : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) sorry] r = ⊥
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0
⊢ Order.pred (Order.pred^[HSub.hSub (α := ℕ) 0 1] r) = ⊥
have this : Order.pred^[0] r = ⊥
Tactic: have : Order.pred^[0] r = ⊥ := by
      rw [← h]
      apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
n : ℕ
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n + 1
⊢ Order.pred (Order.pred^[n + 1 - 1] r) = ⊥
have succ : Order.pred^[n + 1] r = ⊥
Tactic: simp only [Nat.add_sub_cancel_right, ← Function.iterate_succ_apply', Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
n : ℕ
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n + 1
⊢ Order.pred^[n + 1] r = ⊥
have succ : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) sorry] r = ⊥
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1] r = ⊥
⊢ r = ⊥
have this : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) sorry ≤ Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) sorry - 1
Tactic: have := Nat.find_min' (bot_le (a := r)).exists_pred_iterate h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1] r = ⊥
this : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ ≤ Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1
⊢ r = ⊥
have this₁ : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) sorry = 0
Tactic: replace : Nat.find (bot_le (a := r)).exists_pred_iterate = 0 := by lia
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ IsAtom (findAtom r)
have left : findAtom r ≠ ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
hr : r ≠ ⊥
left : findAtom r ≠ ⊥
⊢ IsAtom (findAtom r)
have right : ∀ b < findAtom r, b = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b < findAtom r
⊢ b = ⊥
have hb₁ : b ≤ Order.pred (findAtom r)
Tactic: apply Order.le_pred_of_lt at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : IsAtom (findAtom r)
nh : r = ⊥
⊢ False
have h₁ : IsAtom.{u_1} (α := α) ⊥
Tactic: simp only [nh, findAtom_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
b : α
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have rw : ¬b = ⊥ → ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
b : α
hb : ¬b = ⊥
w : α
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b
have left : IsAtom (findAtom b)
Tactic: use findAtom b, isAtom_findAtom hb, findAtom_le b
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
b : α
hb : ¬b = ⊥
w : α
left : IsAtom (findAtom b)
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b
have right : findAtom b ≤ b
Tactic: use findAtom b, isAtom_findAtom hb, findAtom_le b
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
b : α
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have rw : ¬b = ⊥ → ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: classical
    rw [or_iff_not_imp_left]
    intro hb
    use findAtom b, isAtom_findAtom hb, findAtom_le b
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ t₁.root ≤ v₁ ⊓ v₂
have simp : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
Tactic: simp only [le_inf_iff]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ False
have this : t₁.root ≤ v₁ ⊓ v₂
Tactic: have : t₁.root ≤ (v₁ : t) ⊓ (v₂ : t) := by
      simp only [le_inf_iff]
      exact ⟨h₁, nh ▸ h₂⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root ≤ v₁ ⊓ v₂
⊢ False
have this₁ : t₁.root ≤ ⊥
Tactic: rw [h.eq_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root ≤ ⊥
⊢ False
have this₁ : t₁.root = ⊥
Tactic: simp only [le_bot_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : t₁ ≠ t₂
⊢ Disjoint v₁ v₂
have h₃ : t₁.root ≤ v₁
Tactic: rw [SubRootedTree.mem_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : t₁ ≠ t₂
h₃ : t₁.root ≤ v₁
⊢ Disjoint v₁ v₂
have h₄ : t₂.root ≤ v₂
Tactic: rw [SubRootedTree.mem_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : t₁ ≠ t₂
⊢ Disjoint v₁ v₂
have contrapose : ∀ (h : ¬Disjoint v₁ v₂), t₁ = t₂
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ¬Disjoint v₁ v₂
⊢ t₁ = t₂
have h₃ : ⊥ < v₁ ⊓ v₂
Tactic: rw [disjoint_iff, ← ne_eq, ← bot_lt_iff_ne_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
⊢ t₁ = t₂
have inl : ∀ (oh : v₁ ⊓ v₂ < t₁.root), t₁ = t₂
Tactic: rcases lt_or_le_of_directed (by simp : v₁ ⊓ v₂ ≤ v₁) h₁ with oh | oh
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (goal)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
inl : ∀ (oh : v₁ ⊓ v₂ < t₁.root), t₁ = t₂
⊢ t₁ = t₂
have inr : ∀ (oh : t₁.root ≤ v₁ ⊓ v₂), t₁ = t₂
Tactic: rcases lt_or_le_of_directed (by simp : v₁ ⊓ v₂ ≤ v₁) h₁ with oh | oh
-- Lean 4 proof step from Mathlib.Order.SuccPred.Tree (hypothesis)
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ⊓ v₂
⊢ t₁ = t₂
have oh₁ : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
Tactic: rw [le_inf_iff] at oh
Cleared hypotheses: oh