-- Mathlib/Data/Nat/Nth.lean
lemma nth_mem_anti {a b : ℕ} (hab : a ≤ b) (h : p (nth p b)) : p (nth p a)

Proof state:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
⊢ p (nth p a)

Tactic:
have hb0 : nth p b = 0 := by simp [nth_eq_zero, h'b]

Result:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p (nth p a)

Proof state:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
⊢ p (nth p a)

Tactic:
have ha0 : nth p a = 0 := by simp [nth_eq_zero, h']

Result:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
⊢ p (nth p a)

Proof state:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
⊢ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b

Tactic:
rcases h' with ⟨hf, ha⟩

Result:
case intro
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
hf : (setOf p).Finite
ha : #⋯.toFinset ≤ a
⊢ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b

Proof state:
case intro
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
hf : (setOf p).Finite
ha : #⋯.toFinset ≤ a
⊢ ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b

Tactic:
exact ⟨hf, ha.trans hab⟩

Result:
no goals

Proof state:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
⊢ nth p b = 0

Tactic:
simp [nth_eq_zero, h'b]

Result:
no goals

Proof state:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ¬∀ (hf : (setOf p).Finite), a < #hf.toFinset
⊢ p (nth p a)

Tactic:
simp only [not_forall, not_lt] at h'

Result:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
⊢ p (nth p a)

Proof state:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
⊢ p (nth p a)

Tactic:
have h'b : ∃ hf : (setOf p).Finite, #hf.toFinset ≤ b := by
  rcases h' with ⟨hf, ha⟩
  exact ⟨hf, ha.trans hab⟩

Result:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
⊢ p (nth p a)

Proof state:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p (nth p a)

Tactic:
rw [ha0]

Result:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p 0

Proof state:
case pos
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∀ (hf : (setOf p).Finite), a < #hf.toFinset
⊢ p (nth p a)

Tactic:
exact nth_mem a h'

Result:
no goals

Proof state:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
⊢ p (nth p a)

Tactic:
by_cases h' : ∀ hf : (setOf p).Finite, a < #hf.toFinset

Result:
case pos
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∀ (hf : (setOf p).Finite), a < #hf.toFinset
⊢ p (nth p a)

case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ¬∀ (hf : (setOf p).Finite), a < #hf.toFinset
⊢ p (nth p a)

Proof state:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p 0

Tactic:
rwa [hb0] at h

Result:
no goals

Proof state:
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (setOf p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (setOf p).Finite), #hf.toFinset ≤ b
⊢ nth p a = 0

Tactic:
simp [nth_eq_zero, h']

Result:
no goals