awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj ⊔ y.Adj) v w
rwa : (x.Adj w ⊔ y.Adj w) v
⊢ (x.Adj ⊔ y.Adj) w v
have rwa₁ : max (x.Adj w v) (y.Adj w v)
Tactic: rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj ⊔ y.Adj) v w
rwa : (x.Adj w ⊔ y.Adj w) v
rwa₁ : max (x.Adj w v) (y.Adj w v)
⊢ (x.Adj ⊔ y.Adj) w v
have rwa₂ : max (x.Adj v w) (y.Adj w v)
Tactic: rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj ⊔ y.Adj) v w
rwa : (x.Adj w ⊔ y.Adj w) v
rwa₁ : max (x.Adj w v) (y.Adj w v)
rwa₂ : max (x.Adj v w) (y.Adj w v)
⊢ (x.Adj ⊔ y.Adj) w v
have rwa₃ : max (x.Adj v w) (y.Adj v w)
Tactic: rwa [Pi.sup_apply, Pi.sup_apply, x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj ⊓ y.Adj) v w
⊢ (x.Adj ⊓ y.Adj) w v
have rwa : (x.Adj w ⊓ y.Adj w) v
Tactic: rwa [Pi.inf_apply, Pi.inf_apply, x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj ⊓ y.Adj) v w
rwa : (x.Adj w ⊓ y.Adj w) v
⊢ (x.Adj ⊓ y.Adj) w v
have rwa₁ : min (x.Adj w v) (y.Adj w v)
Tactic: rwa [Pi.inf_apply, Pi.inf_apply, x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj ⊓ y.Adj) v w
rwa : (x.Adj w ⊓ y.Adj w) v
rwa₁ : min (x.Adj w v) (y.Adj w v)
⊢ (x.Adj ⊓ y.Adj) w v
have rwa₂ : min (x.Adj v w) (y.Adj w v)
Tactic: rwa [Pi.inf_apply, Pi.inf_apply, x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj ⊓ y.Adj) v w
rwa : (x.Adj w ⊓ y.Adj w) v
rwa₁ : min (x.Adj w v) (y.Adj w v)
rwa₂ : min (x.Adj v w) (y.Adj w v)
⊢ (x.Adj ⊓ y.Adj) w v
have rwa₃ : min (x.Adj v w) (y.Adj v w)
Tactic: rwa [Pi.inf_apply, Pi.inf_apply, x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj \ y.Adj) v w
⊢ x.Adj w v ∧ ¬y.Adj w v
have rwa : x.Adj v w ∧ ¬y.Adj w v
Tactic: rwa [x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
h : (x.Adj \ y.Adj) v w
rwa : x.Adj v w ∧ ¬y.Adj w v
⊢ x.Adj w v ∧ ¬y.Adj w v
have rwa₁ : x.Adj v w ∧ ¬y.Adj v w
Tactic: rwa [x.adj_comm, y.adj_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
a b : V
s : Set (SimpleGraph V)
hs : s.Nonempty
⊢ (∀ G ∈ s, G.Adj a b) → a ≠ b
have obtain : ∀ (G : SimpleGraph V) (hG : G ∈ s), (∀ G ∈ s, G.Adj a b) → a ≠ b
Tactic: obtain ⟨G, hG⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
a b : V
inst : Nonempty ι
f : ι → SimpleGraph V
⊢ Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), (f i).Adj a b
have rw : Adj (sInf (Set.range fun (i : ι) ↦ f i)) a b ↔ ∀ (i : ι), (f i).Adj a b
Tactic: rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _), Set.forall_mem_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
a b : V
inst : Nonempty ι
f : ι → SimpleGraph V
rw : Adj (sInf (Set.range fun (i : ι) ↦ f i)) a b ↔ ∀ (i : ι), (f i).Adj a b
⊢ Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), (f i).Adj a b
have rw₁ : (∀ (G : SimpleGraph V), Membership.mem (γ := Set (SimpleGraph V)) (Set.range fun (i : ι) ↦ f i) G → G.Adj a b) ↔
  ∀ (i : ι), (f i).Adj a b
