awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
have have₁ have₂ :
  ∀
    (h :
      Eq (α := ZMod 2) ((fun (n : ℕ) ↦ ((↑n : ZMod 2) : ZMod 2)) (∑ v : V, G.degree v))
        ((fun (n : ℕ) ↦ ((↑n : ZMod 2) : ZMod 2)) (2 * #G.edgeFinset))),
    Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have₃ :
  ∀ (h : Eq (α := ZMod 2) (↑(∑ v : V, G.degree v) : ZMod 2) 0), Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have₄ :
  ∀ (h : Eq (α := ZMod 2) (∑ x : V with Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0, (↑(G.degree x) : ZMod 2)) 0),
    Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have₅ :
  ∀ (h : Eq (α := ZMod 2) (∑ _v : V with Ne (α := ZMod 2) (↑(G.degree _v) : ZMod 2) 0, 1) 0),
    Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have₆ have₇ :
  ∀ (h : Eq (α := ZMod 2) (∑ x : V with Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0, (↑(G.degree x) : ZMod 2)) 0)
    (x : V),
    Membership.mem (γ := Finset V) {x : V | Ne (α := ZMod 2) (↑(G.degree x) : ZMod 2) 0} x →
      Eq (α := ZMod 2) (↑(G.degree x) : ZMod 2) 1
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})

Tactic:
classical
    have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
    simp only [ZMod.natCast_self, zero_mul, Nat.cast_mul] at h
    rw [Nat.cast_sum, ← sum_filter_ne_zero] at h
    rw [sum_congr (g := fun _v ↦ (1 : ZMod 2)) rfl] at h
    · simp only [mul_one, nsmul_eq_mul, sum_const, Ne] at h
      rw [← ZMod.natCast_eq_zero_iff_even]
      convert! h
      exact ZMod.natCast_ne_zero_iff_odd.symm
    · intro v
      rw [mem_filter_univ, Ne, ZMod.natCast_eq_zero_iff_even, ZMod.natCast_eq_one_iff_odd,
        ← Nat.not_even_iff_odd]
      tauto

Premises used: ZMod.natCast_eq_one_iff_odd, ZMod.natCast_self, ZMod.natCast_ne_zero_iff_odd, MulZeroClass.zero_mul, Finset.mem_filter_univ, Nat.not_even_iff_odd, Ne, Finset.sum_filter_ne_zero, Nat.cast_sum, Nat.cast_mul, ZMod.natCast_eq_zero_iff_even, nsmul_eq_mul, mul_one, Finset.sum_congr, Iff.symm, rfl, Finset.sum_const
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
rcases :
  ∀ (k : ℕ) (hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k),
    Odd (card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)})
⊢ Odd (card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)})

Tactic:
rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩

Premises used: SimpleGraph.even_card_odd_degree_vertices
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
h₁ : Membership.mem (γ := Finset V) {v : V | Odd (G.degree v)} v
⊢ Finset.Nonempty.{u} (α := V) {v : V | Odd (G.degree v)}

Tactic:
use v
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
h₁ : Odd (G.degree v)
⊢ Membership.mem (γ := Finset V) {v : V | Odd (G.degree v)} v

Tactic:
rw [mem_filter_univ]

Premises used: Finset.mem_filter_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
⊢ Odd (G.degree v)

Tactic:
h
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
⊢ Odd (G.degree v)

Tactic:
exact h
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
⊢ Finset.Nonempty.{u} (α := V) {v : V | Odd (G.degree v)}

Tactic:
have hh : Finset.Nonempty {v : V | Odd (G.degree v)} := by
      use v
      rw [mem_filter_univ]
      exact h
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hh : Finset.Nonempty.{u} (α := V) {v : V | Odd (G.degree v)}
rwa : ∀ (hh : 0 < 2 * k), LT.lt (α := ℕ) 0 2
⊢ 0 < k

Tactic:
rwa [← card_pos, hg, ← two_mul, mul_pos_iff_of_pos_left] at hh

Premises used: two_mul, mul_pos_iff_of_pos_left, Finset.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hh : 0 < 2 * k
⊢ LT.lt (α := ℕ) 0 2

Tactic:
zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hh : 0 < 2 * k
⊢ LT.lt (α := ℕ) 0 2

Tactic:
exact zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
⊢ 0 < k

Tactic:
have hk : 0 < k := by
    have hh : Finset.Nonempty {v : V | Odd (G.degree v)} := by
      use v
      rw [mem_filter_univ]
      exact h
    rwa [← card_pos, hg, ← two_mul, mul_pos_iff_of_pos_left] at hh
    exact zero_lt_two
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
h₁ : ∀ (w : V), w ≠ v ∧ Odd (G.degree w) ↔ Odd (G.degree w) ∧ w ≠ v
⊢ Eq.{u + 1} (α := (w : V) → Prop) (fun (w : V) ↦ w ≠ v ∧ Odd (G.degree w)) fun (w : V) ↦ Odd (G.degree w) ∧ w ≠ v

Tactic:
ext w
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
w : V
h₁ h₂ : Odd (G.degree w) ∧ w ≠ v ↔ Odd (G.degree w) ∧ w ≠ v
⊢ w ≠ v ∧ Odd (G.degree w) ↔ Odd (G.degree w) ∧ w ≠ v

Tactic:
rw [and_comm]

Premises used: and_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
⊢ Eq.{u + 1} (α := (w : V) → Prop) (fun (w : V) ↦ w ≠ v ∧ Odd (G.degree w)) fun (w : V) ↦ Odd (G.degree w) ∧ w ≠ v

Tactic:
have hc : (fun w : V => w ≠ v ∧ Odd (G.degree w)) = fun w : V => Odd (G.degree w) ∧ w ≠ v := by
    ext w
    rw [and_comm]
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
hc : Eq.{u + 1} (α := (w : V) → Prop) (fun (w : V) ↦ w ≠ v ∧ Odd (G.degree w)) fun (w : V) ↦ Odd (G.degree w) ∧ w ≠ v
simp : Odd (card.{u} (α := V) {w : V | Odd (G.degree w) ∧ w ≠ v})
⊢ Odd (card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)})

Tactic:
simp only [hc]
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
hc : Eq.{u + 1} (α := (w : V) → Prop) (fun (w : V) ↦ w ≠ v ∧ Odd (G.degree w)) fun (w : V) ↦ Odd (G.degree w) ∧ w ≠ v
rw : Odd (card.{u} (α := V) {w : V | Odd (G.degree w)} - 1)
rw₁ : Membership.mem (γ := Finset V) {w : V | Odd (G.degree w)} v
⊢ Odd (card.{u} (α := V) {w : V | Odd (G.degree w) ∧ w ≠ v})

Tactic:
rw [← filter_filter, filter_ne', card_erase_of_mem]

Premises used: Finset.filter_filter, Finset.card_erase_of_mem, Finset.filter_ne'
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
hc : Eq.{u + 1} (α := (w : V) → Prop) (fun (w : V) ↦ w ≠ v ∧ Odd (G.degree w)) fun (w : V) ↦ Odd (G.degree w) ∧ w ≠ v
⊢ Odd (card.{u} (α := V) {w : V | Odd (G.degree w)} - 1)

Tactic:
⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩

Premises used: Odd, HSub.hSub, tsub_eq_of_eq_add, Exists.intro, OfNat.ofNat, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
hc : Eq.{u + 1} (α := (w : V) → Prop) (fun (w : V) ↦ w ≠ v ∧ Odd (G.degree w)) fun (w : V) ↦ Odd (G.degree w) ∧ w ≠ v
refine : k + k = 2 * (k - 1) + 1 + 1
⊢ Odd (card.{u} (α := V) {w : V | Odd (G.degree w)} - 1)

Tactic:
refine ⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
hc : Eq.{u + 1} (α := (w : V) → Prop) (fun (w : V) ↦ w ≠ v ∧ Odd (G.degree w)) fun (w : V) ↦ Odd (G.degree w) ∧ w ≠ v
⊢ k + k = 2 * (k - 1) + 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : card.{u} (α := V) {v : V | Odd (G.degree v)} = k + k
hk : 0 < k
hc : Eq.{u + 1} (α := (w : V) → Prop) (fun (w : V) ↦ w ≠ v ∧ Odd (G.degree w)) fun (w : V) ↦ Odd (G.degree w) ∧ w ≠ v
rwa rwa₁ rwa₂ rwa₃ : Odd (G.degree v)
⊢ Membership.mem (γ := Finset V) {w : V | Odd (G.degree w)} v

Tactic:
rwa [mem_filter_univ]

Premises used: Finset.mem_filter_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
haveI : ∀ (this : DecidableEq V), ∃ (w : V), w ≠ v ∧ Odd (G.degree w)
⊢ ∃ (w : V), w ≠ v ∧ Odd (G.degree w)

Tactic:
haveI := Classical.decEq V
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
rcases :
  ∀ (k : ℕ) (hg : card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1), ∃ (w : V), w ≠ v ∧ Odd (G.degree w)
⊢ ∃ (w : V), w ≠ v ∧ Odd (G.degree w)

Tactic:
rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩

Premises used: SimpleGraph.odd_card_odd_degree_vertices_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
rw : 0 < 2 * k + 1
⊢ 0 < card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)}

Tactic:
rw [hg]
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
⊢ 0 < 2 * k + 1

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
⊢ 0 < card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)}

Tactic:
have hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)} := by
    rw [hg]
    apply Nat.succ_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)}
rcases :
  ∀ (w : V) (hw : Membership.mem (γ := Finset V) {w : V | w ≠ v ∧ Odd (G.degree w)} w),
    ∃ (w : V), w ≠ v ∧ Odd (G.degree w)
⊢ ∃ (w : V), w ≠ v ∧ Odd (G.degree w)

Tactic:
rcases card_pos.mp hg' with ⟨w, hw⟩

Premises used: Iff.mp, Finset.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : Membership.mem (γ := Finset V) {w : V | w ≠ v ∧ Odd (G.degree w)} w
⊢ w ≠ v ∧ Odd (G.degree w)

Tactic:
rw [mem_filter_univ] at hw

Premises used: Finset.mem_filter_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : w ≠ v ∧ Odd (G.degree w)
⊢ ∃ (w : V), w ≠ v ∧ Odd (G.degree w)

Tactic:
⟨w, hw⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)} = 2 * k + 1
hg' : 0 < card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)}
w : V
hw : w ≠ v ∧ Odd (G.degree w)
⊢ ∃ (w : V), w ≠ v ∧ Odd (G.degree w)

Tactic:
exact ⟨w, hw⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s : Set (Sym2 V)
⊢ (G.deleteEdges s).Adj v w ↔ G.Adj v w ∧ s(v, w) ∉ s

Tactic:
and_congr_right fun h ↦ (and_iff_left h.ne).not

Premises used: SimpleGraph.Adj.ne, and_iff_left, Iff.not, and_congr_right
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G G' : SimpleGraph V
Adj : ∀ (x x_1 : V), (G.deleteEdges G'.edgeSet).Adj x x_1 ↔ (G \ G').Adj x x_1
⊢ G.deleteEdges G'.edgeSet = G \ G'

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G G' : SimpleGraph V
x x_1 : V
⊢ (G.deleteEdges G'.edgeSet).Adj x x_1 ↔ (G \ G').Adj x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s s' : Set (Sym2 V)
⊢ (G.deleteEdges s).deleteEdges s' = G.deleteEdges (s ∪ s')

Tactic:
simp [deleteEdges, sdiff_sdiff]

Premises used: SimpleGraph.deleteEdges, sdiff_sdiff
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.deleteEdges ∅ = G

Tactic:
simp [deleteEdges]

Premises used: SimpleGraph.deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.deleteEdges Set.univ = ⊥

Tactic:
simp [deleteEdges]

Premises used: SimpleGraph.deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
rw : G \ fromEdgeSet s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'
rw₁ rw₂ : G ≤ fromEdgeSet s ⊔ G' ↔ G ≤ fromEdgeSet s ⊔ G'
⊢ G.deleteEdges s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'

Tactic:
rw [deleteEdges, sdiff_le_iff]

Premises used: SimpleGraph.deleteEdges, sdiff_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s ≤ G

Tactic:
sdiff_le

Premises used: sdiff_le
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s₁ s₂ : Set (Sym2 V)
h : s₁ ⊆ s₂
⊢ G.deleteEdges s₂ ≤ G.deleteEdges s₁

Tactic:
sdiff_le_sdiff_left <| fromEdgeSet_mono h

Premises used: SimpleGraph.fromEdgeSet_mono, sdiff_le_sdiff_left
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G H : SimpleGraph V
s : Set (Sym2 V)
h : G ≤ H
⊢ G.deleteEdges s ≤ H.deleteEdges s

Tactic:
sdiff_le_sdiff_right h

Premises used: sdiff_le_sdiff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
rw : G \ fromEdgeSet s = G ↔ Disjoint G.edgeSet s
rw₁ : Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s
rw₂ rw₃ : Disjoint G.edgeSet s ↔ Disjoint G.edgeSet s
⊢ G.deleteEdges s = G ↔ Disjoint G.edgeSet s

Tactic:
rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]

Premises used: SimpleGraph.deleteEdges, SimpleGraph.disjoint_fromEdgeSet, sdiff_eq_left
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
Adj : ∀ (x x_1 : V), (G.deleteEdges s).Adj x x_1 ↔ (G.deleteEdges (s ∩ G.edgeSet)).Adj x x_1
⊢ G.deleteEdges s = G.deleteEdges (s ∩ G.edgeSet)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
x x_1 : V
⊢ (G.deleteEdges s).Adj x x_1 ↔ (G.deleteEdges (s ∩ G.edgeSet)).Adj x x_1

Tactic:
simp +contextual [imp_false]

Premises used: imp_false
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
Adj : ∀ (u v : V), (G.deleteEdges s).Adj u v ↔ G.Adj u v
⊢ G.deleteEdges s = G

Tactic:
ext u v
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
u v : V
⊢ (G.deleteEdges s).Adj u v ↔ G.Adj u v

Tactic:
simpa using (·.ne <| hs ·)
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G H : SimpleGraph V
h : H ≤ G
rw : G.deleteEdges (G \ H).edgeSet = H
rw₁ : G \ (G \ H) = H
rw₂ rw₃ : H = H
⊢ G.deleteEdges (G.edgeSet \ H.edgeSet) = H

Tactic:
rw [← edgeSet_sdiff, deleteEdges_edgeSet, sdiff_sdiff_eq_self h]

Premises used: SimpleGraph.deleteEdges_edgeSet, SimpleGraph.edgeSet_sdiff, sdiff_sdiff_eq_self
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ (G.deleteEdges s).edgeSet = G.edgeSet \ s

Tactic:
simp [deleteEdges]

Premises used: SimpleGraph.deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
s : Finset (Sym2 V)
inst_2 : Fintype (↑(G.deleteEdges (↑s : Set (Sym2 V))).edgeSet : Type u_1)
h : ∀ (e : Sym2 V), e ∈ (G.deleteEdges (↑s : Set (Sym2 V))).edgeFinset ↔ e ∈ G.edgeFinset \ s
⊢ (G.deleteEdges (↑s : Set (Sym2 V))).edgeFinset = G.edgeFinset \ s

Tactic:
ext e
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
s : Finset (Sym2 V)
inst_2 : Fintype (↑(G.deleteEdges (↑s : Set (Sym2 V))).edgeSet : Type u_1)
e : Sym2 V
⊢ e ∈ (G.deleteEdges (↑s : Set (Sym2 V))).edgeFinset ↔ e ∈ G.edgeFinset \ s

Tactic:
simp [edgeSet_deleteEdges]

Premises used: SimpleGraph.edgeSet_deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G H : SimpleGraph V
s : Set (Sym2 V)
⊢ (G ⊔ H).deleteEdges s = G.deleteEdges s ⊔ H.deleteEdges s

