internlm/Lean-Github huggingface dataset:
Theorem: Digraph.Walk.map_toDeleteEdges_eq
Proof state before:
case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
e : V × V
⊢ e ∈ edges (Walk.transfer p (deleteEdges G s) (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet (deleteEdges G s))) →
    e ∈ edgeSet G
Tactic:
rw [edges_transfer]
Proof state after:
case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
e : V × V
⊢ e ∈ edges p → e ∈ edgeSet G
Theorem: Digraph.Walk.map_toDeleteEdges_eq
Proof state before:
case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
e : V × V
⊢ e ∈ edges p → e ∈ edgeSet G
Tactic:
apply edges_subset_edgeSet p
Proof state after:
no goals
Theorem: Digraph.Walk.toDeleteEdges_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u' v' : V
s : Set (V × V)
p : Walk G u v
hu : u = u'
hv : v = v'
h : ∀ (e : V × V), e ∈ edges (Walk.copy p hu hv) → ¬e ∈ s
⊢ ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
s : Set (V × V)
p : Walk G u' v'
h : ∀ (e : V × V), e ∈ edges (Walk.copy p (_ : u' = u') (_ : v' = v')) → ¬e ∈ s
⊢ ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
Theorem: Digraph.Walk.toDeleteEdges_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
s : Set (V × V)
p : Walk G u' v'
h : ∀ (e : V × V), e ∈ edges (Walk.copy p (_ : u' = u') (_ : v' = v')) → ¬e ∈ s
⊢ ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: Digraph.Walk.toDeleteEdges_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u' v' : V
s : Set (V × V)
p : Walk G u v
hu : u = u'
hv : v = v'
h : ∀ (e : V × V), e ∈ edges (Walk.copy p hu hv) → ¬e ∈ s
⊢ toDeleteEdges s (Walk.copy p hu hv) h = Walk.copy (toDeleteEdges s p (_ : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s)) hu hv
Tactic:
subst_vars
Proof state after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
s : Set (V × V)
p : Walk G u' v'
h : ∀ (e : V × V), e ∈ edges (Walk.copy p (_ : u' = u') (_ : v' = v')) → ¬e ∈ s
⊢ toDeleteEdges s (Walk.copy p (_ : u' = u') (_ : v' = v')) h =
    Walk.copy (toDeleteEdges s p (_ : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s)) (_ : u' = u') (_ : v' = v')
Theorem: Digraph.Walk.toDeleteEdges_copy
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u' v' : V
s : Set (V × V)
p : Walk G u' v'
h : ∀ (e : V × V), e ∈ edges (Walk.copy p (_ : u' = u') (_ : v' = v')) → ¬e ∈ s
⊢ toDeleteEdges s (Walk.copy p (_ : u' = u') (_ : v' = v')) h =
    Walk.copy (toDeleteEdges s p (_ : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s)) (_ : u' = u') (_ : v' = v')
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Reachable.elim_path
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
p : Prop
u v : V
h : Reachable G u v
hp : Path G u v → p
⊢ p
Tactic:
classical exact h.elim fun q => hp q.toPath
Proof state after:
no goals
Theorem: Digraph.Reachable.elim_path
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
p : Prop
u v : V
h : Reachable G u v
hp : Path G u v → p
⊢ p
Tactic:
exact h.elim fun q => hp q.toPath
Proof state after:
no goals
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Reachable G u v ↔ Relation.ReflTransGen G.Adj u v
Tactic:
constructor
Proof state after:
case mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Reachable G u v → Relation.ReflTransGen G.Adj u v

