internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Tactic:
cases h2
Proof state after:
case intro
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
left✝ : X = Y
right✝ : isAlphaEqvVarList binders xs ys
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Tactic:
case intro h2_left h2_right =>
  simp only [isAlphaEqvVarList_length binders xs ys h2_right] at c1
  subst h2_left
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Tactic:
simp only [isAlphaEqvVarList_length binders xs ys h2_right] at c1
Proof state after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ ys.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ ys.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Tactic:
subst h2_left
Proof state after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2_right : isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ ys.length = hd.args.length
c2 : ¬(X = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ X ys)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2_right : isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ ys.length = hd.args.length
c2 : ¬(X = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ X ys)
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : Y = hd.name ∧ ys.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Tactic:
cases h2
Proof state after:
case intro
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : Y = hd.name ∧ ys.length = hd.args.length
left✝ : X = Y
right✝ : isAlphaEqvVarList binders xs ys
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Tactic:
case intro h2_left h2_right =>
  simp only [← isAlphaEqvVarList_length binders xs ys h2_right] at c2
  subst h2_left
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Tactic:
simp only [← isAlphaEqvVarList_length binders xs ys h2_right] at c2
Proof state after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
c2 : Y = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
c2 : Y = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Tactic:
subst h2_left
Proof state after:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
h2_right : isAlphaEqvVarList binders xs ys
c2 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
h2_right : isAlphaEqvVarList binders xs ys
c2 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ Y ys)
Tactic:
exact ih V V' (def_ X xs) (def_ Y ys) binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.isalphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F F' : Formula
h1 : isAlphaEqv F F'
⊢ Holds D I V E F ↔ Holds D I V E F'
Tactic:
simp only [isAlphaEqv] at h1
Proof state after:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F F' : Formula
h1 : isAlphaEqvAux [] F F'
⊢ Holds D I V E F ↔ Holds D I V E F'
Theorem: FOL.NV.isalphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F F' : Formula
h1 : isAlphaEqvAux [] F F'
⊢ Holds D I V E F ↔ Holds D I V E F'
Tactic:
exact isAlphaEqv_Holds_aux D I V V E F F' [] AlphaEqvVarAssignment.nil h1
Proof state after:
no goals
Theorem: Finset.union_subset_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ A ∪ B ⊆ C ∪ D
Tactic:
apply Finset.union_subset_iff.mpr
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ A ⊆ C ∪ D ∧ B ⊆ C ∪ D
Theorem: Finset.union_subset_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ A ⊆ C ∪ D ∧ B ⊆ C ∪ D
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ A ⊆ C ∪ D

case right
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ B ⊆ C ∪ D
Theorem: Finset.union_subset_left_right
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ A ⊆ C ∪ D
Tactic:
trans C
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ A ⊆ C

α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ C ⊆ C ∪ D
Theorem: Finset.union_subset_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ A ⊆ C
Tactic:
exact h1
Proof state after:
no goals
Theorem: Finset.union_subset_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ C ⊆ C ∪ D
Tactic:
exact Finset.subset_union_left C D
Proof state after:
no goals
Theorem: Finset.union_subset_left_right
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ B ⊆ C ∪ D
Tactic:
trans D
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ B ⊆ D

α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ D ⊆ C ∪ D
Theorem: Finset.union_subset_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ B ⊆ D
Tactic:
exact h2
Proof state after:
no goals
Theorem: Finset.union_subset_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ D ⊆ C ∪ D
Tactic:
exact Finset.subset_union_right C D
Proof state after:
no goals
Theorem: Finset.union_subset_union_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ A ∪ B ⊆ C ∪ D ∪ E
Tactic:
apply Finset.union_subset_iff.mpr
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ A ⊆ C ∪ D ∪ E ∧ B ⊆ C ∪ D ∪ E
Theorem: Finset.union_subset_union_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ A ⊆ C ∪ D ∪ E ∧ B ⊆ C ∪ D ∪ E
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ A ⊆ C ∪ D ∪ E