Tactic:
sup_sdiff

Premises used: SimpleGraph.deleteEdges, sup_sdiff
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
s t : Set (Sym2 V)
Adj : ∀ (x x_1 : V), ((fromEdgeSet s).deleteEdges t).Adj x x_1 ↔ (fromEdgeSet (s \ t)).Adj x x_1
⊢ (fromEdgeSet s).deleteEdges t = fromEdgeSet (s \ t)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
s t : Set (Sym2 V)
x x_1 : V
⊢ ((fromEdgeSet s).deleteEdges t).Adj x x_1 ↔ (fromEdgeSet (s \ t)).Adj x x_1

Tactic:
simp +contextual
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s = ⊥ ↔ G.edgeSet ⊆ s

Tactic:
simp [deleteEdges]

Premises used: SimpleGraph.deleteEdges
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
rw : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
⊢ (G.deleteIncidenceSet x).Adj v₁ v₂ ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x

Tactic:
rw [deleteIncidenceSet, deleteEdges_adj, mk'_mem_incidenceSet_iff]

Premises used: SimpleGraph.deleteEdges_adj, SimpleGraph.deleteIncidenceSet, SimpleGraph.mk'_mem_incidenceSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₁ mp₂ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
mpr₁ mpr₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mpr₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂
mpr₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
mp₆ : G.Adj v₁ v₂ → v₁ = x → ¬G.Adj v₁ v₂ → False
mp₇ mp₈ mp₉ : G.Adj v₁ v₂ → v₁ = x → ¬(x = v₁ ∨ x = v₂) → False
mp₁₀ : G.Adj v₁ v₂ → v₂ = x → ¬G.Adj v₁ v₂ → False
mp₁₁ mp₁₂ mp₁₃ : G.Adj v₁ v₂ → v₂ = x → ¬(x = v₁ ∨ x = v₂) → False
mpr₅ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₆ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mpr₇ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₈ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mpr₉ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₁₀ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mp₁₄ mp₁₅ mp₁₆ : G.Adj v₁ v₂ → v₁ = x → ¬x = v₁ → ¬x = v₂ → False
mp₁₇ mp₁₈ mp₁₉ : G.Adj v₁ v₂ → v₂ = x → ¬x = v₁ → ¬x = v₂ → False
mpr₁₁ mpr₁₂ mpr₁₃ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₁₄ mpr₁₅ mpr₁₆ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mp₂₀ mp₂₁ mp₂₂ : G.Adj v₁ v₂ → v₁ = x → ¬x = v₁ → ¬x = v₂ → False
mp₂₃ mp₂₄ mp₂₅ : G.Adj v₁ v₂ → v₂ = x → ¬x = v₁ → ¬x = v₂ → False
mpr₁₇ mpr₁₈ mpr₁₉ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₂₀ mpr₂₁ mpr₂₂ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
mp₂₆ mp₂₇ : G.Adj v₁ v₂ → v₁ = x → ¬x = v₁ → ¬x = v₂ → False
mp₂₈ mp₂₉ : G.Adj v₁ v₂ → v₂ = x → ¬x = v₁ → ¬x = v₂ → False
mpr₂₃ mpr₂₄ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₁ → False
mpr₂₅ mpr₂₆ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ → x = v₂ → False
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x : V
⊢ G.deleteIncidenceSet x ≤ G

Tactic:
deleteEdges_le (G.incidenceSet x)

Premises used: SimpleGraph.incidenceSet, SimpleGraph.deleteEdges_le
-- Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges
Goal:
V : Type u_1
G : SimpleGraph V
x : V
rw : G.incidenceSet x ⊆ Sym2.diagSetᶜ
⊢ (fromEdgeSet (G.incidenceSet x)).edgeSet = G.incidenceSet x

Tactic:
rw [edgeSet_fromEdgeSet, sdiff_eq_left, ← Set.subset_compl_iff_disjoint_right]

Premises used: SimpleGraph.edgeSet_fromEdgeSet, Set.subset_compl_iff_disjoint_right, sdiff_eq_left