awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
n : ℕ
hi :
  ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c) (hn : pred^[n] c = b),
    pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α) ∉ s
⊢ pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have this : pred (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
Tactic: have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
n : ℕ
hi :
  ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c) (hn : pred^[n] c = b),
    pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α) ∉ s
this : pred (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
⊢ pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have neg : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: rw [Function.iterate_fixed]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
n : ℕ
hi :
  ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c) (hn : pred^[n] c = b),
    pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α) ∉ s
this : pred (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have this₁ : IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc)
Tactic: simp only [Order.pred_eq_iff_isMin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
n : ℕ
hi :
  ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c) (hn : pred^[n] c = b),
    pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α) ∉ s
this : IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have apply : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
Tactic: apply (this.eq_of_le _).symm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : b ≤ c
n : ℕ
hn : pred^[n] c = b
⊢ pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have h : ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c) (hn : pred^[0] c = b),
  pred^[0] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: induction n generalizing c with
    | zero => simp_all
    | succ n hi =>
      simp_all only [Function.iterate_succ, Function.comp_apply]
      change Order.pred^[n] (dite ..) = _
      split_ifs with h
      · dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le
      · have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this
Cleared hypotheses: c, hc, hbc, n, hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : b ≤ c
n : ℕ
hn : pred^[n] c = b
h :
  ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c) (hn : pred^[0] c = b),
    pred^[0] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
⊢ pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have h₁ : ∀ (n : ℕ)
  (hi :
    ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c) (hn : pred^[n] c = b),
      pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb)
  (c : α) (hc : c ∈ s) (hbc : b ≤ c) (hn : pred^[n + 1] c = b),
  pred^[n + 1] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: induction n generalizing c with
    | zero => simp_all
    | succ n hi =>
      simp_all only [Function.iterate_succ, Function.comp_apply]
      change Order.pred^[n] (dite ..) = _
      split_ifs with h
      · dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le
      · have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this
Cleared hypotheses: c, hc, hbc, n, hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
⊢ ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have simp : ∀ (hbc : b ≤ c),
  ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: classical
    simp only [Subtype.mk_le_mk] at hbc
    obtain ⟨n, hn⟩ := hbc.exists_pred_iterate
    use n
    induction n generalizing c with
    | zero => simp_all
    | succ n hi =>
      simp_all only [Function.iterate_succ, Function.comp_apply]
      change Order.pred^[n] (dite ..) = _
      split_ifs with h
      · dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le
      · have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
simp :
  ∀ (hbc : b ≤ c),
    ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
⊢ ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have simp₁ : ∀ (hbc : b ≤ c) (n : ℕ) (hn : pred^[n] c = b),
  ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: classical
    simp only [Subtype.mk_le_mk] at hbc
    obtain ⟨n, hn⟩ := hbc.exists_pred_iterate
    use n
    induction n generalizing c with
    | zero => simp_all
    | succ n hi =>
      simp_all only [Function.iterate_succ, Function.comp_apply]
      change Order.pred^[n] (dite ..) = _
      split_ifs with h
      · dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le
      · have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
s : Set α
inst_3 : s.OrdConnected
x x_1 : (↑s : Type u_1)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
simp :
  ∀ (hbc : b ≤ c),
    ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
simp₁ :
  ∀ (hbc : b ≤ c) (n : ℕ) (hn : pred^[n] c = b),
    ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
