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

State before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
⊢ Late (A ∆ B) m
Tactic:
intro n ab
State after:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A ∆ B
⊢ n ≥ m

State before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A ∆ B
⊢ n ≥ m
Tactic:
rw [symmDiff_def, Finset.sup_eq_union, Finset.mem_union] at ab
State after:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
⊢ n ≥ m

State before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
⊢ n ≥ m
Tactic:
by_contra h
State after:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
h : ¬n ≥ m
⊢ False

State before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
h : ¬n ≥ m
⊢ False
Tactic:
simp at h
State after:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
h : n < m
⊢ False

State before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
h : n < m
⊢ False
Tactic:
cases' ab with a b
State after:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
a : n ∈ A \ B
⊢ False

case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
b : n ∈ B \ A
⊢ False

State before:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
a : n ∈ A \ B
⊢ False
Tactic:
rw [Finset.mem_sdiff] at a
State after:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
a : n ∈ A ∧ n ∉ B
⊢ False

State before:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
a : n ∈ A ∧ n ∉ B
⊢ False
Tactic:
have h := Finset.mem_of_subset hb (Finset.mem_range.mpr h)
State after:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h✝ : n < m
a : n ∈ A ∧ n ∉ B
h : n ∈ B
⊢ False

State before:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h✝ : n < m
a : n ∈ A ∧ n ∉ B
h : n ∈ B
⊢ False
Tactic:
exact a.2 h
State after:
no goals

State before:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
b : n ∈ B \ A
⊢ False
Tactic:
rw [Finset.mem_sdiff] at b
State after:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
b : n ∈ B ∧ n ∉ A
⊢ False

State before:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
b : n ∈ B ∧ n ∉ A
⊢ False
Tactic:
have h := Finset.mem_of_subset ha (Finset.mem_range.mpr h)
State after:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h✝ : n < m
b : n ∈ B ∧ n ∉ A
h : n ∈ A
⊢ False

State before:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h✝ : n < m
b : n ∈ B ∧ n ∉ A
h : n ∈ A
⊢ False
Tactic:
exact b.2 h
State after:
no goals