awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h' : pred x ∉ s
h_1 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
y : α
hy : y ∈ s
h_2 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy < Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
have h₁ : y < x
Tactic: simp only [Subtype.mk_lt_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h' : pred x ∉ s
h_1 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
y : α
hy : y ∈ s
h_2 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
h : y < x
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
have this : y ≤ pred x
Tactic: have := h.le_pred
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h' : pred x ∉ s
h_1 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
y : α
hy : y ∈ s
h_2 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
h : y < x
this : y ≤ pred x
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
have neg : pred x ∈ s
Tactic: absurd h'
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h' : pred x ∉ s
h_1 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
y : α
hy : y ∈ s
h_2 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
h : y < x
this : y ≤ pred x
⊢ pred x ∈ s
have neg : pred x ∈ Icc y x
Tactic: apply out' hy hx
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x x_1 : (↑s : Type u_3)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : 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) b hb ≤
    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
have h₁ : b < c
Tactic: rw [Subtype.mk_lt_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x x_1 : (↑s : Type u_3)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤
    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
have dsimp : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤
  if h : pred c ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h
  else Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x x_1 : (↑s : Type u_3)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤
    if h : pred c ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
have isTrue : ∀ (h : pred c ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h
Tactic: split
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x x_1 : (↑s : Type u_3)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
isTrue :
  ∀ (h : pred c ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤
    if h : pred c ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
have isFalse : pred c ∉ s → Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc
Tactic: split
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∈ s
⊢ (↑(pred a) : α) = pred (↑a : α)
have change : (↑(if h : pred (↑a : α) ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑a : α)) h else a) : α) = pred (↑a : α)
Tactic: change Subtype.val (dite ..) = _
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∈ s
⊢ (↑(pred a) : α) = pred (↑a : α)
have change : (↑(if h : pred (↑a : α) ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑a : α)) h else a) : α) = pred (↑a : α)
Tactic: classical
  change Subtype.val (dite ..) = _
  simp [h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∉ s
⊢ IsMin a
have rw : pred a = a
Tactic: rw [← pred_eq_iff_isMin]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∉ s
⊢ IsMin a
have rw : pred a = a
Tactic: classical
  rw [← pred_eq_iff_isMin]
  change dite .. = _
  simp [h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∉ s
rw rw₁ rw₂ : pred a = a
⊢ IsMin a
have rw₃ : (if h : pred (↑a : α) ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑a : α)) h else a) = a
Tactic: classical
  rw [← pred_eq_iff_isMin]
  change dite .. = _
  simp [h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a : (↑s : Type u_3)
h : IsMin a
nh : pred (↑a : α) ∈ s
⊢ False
have h₁ : (↑(pred a) : α) = (↑a : α)
Tactic: replace h := congr($h.pred_eq.1)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
inst_3 : NoMinOrder α
a : (↑s : Type u_3)
nh : pred (↑a : α) ∈ s
h : (↑(pred a) : α) = (↑a : α)
⊢ False
have h₁ : pred (↑a : α) = (↑a : α)
Tactic: rw [coe_pred_of_mem nh] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∈ s
⊢ (↑(succ a) : α) = succ (↑a : α)
have change : (↑(if h :
          Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
            (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) then
        Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
          (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h
      else (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) :
    α) =
  succ (↑a : α)
Tactic: change Subtype.val (dite ..) = _
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∈ s
⊢ (↑(if h :
            Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
              (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) then
          Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
            (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h
        else (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) :
      α) =
    succ (↑a : α)
have pos : ∀
  (h :
    Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
      (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ))),
  (↑(Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
          (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h) :
      α) =
    succ (↑a : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∈ s
pos :
  ∀
    (h :
      Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
        (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ))),
    (↑(Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
            (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h) :
        α) =
      succ (↑a : α)
⊢ (↑(if h :
            Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
              (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) then
          Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
            (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h
        else (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) :
      α) =
    succ (↑a : α)
have neg : pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ) ∉ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s →
  (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : α) = succ (↑a : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∈ s
⊢ (↑(succ a) : α) = succ (↑a : α)
have change : (↑(if h :
          Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
            (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) then
        Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
          (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h
      else (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) :
    α) =
  succ (↑a : α)
Tactic: classical
  change Subtype.val (dite ..) = _
  split_ifs <;> trivial
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
⊢ IsMax a
have rw : succ a = a
Tactic: rw [← succ_eq_iff_isMax]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
⊢ succ a = a
have change : (if h :
      Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
        (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) then
    Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
      (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h
  else (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) =
  a
Tactic: change dite .. = _
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
⊢ (if h :
        Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
          (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) then
      Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
        (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h
    else (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) =
    a
have pos : ∀
  (h :
    Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
      (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ))),
  Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
      (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h =
    a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
pos :
  ∀
    (h :
      Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
        (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ))),
    Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
        (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h =
      a
⊢ (if h :
        Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
          (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) then
      Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
        (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h
    else (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) =
    a
have neg : pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ) ∉ (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s →
  (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
⊢ IsMax a
have rw : succ a = a
Tactic: classical
  rw [← succ_eq_iff_isMax]
  change dite .. = _
  split_ifs <;> trivial
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
rw rw₁ rw₂ : succ a = a
⊢ IsMax a
have rw₃ : (if h :
      Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s)
        (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) then
    Subtype.mk (p := fun (x : αᵒᵈ) ↦ Membership.mem (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) x)
      (pred (↑((ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) : αᵒᵈ)) h
  else (ofDual : (a : (↑s : Type u_3)ᵒᵈᵒᵈ) → (↑s : Type u_3)ᵒᵈ) a) =
  a
Tactic: classical
  rw [← succ_eq_iff_isMax]
  change dite .. = _
  split_ifs <;> trivial
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
a : (↑s : Type u_3)
h : IsMax a
nh : succ (↑a : α) ∈ s
⊢ False
have h₁ : (↑(succ a) : α) = (↑a : α)
Tactic: replace h := congr($h.succ_eq.1)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
a : (↑s : Type u_3)
nh : succ (↑a : α) ∈ s
h : (↑(succ a) : α) = (↑a : α)
⊢ False
have h₁ : succ (↑a : α) = (↑a : α)
Tactic: rw [coe_succ_of_mem nh] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
have obtain : ∀ (y : α) (hy : y ⋖ sSup s), sSup s ∈ s
Tactic: obtain ⟨y, hy⟩ := not_forall_not.mp hlim
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
⊢ sSup s ∈ s
have obtain : ∀ (i : α) (his : i ∈ s) (hi : y < i), sSup s ∈ s
Tactic: obtain ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
⊢ sInf s ∈ s
have obtain : ∀ (y : α) (hy : sInf s ⋖ y), sInf s ∈ s
Tactic: obtain ⟨y, hy⟩ := not_forall_not.mp hlim
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
⊢ sInf s ∈ s
have obtain : ∀ (i : α) (his : i ∈ s) (hi : i < y), sInf s ∈ s
Tactic: obtain ⟨i, his, hi⟩ := exists_lt_of_csInf_lt hne hy.lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
have inl : ∀ (hlim : ¬IsSuccPrelimit.{u_2} (α := α) (sSup ∅)), Membership.mem (γ := Set α) ∅ (sSup ∅)
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s, hlim
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
inl : ∀ (hlim : ¬IsSuccPrelimit.{u_2} (α := α) (sSup ∅)), Membership.mem (γ := Set α) ∅ (sSup ∅)
⊢ sSup s ∈ s
have inr : ∀ (hs : s.Nonempty), sSup s ∈ s
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ sSup s ∈ s
have apply : BddAbove s
Tactic: apply csSup_mem_of_not_isSuccPrelimit hs _ hlim
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ BddAbove s
have contrapose! : ∀ (hlim : ¬BddAbove s), IsSuccPrelimit (sSup s)
Tactic: contrapose! hlim
Cleared hypotheses: hlim
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit (sSup s)
have rw : IsSuccPrelimit.{u_2} (α := α) ⊥
Tactic: rw [csSup_of_not_bddAbove hlim, csSup_empty]
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (hypothesis)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hne : s.Nonempty
hbbd : BddAbove s
hlim : ¬IsSuccLimit (sSup s)
⊢ sSup s ∈ s
have hlim₁ : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
Tactic: rw [isSuccLimit_iff_of_orderBot, not_and_or, not_ne_iff] at hlim
Cleared hypotheses: hlim
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (hypothesis)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hne : s.Nonempty
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
have h : sSup s = ⊥
Tactic: refine hlim.elim (fun h ↦ ?_) csSup_mem_of_not_isSuccPrelimit'
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hne : s.Nonempty
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
h : sSup s = ⊥
⊢ sSup s ∈ s
have obtain : ∀ (a : α) (ha : a ∈ s), sSup s ∈ s
Tactic: obtain ⟨a, ha⟩ := hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
h : sSup s = ⊥
a : α
ha : a ∈ s
⊢ sSup s ∈ s
have inl : ∀ (ha : ⊥ ∈ s), sSup s ∈ s
Tactic: obtain rfl | ha' := eq_or_ne ⊥ a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hbbd : BddAbove s
hlim : sSup s = ⊥ ∨ ¬IsSuccPrelimit (sSup s)
h : sSup s = ⊥
a : α
ha : a ∈ s
inl : ∀ (ha : ⊥ ∈ s), sSup s ∈ s
⊢ sSup s ∈ s
have inr : ∀ (ha' : ⊥ ≠ a), sSup s ∈ s
Tactic: obtain rfl | ha' := eq_or_ne ⊥ a
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ sSup (Iio x) = x
have inl : ∀ (h : IsSuccPrelimit.{u_2} (α := α) ⊥), Eq.{u_2 + 1} (α := α) (sSup (Iio ⊥)) ⊥
Tactic: obtain rfl | hx := eq_bot_or_bot_lt x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
inl : ∀ (h : IsSuccPrelimit.{u_2} (α := α) ⊥), Eq.{u_2 + 1} (α := α) (sSup (Iio ⊥)) ⊥
⊢ sSup (Iio x) = x
have inr : ∀ (hx : ⊥ < x), sSup (Iio x) = x
Tactic: obtain rfl | hx := eq_bot_or_bot_lt x
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), (↑a : α) = x
have rw : sSup (Iio x) = x
Tactic: rw [← sSup_eq_iSup', h.sSup_Iio]
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
rw : sSup (Iio x) = x
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), (↑a : α) = x
have rw₁ : x = x
Tactic: rw [← sSup_eq_iSup', h.sSup_Iio]
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x
have refine : ∀ (h : sSup (Iio x) = x), IsSuccPrelimit x
Tactic: refine ⟨fun h ↦ ?_, IsSuccPrelimit.sSup_Iio⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
⊢ IsSuccPrelimit x
have by_contra : ∀ (hx : ¬IsSuccPrelimit x), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (hypothesis)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit x
⊢ False
have hx₁ : ¬IsSuccPrelimit (sSup (Iio x))
Tactic: rw [← h] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), (↑a : α) = x ↔ IsSuccPrelimit x
have rw : sSup (Iio x) = x ↔ IsSuccPrelimit x
Tactic: rw [← sSup_eq_iSup', sSup_Iio_eq_self_iff_isSuccPrelimit]
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
x : α
rw : sSup (Iio x) = x ↔ IsSuccPrelimit x
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), (↑a : α) = x ↔ IsSuccPrelimit x
have rw₁ : IsSuccPrelimit x ↔ IsSuccPrelimit x
Tactic: rw [← sSup_eq_iSup', sSup_Iio_eq_self_iff_isSuccPrelimit]