awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Basic
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
dsimp :
  (if h : pred x ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) ≤
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
⊢ (if h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : α) ∈ s then
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : α)) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) ≤
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx

Tactic:
dsimp
-- Module: Mathlib.Order.SuccPred.Basic
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
isTrue :
  ∀ (h : pred x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
isFalse : pred x ∉ s → Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
⊢ (if h : pred x ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) ≤
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx

Tactic:
split
-- Module: Mathlib.Order.SuccPred.Basic
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
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx

Tactic:
simp_all [Order.pred_le]

Premises used: Order.pred_le
-- Module: Mathlib.Order.SuccPred.Basic
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
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx

Tactic:
simp_all [Order.pred_le]

Premises used: Order.pred_le
-- Module: Mathlib.Order.SuccPred.Basic
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 :
  Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤
    if h : pred x ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
pos :
  ∀ (h' : pred x ∈ s)
    (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h'),
    IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
neg :
  ∀ (h' : pred x ∉ s) (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
    IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
⊢ IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)

Tactic:
split_ifs at h with h'
-- Module: Mathlib.Order.SuccPred.Basic
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 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h'
⊢ IsMin x

Tactic:
simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h

Premises used: Order.le_pred_iff_isMin, Subtype.mk_le_mk
-- Module: Mathlib.Order.SuccPred.Basic
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 : IsMin x
y : α
property : y ∈ s
hy : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y property ≤ 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 property

Tactic:
simp [h hy]
-- Module: Mathlib.Order.SuccPred.Basic
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 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
neg :
  ∀ (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
neg₁ :
  ∀ (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
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy

Tactic:
rcases h.lt_or_eq with h | h

Premises used: LE.le.lt_or_eq
-- Module: Mathlib.Order.SuccPred.Basic
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
⊢ y < x

Tactic:
simp only [Subtype.mk_lt_mk] at h

Premises used: Subtype.mk_lt_mk
-- Module: Mathlib.Order.SuccPred.Basic
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
⊢ y ≤ pred x

Tactic:
have := h.le_pred
-- Module: Mathlib.Order.SuccPred.Basic
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
neg : pred x ∈ s
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy

Tactic:
absurd h'
-- Module: Mathlib.Order.SuccPred.Basic
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
neg : pred x ∈ Icc y x
⊢ pred x ∈ s

Tactic:
apply out' hy hx

Premises used: Set.OrdConnected.out'
-- Module: Mathlib.Order.SuccPred.Basic
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 ∈ Icc y x

Tactic:
simp [this, Order.pred_le]

Premises used: Order.pred_le
-- Module: Mathlib.Order.SuccPred.Basic
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

Tactic:
simp [h]
-- Module: Mathlib.Order.SuccPred.Basic
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
⊢ b < c

Tactic:
rw [Subtype.mk_lt_mk] at h

Premises used: Subtype.mk_lt_mk
-- Module: Mathlib.Order.SuccPred.Basic
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
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
⊢ 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

Tactic:
dsimp only
-- Module: Mathlib.Order.SuccPred.Basic
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
isFalse : pred c ∉ s → 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 c ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc

Tactic:
split
-- Module: Mathlib.Order.SuccPred.Basic
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
h_1 : pred c ∈ s
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h_1

Tactic:
h.le_pred

Premises used: LT.lt.le_pred, Order.pred
-- Module: Mathlib.Order.SuccPred.Basic
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
h_1 : pred c ∈ s
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred c) h_1

Tactic:
exact h.le_pred

Premises used: LT.lt.le_pred
-- Module: Mathlib.Order.SuccPred.Basic
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
h_1 : pred c ∉ s
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc

Tactic:
h.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.SuccPred.Basic
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
h_1 : pred c ∉ s
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc

Tactic:
exact h.le

Premises used: LT.lt.le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∈ s
change :
  (↑(if h : pred (↑a : α) ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑a : α)) h else a) : α) = pred (↑a : α)
⊢ (↑(pred a) : α) = pred (↑a : α)

Tactic:
change Subtype.val (dite ..) = _

Premises used: dite, Subtype.val
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∈ s
⊢ (↑(if h : pred (↑a : α) ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑a : α)) h else a) : α) = pred (↑a : α)

