-- Mathlib/Order/RelSeries.lean
lemma Rel.not_finiteDimensional_iff [Nonempty α] :
    ¬ r.FiniteDimensional ↔ r.InfiniteDimensional

Proof state:
case mp
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) → ∀ (n : ℕ), ∃ x, x.length = n

Tactic:
intro H n

Result:
case mp
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
⊢ ∃ x, x.length = n

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ ¬r.FiniteDimensional ↔ r.InfiniteDimensional

Tactic:
rw [finiteDimensional_iff, infiniteDimensional_iff]

Result:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ (¬∃ x, ∀ (y : RelSeries r), y.length ≤ x.length) ↔ ∀ (n : ℕ), ∃ x, x.length = n

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ { length := 0, toFun := ![inst✝.some], step := ⋯ }.length = 0

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l l' : RelSeries r
hl' : l'.length = l.length + 1
⊢ ∃ y, l.length < y.length

Tactic:
exact ⟨l', by simp [hl']⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l : RelSeries r
⊢ ∃ y, l.length < y.length

Tactic:
obtain ⟨l', hl'⟩ := H (l.length + 1)

Result:
case mpr.intro
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l l' : RelSeries r
hl' : l'.length = l.length + 1
⊢ ∃ y, l.length < y.length

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ (¬∃ x, ∀ (y : RelSeries r), y.length ≤ x.length) ↔ ∀ (n : ℕ), ∃ x, x.length = n

Tactic:
push_neg

Result:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) ↔ ∀ (n : ℕ), ∃ x, x.length = n

Proof state:
case mp.zero
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ ∃ x, x.length = 0

Tactic:
refine ⟨⟨0, ![Nonempty.some ‹_›], by simp⟩, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
⊢ ∀ (i : Fin 0), r (![inst✝.some] i.castSucc) (![inst✝.some] i.succ)

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length

Tactic:
intro H l

Result:
case mpr
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l : RelSeries r
⊢ ∃ y, l.length < y.length

Proof state:
case mp.succ.intro.intro
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
l : RelSeries r
hl : l.length = n
l' : RelSeries r
hl' : l.length < l'.length
⊢ ∃ x, x.length = n + 1

Tactic:
exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩

Result:
no goals

Proof state:
case mp.succ.intro
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
l : RelSeries r
hl : l.length = n
⊢ ∃ x, x.length = n + 1

Tactic:
obtain ⟨l', hl'⟩ := H l

Result:
case mp.succ.intro.intro
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
l : RelSeries r
hl : l.length = n
l' : RelSeries r
hl' : l.length < l'.length
⊢ ∃ x, x.length = n + 1

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
l : RelSeries r
hl : l.length = n
l' : RelSeries r
hl' : l.length < l'.length
⊢ n + 1 < l'.length + 1

Tactic:
simpa [hl] using hl'

Result:
no goals

Proof state:
case mp.succ
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
IH : ∃ x, x.length = n
⊢ ∃ x, x.length = n + 1

Tactic:
obtain ⟨l, hl⟩ := IH

Result:
case mp.succ.intro
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
l : RelSeries r
hl : l.length = n
⊢ ∃ x, x.length = n + 1

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l l' : RelSeries r
hl' : l'.length = l.length + 1
⊢ l.length < l'.length

Tactic:
simp [hl']

Result:
no goals

Proof state:
case mp
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
H : ∀ (x : RelSeries r), ∃ y, x.length < y.length
n : ℕ
⊢ ∃ x, x.length = n

Tactic:
induction n with
| zero => refine ⟨⟨0, ![Nonempty.some ‹_›], by simp⟩, by simp⟩
| succ n IH =>
  obtain ⟨l, hl⟩ := IH
  obtain ⟨l', hl'⟩ := H l
  exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) ↔ ∀ (n : ℕ), ∃ x, x.length = n

Tactic:
constructor

Result:
case mp
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) → ∀ (n : ℕ), ∃ x, x.length = n

case mpr
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length