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

State before:
m : ℕ
B A : Finset ℕ
⊢ B ≥ Finset.range m → Late (A \ B) m
Tactic:
intro Bm n nAB
State after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A \ B
⊢ n ≥ m

State before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A \ B
⊢ n ≥ m
Tactic:
rw [Finset.mem_sdiff] at nAB
State after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
⊢ n ≥ m

State before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
⊢ n ≥ m
Tactic:
by_contra h
State after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : ¬n ≥ m
⊢ False

State before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : ¬n ≥ m
⊢ False
Tactic:
simp only [not_le] at h
State after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
⊢ False

State before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
⊢ False
Tactic:
have nr := Finset.mem_range.mpr h
State after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
nr : n ∈ Finset.range m
⊢ False

State before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
nr : n ∈ Finset.range m
⊢ False
Tactic:
have nB := Finset.mem_of_subset Bm nr
State after:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
nr : n ∈ Finset.range m
nB : n ∈ B
⊢ False

State before:
m : ℕ
B A : Finset ℕ
Bm : B ≥ Finset.range m
n : ℕ
nAB : n ∈ A ∧ n ∉ B
h : n < m
nr : n ∈ Finset.range m
nB : n ∈ B
⊢ False
Tactic:
exact nAB.2 nB
State after:
no goals