Tactic:
simp [h]
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∈ s
change :
  (↑(if h : pred (↑a : α) ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑a : α)) h else a) : α) = pred (↑a : α)
⊢ (↑(pred a) : α) = pred (↑a : α)

Tactic:
classical
  change Subtype.val (dite ..) = _
  simp [h]

Premises used: dite, Subtype.val
-- Module: Mathlib.Order.SuccPred.Basic
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 : pred a = a
⊢ IsMin a

Tactic:
rw [← pred_eq_iff_isMin]

Premises used: Order.pred_eq_iff_isMin
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
a : (↑s : Type u_3)
h : pred (↑a : α) ∉ s
⊢ (if h : pred (↑a : α) ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑a : α)) h else a) = a

Tactic:
simp [h]
-- Module: Mathlib.Order.SuccPred.Basic
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
rw₃ : (if h : pred (↑a : α) ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑a : α)) h else a) = a
⊢ IsMin a

Tactic:
classical
  rw [← pred_eq_iff_isMin]
  change dite .. = _
  simp [h]

Premises used: dite, Order.pred_eq_iff_isMin
-- Module: Mathlib.Order.SuccPred.Basic
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
⊢ (↑(pred a) : α) = (↑a : α)

Tactic:
replace h := congr($h.pred_eq.1)
-- Module: Mathlib.Order.SuccPred.Basic
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 : α)
⊢ pred (↑a : α) = (↑a : α)

Tactic:
rw [coe_pred_of_mem nh] at h

Premises used: coe_pred_of_mem
-- Module: Mathlib.Order.SuccPred.Basic
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

Tactic:
simp at h
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∈ s
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 : α)
⊢ (↑(succ a) : α) = succ (↑a : α)

Tactic:
change Subtype.val (dite ..) = _

Premises used: dite, Subtype.val
-- Module: Mathlib.Order.SuccPred.Basic
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 : α)
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 : α)
⊢ (↑(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:
split_ifs
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∈ s
h_1 :
  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_1) :
      α) =
    succ (↑a : α)

Tactic:
trivial
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∈ s
h_1 : 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:
trivial
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∈ s
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 : α)
⊢ (↑(succ a) : α) = succ (↑a : α)

Tactic:
classical
  change Subtype.val (dite ..) = _
  split_ifs <;> trivial

Premises used: dite, Subtype.val
-- Module: Mathlib.Order.SuccPred.Basic
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 : succ a = a
⊢ IsMax a

Tactic:
rw [← succ_eq_iff_isMax]

Premises used: Order.succ_eq_iff_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
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
⊢ succ a = a

Tactic:
change dite .. = _

Premises used: dite
-- Module: Mathlib.Order.SuccPred.Basic
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
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
⊢ (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:
split_ifs
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
h_1 :
  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_1 =
    a

Tactic:
trivial
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : SuccOrder α
a : (↑s : Type u_3)
h : succ (↑a : α) ∉ s
h_1 : 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:
trivial
-- Module: Mathlib.Order.SuccPred.Basic
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
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
⊢ IsMax a

Tactic:
classical
  rw [← succ_eq_iff_isMax]
  change dite .. = _
  split_ifs <;> trivial

Premises used: Order.succ_eq_iff_isMax, dite
-- Module: Mathlib.Order.SuccPred.Basic
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
⊢ (↑(succ a) : α) = (↑a : α)

Tactic:
replace h := congr($h.succ_eq.1)
-- Module: Mathlib.Order.SuccPred.Basic
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 : α)
⊢ succ (↑a : α) = (↑a : α)

Tactic:
rw [coe_succ_of_mem nh] at h

Premises used: coe_succ_of_mem
-- Module: Mathlib.Order.SuccPred.Basic
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

Tactic:
simp at h
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
obtain : ∀ (y : α) (hy : y ⋖ sSup s), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim

Premises used: not_forall_not, Iff.mp
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
obtain : ∀ (i : α) (his : i ∈ s) (hi : y < i), sSup s ∈ s
⊢ sSup s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt

Premises used: exists_lt_of_lt_csSup, CovBy.lt
-- Module: Mathlib.Order.SuccPred.CompleteLinearOrder
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Tactic:
eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his

Premises used: Set.Mem, Eq.rec, And.right, le_csSup, eq_of_le_of_not_lt