awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Archimedean
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
refine : ∀ (a_1 : ℕ), pred^[a_1] (EquivLike.inv f b) = EquivLike.inv f a → pred^[a_1] b = a
⊢ ∃ (n : ℕ), pred^[n] b = a

Tactic:
refine (exists_pred_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_

Premises used: Iff.mpr, IsPredArchimedean.exists_pred_iterate_of_le, Exists.imp, map_inv_le_map_inv_iff
-- Module: Mathlib.Order.SuccPred.Archimedean
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 : ℕ
rw : (f : (a : X) → Y) (pred^[n] (EquivLike.inv f b)) = a → pred^[n] b = a
⊢ pred^[n] (EquivLike.inv f b) = EquivLike.inv f a → pred^[n] b = a

Tactic:
rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]

Premises used: OrderIso.apply_eq_iff_eq, EquivLike.apply_inv_apply
-- Module: Mathlib.Order.SuccPred.Archimedean
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
⊢ pred^[0] b = (f : (a : X) → Y) (pred^[0] (EquivLike.inv f b))

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Archimedean
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
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:
simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_pred]

Premises used: OrderIso.map_pred, Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Order.SuccPred.Archimedean
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))
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))
⊢ pred^[n] b = (f : (a : X) → Y) (pred^[n] (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]

Premises used: Order.succ, OrderIso.map_pred, Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Order.SuccPred.Archimedean
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
⊢ b ≤ c

Tactic:
simp only [Subtype.mk_le_mk] at hbc

Premises used: Subtype.mk_le_mk
-- Module: Mathlib.Order.SuccPred.Archimedean
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
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
⊢ ∃ (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

Premises used: LE.le.exists_pred_iterate
-- Module: Mathlib.Order.SuccPred.Archimedean
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 : 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

Tactic:
use n
-- Module: Mathlib.Order.SuccPred.Archimedean
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
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:
simp_all
-- Module: Mathlib.Order.SuccPred.Archimedean
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
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
⊢ pred^[n + 1] (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]

Premises used: Function.iterate_succ, Function.comp_apply
-- Module: Mathlib.Order.SuccPred.Archimedean
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
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
⊢ 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

Tactic:
split_ifs with h
-- Module: Mathlib.Order.SuccPred.Archimedean
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
pos : pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
⊢ 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:
dsimp only at h ⊢
-- Module: Mathlib.Order.SuccPred.Archimedean
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
apply : b ≤ pred c
⊢ pred^[n] (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb

Tactic:
apply hi _ _ _ hn
-- Module: Mathlib.Order.SuccPred.Archimedean
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
rw : pred^[n] (pred c) ≤ pred c
⊢ b ≤ pred c

Tactic:
rw [← hn]
-- Module: Mathlib.Order.SuccPred.Archimedean
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] (pred c) ≤ pred c

Tactic:
apply Order.pred_iterate_le

Premises used: Order.pred_iterate_le
-- Module: Mathlib.Order.SuccPred.Archimedean
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
⊢ (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) c hc

Tactic:
simp [h]
-- Module: Mathlib.Order.SuccPred.Archimedean
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 (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]
-- Module: Mathlib.Order.SuccPred.Archimedean
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
neg : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc = Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb
neg₁ : 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

Tactic:
rw [Function.iterate_fixed]

Premises used: Function.iterate_fixed
-- Module: Mathlib.Order.SuccPred.Archimedean
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
⊢ IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc)

Tactic:
simp only [Order.pred_eq_iff_isMin] at this

Premises used: Order.pred_eq_iff_isMin
-- Module: Mathlib.Order.SuccPred.Archimedean
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)
apply : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ 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

Tactic:
apply (this.eq_of_le _).symm

Premises used: Eq.symm, IsMin.eq_of_le
-- Module: Mathlib.Order.SuccPred.Archimedean
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) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc

Tactic:
hbc
-- Module: Mathlib.Order.SuccPred.Archimedean
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) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc

Tactic:
exact hbc
-- Module: Mathlib.Order.SuccPred.Archimedean
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 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc

Tactic:
this
-- Module: Mathlib.Order.SuccPred.Archimedean
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 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc) = Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc

Tactic:
exact this
-- Module: Mathlib.Order.SuccPred.Archimedean
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
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
⊢ pred^[n] (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

Premises used: Order.succ, Function.iterate_succ, Nat.iterate, dite, Order.pred_iterate_le, Order.pred_eq_iff_isMin, Order.pred, Function.comp_apply, Function.iterate_fixed
-- Module: Mathlib.Order.SuccPred.Archimedean
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
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
⊢ ∃ (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

Premises used: Order.succ, Function.iterate_succ, LE.le.exists_pred_iterate, Order.pred_iterate_le, Order.pred_eq_iff_isMin, Function.comp_apply, Function.iterate_fixed, Subtype.mk_le_mk
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
s : Set α
inst_3 : s.OrdConnected
⊢ IsSuccArchimedean.{u_1} (↑s : Type u_1)

Tactic:
letI : IsPredArchimedean sᵒᵈ := inferInstanceAs (IsPredArchimedean (OrderDual.ofDual ⁻¹' s))
  inferInstanceAs (IsSuccArchimedean sᵒᵈᵒᵈ)

Premises used: _private.0.Set.OrdConnected.isSuccArchimedean._proof_2
-- Module: Mathlib.Order.SuccPred.Archimedean
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
obtain : ∀ (n : ℕ) (hb : succ^[n] a ∈ s) (hab : a ≤ succ^[n] a), f a ≤ f (succ^[n] a)
⊢ f a ≤ f b

Tactic:
obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab

Premises used: IsSuccArchimedean.exists_succ_iterate_of_le, rfl
-- Module: Mathlib.Order.SuccPred.Archimedean
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
hb : succ^[0] a ∈ s
⊢ f a ≤ f (succ^[0] a)

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Archimedean
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 : ℕ
hn : ∀ (hb : Order.succ^[n] a ∈ s), f a ≤ f (Order.succ^[n] a)
hb : Order.succ^[n + 1] a ∈ s
succ : ∀ (hb : Order.succ (Order.succ^[n] a) ∈ s), f a ≤ f (Order.succ (Order.succ^[n] a))
⊢ f a ≤ f (Order.succ^[n + 1] a)

Tactic:
rw [Function.iterate_succ_apply'] at hb ⊢

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.SuccPred.Archimedean
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
⊢ succ^[n] a ∈ s

Tactic:
have : succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
-- Module: Mathlib.Order.SuccPred.Archimedean
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))
neg : ∀ (hb' : ¬IsMax (succ^[n] a)), f a ≤ f (succ (succ^[n] a))
⊢ f a ≤ f (succ (succ^[n] a))

Tactic:
by_cases hb' : IsMax (succ^[n] a)

Premises used: Order.succ, Nat.iterate, IsMax
-- Module: Mathlib.Order.SuccPred.Archimedean
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)
pos : f a ≤ f (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))

Tactic:
rw [succ_eq_iff_isMax.2 hb']

Premises used: Iff.mpr, Order.succ_eq_iff_isMax
-- Module: Mathlib.Order.SuccPred.Archimedean
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^[n] a)

Tactic:
hn this
-- Module: Mathlib.Order.SuccPred.Archimedean
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^[n] a)

Tactic:
exact hn this