Theorem: late_iff_disjoint_range (Ray/Misc/Bounds.lean)

State before:
m : ℕ
A : Finset ℕ
⊢ Late A m ↔ Disjoint A (Finset.range m)
Tactic:
simp only [Late, ge_iff_le, Finset.disjoint_iff_ne, Finset.mem_range, ne_eq]
State after:
m : ℕ
A : Finset ℕ
⊢ (∀ n ∈ A, m ≤ n) ↔ ∀ a ∈ A, ∀ b < m, ¬a = b

State before:
m : ℕ
A : Finset ℕ
⊢ (∀ n ∈ A, m ≤ n) ↔ ∀ a ∈ A, ∀ b < m, ¬a = b
Tactic:
constructor
State after:
case mp
m : ℕ
A : Finset ℕ
⊢ (∀ n ∈ A, m ≤ n) → ∀ a ∈ A, ∀ b < m, ¬a = b

case mpr
m : ℕ
A : Finset ℕ
⊢ (∀ a ∈ A, ∀ b < m, ¬a = b) → ∀ n ∈ A, m ≤ n

State before:
case mp
m : ℕ
A : Finset ℕ
⊢ (∀ n ∈ A, m ≤ n) → ∀ a ∈ A, ∀ b < m, ¬a = b
Tactic:
intro h n na b bm
State after:
case mp
m : ℕ
A : Finset ℕ
h : ∀ n ∈ A, m ≤ n
n : ℕ
na : n ∈ A
b : ℕ
bm : b < m
⊢ ¬n = b

State before:
case mp
m : ℕ
A : Finset ℕ
h : ∀ n ∈ A, m ≤ n
n : ℕ
na : n ∈ A
b : ℕ
bm : b < m
⊢ ¬n = b
Tactic:
linarith [h _ na]
State after:
no goals

State before:
case mpr
m : ℕ
A : Finset ℕ
⊢ (∀ a ∈ A, ∀ b < m, ¬a = b) → ∀ n ∈ A, m ≤ n
Tactic:
intro h n na
State after:
case mpr
m : ℕ
A : Finset ℕ
h : ∀ a ∈ A, ∀ b < m, ¬a = b
n : ℕ
na : n ∈ A
⊢ m ≤ n

State before:
case mpr
m : ℕ
A : Finset ℕ
h : ∀ a ∈ A, ∀ b < m, ¬a = b
n : ℕ
na : n ∈ A
⊢ m ≤ n
Tactic:
specialize h n na n
State after:
case mpr
m : ℕ
A : Finset ℕ
n : ℕ
na : n ∈ A
h : n < m → ¬n = n
⊢ m ≤ n

State before:
case mpr
m : ℕ
A : Finset ℕ
n : ℕ
na : n ∈ A
h : n < m → ¬n = n
⊢ m ≤ n
Tactic:
simpa [not_true, imp_false, not_lt] using h
State after:
no goals