awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : v ∈ H.verts
⊢ (G.singletonSubgraph v).verts ⊆ H.verts
have left : {v} ⊆ H.verts
Tactic: rwa [singletonSubgraph_verts, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
⊢ Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph ((f : (a : V) → W) v)
have verts : ∀ (x : W), x ∈ (Subgraph.map f (G.singletonSubgraph v)).verts ↔ x ∈ (G'.singletonSubgraph ((f : (a : V) → W) v)).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
verts :
  ∀ (x : W), x ∈ (Subgraph.map f (G.singletonSubgraph v)).verts ↔ x ∈ (G'.singletonSubgraph ((f : (a : V) → W) v)).verts
⊢ Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph ((f : (a : V) → W) v)
have Adj : ∀ (x x_1 : W),
  (Subgraph.map f (G.singletonSubgraph v)).Adj x x_1 ↔ (G'.singletonSubgraph ((f : (a : V) → W) v)).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x x_1 : W
⊢ (Subgraph.map f (G.singletonSubgraph v)).Adj x x_1 ↔ (G'.singletonSubgraph ((f : (a : V) → W) v)).Adj x x_1
have Adj : ⊥ → ∃ (x_2 : V), (f : (a : V) → W) x_2 = x ∧ ∃ (x : V), (f : (a : V) → W) x = x_1
Tactic: simp only [Relation.Map, Subgraph.map_adj, singletonSubgraph_adj, Pi.bot_apply,
    exists_and_left, and_iff_left_iff_imp, Subgraph.map_verts,
    singletonSubgraph_verts, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H = G.singletonSubgraph v
⊢ H.verts = {v}
have rw : (G.singletonSubgraph v).verts = {v}
Tactic: rw [h, singletonSubgraph_verts]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H = G.singletonSubgraph v
rw : (G.singletonSubgraph v).verts = {v}
⊢ H.verts = {v}
have rw₁ : Eq (α := Set V) {v} {v}
Tactic: rw [h, singletonSubgraph_verts]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
⊢ H = G.singletonSubgraph v ↔ H.verts = {v}
have refine : ∀ (h : H.verts = {v}), H = G.singletonSubgraph v
Tactic: refine ⟨fun h ↦ by rw [h, singletonSubgraph_verts], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
⊢ H = G.singletonSubgraph v
have verts : ∀ (x : V), x ∈ H.verts ↔ x ∈ (G.singletonSubgraph v).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
verts : ∀ (x : V), x ∈ H.verts ↔ x ∈ (G.singletonSubgraph v).verts
⊢ H = G.singletonSubgraph v
have Adj : ∀ (x x_1 : V), H.Adj x x_1 ↔ (G.singletonSubgraph v).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x : V
⊢ x ∈ H.verts ↔ x ∈ (G.singletonSubgraph v).verts
have verts : Membership.mem (γ := Set V) {v} x ↔ x ∈ (G.singletonSubgraph v).verts
Tactic: rw [h, singletonSubgraph_verts]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x : V
verts : Membership.mem (γ := Set V) {v} x ↔ x ∈ (G.singletonSubgraph v).verts
⊢ x ∈ H.verts ↔ x ∈ (G.singletonSubgraph v).verts
have verts₁ : Membership.mem (γ := Set V) {v} x ↔ Membership.mem (γ := Set V) {v} x
Tactic: rw [h, singletonSubgraph_verts]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
⊢ H.Adj x x_1 ↔ (G.singletonSubgraph v).Adj x x_1
have Adj : ¬H.Adj x x_1
Tactic: simp only [Prop.bot_eq_false, singletonSubgraph_adj, Pi.bot_apply, iff_false]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
⊢ False
have ha1 : x ∈ H.verts
Tactic: have ha1 := ha.fst_mem
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x ∈ H.verts
⊢ False
have ha2 : x_1 ∈ H.verts
Tactic: have ha2 := ha.snd_mem
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x ∈ H.verts
ha2 : x_1 ∈ H.verts
⊢ False
have ha1₁ : x = v
Tactic: rw [h, Set.mem_singleton_iff] at ha1 ha2
Cleared hypotheses: ha1, ha2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x ∈ H.verts
ha2 : x_1 ∈ H.verts
ha1₁ : x = v
⊢ False
have ha2₁ : x_1 = v
Tactic: rw [h, Set.mem_singleton_iff] at ha1 ha2
Cleared hypotheses: ha1, ha2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x = v
ha2 : x_1 = v
⊢ False
have ha₁ : H.Adj x_1 x_1
Tactic: subst_vars
Cleared hypotheses: v, h, x, ha, ha1, ha2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x x_1 : V
ha : H.Adj x x_1
ha1 : x = v
ha2 : x_1 = v
ha₁ : H.Adj x_1 x_1
⊢ False
have h₁ : H.verts = {x_1}
Tactic: subst_vars
Cleared hypotheses: v, h, x, ha, ha1, ha2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).edgeSet = {s(v, w)}
have h : ∀ (e : Sym2 V), e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) {s(v, w)} e
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) {s(v, w)} e
have h : ∀ (x y : V), s(x, y) ∈ (G.subgraphOfAdj hvw).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) {s(v, w)} s(x, y)
Tactic: refine e.ind ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
⊢ G.subgraphOfAdj ⋯ ≤ H
have left : (G.subgraphOfAdj sorry).verts ⊆ H.verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
h : H.Adj v w
left : (G.subgraphOfAdj ⋯).verts ⊆ H.verts
⊢ G.subgraphOfAdj ⋯ ≤ H
have right : ∀ ⦃v_1 w_1 : V⦄, (G.subgraphOfAdj sorry).Adj v_1 w_1 → H.Adj v_1 w_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ G.subgraphOfAdj ⋯ = G.subgraphOfAdj hvw
have verts : ∀ (x : V), x ∈ (G.subgraphOfAdj sorry).verts ↔ x ∈ (G.subgraphOfAdj hvw).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
verts : ∀ (x : V), x ∈ (G.subgraphOfAdj ⋯).verts ↔ x ∈ (G.subgraphOfAdj hvw).verts
⊢ G.subgraphOfAdj ⋯ = G.subgraphOfAdj hvw
have Adj : ∀ (x x_1 : V), (G.subgraphOfAdj sorry).Adj x x_1 ↔ (G.subgraphOfAdj hvw).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj ⋯
have verts : ∀ (x : W), x ∈ (Subgraph.map f (G.subgraphOfAdj hvw)).verts ↔ x ∈ (G'.subgraphOfAdj sorry).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
verts : ∀ (x : W), x ∈ (Subgraph.map f (G.subgraphOfAdj hvw)).verts ↔ x ∈ (G'.subgraphOfAdj ⋯).verts
⊢ Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj ⋯
have Adj : ∀ (x x_1 : W), (Subgraph.map f (G.subgraphOfAdj hvw)).Adj x x_1 ↔ (G'.subgraphOfAdj sorry).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w}
have h : ∀ (u : V), u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ Membership.mem (γ := Set V) {w} u
Tactic: ext u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ Membership.mem (γ := Set V) {w} u
have h : w = u ↔ u = w
Tactic: suffices w = u ↔ u = w by simpa [hvw.ne.symm] using this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
⊢ w = u ↔ u = w
have h : u = w ↔ u = w
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet w = {v}
have rw : (G.subgraphOfAdj sorry).neighborSet w = {v}
Tactic: rw [subgraphOfAdj_symm hvw.symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
hvw : G.Adj v w
hv : u ≠ v
hw : u ≠ w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅
have h : ∀ (x : V), x ∈ (G.subgraphOfAdj hvw).neighborSet u ↔ Membership.mem (γ := Set V) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
have pos : u = v → u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
pos : u = v → u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}
⊢ (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
have neg : u = v → ¬u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
pos : u = v → u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}
neg : u = v → ¬u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅
⊢ (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
have pos₁ : ¬u = v → u = w → (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ {v}
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
pos : u = v → u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}
neg : u = v → ¬u = w → (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅
pos₁ : ¬u = v → u = w → (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ {v}
⊢ (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
have neg₁ : ¬u = v → ¬u = w → (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
h : u = v
h_1 : u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}
have pos : ∀ (hvw : G.Adj w w), (G.subgraphOfAdj hvw).neighborSet w = {w} ∪ {w}
Tactic: subst_vars
Cleared hypotheses: u, v, hvw, h, h_1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
h : u = v
h_1 : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅
have neg : ¬v = w → (G.subgraphOfAdj hvw).neighborSet v = {w} ∪ ∅
Tactic: subst_vars
Cleared hypotheses: u, h, h_1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
hvw : G.Adj v w
h : ¬u = v
h_1 : u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ {v}
have pos : ¬w = v → (G.subgraphOfAdj hvw).neighborSet w = ∅ ∪ {v}
Tactic: subst_vars
Cleared hypotheses: u, h, h_1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (G.subgraphOfAdj h).support = {u, v}
have h₁ : ∀ (x : V), x ∈ (G.subgraphOfAdj h).support ↔ Membership.mem (γ := Set V) {u, v} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x : V
⊢ (∃ (w : V), (G.subgraphOfAdj h).Adj x w) ↔ Membership.mem (γ := Set V) {u, v} x
have h₁ : (∃ (w : V), u = x ∧ v = w ∨ u = w ∧ v = x) ↔ Membership.mem (γ := Set V) {u, v} x
Tactic: simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x : V
⊢ (∃ (w : V), u = x ∧ v = w ∨ u = w ∧ v = x) ↔ Membership.mem (γ := Set V) {u, v} x
have h₁ : (∃ (w : V), u = x ∧ v = w ∨ u = w ∧ v = x) → Membership.mem (γ := Set V) {u, v} x
Tactic: refine ⟨?_, fun h ↦ h.elim (fun hl ↦ ⟨v, .inl ⟨hl.symm, rfl⟩⟩) fun hr ↦ ⟨u, .inr ⟨rfl, hr.symm⟩⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
⊢ Subgraph.restrict (Subgraph.coeSubgraph G'') = G''
have verts : ∀ (x : (↑G'.verts : Type u)),
  Membership.mem (γ := Set (↑G'.verts : Type u)) (verts (Subgraph.restrict (Subgraph.coeSubgraph G''))) x ↔
    x ∈ G''.verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
verts :
  ∀ (x : (↑G'.verts : Type u)),
    Membership.mem (γ := Set (↑G'.verts : Type u)) (Subgraph.verts (Subgraph.restrict (Subgraph.coeSubgraph G''))) x ↔
      x ∈ G''.verts
⊢ Subgraph.restrict (Subgraph.coeSubgraph G'') = G''
have Adj : ∀ (x x_1 : (↑G'.verts : Type u)), Adj (Subgraph.restrict (Subgraph.coeSubgraph G'')) x x_1 ↔ G''.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
x x_1 : (↑G'.verts : Type u)
⊢ Adj (Subgraph.restrict (Subgraph.coeSubgraph G'')) x x_1 ↔ G''.Adj x x_1
have Adj : (G'.Adj (↑x : V) (↑x_1 : V) ∧
    ∃ (hv : (↑x : V) ∈ G'.verts) (hw : (↑x_1 : V) ∈ G'.verts),
      G''.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) (↑x : V) hv)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) (↑x_1 : V) hw)) ↔
  G''.Adj x x_1
Tactic: rw [restrict_adj, coeSubgraph_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ Subgraph.coeSubgraph H' ≤ H
have left : (Subgraph.coeSubgraph H').verts ⊆ H.verts
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
left : (Subgraph.coeSubgraph H').verts ⊆ H.verts
⊢ Subgraph.coeSubgraph H' ≤ H
have right : ∀ ⦃v w : V⦄, (Subgraph.coeSubgraph H').Adj v w → H.Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H') = H ⊓ H'
have verts : ∀ (x : V), x ∈ (Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H')).verts ↔ x ∈ (H ⊓ H').verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
verts : ∀ (x : V), x ∈ (Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H')).verts ↔ x ∈ (H ⊓ H').verts
⊢ Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H') = H ⊓ H'
have Adj : ∀ (x x_1 : V), (Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H')).Adj x x_1 ↔ (H ⊓ H').Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x x_1 : V
⊢ (Subgraph.coeSubgraph (G' := H) (Subgraph.restrict H')).Adj x x_1 ↔ (H ⊓ H').Adj x x_1
have Adj : (∃ (_ : x ∈ H.verts) (_ : x_1 ∈ H.verts), H.Adj x x_1 ∧ H'.Adj x x_1) ↔ (H ⊓ H').Adj x x_1
Tactic: simp_rw [coeSubgraph_adj, restrict_adj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x x_1 : V
⊢ (∃ (_ : x ∈ H.verts) (_ : x_1 ∈ H.verts), H.Adj x x_1 ∧ H'.Adj x x_1) ↔ (H ⊓ H').Adj x x_1
have Adj : H.Adj x x_1 → (x_1 ∈ H.verts ∧ x ∈ H.verts ∧ H'.Adj x x_1 ↔ H'.Adj x x_1)
Tactic: simp only [exists_and_left, exists_prop, inf_adj, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
⊢ (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')
have verts : ∀ (x : V), x ∈ ((G'.deleteEdges s).deleteEdges s').verts ↔ x ∈ (G'.deleteEdges (s ∪ s')).verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
verts : ∀ (x : V), x ∈ ((G'.deleteEdges s).deleteEdges s').verts ↔ x ∈ (G'.deleteEdges (s ∪ s')).verts
⊢ (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')
have Adj : ∀ (x x_1 : V), ((G'.deleteEdges s).deleteEdges s').Adj x x_1 ↔ (G'.deleteEdges (s ∪ s')).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.deleteEdges ∅ = G'
have verts : ∀ (x : V), x ∈ (G'.deleteEdges ∅).verts ↔ x ∈ G'.verts
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
verts : ∀ (x : V), x ∈ (G'.deleteEdges ∅).verts ↔ x ∈ G'.verts
⊢ G'.deleteEdges ∅ = G'
have Adj : ∀ (x x_1 : V), (G'.deleteEdges ∅).Adj x x_1 ↔ G'.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe
have Adj : ∀ (x x_1 : V), (G'.spanningCoe.deleteEdges s).Adj x x_1 ↔ (G'.deleteEdges s).spanningCoe.Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
⊢ G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' s)).coe
have Adj : ∀ (v : V) (hv : v ∈ G'.verts) (w : V) (hw : w ∈ G'.verts),
  (G'.coe.deleteEdges s).Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ↔
    (G'.deleteEdges (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' s)).coe.Adj
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw)
Tactic: ext ⟨v, hv⟩ ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
⊢ (G'.coe.deleteEdges s).Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv)
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ↔
    (G'.deleteEdges (Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) '' s)).coe.Adj
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw)
have Adj : G'.Adj v w →
  (s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s ↔
    ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w))
Tactic: simp only [SimpleGraph.deleteEdges_adj, coe_adj, deleteEdges_adj, Set.mem_image, not_exists,
    not_and, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
h : G'.Adj v w
⊢ s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s ↔
    ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)
have Adj : s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s →
  ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
h : G'.Adj v w
Adj :
  s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s →
    ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)
⊢ s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s ↔
    ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)
have Adj₁ : (∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)) →
  s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
h : G'.Adj v w
hs : s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s
⊢ ∀ x ∈ s, ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) x = s(v, w)
have Adj : ∀ (x y : (↑G'.verts : Type u)),
  s(x, y) ∈ s → ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts)) s(x, y) = s(v, w)
Tactic: refine Sym2.ind ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Subgraph (goal)
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 (↑G'.verts : Type u))
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
h : G'.Adj v w
hs : s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v hv, Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w hw) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v' hv', Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w' hw') ∈ s →
    ¬Sym2.map (Subtype.val (p := fun (x : V) ↦ x ∈ G'.verts))
          s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v' hv', Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w' hw') =
        s(v, w)
have Adj : s(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v' hv', Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) w' hw') ∈ s →
  ¬Sym2.Rel V (v', w') (v, w)
Tactic: simp only [Sym2.map_mk, Sym2.eq]