case right
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ B ⊆ C ∪ D ∪ E
Theorem: Finset.union_subset_union_left_right
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ A ⊆ C ∪ D ∪ E
Tactic:
trans C ∪ E
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ A ⊆ C ∪ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ C ∪ E ⊆ C ∪ D ∪ E
Theorem: Finset.union_subset_union_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ A ⊆ C ∪ E
Tactic:
exact h1
Proof state after:
no goals
Theorem: Finset.union_subset_union_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ C ∪ E ⊆ C ∪ D ∪ E
Tactic:
apply Finset.union_subset_union_left
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ C ⊆ C ∪ D
Theorem: Finset.union_subset_union_left_right
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ C ⊆ C ∪ D
Tactic:
exact Finset.subset_union_left C D
Proof state after:
no goals
Theorem: Finset.union_subset_union_left_right
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ B ⊆ C ∪ D ∪ E
Tactic:
trans D ∪ E
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ B ⊆ D ∪ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ D ∪ E ⊆ C ∪ D ∪ E
Theorem: Finset.union_subset_union_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ B ⊆ D ∪ E
Tactic:
exact h2
Proof state after:
no goals
Theorem: Finset.union_subset_union_left_right
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ D ∪ E ⊆ C ∪ D ∪ E
Tactic:
apply Finset.union_subset_union_left
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ D ⊆ C ∪ D
Theorem: Finset.union_subset_union_left_right
Proof state before:
case h
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ D ⊆ C ∪ D
Tactic:
exact Finset.subset_union_right C D
Proof state after:
no goals
Theorem: Finset.union_subset_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ∪ B ⊆ (C ∪ D) \ E
Tactic:
apply Finset.union_subset_iff.mpr
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ (C ∪ D) \ E ∧ B ⊆ (C ∪ D) \ E
Theorem: Finset.union_subset_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ (C ∪ D) \ E ∧ B ⊆ (C ∪ D) \ E
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ (C ∪ D) \ E

case right
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ B ⊆ (C ∪ D) \ E
Theorem: Finset.union_subset_diff
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ (C ∪ D) \ E
Tactic:
trans C \ E
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ C \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ C \ E ⊆ (C ∪ D) \ E
Theorem: Finset.union_subset_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ C \ E
Tactic:
exact h1
Proof state after:
no goals
Theorem: Finset.union_subset_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ C \ E ⊆ (C ∪ D) \ E
Tactic:
apply Finset.sdiff_subset_sdiff
Proof state after:
case hst
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ C ⊆ C ∪ D

case hvu
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ E ⊆ E
Theorem: Finset.union_subset_diff
Proof state before:
case hst
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ C ⊆ C ∪ D
Tactic:
exact Finset.subset_union_left C D
Proof state after:
no goals
Theorem: Finset.union_subset_diff
Proof state before:
case hvu
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ E ⊆ E
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.union_subset_diff
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ B ⊆ (C ∪ D) \ E
Tactic:
trans D \ E
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ B ⊆ D \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ D \ E ⊆ (C ∪ D) \ E
Theorem: Finset.union_subset_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ B ⊆ D \ E
Tactic:
exact h2
Proof state after:
no goals
Theorem: Finset.union_subset_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ D \ E ⊆ (C ∪ D) \ E
Tactic:
apply Finset.sdiff_subset_sdiff
Proof state after:
case hst
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ D ⊆ C ∪ D

case hvu
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ E ⊆ E
Theorem: Finset.union_subset_diff
Proof state before:
case hst
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ D ⊆ C ∪ D
Tactic:
exact Finset.subset_union_right C D
Proof state after:
no goals
Theorem: Finset.union_subset_left_right_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ A ∪ B ⊆ E ∪ (C ∪ D) \ F
Tactic:
apply Finset.union_subset_iff.mpr
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ A ⊆ E ∪ (C ∪ D) \ F ∧ B ⊆ E ∪ (C ∪ D) \ F
Theorem: Finset.union_subset_left_right_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ A ⊆ E ∪ (C ∪ D) \ F ∧ B ⊆ E ∪ (C ∪ D) \ F
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ A ⊆ E ∪ (C ∪ D) \ F

case right
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ B ⊆ E ∪ (C ∪ D) \ F
Theorem: Finset.union_subset_left_right_diff
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ A ⊆ E ∪ (C ∪ D) \ F
Tactic:
trans E ∪ C \ F
Proof state after:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ A ⊆ E ∪ C \ F

α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ E ∪ C \ F ⊆ E ∪ (C ∪ D) \ F
Theorem: Finset.union_subset_left_right_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ A ⊆ E ∪ C \ F
Tactic:
exact h1
Proof state after:
no goals
Theorem: Finset.union_subset_left_right_diff
Proof state before:
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ E ∪ C \ F ⊆ E ∪ (C ∪ D) \ F
Tactic:
apply Finset.union_subset_union_right
Proof state after:
case h
α : Type
inst✝ : DecidableEq α
A B C D E F : Finset α
h1 : A ⊆ E ∪ C \ F
h2 : B ⊆ E ∪ D \ F
⊢ C \ F ⊆ (C ∪ D) \ F