internlm/Lean-Github huggingface dataset:
Theorem: Digraph.deleteEdges_sdiff_eq_of_le
Proof state before:
ι : Sort ?u.66345
𝕜 : Type ?u.66348
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
H : Digraph V
h : H ≤ G
⊢ deleteEdges G (edgeSet G \ edgeSet H) = H
Tactic:
ext (v w)
Proof state after:
case Adj.h.h.a
ι : Sort ?u.66345
𝕜 : Type ?u.66348
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
H : Digraph V
h : H ≤ G
v w : V
⊢ (deleteEdges G (edgeSet G \ edgeSet H)).Adj v w ↔ H.Adj v w
Theorem: Digraph.deleteEdges_sdiff_eq_of_le
Proof state before:
case Adj.h.h.a
ι : Sort ?u.66345
𝕜 : Type ?u.66348
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v✝ w✝ : V
H : Digraph V
h : H ≤ G
v w : V
⊢ (deleteEdges G (edgeSet G \ edgeSet H)).Adj v w ↔ H.Adj v w
Tactic:
constructor <;> simp (config := { contextual := true }) [@h v w]
Proof state after:
no goals
Theorem: Digraph.edgeSet_deleteEdges
Proof state before:
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
⊢ edgeSet (deleteEdges G s) = edgeSet G \ s
Tactic:
ext e
Proof state after:
case h
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
e : V × V
⊢ e ∈ edgeSet (deleteEdges G s) ↔ e ∈ edgeSet G \ s
Theorem: Digraph.edgeSet_deleteEdges
Proof state before:
case h
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
e : V × V
⊢ e ∈ edgeSet (deleteEdges G s) ↔ e ∈ edgeSet G \ s
Tactic:
cases e
Proof state after:
case h.mk
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
fst✝ snd✝ : V
⊢ (fst✝, snd✝) ∈ edgeSet (deleteEdges G s) ↔ (fst✝, snd✝) ∈ edgeSet G \ s
Theorem: Digraph.edgeSet_deleteEdges
Proof state before:
case h.mk
ι : Sort ?u.68599
𝕜 : Type ?u.68602
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)
fst✝ snd✝ : V
⊢ (fst✝, snd✝) ∈ edgeSet (deleteEdges G s) ↔ (fst✝, snd✝) ∈ edgeSet G \ s
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.map_monotone
Proof state before:
ι : Sort ?u.69221
𝕜 : Type ?u.69224
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : V → W
⊢ Monotone (Digraph.map f)
Tactic:
rintro G G' h _ _ ⟨u, v, ha, rfl, rfl⟩
Proof state after:
case intro.intro.intro.intro
ι : Sort ?u.69221
𝕜 : Type ?u.69224
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u✝ v✝ w : V
f : V → W
G G' : Digraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
⊢ (Digraph.map f G').Adj (f u) (f v)
Theorem: Digraph.map_monotone
Proof state before:
case intro.intro.intro.intro
ι : Sort ?u.69221
𝕜 : Type ?u.69224
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u✝ v✝ w : V
f : V → W
G G' : Digraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
⊢ (Digraph.map f G').Adj (f u) (f v)
Tactic:
exact ⟨_, _, h ha, rfl, rfl⟩
Proof state after:
no goals
Theorem: Digraph.comap_monotone
Proof state before:
ι : Sort ?u.70267
𝕜 : Type ?u.70270
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : V → W
⊢ Monotone (Digraph.comap f)
Tactic:
intro G G' h _ _ ha
Proof state after:
ι : Sort ?u.70267
𝕜 : Type ?u.70270
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
f : V → W
G G' : Digraph W
h : G ≤ G'
v✝ w✝ : V
ha : (Digraph.comap f G).Adj v✝ w✝
⊢ (Digraph.comap f G').Adj v✝ w✝
Theorem: Digraph.comap_monotone
Proof state before:
ι : Sort ?u.70267
𝕜 : Type ?u.70270
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
f : V → W
G G' : Digraph W
h : G ≤ G'
v✝ w✝ : V
ha : (Digraph.comap f G).Adj v✝ w✝
⊢ (Digraph.comap f G').Adj v✝ w✝
Tactic:
exact h ha
Proof state after:
no goals
Theorem: Digraph.comap_map_eq
Proof state before:
ι : Sort ?u.70997
𝕜 : Type ?u.71000
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
f : V ↪ W
G : Digraph V
⊢ Digraph.comap (↑f) (Digraph.map (↑f) G) = G
Tactic:
ext
Proof state after:
case Adj.h.h.a
ι : Sort ?u.70997
𝕜 : Type ?u.71000
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
f : V ↪ W
G : Digraph V
x✝¹ x✝ : V
⊢ (Digraph.comap (↑f) (Digraph.map (↑f) G)).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Theorem: Digraph.comap_map_eq
Proof state before:
case Adj.h.h.a
ι : Sort ?u.70997
𝕜 : Type ?u.71000
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
f : V ↪ W
G : Digraph V
x✝¹ x✝ : V
⊢ (Digraph.comap (↑f) (Digraph.map (↑f) G)).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Digraph.map_le_iff_le_comap
Proof state before:
ι : Sort ?u.118218
𝕜 : Type ?u.118221
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u v w : V
f : V ↪ W
G : Digraph V
G' : Digraph W
⊢ G ≤ Digraph.comap (↑f) G' → Digraph.map (↑f) G ≤ G'
Tactic:
rintro h _ _ ⟨u, v, ha, rfl, rfl⟩
Proof state after:
case intro.intro.intro.intro
ι : Sort ?u.118218
𝕜 : Type ?u.118221
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u✝ v✝ w : V
f : V ↪ W
G : Digraph V
G' : Digraph W
h : G ≤ Digraph.comap (↑f) G'
u v : V
ha : G.Adj u v
⊢ G'.Adj (↑f u) (↑f v)
Theorem: Digraph.map_le_iff_le_comap
Proof state before:
case intro.intro.intro.intro
ι : Sort ?u.118218
𝕜 : Type ?u.118221
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G'✝ : Digraph W
a b c u✝ v✝ w : V
f : V ↪ W
G : Digraph V
G' : Digraph W
h : G ≤ Digraph.comap (↑f) G'
u v : V
ha : G.Adj u v
⊢ G'.Adj (↑f u) (↑f v)
Tactic:
exact h ha
Proof state after:
no goals
Theorem: Digraph.map_comap_le
Proof state before:
ι : Sort ?u.133674
𝕜 : Type ?u.133677
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
f : V ↪ W
G : Digraph W
⊢ Digraph.map (↑f) (Digraph.comap (↑f) G) ≤ G
Tactic:
rw [map_le_iff_le_comap]
Proof state after:
no goals
Theorem: Digraph.Hom.map_mem_edgeSet
Proof state before:
ι : Sort ?u.200863
𝕜 : Type ?u.200866
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
e : V × V
h : e ∈ edgeSet G
⊢ Prod.map (↑f) (↑f) e ∈ edgeSet G'
Tactic:
cases e
Proof state after:
case mk
ι : Sort ?u.200863
𝕜 : Type ?u.200866
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
fst✝ snd✝ : V
h : (fst✝, snd✝) ∈ edgeSet G
⊢ Prod.map ↑f ↑f (fst✝, snd✝) ∈ edgeSet G'
Theorem: Digraph.Hom.map_mem_edgeSet
Proof state before:
case mk
ι : Sort ?u.200863
𝕜 : Type ?u.200866
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
fst✝ snd✝ : V
h : (fst✝, snd✝) ∈ edgeSet G
⊢ Prod.map ↑f ↑f (fst✝, snd✝) ∈ edgeSet G'
Tactic:
exact f.map_rel' h
Proof state after:
no goals
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
⊢ Injective (mapEdgeSet f)
Tactic:
rintro ⟨e₁, h₁⟩ ⟨e₂, h₂⟩
Proof state after:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ mapEdgeSet f { val := e₁, property := h₁ } = mapEdgeSet f { val := e₂, property := h₂ } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ mapEdgeSet f { val := e₁, property := h₁ } = mapEdgeSet f { val := e₂, property := h₂ } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
Tactic:
dsimp [Hom.mapEdgeSet]
Proof state after:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ { val := (↑f e₁.fst, ↑f e₁.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₁, property := h₁ } ∈ edgeSet G') } =
      { val := (↑f e₂.fst, ↑f e₂.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₂, property := h₂ } ∈ edgeSet G') } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ { val := (↑f e₁.fst, ↑f e₁.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₁, property := h₁ } ∈ edgeSet G') } =
      { val := (↑f e₂.fst, ↑f e₂.snd), property := (_ : Prod.map ↑f ↑f ↑{ val := e₂, property := h₂ } ∈ edgeSet G') } →
    { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
Tactic:
repeat' rw [Subtype.mk_eq_mk]
Proof state after:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ (↑f e₁.fst, ↑f e₁.snd) = (↑f e₂.fst, ↑f e₂.snd) → e₁ = e₂
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ (↑f e₁.fst, ↑f e₁.snd) = (↑f e₂.fst, ↑f e₂.snd) → e₁ = e₂
Tactic:
cases e₁
Proof state after:
case mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
fst✝ snd✝ : V
h₁ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) = (↑f e₂.fst, ↑f e₂.snd) → (fst✝, snd✝) = e₂
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
case mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
fst✝ snd✝ : V
h₁ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) = (↑f e₂.fst, ↑f e₂.snd) → (fst✝, snd✝) = e₂
Tactic:
cases e₂
Proof state after:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝¹, snd✝¹).fst, ↑f (fst✝¹, snd✝¹).snd) = (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) →
    (fst✝¹, snd✝¹) = (fst✝, snd✝)
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ (↑f (fst✝¹, snd✝¹).fst, ↑f (fst✝¹, snd✝¹).snd) = (↑f (fst✝, snd✝).fst, ↑f (fst✝, snd✝).snd) →
    (fst✝¹, snd✝¹) = (fst✝, snd✝)
Tactic:
simp
Proof state after:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ ↑f fst✝¹ = ↑f fst✝ → ↑f snd✝¹ = ↑f snd✝ → fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ ↑f fst✝¹ = ↑f fst✝ → ↑f snd✝¹ = ↑f snd✝ → fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Tactic:
intro h1 h2
Proof state after:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
h1 : ↑f fst✝¹ = ↑f fst✝
h2 : ↑f snd✝¹ = ↑f snd✝
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
h1 : ↑f fst✝¹ = ↑f fst✝
h2 : ↑f snd✝¹ = ↑f snd✝
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
Tactic:
simp [hinj h1, hinj h2]
Proof state after:
no goals
Theorem: Digraph.Hom.mapEdgeSet.injective
Proof state before:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ (↑f e₁.fst, ↑f e₁.snd) = (↑f e₂.fst, ↑f e₂.snd) → { val := e₁, property := h₁ } = { val := e₂, property := h₂ }
Tactic:
rw [Subtype.mk_eq_mk]
Proof state after:
case mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
e₁ : V × V
h₁ : e₁ ∈ edgeSet G
e₂ : V × V
h₂ : e₂ ∈ edgeSet G
⊢ (↑f e₁.fst, ↑f e₁.snd) = (↑f e₂.fst, ↑f e₂.snd) → e₁ = e₂
Theorem: Digraph.Embedding.map_mem_edgeSet_iff
Proof state before:
ι : Sort ?u.263245
𝕜 : Type ?u.263248
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G ↪g G'
e : V × V
⊢ Prod.map (↑f) (↑f) e ∈ edgeSet G' ↔ e ∈ edgeSet G
Tactic:
cases e
Proof state after:
case mk
ι : Sort ?u.263245
𝕜 : Type ?u.263248
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G ↪g G'
fst✝ snd✝ : V
⊢ Prod.map ↑f ↑f (fst✝, snd✝) ∈ edgeSet G' ↔ (fst✝, snd✝) ∈ edgeSet G
Theorem: Digraph.Embedding.map_mem_edgeSet_iff
Proof state before:
case mk
ι : Sort ?u.263245
𝕜 : Type ?u.263248
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G ↪g G'
fst✝ snd✝ : V
⊢ Prod.map ↑f ↑f (fst✝, snd✝) ∈ edgeSet G' ↔ (fst✝, snd✝) ∈ edgeSet G
Tactic:
simp [f.map_adj_iff]
Proof state after:
no goals
Theorem: Digraph.induceHom_id
Proof state before:
ι : Sort ?u.395639
𝕜 : Type ?u.395642
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s✝ : Set V
t : Set W
r : Set X
φ : G✝ →g G'
φst : Set.MapsTo (↑φ) s✝ t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
G : Digraph V
s : Set V
⊢ InduceHom Hom.id (_ : Set.MapsTo id s s) = Hom.id
Tactic:
ext x
Proof state after:
case h.a
ι : Sort ?u.395639
𝕜 : Type ?u.395642
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s✝ : Set V
t : Set W
r : Set X
φ : G✝ →g G'
φst : Set.MapsTo (↑φ) s✝ t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
G : Digraph V
s : Set V
x : ↑s
⊢ ↑(↑(InduceHom Hom.id (_ : Set.MapsTo id s s)) x) = ↑(↑Hom.id x)
Theorem: Digraph.induceHom_id
Proof state before:
case h.a
ι : Sort ?u.395639
𝕜 : Type ?u.395642
V : Type u
W : Type v
X : Type w
G✝ : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s✝ : Set V
t : Set W
r : Set X
φ : G✝ →g G'
φst : Set.MapsTo (↑φ) s✝ t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
G : Digraph V
s : Set V
x : ↑s
⊢ ↑(↑(InduceHom Hom.id (_ : Set.MapsTo id s s)) x) = ↑(↑Hom.id x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.induceHom_comp
Proof state before:
ι : Sort ?u.407307
𝕜 : Type ?u.407310
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (↑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
⊢ Hom.comp (InduceHom ψ ψtr) (InduceHom φ φst) = InduceHom (Hom.comp ψ φ) (_ : Set.MapsTo (↑ψ ∘ fun x => ↑φ x) s r)
Tactic:
ext x
Proof state after:
case h.a
ι : Sort ?u.407307
𝕜 : Type ?u.407310
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (↑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
x : ↑s
⊢ ↑(↑(Hom.comp (InduceHom ψ ψtr) (InduceHom φ φst)) x) =
    ↑(↑(InduceHom (Hom.comp ψ φ) (_ : Set.MapsTo (↑ψ ∘ fun x => ↑φ x) s r)) x)
Theorem: Digraph.induceHom_comp
Proof state before:
case h.a
ι : Sort ?u.407307
𝕜 : Type ?u.407310
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G'' : Digraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (↑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (↑ψ) t r
x : ↑s
⊢ ↑(↑(Hom.comp (InduceHom ψ ψtr) (InduceHom φ φst)) x) =
    ↑(↑(InduceHom (Hom.comp ψ φ) (_ : Set.MapsTo (↑ψ ∘ fun x => ↑φ x) s r)) x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Digraph.Iso.map_mem_edgeSet_iff
Proof state before:
ι : Sort ?u.420032
𝕜 : Type ?u.420035
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G ≃g G'
e : V × V
⊢ Prod.map (↑f) (↑f) e ∈ edgeSet G' ↔ e ∈ edgeSet G
Tactic:
cases e
Proof state after:
case mk
ι : Sort ?u.420032
𝕜 : Type ?u.420035
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G ≃g G'
fst✝ snd✝ : V
⊢ Prod.map ↑f ↑f (fst✝, snd✝) ∈ edgeSet G' ↔ (fst✝, snd✝) ∈ edgeSet G
Theorem: Digraph.Iso.map_mem_edgeSet_iff
Proof state before:
case mk
ι : Sort ?u.420032
𝕜 : Type ?u.420035
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G ≃g G'
fst✝ snd✝ : V
⊢ Prod.map ↑f ↑f (fst✝, snd✝) ∈ edgeSet G' ↔ (fst✝, snd✝) ∈ edgeSet G
Tactic:
simp [f.map_adj_iff]
Proof state after:
no goals
Theorem: Digraph.Iso.card_eq_of_iso
Proof state before:
ι : Sort ?u.420619
𝕜 : Type ?u.420622
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card V = Fintype.card W
Tactic:
rw [← Fintype.ofEquiv_card f.toEquiv]
Proof state after:
ι : Sort ?u.420619
𝕜 : Type ?u.420622
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card W = Fintype.card W
Theorem: Digraph.Iso.card_eq_of_iso
Proof state before:
ι : Sort ?u.420619
𝕜 : Type ?u.420622
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f✝ : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
f : G ≃g G'
⊢ Fintype.card W = Fintype.card W
Tactic:
apply @Fintype.card_congr' _ _ (_) (_) rfl
Proof state after:
no goals
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
V : Type u_1
G G' : Digraph V
⊢ G ≤ G' ↔ ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
constructor
Proof state after:
case mp
V : Type u_1
G G' : Digraph V
⊢ G ≤ G' → ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s

case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G ≤ G'
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
case mp
V : Type u_1
G G' : Digraph V
⊢ G ≤ G' → ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
intro h
Proof state after:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ ∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
use G'.edgeSet \ G.edgeSet
Proof state after:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Tactic:
refine ⟨Set.diff_subset _ _, ?_⟩
Proof state after:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
case mp
V : Type u_1
G G' : Digraph V
h : G ≤ G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Tactic:
ext v w
Proof state after:
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ (deleteEdges G' (edgeSet G' \ edgeSet G)).Adj v w
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ (deleteEdges G' (edgeSet G' \ edgeSet G)).Adj v w
Tactic:
simp only [deleteEdges_adj, Set.mem_diff, mem_edgeSet, not_and, not_not]
Proof state after:
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
case mp.Adj.h.h.a
V : Type u_1
G G' : Digraph V
h : G ≤ G'
v w : V
⊢ G.Adj v w ↔ G'.Adj v w ∧ (G'.Adj v w → G.Adj v w)
Tactic:
constructor <;> simp (config := {contextual := true}) [@h v w]
Proof state after:
no goals
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G ≤ G'
Tactic:
rintro ⟨s, _, rfl⟩
Proof state after:
case mpr.intro.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
left✝ : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'
Theorem: Digraph.le_iff_eq_deleteEdges
Proof state before:
case mpr.intro.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
left✝ : s ⊆ edgeSet G'
⊢ deleteEdges G' s ≤ G'
Tactic:
apply deleteEdges_le
Proof state after:
no goals
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
V : Type u_1
G G' : Digraph V
⊢ G < G' ↔ ∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
constructor
Proof state after:
case mp
V : Type u_1
G G' : Digraph V
⊢ G < G' → ∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s

case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G < G'
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp
V : Type u_1
G G' : Digraph V
⊢ G < G' → ∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
intro h
Proof state after:
case mp
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ ∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ ∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s
Tactic:
use G'.edgeSet \ G.edgeSet
Proof state after:
case mp
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ Set.Nonempty (edgeSet G' \ edgeSet G) ∧
    edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ Set.Nonempty (edgeSet G' \ edgeSet G) ∧
    edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Tactic:
constructor
Proof state after:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ Set.Nonempty (edgeSet G' \ edgeSet G)

case mp.right
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.right
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G' ∧ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Tactic:
constructor
Proof state after:
case mp.right.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ edgeSet G' \ edgeSet G ⊆ edgeSet G'

case mp.right.right
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ G = deleteEdges G' (edgeSet G' \ edgeSet G)
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
⊢ Set.Nonempty (edgeSet G' \ edgeSet G)
Tactic:
by_contra hn
Proof state after:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : ¬Set.Nonempty (edgeSet G' \ edgeSet G)
⊢ False
Theorem: Digraph.lt_iff_eq_deleteEdges
Proof state before:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : ¬Set.Nonempty (edgeSet G' \ edgeSet G)
⊢ False
Tactic:
rw [Set.not_nonempty_iff_eq_empty, Set.diff_eq_empty, edgeSet_subset_edgeSet] at hn
Proof state after:
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : G' ≤ G
⊢ False