Theorem: push_le_push (Ray/Misc/Finset.lean)

State before:
A B : Finset ℕ
⊢ push A ≤ push B ↔ A ≤ B
Tactic:
simp
State after:
A B : Finset ℕ
⊢ push A ⊆ push B ↔ A ⊆ B

State before:
A B : Finset ℕ
⊢ push A ⊆ push B ↔ A ⊆ B
Tactic:
rw [push]
State after:
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ push B ↔ A ⊆ B

State before:
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ push B ↔ A ⊆ B
Tactic:
rw [push]
State after:
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B) ↔ A ⊆ B

State before:
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B) ↔ A ⊆ B
Tactic:
constructor
State after:
case mp
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B) → A ⊆ B

case mpr
A B : Finset ℕ
⊢ A ⊆ B → insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)

State before:
case mp
A B : Finset ℕ
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B) → A ⊆ B
Tactic:
intro AB
State after:
case mp
A B : Finset ℕ
AB : insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
⊢ A ⊆ B

State before:
case mp
A B : Finset ℕ
AB : insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
⊢ A ⊆ B
Tactic:
rw [Finset.subset_iff] at AB ⊢
State after:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
⊢ ∀ ⦃x : ℕ⦄, x ∈ A → x ∈ B

State before:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
⊢ ∀ ⦃x : ℕ⦄, x ∈ A → x ∈ B
Tactic:
intro x xA
State after:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
⊢ x ∈ B

State before:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
⊢ x ∈ B
Tactic:
have h : x + 1 ∈ insert 0 (Finset.image (fun n : ℕ ↦ n + 1) A) := by simpa
State after:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
⊢ x ∈ B

State before:
case mp
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
⊢ x ∈ B
Tactic:
specialize AB h
State after:
case mp
A B : Finset ℕ
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
AB : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) B)
⊢ x ∈ B

State before:
case mp
A B : Finset ℕ
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
AB : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) B)
⊢ x ∈ B
Tactic:
simp at AB
State after:
case mp
A B : Finset ℕ
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
AB : x ∈ B
⊢ x ∈ B

State before:
case mp
A B : Finset ℕ
x : ℕ
xA : x ∈ A
h : x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
AB : x ∈ B
⊢ x ∈ B
Tactic:
assumption
State after:
no goals

State before:
A B : Finset ℕ
AB : ∀ ⦃x : ℕ⦄, x ∈ insert 0 (Finset.image (fun n => n + 1) A) → x ∈ insert 0 (Finset.image (fun n => n + 1) B)
x : ℕ
xA : x ∈ A
⊢ x + 1 ∈ insert 0 (Finset.image (fun n => n + 1) A)
Tactic:
simpa
State after:
no goals

State before:
case mpr
A B : Finset ℕ
⊢ A ⊆ B → insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
Tactic:
intro AB
State after:
case mpr
A B : Finset ℕ
AB : A ⊆ B
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)

State before:
case mpr
A B : Finset ℕ
AB : A ⊆ B
⊢ insert 0 (Finset.image (fun n => n + 1) A) ⊆ insert 0 (Finset.image (fun n => n + 1) B)
Tactic:
apply Finset.insert_subset_insert
State after:
case mpr.h
A B : Finset ℕ
AB : A ⊆ B
⊢ Finset.image (fun n => n + 1) A ⊆ Finset.image (fun n => n + 1) B

State before:
case mpr.h
A B : Finset ℕ
AB : A ⊆ B
⊢ Finset.image (fun n => n + 1) A ⊆ Finset.image (fun n => n + 1) B
Tactic:
apply Finset.image_mono
State after:
case mpr.h.a
A B : Finset ℕ
AB : A ⊆ B
⊢ A ≤ B

State before:
case mpr.h.a
A B : Finset ℕ
AB : A ⊆ B
⊢ A ≤ B
Tactic:
assumption
State after:
no goals