awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Sum (goal)
Goal:
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w_1 w' : W
inst : DecidableEq V
inst_1 : DecidableEq W
inst_2 : G.LocallyFinite
inst_3 : H.LocallyFinite
w : W
⊢ Fintype (↑((G ⊕g H).neighborSet (Sum.inr w)) : Type (max u_5 u_3))
have inr : Fintype (↑(Sum.inr '' H.neighborSet w) : Type (max u_5 u_3))
Tactic: simp only [neighborSet_sum_inl, neighborSet_sum_inr]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (ht : p.IsTrail), Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
ht : (cons huv p).IsTrail
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (cons huv p).edges) ↔ u_1 ≠ w → x ≠ u_1 ∧ x ≠ w
have ht₁ : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
Tactic: rw [isTrail_cons] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ (ht : p.IsTrail), Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (cons huv p).edges) ↔ u_1 ≠ w → x ≠ u_1 ∧ x ≠ w
have ih₁ : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
Tactic: specialize ih ht.1
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (cons huv p).edges) ↔ u_1 ≠ w → x ≠ u_1 ∧ x ≠ w
have cons : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + if decide (x = u_1 ∨ x = v_1) = true then 1 else 0) ↔
  ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
Tactic: simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + if decide (x = u_1 ∨ x = v_1) = true then 1 else 0) ↔
    ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
have pos : ∀ (h : decide (x = u_1 ∨ x = v_1) = true),
  Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
pos :
  ∀ (h : decide (x = u_1 ∨ x = v_1) = true),
    Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + if decide (x = u_1 ∨ x = v_1) = true then 1 else 0) ↔
    ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
have neg : ∀ (h : ¬decide (x = u_1 ∨ x = v_1) = true),
  Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 0) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
h : decide (x = u_1 ∨ x = v_1) = true
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
have h₁ : x = u_1 ∨ x = v_1
Tactic: rw [decide_eq_true_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
h : x = u_1 ∨ x = v_1
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
have pos : ∀ (huv : G.Adj x v_1) (ht : p.IsTrail ∧ s(x, v_1) ∉ p.edges),
  Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬x = w → ¬x = x ∧ ¬x = w
Tactic: obtain (rfl | rfl) := h
Cleared hypotheses: u_1, huv, ht, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 v_1 w : V
huv : G.Adj u_1 v_1
p : G.Walk v_1 w
ht : p.IsTrail ∧ s(u_1, v_1) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
h : x = u_1 ∨ x = v_1
pos :
  ∀ (huv : G.Adj x v_1) (ht : p.IsTrail ∧ s(x, v_1) ∉ p.edges),
    Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬x = w → ¬x = x ∧ ¬x = w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
have pos₁ : ∀ (huv : G.Adj u_1 x) (p : G.Walk x w) (ht : p.IsTrail ∧ s(u_1, x) ∉ p.edges)
  (ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w → x ≠ x ∧ x ≠ w),
  Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
Tactic: obtain (rfl | rfl) := h
Cleared hypotheses: v_1, huv, p, ht, ih, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x v_1 w : V
p : G.Walk v_1 w
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
huv : G.Adj x v_1
ht : p.IsTrail ∧ s(x, v_1) ∉ p.edges
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬x = w → ¬x = x ∧ ¬x = w
have pos : ¬(v_1 ≠ w → x ≠ v_1 ∧ x ≠ w) ↔ ¬x = w → ¬x = x ∧ ¬x = w
Tactic: rw [Nat.even_add_one, ih]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x v_1 w : V
p : G.Walk v_1 w
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v_1 ≠ w → x ≠ v_1 ∧ x ≠ w
huv : G.Adj x v_1
ht : p.IsTrail ∧ s(x, v_1) ∉ p.edges
⊢ ¬(v_1 ≠ w → x ≠ v_1 ∧ x ≠ w) ↔ ¬x = w → ¬x = x ∧ ¬x = w
have pos : x = w → ¬v_1 = w
Tactic: simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
          Classical.not_not, exists_prop, not_true, false_and,
          and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v x u_1 w : V
huv : G.Adj u_1 x
p : G.Walk x w
ht : p.IsTrail ∧ s(u_1, x) ∉ p.edges
ih : Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w → x ≠ x ∧ x ≠ w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u_1 = w → ¬x = u_1 ∧ ¬x = w
have this : u_1 ≠ x
Tactic: have := huv.ne
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
ht : p.IsTrail
x : V
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v
have nil : ∀ {u : V} (ht : IsTrail.{u_1} (V := V) (G := G) (u := u) Walk.nil),
  Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (edges (G := G) (u := u) Walk.nil)) ↔ u ≠ u → x ≠ u ∧ x ≠ u
Tactic: induction p with
  | nil => simp
  | cons huv p ih =>
    rw [isTrail_cons] at ht
    specialize ih ht.1
    simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]
    split_ifs with h
    · rw [decide_eq_true_eq] at h
      obtain (rfl | rfl) := h
      · rw [Nat.even_add_one, ih]
        simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
          Classical.not_not, exists_prop, not_true, false_and,
          and_iff_right_iff_imp]
        rintro rfl rfl
        exact G.loopless.irrefl _ huv
      · have := huv.ne; grind
    · grind
Cleared hypotheses: p, ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
ht : p.IsTrail
x : V
nil :
  ∀ {u : V} (ht : IsTrail.{u_1} (V := V) (G := G) (u := u) Walk.nil),
    Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (edges (G := G) (u := u) Walk.nil)) ↔ u ≠ u → x ≠ u ∧ x ≠ u
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v
have cons : ∀ {u v w : V} (huv : G.Adj u v) (p : G.Walk v w)
  (ih : ∀ (ht : p.IsTrail), Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ v ≠ w → x ≠ v ∧ x ≠ w)
  (ht : (cons huv p).IsTrail),
  Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (cons huv p).edges) ↔ u ≠ w → x ≠ u ∧ x ≠ w
Tactic: induction p with
  | nil => simp
  | cons huv p ih =>
    rw [isTrail_cons] at ht
    specialize ih ht.1
    simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]
    split_ifs with h
    · rw [decide_eq_true_eq] at h
      obtain (rfl | rfl) := h
      · rw [Nat.even_add_one, ih]
        simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
          Classical.not_not, exists_prop, not_true, false_and,
          and_iff_right_iff_imp]
        rintro rfl rfl
        exact G.loopless.irrefl _ huv
      · have := huv.ne; grind
    · grind
Cleared hypotheses: p, ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsTrail
have rw : ∀ (a : Sym2 V), List.count a p.edges ≤ 1
Tactic: rw [isTrail_def, List.nodup_iff_count_le_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ List.count e p.edges ≤ 1
have pos : ∀ (he : e ∈ p.edges), List.count e p.edges ≤ 1
Tactic: by_cases he : e ∈ p.edges
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
pos : ∀ (he : e ∈ p.edges), List.count e p.edges ≤ 1
⊢ List.count e p.edges ≤ 1
have neg : ∀ (he : e ∉ p.edges), List.count e p.edges ≤ 1
Tactic: by_cases he : e ∈ p.edges
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
⊢ p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges
have mp : p.IsEulerian → p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
mp : p.IsEulerian → p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges
⊢ p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges
have mpr : (p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges) → p.IsEulerian
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype (↑G.edgeSet : Type u_1)
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ ⋯.edgesFinset = G.edgeFinset
have h₁ : ∀ (e : Sym2 V), e ∈ sorry.edgesFinset ↔ e ∈ G.edgeFinset
Tactic: ext e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
⊢ Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v
have h : G.degree x = List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges
Tactic: convert! ht.isTrail.even_countP_edges_iff x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
⊢ G.degree x = List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges
have h : (G.incidenceFinset x).card = (Multiset.filter (fun (e : Sym2 V) ↦ x ∈ e) (↑p.edges : Multiset (Sym2 V))).card
Tactic: rw [← Multiset.coe_countP, Multiset.countP_eq_card_filter, ← card_incidenceFinset_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
⊢ (G.incidenceFinset x).val.card = (Multiset.filter (fun (e : Sym2 V) ↦ x ∈ e) (↑p.edges : Multiset (Sym2 V))).card
have h : (G.incidenceFinset x).val = Multiset.filter (fun (e : Sym2 V) ↦ x ∈ e) (↑p.edges : Multiset (Sym2 V))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
⊢ (G.incidenceFinset x).val = {x_1 ∈ ⋯.edgesFinset | x ∈ x_1}.val
have h : (G.incidenceFinset x).val = {x_1 ∈ G.edgeFinset | x ∈ x_1}.val
Tactic: rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
h : (G.incidenceFinset x).val = {x_1 ∈ G.edgeFinset | x ∈ x_1}.val
⊢ (G.incidenceFinset x).val = {x_1 ∈ ⋯.edgesFinset | x ∈ x_1}.val
have h₁ : {e ∈ G.edgeFinset | x ∈ e}.val = {x_1 ∈ G.edgeFinset | x ∈ x_1}.val
Tactic: rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
s : Finset V
h : s = {v : V | Odd (G.degree v)}
⊢ s.card = 0 ∨ s.card = 2
have subst : Finset.card.{u_1} (α := V) {v : V | Odd (G.degree v)} = 0 ∨ Finset.card.{u_1} (α := V) {v : V | Odd (G.degree v)} = 2
Tactic: subst s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Finset.card.{u_1} (α := V) {v : V | Odd (G.degree v)} = 0 ∨ Finset.card.{u_1} (α := V) {v : V | Odd (G.degree v)} = 2
have simp : Eq.{u_1 + 1} (α := Finset V) {x : V | ¬Even (G.degree x)} ∅ ∨
  Finset.card.{u_1} (α := V) {x : V | ¬Even (G.degree x)} = 2
Tactic: simp only [← Nat.not_even_iff_odd, Finset.card_eq_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Eq.{u_1 + 1} (α := Finset V) {x : V | ¬Even (G.degree x)} ∅ ∨
    Finset.card.{u_1} (α := V) {x : V | ¬Even (G.degree x)} = 2
have simp : Eq.{u_1 + 1} (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} ∅ ∨
  Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2
Tactic: simp only [ht.even_degree_iff, Ne, not_forall, not_and, Classical.not_not, exists_prop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Eq.{u_1 + 1} (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} ∅ ∨
    Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2
have inl : ∀ {p : G.Walk u u} (ht : p.IsEulerian),
  Eq.{u_1 + 1} (α := Finset V) {x : V | ¬u = u ∧ (¬x = u → x = u)} ∅ ∨
    Finset.card.{u_1} (α := V) {x : V | ¬u = u ∧ (¬x = u → x = u)} = 2
Tactic: obtain rfl | hn := eq_or_ne u v
Cleared hypotheses: v, p, ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
inl :
  ∀ {p : G.Walk u u} (ht : p.IsEulerian),
    Eq.{u_1 + 1} (α := Finset V) {x : V | ¬u = u ∧ (¬x = u → x = u)} ∅ ∨
      Finset.card.{u_1} (α := V) {x : V | ¬u = u ∧ (¬x = u → x = u)} = 2
⊢ Eq.{u_1 + 1} (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} ∅ ∨
    Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2
have inr : ∀ (hn : u ≠ v),
  Eq.{u_1 + 1} (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} ∅ ∨
    Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2
Tactic: obtain rfl | hn := eq_or_ne u v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ Eq.{u_1 + 1} (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} ∅ ∨
    Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2
have inr : Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2
Tactic: right
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2
have h : 2 = Finset.card (α := V) {u, v}
Tactic: convert_to _ = ({u, v} : Finset V).card
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
h : 2 = Finset.card (α := V) {u, v}
⊢ Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2
have inr : Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = Finset.card (α := V) {u, v}
Tactic: convert_to _ = ({u, v} : Finset V).card
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = Finset.card (α := V) {u, v}
have inr : Eq (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} {u, v}
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ Eq (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} {u, v}
have inr : ∀ (x : V),
  Membership.mem (γ := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} x ↔ Membership.mem (γ := Finset V) {u, v} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Fintype.card.{u_1} (↑{v : V | Odd (G.degree v)} : Type u_1) = 0 ∨
    Fintype.card.{u_1} (↑{v : V | Odd (G.degree v)} : Type u_1) = 2
have rw : Finset.card.{u_1} (α := V) (Set.toFinset {v : V | Odd (G.degree v)}) = 0 ∨
  Finset.card.{u_1} (α := V) (Set.toFinset {v : V | Odd (G.degree v)}) = 2
Tactic: rw [← Set.toFinset_card]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Trails (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Finset.card.{u_1} (α := V) (Set.toFinset {v : V | Odd (G.degree v)}) = 0 ∨
    Finset.card.{u_1} (α := V) (Set.toFinset {v : V | Odd (G.degree v)}) = 2
have apply : Eq.{u_1 + 1} (α := Finset V) (Set.toFinset {v : V | Odd (G.degree v)}) {v : V | Odd (G.degree v)}
Tactic: apply IsEulerian.card_filter_odd_degree ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ EdgeDisjointTriangles.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G)
have rw : (G.cliqueSet 3).Pairwise
  (Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f))
Tactic: rw [EdgeDisjointTriangles, cliqueSet_map (by simp : 3 ≠ 1),
    (Finset.map_injective f).injOn.pairwise_image]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
s : Finset α
hs : s ∈ G.cliqueSet 3
t : Finset α
ht : t ∈ G.cliqueSet 3
hst : s ≠ t
⊢ ((↑(Finset.map f s) : Set β) ∩ (↑(Finset.map f t) : Set β)).Subsingleton
have rw : Set.Subsingleton.{u_2} (α := β) ((⇑f : (a : α) → β) '' ((↑s : Set α) ∩ (↑t : Set α)))
Tactic: rw [← coe_inter, ← map_inter, coe_map, coe_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ (G.cliqueSet 3).Pairwise
    (Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f))
have rintro : ∀ ⦃s : Finset α⦄ (hs : s ∈ G.cliqueSet 3) ⦃t : Finset α⦄ (ht : t ∈ G.cliqueSet 3) (hst : s ≠ t),
  Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f) s t
Tactic: classical
  rintro s hs t ht hst
  dsimp [Function.onFun]
  rw [← coe_inter, ← map_inter, coe_map, coe_inter]
  exact (hG hs ht hst).image _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
rintro :
  ∀ ⦃s : Finset α⦄ (hs : s ∈ G.cliqueSet 3) ⦃t : Finset α⦄ (ht : t ∈ G.cliqueSet 3) (hst : s ≠ t),
    Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f) s t
⊢ (G.cliqueSet 3).Pairwise
    (Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f))
have rintro₁ : ∀ ⦃s : Finset α⦄ (hs : s ∈ G.cliqueSet 3) ⦃t : Finset α⦄ (ht : t ∈ G.cliqueSet 3) (hst : s ≠ t),
  ((↑(Finset.map f s) : Set β) ∩ (↑(Finset.map f t) : Set β)).Subsingleton
Tactic: classical
  rintro s hs t ht hst
  dsimp [Function.onFun]
  rw [← coe_inter, ← map_inter, coe_map, coe_inter]
  exact (hG hs ht hst).image _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
rintro :
  ∀ ⦃s : Finset α⦄ (hs : s ∈ G.cliqueSet 3) ⦃t : Finset α⦄ (ht : t ∈ G.cliqueSet 3) (hst : s ≠ t),
    Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f) s t
rintro₁ :
  ∀ ⦃s : Finset α⦄ (hs : s ∈ G.cliqueSet 3) ⦃t : Finset α⦄ (ht : t ∈ G.cliqueSet 3) (hst : s ≠ t),
    ((↑(Finset.map f s) : Set β) ∩ (↑(Finset.map f t) : Set β)).Subsingleton
⊢ (G.cliqueSet 3).Pairwise
    (Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f))
have rintro₂ : ∀ ⦃s : Finset α⦄ (hs : s ∈ G.cliqueSet 3) ⦃t : Finset α⦄ (ht : t ∈ G.cliqueSet 3) (hst : s ≠ t),
  Set.Subsingleton.{u_2} (α := β) ((⇑f : (a : α) → β) '' ((↑s : Set α) ∩ (↑t : Set α)))
Tactic: classical
  rintro s hs t ht hst
  dsimp [Function.onFun]
  rw [← coe_inter, ← map_inter, coe_map, coe_inter]
  exact (hG hs ht hst).image _