Theorem: biUnion_subset (Pdl/Closure.lean)

State before:
α : Type u_1
f : α → List α
⊢ ∀ (i : ℕ) (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
Tactic:
intro i
State after:
α : Type u_1
f : α → List α
i : ℕ
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y

State before:
α : Type u_1
f : α → List α
i : ℕ
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
Tactic:
induction i
State after:
case zero
α : Type u_1
f : α → List α
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y

case succ
α : Type u_1
f : α → List α
n✝ : ℕ
a✝ : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[n✝] X ⊆ (fun X => (List.map f X).join)^[n✝] Y
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[n✝ + 1] X ⊆ (fun X => (List.map f X).join)^[n✝ + 1] Y

State before:
α : Type u_1
f : α → List α
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Tactic:
case zero =>
  intro X Y
  intro X_sub_Y
  simp at *
  assumption
State after:
no goals

State before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y
Tactic:
case succ i IH =>
  intro X Y
  simp
  intro X_sub_Y
  apply IH
  have := List.map_subset f X_sub_Y
  intro a a_in
  aesop
State after:
no goals

State before:
α : Type u_1
f : α → List α
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Tactic:
intro X Y
State after:
α : Type u_1
f : α → List α
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y

State before:
α : Type u_1
f : α → List α
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Tactic:
intro X_sub_Y
State after:
α : Type u_1
f : α → List α
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y

State before:
α : Type u_1
f : α → List α
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
Tactic:
simp at *
State after:
α : Type u_1
f : α → List α
X Y : List α
X_sub_Y : X ⊆ Y
⊢ X ⊆ Y

State before:
α : Type u_1
f : α → List α
X Y : List α
X_sub_Y : X ⊆ Y
⊢ X ⊆ Y
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y
Tactic:
intro X Y
State after:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y

State before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y
Tactic:
simp
State after:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
⊢ X ⊆ Y →
    (fun X => (List.map f X).join)^[i] (List.map f X).join ⊆ (fun X => (List.map f X).join)^[i] (List.map f Y).join

State before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
⊢ X ⊆ Y →
    (fun X => (List.map f X).join)^[i] (List.map f X).join ⊆ (fun X => (List.map f X).join)^[i] (List.map f Y).join
Tactic:
intro X_sub_Y
State after:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (fun X => (List.map f X).join)^[i] (List.map f X).join ⊆ (fun X => (List.map f X).join)^[i] (List.map f Y).join

State before:
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (fun X => (List.map f X).join)^[i] (List.map f X).join ⊆ (fun X => (List.map f X).join)^[i] (List.map f Y).join
Tactic:
apply IH
State after:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (List.map f X).join ⊆ (List.map f Y).join

State before:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
⊢ (List.map f X).join ⊆ (List.map f Y).join
Tactic:
have := List.map_subset f X_sub_Y
State after:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
this : List.map f X ⊆ List.map f Y
⊢ (List.map f X).join ⊆ (List.map f Y).join

State before:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
this : List.map f X ⊆ List.map f Y
⊢ (List.map f X).join ⊆ (List.map f Y).join
Tactic:
intro a a_in
State after:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
this : List.map f X ⊆ List.map f Y
a : α
a_in : a ∈ (List.map f X).join
⊢ a ∈ (List.map f Y).join

State before:
case a
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
X Y : List α
X_sub_Y : X ⊆ Y
this : List.map f X ⊆ List.map f Y
a : α
a_in : a ∈ (List.map f X).join
⊢ a ∈ (List.map f Y).join
Tactic:
aesop
State after:
no goals