⊢ ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have h : ∀ (hbc : b ≤ c) (n : ℕ) (hn : pred^[n] c = b),
  pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: classical
    simp only [Subtype.mk_le_mk] at hbc
    obtain ⟨n, hn⟩ := hbc.exists_pred_iterate
    use n
    induction n generalizing c with
    | zero => simp_all
    | succ n hi =>
      simp_all only [Function.iterate_succ, Function.comp_apply]
      change Order.pred^[n] (dite ..) = _
      split_ifs with h
      · dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le
      · have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]
        rw [Function.iterate_fixed]
        · simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc
        · exact this
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f a ≤ f b
have obtain : ∀ (n : ℕ) (hb : succ^[n] a ∈ s) (hab : a ≤ succ^[n] a), f a ≤ f (succ^[n] a)
Tactic: obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : ∀ (hb : succ^[n] a ∈ s), f a ≤ f (succ^[n] a)
hb : succ^[n + 1] a ∈ s
⊢ f a ≤ f (succ^[n + 1] a)
have succ : ∀ (hb : succ (succ^[n] a) ∈ s), f a ≤ f (succ (succ^[n] a))
Tactic: rw [Function.iterate_succ_apply'] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : ∀ (hb : succ^[n] a ∈ s), f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
⊢ f a ≤ f (succ (succ^[n] a))
have this : succ^[n] a ∈ s
Tactic: have : succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : ∀ (hb : succ^[n] a ∈ s), f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
⊢ f a ≤ f (succ (succ^[n] a))
have pos : ∀ (hb' : IsMax (succ^[n] a)), f a ≤ f (succ (succ^[n] a))
Tactic: by_cases hb' : IsMax (succ^[n] a)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : ∀ (hb : succ^[n] a ∈ s), f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
pos : ∀ (hb' : IsMax (succ^[n] a)), f a ≤ f (succ (succ^[n] a))
⊢ f a ≤ f (succ (succ^[n] a))
have neg : ∀ (hb' : ¬IsMax (succ^[n] a)), f a ≤ f (succ (succ^[n] a))
Tactic: by_cases hb' : IsMax (succ^[n] a)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : ∀ (hb : succ^[n] a ∈ s), f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
hb' : IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))
have pos : f a ≤ f (succ^[n] a)
Tactic: rw [succ_eq_iff_isMax.2 hb']
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n] a ∈ s
⊢ f a ≤ f (succ^[n] a)
have zero : ∀ (hb : succ^[0] a ∈ s), f a ≤ f (succ^[0] a)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n] a ∈ s
zero : ∀ (hb : succ^[0] a ∈ s), f a ≤ f (succ^[0] a)
⊢ f a ≤ f (succ^[n] a)
have succ : ∀ (n : ℕ) (hn : ∀ (hb : succ^[n] a ∈ s), f a ≤ f (succ^[n] a)) (hb : succ^[n + 1] a ∈ s), f a ≤ f (succ^[n + 1] a)
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b
have obtain : ∀ (n : ℕ) (hb : succ^[n] a ∈ s) (hab : a < succ^[n] a), f a < f (succ^[n] a)
Tactic: obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab.le
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n] a ∈ s
hab : a < succ^[n] a
⊢ f a < f (succ^[n] a)
have zero : ∀ (hb : succ^[0] a ∈ s) (hab : a < succ^[0] a), f a < f (succ^[0] a)
Tactic: obtain _ | n := n
Cleared hypotheses: n, hb, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n] a ∈ s
hab : a < succ^[n] a
zero : ∀ (hb : succ^[0] a ∈ s) (hab : a < succ^[0] a), f a < f (succ^[0] a)
⊢ f a < f (succ^[n] a)
have succ : ∀ (n : ℕ) (hb : succ^[n + 1] a ∈ s) (hab : a < succ^[n + 1] a), f a < f (succ^[n + 1] a)
Tactic: obtain _ | n := n
Cleared hypotheses: n, hb, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n + 1] a ∈ s
hab : a < succ^[n + 1] a
⊢ f a < f (succ^[n + 1] a)
have hab₁ : ¬IsMax a
Tactic: apply not_isMax_of_lt at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ^[n + 1 + 1] a ∈ s
⊢ f a < f (succ^[n + 1 + 1] a)
have succ : ∀ (hb : succ (succ^[n + 1] a) ∈ s), f a < f (succ (succ^[n + 1] a))
Tactic: rw [Function.iterate_succ_apply'] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
⊢ f a < f (succ (succ^[n + 1] a))
have this : succ^[n + 1] a ∈ s
Tactic: have : succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
⊢ f a < f (succ (succ^[n + 1] a))
have pos : ∀ (hb' : IsMax (succ^[n + 1] a)), f a < f (succ (succ^[n + 1] a))
Tactic: by_cases hb' : IsMax (succ^[n + 1] a)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
pos : ∀ (hb' : IsMax (succ^[n + 1] a)), f a < f (succ (succ^[n + 1] a))
⊢ f a < f (succ (succ^[n + 1] a))
have neg : ∀ (hb' : ¬IsMax (succ^[n + 1] a)), f a < f (succ (succ^[n + 1] a))
Tactic: by_cases hb' : IsMax (succ^[n + 1] a)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
n : ℕ
hn : ∀ (hb : succ^[n + 1] a ∈ s), f a < f (succ^[n + 1] a)
hb : succ (succ^[n + 1] a) ∈ s
this : succ^[n + 1] a ∈ s
hb' : IsMax (succ^[n + 1] a)
⊢ f a < f (succ (succ^[n + 1] a))
have pos : f a < f (succ^[n + 1] a)
Tactic: rw [succ_eq_iff_isMax.2 hb']
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n + 1] a ∈ s
hab : ¬IsMax a
⊢ f a < f (succ^[n + 1] a)
have succ : ∀ (hb : succ^[HAdd.hAdd (α := ℕ) 0 1] a ∈ s), f a < f (succ^[HAdd.hAdd (α := ℕ) 0 1] a)
Tactic: induction n with
  | zero => simpa using hf _ hab ha hb
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n + 1] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a < f (Order.succ a)
a : α
ha : a ∈ s
n : ℕ
hb : Order.succ^[n + 1] a ∈ s
hab : ¬IsMax a
succ : ∀ (hb : Order.succ^[HAdd.hAdd (α := ℕ) 0 1] a ∈ s), f a < f (Order.succ^[HAdd.hAdd (α := ℕ) 0 1] a)
⊢ f a < f (Order.succ^[n + 1] a)
have succ₁ : ∀ (n : ℕ) (hn : ∀ (hb : Order.succ^[n + 1] a ∈ s), f a < f (Order.succ^[n + 1] a)) (hb : Order.succ^[n + 1 + 1] a ∈ s),
  f a < f (Order.succ^[n + 1 + 1] a)
Tactic: induction n with
  | zero => simpa using hf _ hab ha hb
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n + 1] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f a ≤ f b
have obtain : ∀ (n : ℕ) (ha : pred^[n] b ∈ s) (hab : pred^[n] b ≤ b), f (pred^[n] b) ≤ f b
Tactic: obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred^[n + 1] b ∈ s
⊢ f (pred^[n + 1] b) ≤ f b
have succ : ∀ (ha : pred (pred^[n] b) ∈ s), f (pred (pred^[n] b)) ≤ f b
Tactic: rw [Function.iterate_succ_apply'] at ha ⊢
Cleared hypotheses: ha