awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
Adj₁₁ : s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t → ¬v = w → s(v, w) ∈ t
⊢ (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 → ¬v = w
Tactic: tauto
-- 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)
⊢ 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
⊢ (fromEdgeSet (s \ t)).Adj v w ↔ (fromEdgeSet s \ fromEdgeSet t).Adj v w
have Adj : (fromEdgeSet (s \ t)).Adj v w → (fromEdgeSet s \ fromEdgeSet t).Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
v w : V
Adj : (fromEdgeSet (s \ t)).Adj v w → (fromEdgeSet s \ fromEdgeSet t).Adj v w
⊢ (fromEdgeSet (s \ t)).Adj v w ↔ (fromEdgeSet s \ fromEdgeSet t).Adj v w
have Adj₁ : (fromEdgeSet s \ fromEdgeSet t).Adj v w → (fromEdgeSet (s \ t)).Adj v w
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
⊢ fromEdgeSet s ≤ fromEdgeSet t
have simp : s \ Sym2.diagSet ⊆ t
Tactic: simp only [le_fromEdgeSet_iff, edgeSet_fromEdgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
s t : Set (Sym2 V)
h : s ⊆ t
⊢ s \ Sym2.diagSet ⊆ t
have grw : t \ Sym2.diagSet ⊆ t
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
| Disjoint G.edgeSet s
have rw : Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
Tactic: rw [← Set.diff_union_inter s Sym2.diagSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s
have conv_rhs : Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
Tactic: conv_rhs => rw [← Set.diff_union_inter s Sym2.diagSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
have rw : Disjoint G.edgeSet (s \ Sym2.diagSet) ↔ Disjoint G.edgeSet (s \ Sym2.diagSet ∪ s ∩ Sym2.diagSet)
Tactic: rw [← disjoint_edgeSet, edgeSet_fromEdgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet
have rw : Disjoint G (fromEdgeSet s) ↔ Disjoint s G.edgeSet
Tactic: rw [disjoint_comm, disjoint_fromEdgeSet, disjoint_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
rw : Disjoint G (fromEdgeSet s) ↔ Disjoint s G.edgeSet
⊢ Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet
have rw₁ : Disjoint G.edgeSet s ↔ Disjoint s G.edgeSet
Tactic: rw [disjoint_comm, disjoint_fromEdgeSet, disjoint_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
rw : Disjoint G (fromEdgeSet s) ↔ Disjoint s G.edgeSet
rw₁ : Disjoint G.edgeSet s ↔ Disjoint s G.edgeSet
⊢ Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet
have rw₂ : Disjoint s G.edgeSet ↔ Disjoint s G.edgeSet
Tactic: rw [disjoint_comm, disjoint_fromEdgeSet, disjoint_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 w : V
e : Sym2 V
s : Set (Sym2 V)
inst : DecidableEq V
inst_1 : Fintype (↑s : Type u)
⊢ Fintype (↑(fromEdgeSet s).edgeSet : Type u)
have rw : Fintype (↑(s \ Sym2.diagSet) : Type u)
Tactic: rw [edgeSet_fromEdgeSet s]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)}
have refine : {s(a, b)} ⊆ G.incidenceSet a ∩ G.incidenceSet b
Tactic: refine (G.incidenceSet_inter_incidenceSet_subset <| h.ne).antisymm ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
e : Sym2 V
h : a ≠ b
ha : e ∈ G.incidenceSet a
hb : e ∈ G.incidenceSet b
⊢ G.Adj a b
have rwa : s(a, b) ∈ G.incidenceSet a
Tactic: rwa [← mk'_mem_incidenceSet_left_iff, ←
    Set.mem_singleton_iff.1 <| G.incidenceSet_inter_incidenceSet_subset h ⟨ha, hb⟩]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ G.incidenceSet a ∩ G.incidenceSet b = ∅
have simp_rw : ∀ x ∈ G.incidenceSet a, x ∉ G.incidenceSet b
Tactic: simp_rw [Set.eq_empty_iff_forall_notMem, Set.mem_inter_iff, not_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
⊢ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}
have h₁ : ∀ (e' : Sym2 V), e' ∈ G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) ↔ Membership.mem (γ := Set (Sym2 V)) {e} e'
Tactic: ext e'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e' ↔ e' = e
have h₁ : ∀ (h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'), e' = e
Tactic: refine ⟨fun h' => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h₁ : ∀ (h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'), e' = e
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e' ↔ e' = e
have h₂ : e' = e → (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
Tactic: refine ⟨fun h' => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = e
have h₁ : e' = s(v, Sym2.Mem.other h)
Tactic: rw [← Sym2.other_spec h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Disjoint (G.neighborSet v) (Gᶜ.neighborSet v)
have rw : G.neighborSet v ∩ Gᶜ.neighborSet v ⊆ ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : w ∈ Gᶜ.neighborSet v
⊢ Membership.mem (γ := Set V) ∅ w
have h'₁ : v ≠ w ∧ ¬G.Adj v w
Tactic: rw [mem_neighborSet, compl_adj] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ
have h : ∀ (w : V), w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ Membership.mem (γ := Set V) {v}ᶜ w
Tactic: ext w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
v w : V
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ Membership.mem (γ := Set V) {v}ᶜ w
have h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
Tactic: have h := @ne_of_adj _ G
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
⊢ w ∈ G.neighborSet v ∪ Gᶜ.neighborSet v ↔ Membership.mem (γ := Set V) {v}ᶜ w
have h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
Tactic: simp_rw [Set.mem_union, mem_neighborSet, compl_adj, Set.mem_compl_iff, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
have h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w → ¬w = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w → ¬w = v
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
have h₂ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w → ¬w = v
h₂ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
have h₃ : G.Adj v w → ¬w = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w → ¬w = v
h₂ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
h₃ : G.Adj v w → ¬w = v
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
have h₄ : v ≠ w → ¬G.Adj v w → ¬w = v
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w → ¬w = v
h₂ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
h₃ : G.Adj v w → ¬w = v
h₄ : v ≠ w → ¬G.Adj v w → ¬w = v
h₅ : G.Adj v w → ¬w = v
h₆ : v ≠ w → ¬G.Adj v w → ¬w = v
h₇ : G.Adj v w → w = v → False
h₈ : v ≠ w → ¬G.Adj v w → w = v → False
h₉ h₁₀ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
have h₁₁ : ¬w = v → ¬G.Adj v w → v ≠ w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ {a b : V} (h : G.Adj a b), a ≠ b
h₁ : G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w → ¬w = v
h₂ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
h₃ : G.Adj v w → ¬w = v
h₄ : v ≠ w → ¬G.Adj v w → ¬w = v
h₅ : G.Adj v w → ¬w = v
h₆ : v ≠ w → ¬G.Adj v w → ¬w = v
h₇ : G.Adj v w → w = v → False
h₈ : v ≠ w → ¬G.Adj v w → w = v → False
h₉ h₁₀ : ¬w = v → G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w
h₁₁ : ¬w = v → ¬G.Adj v w → v ≠ w
⊢ G.Adj v w ∨ v ≠ w ∧ ¬G.Adj v w ↔ ¬w = v
have h₁₂ : ¬w = v → ¬G.Adj v w → ¬G.Adj v w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
have simp_rw : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
Tactic: simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
simp_rw : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
have simp_rw₁ : card (α := V) (Set.toFinset {v})ᶜ = Fintype.card V - 1
Tactic: simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
simp_rw : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
simp_rw₁ : card (α := V) (Set.toFinset {v})ᶜ = Fintype.card V - 1
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
have simp_rw₂ : Fintype.card V - card (α := V) (Set.toFinset {v}) = Fintype.card V - 1
Tactic: simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
simp_rw : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
simp_rw₁ : card (α := V) (Set.toFinset {v})ᶜ = Fintype.card V - 1
simp_rw₂ : Fintype.card V - card (α := V) (Set.toFinset {v}) = Fintype.card V - 1
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
have simp_rw₃ : Fintype.card V - Fintype.card.{u} (↑{v} : Type u) = Fintype.card V - 1
Tactic: simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
have classical : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
Tactic: classical simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
classical : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
have classical₁ : card (α := V) (Set.toFinset {v})ᶜ = Fintype.card V - 1
Tactic: classical simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
classical : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
classical₁ : card (α := V) (Set.toFinset {v})ᶜ = Fintype.card V - 1
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
have classical₂ : Fintype.card V - card (α := V) (Set.toFinset {v}) = Fintype.card V - 1
Tactic: classical simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
inst : Fintype V
G : SimpleGraph V
v : V
inst_1 : Fintype (↑(G.neighborSet v ∪ Gᶜ.neighborSet v) : Type u)
classical : card (α := V) (Set.toFinset {v}ᶜ) = Fintype.card V - 1
classical₁ : card (α := V) (Set.toFinset {v})ᶜ = Fintype.card V - 1
classical₂ : Fintype.card V - card (α := V) (Set.toFinset {v}) = Fintype.card V - 1
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1
have classical₃ : Fintype.card V - Fintype.card.{u} (↑{v} : Type u) = Fintype.card V - 1
Tactic: classical simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
      Finset.card_compl, Set.toFinset_card, Set.card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ {v}
have h : ∀ (w : V), w ∈ Gᶜ.neighborSet v ↔ w ∈ (G.neighborSet v)ᶜ \ {v}
Tactic: ext w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
v w : V
⊢ commonNeighbors ⊤ v w = Set.univ \ {v, w}
have h : ∀ (u : V), u ∈ commonNeighbors ⊤ v w ↔ Membership.mem (γ := Set V) (Set.univ \ {v, w}) u
Tactic: ext u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ e ∈ G.incidenceSet (G.otherVertexOfIncident h)
have right : G.otherVertexOfIncident h ∈ e
Tactic: use h.1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ G.otherVertexOfIncident h ∈ G.neighborSet v
have he : e ∈ G.edgeSet
Tactic: obtain ⟨he, hv⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
he : e ∈ G.edgeSet
⊢ G.otherVertexOfIncident h ∈ G.neighborSet v
have hv : v ∈ e
Tactic: obtain ⟨he, hv⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v
have rwa : ∀ (he_1 : s(v, Sym2.Mem.other' hv) ∈ G.edgeSet), G.otherVertexOfIncident sorry ∈ G.neighborSet v
Tactic: rwa [← Sym2.other_spec' hv, mem_edgeSet] at he
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e
rwa : ∀ (he_1 : s(v, Sym2.Mem.other' hv) ∈ G.edgeSet), G.otherVertexOfIncident ⋯ ∈ G.neighborSet v
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v
have rwa₁ : ∀ (he_1 : G.Adj v (Sym2.Mem.other' hv)), G.otherVertexOfIncident sorry ∈ G.neighborSet v
Tactic: rwa [← Sym2.other_spec' hv, mem_edgeSet] at 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_1 w_1 : V
e : Sym2 V
inst : DecidableEq V
v : V
x : (↑(G.neighborSet v) : Type u)
w : V
hw : w ∈ G.neighborSet v
⊢ (fun (e : (↑(G.incidenceSet v) : Type u)) ↦
        Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) (G.otherVertexOfIncident ⋯) ⋯)
      ((fun (w : (↑(G.neighborSet v) : Type u)) ↦
          Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.incidenceSet v) s(v, (↑w : V)) ⋯)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w hw)) =
    Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w hw
have simp : G.otherVertexOfIncident (v := v) (e := s(v, w)) sorry = w
Tactic: simp only [Subtype.mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
⊢ Subsingleton.{u + 1} (SimpleGraph V) ↔ Subsingleton V
have refine : ∀ (h : Subsingleton.{u + 1} (SimpleGraph V)), Subsingleton V
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ Unique.instSubsingleton⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
h : Subsingleton.{u + 1} (SimpleGraph V)
⊢ Subsingleton V
have contrapose! : ∀ (h : Nontrivial V), Nontrivial.{u} (SimpleGraph V)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
⊢ Nontrivial.{u} (SimpleGraph V) ↔ Nontrivial V
have refine : ∀ (h : Nontrivial.{u} (SimpleGraph V)), Nontrivial V
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ instNontrivial⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Basic (goal)
Goal:
V : Type u
h : Nontrivial.{u} (SimpleGraph V)
⊢ Nontrivial V
have contrapose! : ∀ (h : Subsingleton V), Subsingleton.{u + 1} (SimpleGraph V)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hadj : G.Adj v w
⊢ v ∈ t ∧ w ∈ s ∨ v ∈ s ∧ w ∈ t
have rw : w ∈ s ∧ v ∈ t ∨ w ∈ t ∧ v ∈ s
Tactic: rw [@and_comm (v ∈ t) (w ∈ s), @and_comm (v ∈ s) (w ∈ t)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
hadj : G.Adj v w
⊢ w ∈ t
have hadj₁ : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
Tactic: apply h.mem_of_adj at hadj
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
hadj : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
⊢ w ∈ t
have nhv : v ∉ t
Tactic: have nhv : v ∉ t := Set.disjoint_left.mp h.disjoint hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ G.neighborSet v = {w : V | w ∈ t ∧ G.Adj v w}
have h₁ : ∀ (w : V), w ∈ G.neighborSet v ↔ Membership.mem (γ := Set V) {w : V | w ∈ t ∧ G.Adj v w} w
Tactic: ext w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
w : V
⊢ w ∈ G.neighborSet v ↔ Membership.mem (γ := Set V) {w : V | w ∈ t ∧ G.Adj v w} w
have h₁ : G.Adj v w → w ∈ t
Tactic: rw [mem_neighborSet, Set.mem_setOf_eq, iff_and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
⊢ G.neighborSet v ⊆ t
have rw : {w : V | w ∈ t ∧ G.Adj v w} ⊆ t
Tactic: rw [isBipartiteWith_neighborSet h hv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
hadj : G.Adj v w
⊢ v ∈ s
have hadj₁ : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
Tactic: apply h.mem_of_adj at hadj
Cleared hypotheses: hadj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (hypothesis)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
hadj : v ∈ s ∧ w ∈ t ∨ v ∈ t ∧ w ∈ s
⊢ v ∈ s
have nhw : w ∉ s
Tactic: have nhw : w ∉ s := Set.disjoint_right.mp h.disjoint hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ G.neighborSet w = {v : V | v ∈ s ∧ G.Adj v w}
have h₁ : ∀ (v : V), v ∈ G.neighborSet w ↔ Membership.mem (γ := Set V) {v : V | v ∈ s ∧ G.Adj v w} v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
v : V
⊢ v ∈ G.neighborSet w ↔ Membership.mem (γ := Set V) {v : V | v ∈ s ∧ G.Adj v w} v
have h₁ : G.Adj v w → v ∈ s
Tactic: rw [mem_neighborSet, adj_comm, Set.mem_setOf_eq, iff_and_self]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ G.neighborSet w ⊆ s
have rw : {v : V | v ∈ s ∧ G.Adj v w} ⊆ s
Tactic: rw [isBipartiteWith_neighborSet' h hw]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v : V
⊢ v ∈ G.support → v ∈ s ∪ t
have this : ∀ (w : V)
  (hadj :
    Membership.mem (γ := SetRel V V)
      {x : V × V |
        match (motive := V × V → Prop) x with
        | (u, v) => G.Adj u v}
      (v, w)),
  v ∈ s ∪ t
Tactic: ⟨w, hadj⟩