awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inl : ∀ (ih : ∀ y < a, (fun (b : α) ↦ a ≤ b → ∃ (n : ℕ), pred^[n] b = a) y), ∃ (n : ℕ), pred^[n] a = a
⊢ ∃ (n : ℕ), pred^[n] b = a
have inr : ∀ (hab : a < b), ∃ (n : ℕ), pred^[n] b = a
Tactic: rcases hab with (rfl | 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
⊢ ∃ (n : ℕ), pred^[n] b = a
have inr : ∀ (hb : pred b = b), ∃ (n : ℕ), pred^[n] b = a
Tactic: rcases eq_or_lt_of_le (pred_le b) with hb | hb
-- 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
inr : ∀ (hb : pred b = b), ∃ (n : ℕ), pred^[n] b = a
⊢ ∃ (n : ℕ), pred^[n] b = a
have inr₁ : ∀ (hb : pred b < b), ∃ (n : ℕ), pred^[n] b = a
Tactic: rcases eq_or_lt_of_le (pred_le b) with hb | hb
-- 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, a ≤ y → ∃ (n : ℕ), pred^[n] y = a
hab : a < b
hb : pred b < b
⊢ ∃ (n : ℕ), pred^[n] b = a
have inr : ∀ (k : ℕ) (hk : pred^[k] (pred b) = a), ∃ (n : ℕ), pred^[n] b = a
Tactic: obtain ⟨k, hk⟩ := ih (pred b) hb (le_pred_of_lt 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, a ≤ y → ∃ (n : ℕ), pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ ∃ (n : ℕ), pred^[n] b = a
have inr : pred^[k + 1] b = a
Tactic: refine ⟨k + 1, ?_⟩
-- 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, a ≤ y → ∃ (n : ℕ), pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ pred^[k + 1] b = a
have inr : pred^[k] (pred^[1] b) = a
Tactic: rw [iterate_add_apply, iterate_one, hk]
-- 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, a ≤ y → ∃ (n : ℕ), pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
inr : pred^[k] (pred^[1] b) = a
inr₁ : pred^[k] (pred b) = a
⊢ pred^[k + 1] b = a
have inr₂ : a = a
Tactic: rw [iterate_add_apply, iterate_one, hk]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
⊢ (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
have refine : ∀ (h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)) (i : α) (hi : i ≠ ⊥), P i
Tactic: refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
i : α
hi : i ≠ ⊥
⊢ P i
have obtain : ∀ (j : ℕ) (hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥), P (Order.succ^[j] ⊥)
Tactic: obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
⊢ 0 < j
have a : j ≠ 0
Tactic: apply Nat.pos_of_ne_zero
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
⊢ j ≠ 0
have a : ∀ (hi : j = 0), Eq.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
Tactic: contrapose hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
⊢ P (Order.succ^[j] ⊥)
have have : ∀ (hj : 0 < j), P (Order.succ^[j] ⊥)
Tactic: have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose hi; simp [hi]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
hj : 0 < j
⊢ P (Order.succ^[j] ⊥)
have rw : P (Order.succ^[j.pred.succ] ⊥)
Tactic: rw [← Nat.succ_pred_eq_of_pos hj]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : PartialOrder α
inst_2 : OrderBot α
inst_3 : SuccOrder α
inst_4 : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (@succ _ PartialOrder.toPreorder _ i)
j : ℕ
hi : Ne.{u_1 + 1} (α := α) (Order.succ^[j] ⊥) ⊥
hj : 0 < j
⊢ P (Order.succ^[j.pred.succ] ⊥)
have simp : P (Order.succ (Order.succ^[j.pred] ⊥))
Tactic: simp only [Function.iterate_succ', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
hS : BddAbove S
hS' : S.Nonempty
⊢ ∃ (x : X), IsGreatest S x
have obtain : ∀ (m : X) (hm : m ∈ upperBounds S), ∃ (x : X), IsGreatest S x
Tactic: obtain ⟨m, hm⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
hS' : S.Nonempty
m : X
hm : m ∈ upperBounds S
⊢ ∃ (x : X), IsGreatest S x
have obtain : ∀ (n : X) (hn : n ∈ S), ∃ (x : X), IsGreatest S x
Tactic: obtain ⟨n, hn⟩ := hS'
Cleared hypotheses: hS'
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
⊢ ∃ (x : X), IsGreatest S x
have pos : ∀ (hm' : m ∈ S), ∃ (x : X), IsGreatest S x
Tactic: by_cases hm' : m ∈ S
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
pos : ∀ (hm' : m ∈ S), ∃ (x : X), IsGreatest S x
⊢ ∃ (x : X), IsGreatest S x
have neg : ∀ (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
Tactic: by_cases hm' : m ∈ S
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
⊢ ∃ (x : X), IsGreatest S x
have hn' : n ≤ m
Tactic: have hn' := hm hn
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m : X
hm : m ∈ upperBounds S
n : X
hn : n ∈ S
hm' : m ∉ S
hn' : n ≤ m
⊢ ∃ (x : X), IsGreatest S x
have neg : ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
Tactic: revert hn hm hm'
Cleared hypotheses: hm, hn, hm'
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
have neg : ∀ (hm : n ∈ upperBounds S) (hn : n ∈ S) (hm' : n ∉ S), ∃ (x : X), IsGreatest S x
Tactic: refine Succ.rec ?_ ?_ hn'
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
neg : ∀ (hm : n ∈ upperBounds S) (hn : n ∈ S) (hm' : n ∉ S), ∃ (x : X), IsGreatest S x
⊢ ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
have neg₁ : ∀ (n_1 : X) (hmn : n ≤ n_1),
  (∀ (hm : n_1 ∈ upperBounds S) (hn : n ∈ S) (hm' : n_1 ∉ S), ∃ (x : X), IsGreatest S x) →
    ∀ (hm : succ n_1 ∈ upperBounds S) (hn : n ∈ S) (hm' : succ n_1 ∉ S), ∃ (x : X), IsGreatest S x
Tactic: refine Succ.rec ?_ ?_ hn'
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ (x : X), IsGreatest S x
have IH₁ : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
Tactic: rw [mem_upperBounds] at IH hm
Cleared hypotheses: IH, hm, hn, hm'
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : m ∈ upperBounds S) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm : succ m ∈ upperBounds S
hn : n ∈ S
hm' : succ m ∉ S
IH₁ : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
⊢ ∃ (x : X), IsGreatest S x
have hm₁ : ∀ x ∈ S, x ≤ succ m
Tactic: rw [mem_upperBounds] at IH hm
Cleared hypotheses: IH, hm, hn, hm'
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ (x : X), IsGreatest S x
have hm₁ : ∀ x ∈ S, x = succ m ∨ x ≤ m
Tactic: simp_rw [Order.le_succ_iff_eq_or_le] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ x ≤ m
have refine : ¬x = succ m
Tactic: refine (hm x hx).resolve_left ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
⊢ ∃ (x : X), IsGreatest S x
have hm₁ : ∀ x ∈ S, x ≤ m
Tactic: replace hm : ∀ x ∈ S, x ≤ m := by
    intro x hx
    refine (hm x hx).resolve_left ?_
    rintro rfl
    exact hm' hx
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
⊢ ∃ (x : X), IsGreatest S x
have pos : ∀ (hmS : m ∈ S), ∃ (x : X), IsGreatest S x
Tactic: by_cases hmS : m ∈ S
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
inst : LinearOrder X
inst_1 : SuccOrder X
inst_2 : IsSuccArchimedean X
S : Set X
m_1 n : X
hn' : n ≤ m_1
m : X
hmn : n ≤ m
IH : ∀ (hm : ∀ x ∈ S, x ≤ m) (hn : n ∈ S) (hm' : m ∉ S), ∃ (x : X), IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x ≤ m
pos : ∀ (hmS : m ∈ S), ∃ (x : X), IsGreatest S x
⊢ ∃ (x : X), IsGreatest S x
have neg : ∀ (hmS : m ∉ S), ∃ (x : X), IsGreatest S x
Tactic: by_cases hmS : m ∈ S
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ (n : ℕ), succ^[n] a = b
have refine : ∀ (a_1 : ℕ), succ^[a_1] (EquivLike.inv f a) = EquivLike.inv f b → succ^[a_1] a = b
Tactic: refine (exists_succ_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ succ^[n] (EquivLike.inv f a) = EquivLike.inv f b → succ^[n] a = b
have rw : (f : (a : X) → Y) (succ^[n] (EquivLike.inv f a)) = b → succ^[n] a = b
Tactic: rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
⊢ succ^[n] a = (f : (a : X) → Y) (succ^[n] (EquivLike.inv f a))
have zero : ∀ {a : Y}, succ^[0] a = (f : (a : X) → Y) (succ^[0] (EquivLike.inv f a))
Tactic: induction n generalizing a with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]
Cleared hypotheses: a, n
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : SuccOrder X
inst_3 : IsSuccArchimedean X
inst_4 : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
zero : ∀ {a : Y}, succ^[0] a = (f : (a : X) → Y) (succ^[0] (EquivLike.inv f a))
⊢ succ^[n] a = (f : (a : X) → Y) (succ^[n] (EquivLike.inv f a))
have succ : ∀ (n : ℕ) (IH : ∀ {a : Y}, succ^[n] a = (f : (a : X) → Y) (succ^[n] (EquivLike.inv f a))) {a : Y},
  succ^[n + 1] a = (f : (a : X) → Y) (succ^[n + 1] (EquivLike.inv f a))
Tactic: induction n generalizing a with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]
Cleared hypotheses: a, n
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : PredOrder X
inst_3 : IsPredArchimedean X
inst_4 : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
⊢ ∃ (n : ℕ), pred^[n] b = a
have refine : ∀ (a_1 : ℕ), pred^[a_1] (EquivLike.inv f b) = EquivLike.inv f a → pred^[a_1] b = a
Tactic: refine (exists_pred_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : PredOrder X
inst_3 : IsPredArchimedean X
inst_4 : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ pred^[n] (EquivLike.inv f b) = EquivLike.inv f a → pred^[n] b = a
have rw : (f : (a : X) → Y) (pred^[n] (EquivLike.inv f b)) = a → pred^[n] b = a
Tactic: rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : PredOrder X
inst_3 : IsPredArchimedean X
inst_4 : PredOrder Y
f : X ≃o Y
b : Y
n : ℕ
⊢ pred^[n] b = (f : (a : X) → Y) (pred^[n] (EquivLike.inv f b))
have zero : ∀ {b : Y}, pred^[0] b = (f : (a : X) → Y) (pred^[0] (EquivLike.inv f b))
Tactic: induction n generalizing b with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_pred]
Cleared hypotheses: b, n
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : PartialOrder X
inst_1 : PartialOrder Y
inst_2 : PredOrder X
inst_3 : IsPredArchimedean X
inst_4 : PredOrder Y
f : X ≃o Y
b : Y
n : ℕ
zero : ∀ {b : Y}, pred^[0] b = (f : (a : X) → Y) (pred^[0] (EquivLike.inv f b))
⊢ pred^[n] b = (f : (a : X) → Y) (pred^[n] (EquivLike.inv f b))
have succ : ∀ (n : ℕ) (IH : ∀ {b : Y}, pred^[n] b = (f : (a : X) → Y) (pred^[n] (EquivLike.inv f b))) {b : Y},
  pred^[n + 1] b = (f : (a : X) → Y) (pred^[n + 1] (EquivLike.inv f b))
Tactic: induction n generalizing b with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_pred]
Cleared hypotheses: b, n
-- 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
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 hbc₁ : b ≤ c
Tactic: simp only [Subtype.mk_le_mk] at hbc
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 : b ≤ c
⊢ ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have obtain : ∀ (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: obtain ⟨n, hn⟩ := hbc.exists_pred_iterate
-- 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
⊢ ∃ (n : ℕ), pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have h : pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: use n
-- 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 + 1] c = b
⊢ pred^[n + 1] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have h : ∀ (hn : pred^[n] (pred c) = b),
  pred^[n] (pred (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc)) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: simp_all only [Function.iterate_succ, Function.comp_apply]
Cleared hypotheses: 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
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
⊢ pred^[n]
      (if h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α) ∈ s then
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α)) h
      else Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have pos : ∀ (h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α) ∈ s),
  pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α)) h) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: split_ifs with 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
pos :
  ∀ (h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α) ∈ s),
    pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α)) h) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
⊢ pred^[n]
      (if h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α) ∈ s then
        Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α)) h
      else Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have neg : ∀ (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
Tactic: split_ifs with 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
⊢ pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) : α)) h) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have pos : pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
Tactic: dsimp only at 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 c ∈ s
⊢ pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
have apply : b ≤ pred c
Tactic: apply hi _ _ _ 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
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 c ∈ s
⊢ b ≤ pred c
have rw : pred^[n] (pred c) ≤ pred c
Tactic: rw [← hn]