-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem isMax_of_succFn_le [LocallyFiniteOrder ι] (i : ι) (hi : succFn i ≤ i) : IsMax i

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i ∈ Finset.Ioc i j
⊢ False

Tactic:
rw [Finset.mem_Ioc] at hi_mem

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i < i ∧ i ≤ j
⊢ False

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ (Finset.Ioc i j).Nonempty

Tactic:
exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i

Tactic:
exact isGLB_Ioc_of_isGLB_Ioi hij_lt h

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (Set.Ioc i j) i

Tactic:
have h := succFn_spec i

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) (succFn i)
⊢ IsGLB (Set.Ioc i j) i

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) (succFn i)
⊢ IsGLB (Set.Ioc i j) i

Tactic:
rw [h_succFn_eq] at h

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ False

Tactic:
have h_glb : IsGLB (Finset.Ioc i j : Set ι) i := by
  rw [Finset.coe_Ioc]
  have h := succFn_spec i
  rw [h_succFn_eq] at h
  exact isGLB_Ioc_of_isGLB_Ioi hij_lt h

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ False

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i < i ∧ i ≤ j
⊢ False

Tactic:
exact lt_irrefl i hi_mem.1

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ False

Tactic:
have hi_mem : i ∈ Finset.Ioc i j := by
  refine Finset.isGLB_mem _ h_glb ?_
  exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i ∈ Finset.Ioc i j
⊢ False

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ i ∈ Finset.Ioc i j

Tactic:
refine Finset.isGLB_mem _ h_glb ?_

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ (Finset.Ioc i j).Nonempty

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
⊢ IsMax i

Tactic:
refine fun j _ ↦ not_lt.mp fun hij_lt ↦ ?_

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
⊢ False

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (↑(Finset.Ioc i j)) i

Tactic:
rw [Finset.coe_Ioc]

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (Set.Ioc i j) i

Proof state:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
⊢ False

Tactic:
have h_succFn_eq : succFn i = i := le_antisymm hi (le_succFn i)

Result:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ False