awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
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)})
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)})
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have have₃ : ∀ (h : Eq (α := ZMod 2) (↑(∑ v : V, G.degree v) : ZMod 2) 0), 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)})
⊢ 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),
  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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)})
⊢ Even (card.{u} (α := V) {v : V | Odd (G.degree v)})
have 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)})
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)})
⊢ 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)
⊢ Odd (card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)})
have 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)})
Tactic: rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)}
have h₁ : Membership.mem (γ := Finset V) {v : V | Odd (G.degree v)} v
Tactic: use v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
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
have hh : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)}
⊢ 0 < k
have rwa : ∀ (hh : 0 < 2 * k), LT.lt (α := ℕ) 0 2
Tactic: rwa [← card_pos, hg, ← two_mul, mul_pos_iff_of_pos_left] at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
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 (card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)})
have hk : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
have h₁ : ∀ (w : V), w ≠ v ∧ Odd (G.degree w) ↔ Odd (G.degree w) ∧ w ≠ v
Tactic: ext w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ w ≠ v ∧ Odd (G.degree w) ↔ Odd (G.degree w) ∧ w ≠ v
have h₁ : Odd (G.degree w) ∧ w ≠ v ↔ Odd (G.degree w) ∧ w ≠ v
Tactic: rw [and_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
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
⊢ Odd (card.{u} (α := V) {w : V | w ≠ v ∧ Odd (G.degree w)})
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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 | w ≠ v ∧ Odd (G.degree w)})
have simp : Odd (card.{u} (α := V) {w : V | Odd (G.degree w) ∧ w ≠ v})
Tactic: simp only [hc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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) ∧ w ≠ v})
have rw : Odd (card.{u} (α := V) {w : V | Odd (G.degree w)} - 1)
Tactic: rw [← filter_filter, filter_ne', card_erase_of_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)
⊢ Odd (card.{u} (α := V) {w : V | Odd (G.degree w) ∧ w ≠ v})
have rw₁ : Membership.mem (γ := Finset V) {w : V | Odd (G.degree w)} v
Tactic: rw [← filter_filter, filter_ne', card_erase_of_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)
have refine : k + k = 2 * (k - 1) + 1 + 1
Tactic: refine ⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
⊢ ∃ (w : V), w ≠ v ∧ Odd (G.degree w)
have haveI : ∀ (this : DecidableEq V), ∃ (w : V), w ≠ v ∧ Odd (G.degree w)
Tactic: haveI := Classical.decEq V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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
⊢ ∃ (w : V), w ≠ v ∧ Odd (G.degree w)
have 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)
Tactic: rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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)}
have rw : 0 < 2 * k + 1
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
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
⊢ ∃ (w : V), w ≠ v ∧ Odd (G.degree w)
have hg' : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (goal)
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), w ≠ v ∧ Odd (G.degree w)
have 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)
Tactic: rcases card_pos.mp hg' with ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DegreeSum (hypothesis)
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), w ≠ v ∧ Odd (G.degree w)
have hw₁ : w ≠ v ∧ Odd (G.degree w)
Tactic: rw [mem_filter_univ] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
⊢ G.deleteEdges G'.edgeSet = G \ G'
have Adj : ∀ (x x_1 : V), (G.deleteEdges G'.edgeSet).Adj x x_1 ↔ (G \ G').Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
⊢ G.deleteEdges s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'
have rw : G \ fromEdgeSet s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'
Tactic: rw [deleteEdges, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
rw : G \ fromEdgeSet s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'
⊢ G.deleteEdges s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'
have rw₁ : G ≤ fromEdgeSet s ⊔ G' ↔ G ≤ fromEdgeSet s ⊔ G'
Tactic: rw [deleteEdges, sdiff_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s = G ↔ Disjoint G.edgeSet s
have rw : G \ fromEdgeSet s = G ↔ Disjoint G.edgeSet s
Tactic: rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
rw : G \ fromEdgeSet s = G ↔ Disjoint G.edgeSet s
⊢ G.deleteEdges s = G ↔ Disjoint G.edgeSet s
have rw₁ : Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s
Tactic: rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
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
⊢ G.deleteEdges s = G ↔ Disjoint G.edgeSet s
have rw₂ : Disjoint G.edgeSet s ↔ Disjoint G.edgeSet s
Tactic: rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s = G.deleteEdges (s ∩ G.edgeSet)
have Adj : ∀ (x x_1 : V), (G.deleteEdges s).Adj x x_1 ↔ (G.deleteEdges (s ∩ G.edgeSet)).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
s : Set (Sym2 V)
G : SimpleGraph V
hs : s ⊆ Sym2.diagSet
⊢ G.deleteEdges s = G
have Adj : ∀ (u v : V), (G.deleteEdges s).Adj u v ↔ G.Adj u v
Tactic: ext u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G H : SimpleGraph V
h : H ≤ G
⊢ G.deleteEdges (G.edgeSet \ H.edgeSet) = H
have rw : G.deleteEdges (G \ H).edgeSet = H
Tactic: rw [← edgeSet_sdiff, deleteEdges_edgeSet, sdiff_sdiff_eq_self h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G H : SimpleGraph V
h : H ≤ G
rw : G.deleteEdges (G \ H).edgeSet = H
⊢ G.deleteEdges (G.edgeSet \ H.edgeSet) = H
have rw₁ : G \ (G \ H) = H
Tactic: rw [← edgeSet_sdiff, deleteEdges_edgeSet, sdiff_sdiff_eq_self h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G H : SimpleGraph V
h : H ≤ G
rw : G.deleteEdges (G \ H).edgeSet = H
rw₁ : G \ (G \ H) = H
⊢ G.deleteEdges (G.edgeSet \ H.edgeSet) = H
have rw₂ : H = H
Tactic: rw [← edgeSet_sdiff, deleteEdges_edgeSet, sdiff_sdiff_eq_self h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
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)
⊢ (G.deleteEdges (↑s : Set (Sym2 V))).edgeFinset = G.edgeFinset \ s
have h : ∀ (e : Sym2 V), e ∈ (G.deleteEdges (↑s : Set (Sym2 V))).edgeFinset ↔ e ∈ G.edgeFinset \ s
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
s t : Set (Sym2 V)
⊢ (fromEdgeSet s).deleteEdges t = fromEdgeSet (s \ t)
have Adj : ∀ (x x_1 : V), ((fromEdgeSet s).deleteEdges t).Adj x x_1 ↔ (fromEdgeSet (s \ t)).Adj x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ (G.deleteIncidenceSet x).Adj v₁ v₂ ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have rw : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
Tactic: rw [deleteIncidenceSet, deleteEdges_adj, mk'_mem_incidenceSet_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
Goal:
V : Type u_1
G : SimpleGraph V
x v₁ v₂ : V
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp : G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
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
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mpr : G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
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₂))
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₁ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
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
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₃ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → G.Adj v₁ v₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
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₂
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₄ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₁ ≠ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
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
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mp₅ : G.Adj v₁ v₂ → ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) → v₂ ≠ x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.DeleteEdges (goal)
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
⊢ G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂)) ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
have mpr₁ : G.Adj v₁ v₂ → v₁ ≠ x → v₂ ≠ x → G.Adj v₁ v₂ ∧ ¬(G.Adj v₁ v₂ ∧ (x = v₁ ∨ x = v₂))
Tactic: tauto