case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Relation.ReflTransGen G.Adj u v → Reachable G u v
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
case mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Reachable G u v → Relation.ReflTransGen G.Adj u v
Tactic:
rintro ⟨h⟩
Proof state after:
case mp.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : Walk G u v
⊢ Relation.ReflTransGen G.Adj u v
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
case mp.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : Walk G u v
⊢ Relation.ReflTransGen G.Adj u v
Tactic:
induction h with
| nil => rfl
| cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
Proof state after:
no goals
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
case mp.intro.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ : V
⊢ Relation.ReflTransGen G.Adj u✝ u✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
case mp.intro.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : Relation.ReflTransGen G.Adj v✝ w✝
⊢ Relation.ReflTransGen G.Adj u✝ w✝
Tactic:
exact (Relation.ReflTransGen.single h').trans ih
Proof state after:
no goals
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Relation.ReflTransGen G.Adj u v → Reachable G u v
Tactic:
intro h
Proof state after:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ Reachable G u v
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
case mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ Reachable G u v
Tactic:
induction h with
| refl => rfl
| tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩
Proof state after:
no goals
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
case mpr.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
⊢ Reachable G u u
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.reachable_iff_reflTransGen
Proof state before:
case mpr.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v b✝ c✝ : V
a✝ : Relation.ReflTransGen G.Adj u b✝
ha : G.Adj b✝ c✝
hr : Reachable G u b✝
⊢ Reachable G u c✝
Tactic:
exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩
Proof state after:
no goals
Theorem: Digraph.Iso.symm_apply_reachable
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G✝ : Digraph V
G'✝ : Digraph V'
G'' : Digraph V''
G : Digraph V
G' : Digraph V'
φ : G ≃g G'
u : V
v : V'
⊢ Reachable G (↑(symm φ) v) u ↔ Reachable G' v (↑φ u)
Tactic:
rw [← Iso.reachable_iff, RelIso.apply_symm_apply]
Proof state after:
no goals
Theorem: Digraph.set_walk_self_length_zero_eq
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
⊢ {p | Walk.length p = 0} = {Walk.nil}
Tactic:
ext p
Proof state after:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
p : Walk G u u
⊢ p ∈ {p | Walk.length p = 0} ↔ p ∈ {Walk.nil}
Theorem: Digraph.set_walk_self_length_zero_eq
Proof state before:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
p : Walk G u u
⊢ p ∈ {p | Walk.length p = 0} ↔ p ∈ {Walk.nil}
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.set_walk_length_zero_eq_of_ne
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : u ≠ v
⊢ {p | Walk.length p = 0} = ∅
Tactic:
ext p
Proof state after:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : u ≠ v
p : Walk G u v
⊢ p ∈ {p | Walk.length p = 0} ↔ p ∈ ∅
Theorem: Digraph.set_walk_length_zero_eq_of_ne
Proof state before:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : u ≠ v
p : Walk G u v
⊢ p ∈ {p | Walk.length p = 0} ↔ p ∈ ∅
Tactic:
simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false_iff]
Proof state after:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : u ≠ v
p : Walk G u v
⊢ ¬Walk.length p = 0
Theorem: Digraph.set_walk_length_zero_eq_of_ne
Proof state before:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
h : u ≠ v
p : Walk G u v
⊢ ¬Walk.length p = 0
Tactic:
exact fun h' => absurd (Walk.eq_of_length_eq_zero h') h
Proof state after:
no goals
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
⊢ {p | Walk.length p = Nat.succ n} = ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Tactic:
ext p
Proof state after:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
p : Walk G u v
⊢ p ∈ {p | Walk.length p = Nat.succ n} ↔ p ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
p : Walk G u v
⊢ p ∈ {p | Walk.length p = Nat.succ n} ↔ p ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Tactic:
cases' p with _ _ w _ huw pwv
Proof state after:
case h.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
n : ℕ
⊢ Walk.nil ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.nil ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}

case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.cons huw pwv ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.cons huw pwv ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
case h.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
n : ℕ
⊢ Walk.nil ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.nil ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Tactic:
simp [eq_comm]
Proof state after:
no goals
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.cons huw pwv ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.cons huw pwv ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
Tactic:
simp only [Nat.succ_eq_add_one, Set.mem_setOf_eq, Walk.length_cons, add_left_inj,
  Set.mem_iUnion, Set.mem_image, exists_prop]
Proof state after:
case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.length pwv = n ↔ ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.length pwv = n ↔ ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv
Tactic:
constructor
Proof state after:
case h.cons.mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.length pwv = n → ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv

case h.cons.mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ (∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv) → Walk.length pwv = n
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
case h.cons.mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.length pwv = n → ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv
Tactic:
rintro rfl
Proof state after:
case h.cons.mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ ∃ i h x, Walk.length x = Walk.length pwv ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
case h.cons.mp
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ ∃ i h x, Walk.length x = Walk.length pwv ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv
Tactic:
exact ⟨w, huw, pwv, rfl, rfl⟩
Proof state after:
no goals
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
case h.cons.mpr
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ (∃ i h x, Walk.length x = n ∧ Walk.cons (_ : G.Adj u i) x = Walk.cons huw pwv) → Walk.length pwv = n
Tactic:
rintro ⟨w, huw, pwv, rfl, rfl, rfl⟩
Proof state after:
case h.cons.mpr.intro.intro.intro.intro.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
huw✝ : G.Adj u w
pwv : Walk G w v
huw : G.Adj u w
⊢ Walk.length pwv = Walk.length pwv
Theorem: Digraph.set_walk_length_succ_eq
Proof state before:
case h.cons.mpr.intro.intro.intro.intro.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
huw✝ : G.Adj u w
pwv : Walk G w v
huw : G.Adj u w
⊢ Walk.length pwv = Walk.length pwv
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.iSup_adj
Proof state before:
ι : Sort u_1
𝕜 : Type ?u.10671
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : ι → Digraph V
⊢ (⨆ (i : ι), f i).Adj a b ↔ ∃ i, (f i).Adj a b
Tactic:
simp [iSup]
Proof state after:
no goals
Theorem: Digraph.iInf_adj
Proof state before:
ι : Sort u_1
𝕜 : Type ?u.13166
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : ι → Digraph V
⊢ (⨅ (i : ι), f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b
Tactic:
simp [iInf]
Proof state after:
no goals
Theorem: Digraph.edgeSet_bot
Proof state before:
ι : Sort ?u.51631
𝕜 : Type ?u.51634
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ edgeSet ⊥ = ∅
Tactic:
rw [Set.eq_empty_iff_forall_not_mem]
Proof state after:
ι : Sort ?u.51631
𝕜 : Type ?u.51634
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ ∀ (x : V × V), ¬x ∈ edgeSet ⊥
Theorem: Digraph.edgeSet_bot
Proof state before:
ι : Sort ?u.51631
𝕜 : Type ?u.51634
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ ∀ (x : V × V), ¬x ∈ edgeSet ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.edgeSet_sup
Proof state before:
ι : Sort ?u.54704
𝕜 : Type ?u.54707
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ edgeSet (G₁ ⊔ G₂) = edgeSet G₁ ∪ edgeSet G₂
Tactic:
ext ⟨x, y⟩
Proof state after:
case h.mk
ι : Sort ?u.54704
𝕜 : Type ?u.54707
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
x y : V
⊢ (x, y) ∈ edgeSet (G₁ ⊔ G₂) ↔ (x, y) ∈ edgeSet G₁ ∪ edgeSet G₂
Theorem: Digraph.edgeSet_sup
Proof state before:
case h.mk
ι : Sort ?u.54704
𝕜 : Type ?u.54707
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
x y : V
⊢ (x, y) ∈ edgeSet (G₁ ⊔ G₂) ↔ (x, y) ∈ edgeSet G₁ ∪ edgeSet G₂
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.edgeSet_inf
Proof state before:
ι : Sort ?u.54886
𝕜 : Type ?u.54889
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ edgeSet (G₁ ⊓ G₂) = edgeSet G₁ ∩ edgeSet G₂
Tactic:
ext ⟨x, y⟩
Proof state after:
case h.mk
ι : Sort ?u.54886
𝕜 : Type ?u.54889
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
x y : V
⊢ (x, y) ∈ edgeSet (G₁ ⊓ G₂) ↔ (x, y) ∈ edgeSet G₁ ∩ edgeSet G₂
Theorem: Digraph.edgeSet_inf
Proof state before:
case h.mk
ι : Sort ?u.54886
𝕜 : Type ?u.54889
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
x y : V
⊢ (x, y) ∈ edgeSet (G₁ ⊓ G₂) ↔ (x, y) ∈ edgeSet G₁ ∩ edgeSet G₂
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.edgeSet_sdiff
Proof state before:
ι : Sort ?u.55069
𝕜 : Type ?u.55072
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ edgeSet (G₁ \ G₂) = edgeSet G₁ \ edgeSet G₂
Tactic:
ext ⟨x, y⟩
Proof state after:
case h.mk
ι : Sort ?u.55069
𝕜 : Type ?u.55072
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
x y : V
⊢ (x, y) ∈ edgeSet (G₁ \ G₂) ↔ (x, y) ∈ edgeSet G₁ \ edgeSet G₂
Theorem: Digraph.edgeSet_sdiff
Proof state before:
case h.mk
ι : Sort ?u.55069
𝕜 : Type ?u.55072
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
x y : V
⊢ (x, y) ∈ edgeSet (G₁ \ G₂) ↔ (x, y) ∈ edgeSet G₁ \ edgeSet G₂
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.sdiff_eq_deleteEdges
Proof state before:
ι : Sort ?u.60271
𝕜 : Type ?u.60274
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
G G' : Digraph V
⊢ G \ G' = deleteEdges G (edgeSet G')
Tactic:
ext
Proof state after:
case Adj.h.h.a
ι : Sort ?u.60271
𝕜 : Type ?u.60274
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
G G' : Digraph V
x✝¹ x✝ : V
⊢ (G \ G').Adj x✝¹ x✝ ↔ (deleteEdges G (edgeSet G')).Adj x✝¹ x✝
Theorem: Digraph.sdiff_eq_deleteEdges
Proof state before:
case Adj.h.h.a
ι : Sort ?u.60271
𝕜 : Type ?u.60274
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
G G' : Digraph V
x✝¹ x✝ : V
⊢ (G \ G').Adj x✝¹ x✝ ↔ (deleteEdges G (edgeSet G')).Adj x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.compl_eq_deleteEdges
Proof state before:
ι : Sort ?u.60648
𝕜 : Type ?u.60651
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
⊢ Gᶜ = deleteEdges ⊤ (edgeSet G)
Tactic:
ext
Proof state after:
case Adj.h.h.a
ι : Sort ?u.60648
𝕜 : Type ?u.60651
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w x✝¹ x✝ : V
⊢ Gᶜ.Adj x✝¹ x✝ ↔ (deleteEdges ⊤ (edgeSet G)).Adj x✝¹ x✝
Theorem: Digraph.compl_eq_deleteEdges
Proof state before:
case Adj.h.h.a
ι : Sort ?u.60648
𝕜 : Type ?u.60651
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w x✝¹ x✝ : V
⊢ Gᶜ.Adj x✝¹ x✝ ↔ (deleteEdges ⊤ (edgeSet G)).Adj x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.deleteEdges_deleteEdges
Proof state before:
ι : Sort ?u.61070
𝕜 : Type ?u.61073
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s s' : Set (V × V)
⊢ deleteEdges (deleteEdges G s) s' = deleteEdges G (s ∪ s')
Tactic:
ext
Proof state after:
case Adj.h.h.a
ι : Sort ?u.61070
𝕜 : Type ?u.61073
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s s' : Set (V × V)
x✝¹ x✝ : V
⊢ (deleteEdges (deleteEdges G s) s').Adj x✝¹ x✝ ↔ (deleteEdges G (s ∪ s')).Adj x✝¹ x✝
Theorem: Digraph.deleteEdges_deleteEdges
Proof state before:
case Adj.h.h.a
ι : Sort ?u.61070
𝕜 : Type ?u.61073
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s s' : Set (V × V)
x✝¹ x✝ : V
⊢ (deleteEdges (deleteEdges G s) s').Adj x✝¹ x✝ ↔ (deleteEdges G (s ∪ s')).Adj x✝¹ x✝
Tactic:
simp [and_assoc, not_or]
Proof state after:
no goals
Theorem: Digraph.deleteEdges_empty_eq
Proof state before:
ι : Sort ?u.61543
𝕜 : Type ?u.61546
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
⊢ deleteEdges G ∅ = G
Tactic:
ext
Proof state after:
case Adj.h.h.a
ι : Sort ?u.61543
𝕜 : Type ?u.61546
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w x✝¹ x✝ : V
⊢ (deleteEdges G ∅).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Theorem: Digraph.deleteEdges_empty_eq
Proof state before:
case Adj.h.h.a
ι : Sort ?u.61543
𝕜 : Type ?u.61546
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w x✝¹ x✝ : V
⊢ (deleteEdges G ∅).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.deleteEdges_univ_eq
Proof state before:
ι : Sort ?u.61865
𝕜 : Type ?u.61868
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
⊢ deleteEdges G Set.univ = ⊥
Tactic:
ext
Proof state after:
case Adj.h.h.a
ι : Sort ?u.61865
𝕜 : Type ?u.61868
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w x✝¹ x✝ : V
⊢ (deleteEdges G Set.univ).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Theorem: Digraph.deleteEdges_univ_eq
Proof state before:
case Adj.h.h.a
ι : Sort ?u.61865
𝕜 : Type ?u.61868
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w x✝¹ x✝ : V
⊢ (deleteEdges G Set.univ).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.deleteEdges_le
Proof state before:
ι : Sort ?u.62316
𝕜 : Type ?u.62319
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
⊢ deleteEdges G s ≤ G
Tactic:
intro
Proof state after:
ι : Sort ?u.62316
𝕜 : Type ?u.62319
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
v✝ : V
⊢ ∀ ⦃w : V⦄, (deleteEdges G s).Adj v✝ w → G.Adj v✝ w
Theorem: Digraph.deleteEdges_le
Proof state before:
ι : Sort ?u.62316
𝕜 : Type ?u.62319
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
v✝ : V
⊢ ∀ ⦃w : V⦄, (deleteEdges G s).Adj v✝ w → G.Adj v✝ w
Tactic:
simp (config := { contextual := true })
Proof state after:
no goals
Theorem: Digraph.deleteEdges_le_of_le
Proof state before:
ι : Sort ?u.64664
𝕜 : Type ?u.64667
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
s s' : Set (V × V)
h : s ⊆ s'
v w : V
⊢ (deleteEdges G s').Adj v w → (deleteEdges G s).Adj v w
Tactic:
simp (config := { contextual := true }) only [deleteEdges_adj, and_imp, true_and_iff]
Proof state after:
ι : Sort ?u.64664
𝕜 : Type ?u.64667
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
s s' : Set (V × V)
h : s ⊆ s'
v w : V
⊢ G.Adj v w → ¬(v, w) ∈ s' → ¬(v, w) ∈ s
Theorem: Digraph.deleteEdges_le_of_le
Proof state before:
ι : Sort ?u.64664
𝕜 : Type ?u.64667
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
s s' : Set (V × V)
h : s ⊆ s'
v w : V
⊢ G.Adj v w → ¬(v, w) ∈ s' → ¬(v, w) ∈ s
Tactic:
exact fun _ hn hs => hn (h hs)
Proof state after:
no goals
Theorem: Digraph.deleteEdges_eq_inter_edgeSet
Proof state before:
ι : Sort ?u.65081
𝕜 : Type ?u.65084
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
⊢ deleteEdges G s = deleteEdges G (s ∩ edgeSet G)
Tactic:
ext
Proof state after:
case Adj.h.h.a
ι : Sort ?u.65081
𝕜 : Type ?u.65084
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
x✝¹ x✝ : V
⊢ (deleteEdges G s).Adj x✝¹ x✝ ↔ (deleteEdges G (s ∩ edgeSet G)).Adj x✝¹ x✝
Theorem: Digraph.deleteEdges_eq_inter_edgeSet
Proof state before:
case Adj.h.h.a
ι : Sort ?u.65081
𝕜 : Type ?u.65084
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
s : Set (V × V)
x✝¹ x✝ : V
⊢ (deleteEdges G s).Adj x✝¹ x✝ ↔ (deleteEdges G (s ∩ edgeSet G)).Adj x✝¹ x✝
Tactic:
simp (config := { contextual := true }) [imp_false]
Proof state after:
no goals