Tactic: rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _), Set.forall_mem_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
a b : V
inst : Nonempty ι
f : ι → SimpleGraph V
rw : Adj (sInf (Set.range fun (i : ι) ↦ f i)) a b ↔ ∀ (i : ι), (f i).Adj a b
rw₁ :
  (∀ (G : SimpleGraph V), Membership.mem (γ := Set (SimpleGraph V)) (Set.range fun (i : ι) ↦ f i) G → G.Adj a b) ↔
    ∀ (i : ι), (f i).Adj a b
⊢ Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), (f i).Adj a b
have rw₂ : (∀ (i : ι), (f i).Adj a b) ↔ ∀ (i : ι), (f i).Adj a b
Tactic: rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _), Set.forall_mem_range]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
G : SimpleGraph V
v w : V
hvw : Adj { Adj := Ne, symm := ⋯, loopless := ⋯ } v w
⊢ (G ⊔ Gᶜ).Adj v w
have pos : ∀ (h : G.Adj v w), (G ⊔ Gᶜ).Adj v w
Tactic: by_cases h : G.Adj v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
G : SimpleGraph V
v w : V
hvw : Adj { Adj := Ne, symm := ⋯, loopless := ⋯ } v w
pos : ∀ (h : G.Adj v w), (G ⊔ Gᶜ).Adj v w
⊢ (G ⊔ Gᶜ).Adj v w
have neg : ∀ (h : ¬G.Adj v w), (G ⊔ Gᶜ).Adj v w
Tactic: by_cases h : G.Adj v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
x y : SimpleGraph V
⊢ x \ y = x ⊓ yᶜ
have Adj : ∀ (v w : V), (x \ y).Adj v w ↔ (x ⊓ yᶜ).Adj v w
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v_1 w_1 : V
e : Sym2 V
x y : SimpleGraph V
v w : V
⊢ (x \ y).Adj v w ↔ (x ⊓ yᶜ).Adj v w
have Adj : ∀ (h : (x \ y).Adj v w), v ≠ w
Tactic: refine ⟨fun h => ⟨h.1, ⟨?_, h.2⟩⟩, fun h => ⟨h.1, h.2.2⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
ι_1 : Type u
κ : ι_1 → Type u
f : (a : ι_1) → κ a → SimpleGraph V
⊢ Eq.{u + 1} (α := SimpleGraph V) (⨅ (a : ι_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a))
have Adj : ∀ (x x_1 : V), Adj (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔ Adj (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a b c u v w : V
e : Sym2 V
inst : Subsingleton V
G : SimpleGraph V
⊢ G = ⊥
have Adj : ∀ (a b : V), G.Adj a b ↔ Adj ⊥ a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
ι : Sort u_1
V : Type u
G_1 : SimpleGraph V
a_1 b_1 c u v w : V
e : Sym2 V
inst : Subsingleton V
G : SimpleGraph V
a b : V
⊢ G.Adj a b ↔ Adj ⊥ a b
have this : a = b
Tactic: have := Subsingleton.elim a b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ ⊔ G₂).edgeSet = G₁.edgeSet ∪ G₂.edgeSet
have h : ∀ (x : Sym2 V) (x y : V),
  Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊔ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∪ G₂.edgeSet
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet
have h : ∀ (x : Sym2 V) (x y : V),
  Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊓ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∩ G₂.edgeSet
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet
have h : ∀ (x : Sym2 V) (x y : V),
  Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ \ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet \ G₂.edgeSet
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
have rw : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ Disjoint G₁ G₂
Tactic: rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
    OrderEmbedding.le_iff_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
rw : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ Disjoint G₁ G₂
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
have rw₁ : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
Tactic: rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
    OrderEmbedding.le_iff_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
rw : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ Disjoint G₁ G₂
rw₁ : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
have rw₂ : (G₁ ⊓ G₂).edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
Tactic: rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
    OrderEmbedding.le_iff_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
rw : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ Disjoint G₁ G₂
rw₁ : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₂ : (G₁ ⊓ G₂).edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
have rw₃ : (G₁ ⊓ G₂).edgeSet ⊆ edgeSet ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
Tactic: rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
    OrderEmbedding.le_iff_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
rw : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ Disjoint G₁ G₂
rw₁ : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₂ : (G₁ ⊓ G₂).edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₃ : (G₁ ⊓ G₂).edgeSet ⊆ edgeSet ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
have rw₄ : (G₁ ⊓ G₂).edgeSet ≤ edgeSet ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
Tactic: rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
    OrderEmbedding.le_iff_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G₁ G₂ : SimpleGraph V
rw : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ Disjoint G₁ G₂
rw₁ : G₁.edgeSet ∩ G₂.edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₂ : (G₁ ⊓ G₂).edgeSet ⊆ ∅ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₃ : (G₁ ⊓ G₂).edgeSet ⊆ edgeSet ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
rw₄ : (G₁ ⊓ G₂).edgeSet ≤ edgeSet ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
have rw₅ : G₁ ⊓ G₂ ≤ ⊥ ↔ G₁ ⊓ G₂ ≤ ⊥
Tactic: rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
    OrderEmbedding.le_iff_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ G.edgeSet = ∅ ↔ G = ⊥
have rw : G.edgeSet = edgeSet ⊥ ↔ G = ⊥
Tactic: rw [← edgeSet_bot, edgeSet_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
rw : G.edgeSet = edgeSet ⊥ ↔ G = ⊥
⊢ G.edgeSet = ∅ ↔ G = ⊥
have rw₁ : G = ⊥ ↔ G = ⊥
Tactic: rw [← edgeSet_bot, edgeSet_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ G.edgeSet.Nonempty ↔ G ≠ ⊥
have rw : G.edgeSet ≠ ∅ ↔ G ≠ ⊥
Tactic: rw [Set.nonempty_iff_ne_empty, edgeSet_eq_empty.ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
rw : G.edgeSet ≠ ∅ ↔ G ≠ ⊥
⊢ G.edgeSet.Nonempty ↔ G ≠ ⊥
have rw₁ : G ≠ ⊥ ↔ G ≠ ⊥
Tactic: rw [Set.nonempty_iff_ne_empty, edgeSet_eq_empty.ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e
have refine : (v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e) → G.Adj v w
Tactic: refine ⟨fun _ => ⟨G.ne_of_adj ‹_›, s(v, w), by simpa⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e ∧ w ∈ e
⊢ G.Adj v w
have hv₁ : e = s(v, w)
Tactic: rw [Sym2.mem_and_mem_iff hne] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ G.edgeSet
hv : e = s(v, w)
⊢ G.Adj v w
have he₁ : s(v, w) ∈ G.edgeSet
Tactic: subst e
Cleared hypotheses: e, he, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
hne : v ≠ w
he : s(v, w) ∈ G.edgeSet
⊢ G.Adj v w
have rwa : ∀ (he : G.Adj v w), G.Adj v w
Tactic: rwa [mem_edgeSet] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
⊢ G.edgeSet ⊆ s.sym2 ↔ G.support ⊆ s
have refine_1 : ∀ (h : G.edgeSet ⊆ s.sym2) (u : V) (hu : u ∈ G.support), u ∈ s
Tactic: refine ⟨fun h u hu ↦ ?_, fun h e hadj ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
refine_1 : ∀ (h : G.edgeSet ⊆ s.sym2) (u : V) (hu : u ∈ G.support), u ∈ s
⊢ G.edgeSet ⊆ s.sym2 ↔ G.support ⊆ s
have refine_2 : ∀ (h : G.support ⊆ s) (e : Sym2 V) (hadj : e ∈ G.edgeSet), e ∈ s.sym2
Tactic: refine ⟨fun h u hu ↦ ?_, fun h e hadj ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h : G.edgeSet ⊆ s.sym2
u : V
hu : u ∈ G.support
⊢ u ∈ s
have refine_1 : ∀ (v : V)
  (huv :
    Membership.mem (γ := SetRel V V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (u, v) => G.Adj u v}
      (u, v)),
  u ∈ s
Tactic: have ⟨v, huv⟩ := hu
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
e : Sym2 V
hadj : e ∈ G.edgeSet
⊢ e ∈ s.sym2
have refine_2 : ∀ (x y : V) (hadj : s(x, y) ∈ G.edgeSet), s(x, y) ∈ s.sym2
Tactic: cases e
Cleared hypotheses: e, hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
e : Sym2 V
he : e ∈ G.edgeSet
v : V
h : v ∈ e
⊢ Sym2.Mem.other h ≠ v
have he₁ : s(Sym2.Mem.other h, v) ∈ G.edgeSet
Tactic: rw [← Sym2.other_spec h, Sym2.eq_swap] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
⊢ Fintype (↑(edgeSet ⊥) : Type u)
have rw : Fintype (↑∅ : Type u)
Tactic: rw [edgeSet_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
⊢ Fintype (↑(G₁ ⊔ G₂).edgeSet : Type u)
have rw : Fintype (↑(G₁.edgeSet ∪ G₂.edgeSet) : Type u)
Tactic: rw [edgeSet_sup]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
⊢ Fintype (↑(G₁ ⊓ G₂).edgeSet : Type u)
have rw : Fintype (↑(G₁.edgeSet ∩ G₂.edgeSet) : Type u)
Tactic: rw [edgeSet_inf]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G₁.edgeSet : Type u)
inst_2 : Fintype (↑G₂.edgeSet : Type u)
⊢ Fintype (↑(G₁ \ G₂).edgeSet : Type u)
have rw : Fintype (↑(G₁.edgeSet \ G₂.edgeSet) : Type u)
Tactic: rw [edgeSet_sdiff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s : Set (Sym2 V)
⊢ (fromEdgeSet s).edgeSet = s \ Sym2.diagSet
have h : ∀ (e : Sym2 V), e ∈ (fromEdgeSet s).edgeSet ↔ e ∈ s \ Sym2.diagSet
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
⊢ fromEdgeSet G.edgeSet = G
have Adj : ∀ (v w : V), (fromEdgeSet G.edgeSet).Adj v w ↔ G.Adj v w
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G ≤ fromEdgeSet s ↔ G.edgeSet ⊆ s
have simp : (∀ x ∈ G.edgeSet, x ∈ s ∧ ¬x.IsDiag) ↔ ∀ x ∈ G.edgeSet, x ∈ s
Tactic: simp [← edgeSet_subset_edgeSet, Set.subset_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
⊢ Eq.{u + 1} (α := SimpleGraph V) (fromEdgeSet ∅) ⊥
have Adj : ∀ (v w : V), Adj (fromEdgeSet ∅) v w ↔ Adj ⊥ v w
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
⊢ Eq.{u + 1} (α := SimpleGraph V) (fromEdgeSet Sym2.diagSetᶜ) ⊤
have Adj : ∀ (x x_1 : V), Adj (fromEdgeSet Sym2.diagSetᶜ) x x_1 ↔ Adj ⊤ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
⊢ Eq.{u + 1} (α := SimpleGraph V) (fromEdgeSet Set.univ) ⊤
have Adj : ∀ (v w : V), Adj (fromEdgeSet Set.univ) v w ↔ Adj ⊤ v w
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
⊢ fromEdgeSet (s ∩ t) = fromEdgeSet s ⊓ fromEdgeSet t
have Adj : ∀ (v w : V), (fromEdgeSet (s ∩ t)).Adj v w ↔ (fromEdgeSet s ⊓ fromEdgeSet t).Adj v w
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj₂ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₂ Adj₃ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj₄ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₂ Adj₃ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₄ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ s
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj₅ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₂ Adj₃ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₄ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ s
Adj₅ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj₆ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ t
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₂ Adj₃ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₄ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ s
Adj₅ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
Adj₆ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ t
Adj₇ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj₈ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₂ Adj₃ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₄ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ s
Adj₅ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
Adj₆ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ t
Adj₇ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
Adj₈ Adj₉ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj₁₀ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → s(v, w) ∈ s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₁ : (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₂ Adj₃ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
Adj₄ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ s
Adj₅ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
Adj₆ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → s(v, w) ∈ t
Adj₇ : ¬v = w → s(v, w) ∈ s → s(v, w) ∈ t → ¬v = w
Adj₈ Adj₉ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w
Adj₁₀ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → s(v, w) ∈ s
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w
have Adj₁₁ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → s(v, w) ∈ t
Tactic: tauto