awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
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 : (Walk.cons huv p).IsTrail),
    Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) (Walk.cons huv p).edges) ↔ u ≠ w → x ≠ u ∧ x ≠ w
⊢ Even (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v

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

Premises used: Nat.even_add_one, Classical.not_not, imp_false, false_and, Ne, exists_prop, SimpleGraph.Walk.IsTrail.nil, SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, Sym2.mem_iff, List.countP_cons, and_iff_right_iff_imp, not_true, decide_eq_true_eq, not_false_iff, SimpleGraph.Walk.isTrail_cons, Classical.not_forall, rfl, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
rw : ∀ (a : Sym2 V), List.count a p.edges ≤ 1
⊢ p.IsTrail

Tactic:
rw [isTrail_def, List.nodup_iff_count_le_one]

Premises used: SimpleGraph.Walk.isTrail_def, List.nodup_iff_count_le_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
neg : ∀ (he : e ∉ p.edges), List.count e p.edges ≤ 1
⊢ List.count e p.edges ≤ 1

Tactic:
by_cases he : e ∈ p.edges

Premises used: SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
he : e ∈ p.edges
⊢ List.count e p.edges ≤ 1

Tactic:
(h e (edges_subset_edgeSet _ he)).le

Premises used: Eq.le, SimpleGraph.Walk.edges_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
he : e ∈ p.edges
⊢ List.count e p.edges ≤ 1

Tactic:
exact (h e (edges_subset_edgeSet _ he)).le

Premises used: Eq.le, SimpleGraph.Walk.edges_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
he : e ∉ p.edges
⊢ List.count e p.edges ≤ 1

Tactic:
simp [List.count_eq_zero_of_not_mem he]

Premises used: List.count_eq_zero_of_not_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
he : e ∈ G.edgeSet
⊢ e ∈ p.edges

Tactic:
simpa [Nat.succ_le_iff] using (h e he).ge

Premises used: Eq.ge, Nat.succ_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
⊢ e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeSet

Tactic:
simp only [Finset.mem_mk, Multiset.mem_coe, h.mem_edges_iff]

Premises used: Multiset.mem_coe, Finset.mem_mk, SimpleGraph.Walk.IsEulerian.mem_edges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsTrail
hc : ∀ e ∈ G.edgeSet, e ∈ p.edges
⊢ p.IsEulerian

Tactic:
fun e he =>
  List.count_eq_one_of_mem h.edges_nodup (hc e he)

Premises used: SimpleGraph.Walk.IsEulerian, SimpleGraph.Walk.IsTrail.edges_nodup, List.count_eq_one_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
mpr : (p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges) → p.IsEulerian
⊢ p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
⟨h.isTrail, fun _ => h.mem_edges_iff.mpr⟩

Premises used: Iff.mpr, SimpleGraph.Walk.IsEulerian.isTrail, And.intro, SimpleGraph.Walk.IsEulerian.mem_edges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
exact ⟨h.isTrail, fun _ => h.mem_edges_iff.mpr⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsTrail
hl : ∀ e ∈ G.edgeSet, e ∈ p.edges
⊢ p.IsEulerian

Tactic:
h.isEulerian_of_forall_mem hl

Premises used: SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h : p.IsTrail
hl : ∀ e ∈ G.edgeSet, e ∈ p.edges
⊢ p.IsEulerian

Tactic:
exact h.isEulerian_of_forall_mem hl

Premises used: SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
hp : p.IsTrail
h : p.edgeSet = G.edgeSet
⊢ ∀ e ∈ G.edgeSet, e ∈ p.edges

Tactic:
simp [← h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
u v : V
p : G.Walk u v
h rwa rwa₁ rwa₂ rwa₃ : p.IsEulerian
⊢ p.edgeSet = G.edgeSet

Tactic:
rwa [← h.isTrail.isEulerian_iff]

Premises used: SimpleGraph.Walk.IsEulerian.isTrail, SimpleGraph.Walk.IsTrail.isEulerian_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
h₁ : ∀ (e : Sym2 V), e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeFinset
⊢ ⋯.edgesFinset = G.edgeFinset

Tactic:
ext e
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
e : Sym2 V
⊢ e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeFinset

Tactic:
simp [h.mem_edges_iff]

Premises used: SimpleGraph.Walk.IsEulerian.mem_edges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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 (List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Tactic:
ht.isTrail.even_countP_edges_iff x

Premises used: SimpleGraph.Walk.IsEulerian.isTrail, SimpleGraph.Walk.IsTrail.even_countP_edges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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.degree x = List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges
⊢ Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Tactic:
convert! ht.isTrail.even_countP_edges_iff x

Premises used: SimpleGraph.Walk.IsEulerian.isTrail, SimpleGraph.Walk.IsTrail.even_countP_edges_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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).card = (Multiset.filter (fun (e : Sym2 V) ↦ x ∈ e) (↑p.edges : Multiset (Sym2 V))).card
⊢ G.degree x = List.countP (fun (e : Sym2 V) ↦ decide (x ∈ e)) p.edges

Tactic:
rw [← Multiset.coe_countP, Multiset.countP_eq_card_filter, ← card_incidenceFinset_eq_degree]

Premises used: Multiset.coe_countP, SimpleGraph.card_incidenceFinset_eq_degree, Multiset.countP_eq_card_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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 = Multiset.filter (fun (e : Sym2 V) ↦ x ∈ e) (↑p.edges : Multiset (Sym2 V))
⊢ (G.incidenceFinset x).val.card = (Multiset.filter (fun (e : Sym2 V) ↦ x ∈ e) (↑p.edges : Multiset (Sym2 V))).card

Tactic:
congr 1
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
h₁ h₂ : {e ∈ G.edgeFinset | x ∈ e}.val = {x_1 ∈ G.edgeFinset | x ∈ x_1}.val
⊢ (G.incidenceFinset x).val = {x_1 ∈ ⋯.edgesFinset | x ∈ x_1}.val

Tactic:
rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]

Premises used: SimpleGraph.incidenceFinset_eq_filter, SimpleGraph.Walk.IsEulerian.edgesFinset_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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)}
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
⊢ s.card = 0 ∨ s.card = 2

Tactic:
subst s
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
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
⊢ 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:
simp only [← Nat.not_even_iff_odd, Finset.card_eq_zero]

Premises used: Nat.not_even_iff_odd, Finset.card_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
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
⊢ 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 [ht.even_degree_iff, Ne, not_forall, not_and, Classical.not_not, exists_prop]

Premises used: Classical.not_not, Ne, SimpleGraph.Walk.IsEulerian.even_degree_iff, exists_prop, not_and, Classical.not_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
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
⊢ 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
Goal:
V : Type u_1
G : SimpleGraph V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
u : V
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:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
inr : Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 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

Tactic:
right
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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}
inr : Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = Finset.card (α := V) {u, v}
⊢ Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = 2

Tactic:
convert_to _ = ({u, v} : Finset V).card

Premises used: Insert.insert, Finset.card, Singleton.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
⊢ 2 = Finset.card (α := V) {u, v}

Tactic:
simp [hn]
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
inr : Eq (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} {u, v}
⊢ Finset.card.{u_1} (α := V) {x : V | ¬u = v ∧ (¬x = u → x = v)} = Finset.card (α := V) {u, v}

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
inr :
  ∀ (x : V),
    Membership.mem (γ := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} x ↔ Membership.mem (γ := Finset V) {u, v} x
⊢ Eq (α := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} {u, v}

Tactic:
ext x
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
x : V
⊢ Membership.mem (γ := Finset V) {x : V | ¬u = v ∧ (¬x = u → x = v)} x ↔ Membership.mem (γ := Finset V) {u, v} x

Tactic:
simp [hn, imp_iff_not_or]

Premises used: imp_iff_not_or
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
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
⊢ 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

Tactic:
rw [← Set.toFinset_card]

Premises used: Set.toFinset_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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
apply : Eq.{u_1 + 1} (α := Finset V) (Set.toFinset {v : V | Odd (G.degree v)}) {v : V | Odd (G.degree v)}
⊢ 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:
apply IsEulerian.card_filter_odd_degree ht

Premises used: SimpleGraph.Walk.IsEulerian.card_filter_odd_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Trails
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) (Set.toFinset {v : V | Odd (G.degree v)}) {v : V | Odd (G.degree v)}

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.LocallyLinear → G.EdgeDisjointTriangles

Tactic:
And.left

Premises used: SimpleGraph.LocallyLinear, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
h : G ≤ H
hH : H.EdgeDisjointTriangles
⊢ G.EdgeDisjointTriangles

Tactic:
hH.mono <| cliqueSet_mono h

Premises used: SimpleGraph.cliqueSet_mono, Set.Pairwise.mono, SimpleGraph.EdgeDisjointTriangles
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
⊢ EdgeDisjointTriangles.{u_1} (α := α) ⊥

Tactic:
simp [EdgeDisjointTriangles]

Premises used: SimpleGraph.EdgeDisjointTriangles
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
⊢ LocallyLinear.{u_1} (α := α) ⊥

Tactic:
simp [LocallyLinear]

Premises used: SimpleGraph.LocallyLinear
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
⊢ Ne (α := ℕ) 3 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.EdgeDisjointTriangles
rw :
  (G.cliqueSet 3).Pairwise
    (Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f))
⊢ EdgeDisjointTriangles.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G)

Tactic:
rw [EdgeDisjointTriangles, cliqueSet_map (by simp : 3 ≠ 1),
    (Finset.map_injective f).injOn.pairwise_image]

Premises used: Function.Injective.injOn, SimpleGraph.EdgeDisjointTriangles, SimpleGraph.cliqueSet_map, Finset.map_injective, Set.InjOn.pairwise_image
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
rw : Set.Subsingleton.{u_2} (α := β) ((⇑f : (a : α) → β) '' ((↑s : Set α) ∩ (↑t : Set α)))
⊢ ((↑(Finset.map f s) : Set β) ∩ (↑(Finset.map f t) : Set β)).Subsingleton

Tactic:
rw [← coe_inter, ← map_inter, coe_map, coe_inter]

Premises used: Finset.coe_map, Finset.coe_inter, Finset.map_inter
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ Set.Subsingleton.{u_2} (α := β) ((⇑f : (a : α) → β) '' ((↑s : Set α) ∩ (↑t : Set α)))

Tactic:
(hG hs ht hst).image _

Premises used: Set.Subsingleton.image
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ Set.Subsingleton.{u_2} (α := β) ((⇑f : (a : α) → β) '' ((↑s : Set α) ∩ (↑t : Set α)))

Tactic:
exact (hG hs ht hst).image _

Premises used: Set.Subsingleton.image
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
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 α)))
⊢ (G.cliqueSet 3).Pairwise
    (Function.onFun (fun (x y : Finset β) ↦ ((↑x : Set β) ∩ (↑y : Set β)).Subsingleton) (Finset.map f))

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 _

Premises used: Function.onFun, Finset.coe_map, Finset.coe_inter, Finset.map_inter
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
⊢ LocallyLinear.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G)

Tactic:
⟨hG.1.map _, ?_⟩

Premises used: SimpleGraph.LocallyLinear, And.left, And.intro, SimpleGraph.EdgeDisjointTriangles.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
refine :
  ∀ ⦃x y : β⦄,
    Adj (SimpleGraph.map (⇑f : (a : α) → β) G) x y →
      ∃ (s : Finset β), IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) 3 s ∧ x ∈ s ∧ y ∈ s
⊢ LocallyLinear.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G)

Tactic:
refine ⟨hG.1.map _, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
obtain :
  ∀ (s : Finset α) (hs : G.IsNClique 3 s) (ha : a ∈ s) (hb : b ∈ s),
    ∃ (s : Finset β),
      IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) 3 s ∧
        Membership.mem (α := β) s ((f : (a : α) → β) a : β) ∧ Membership.mem (α := β) s ((f : (a : α) → β) b : β)
⊢ ∃ (s : Finset β),
    IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) 3 s ∧
      Membership.mem (α := β) s ((f : (a : α) → β) a : β) ∧ Membership.mem (α := β) s ((f : (a : α) → β) b : β)

Tactic:
obtain ⟨s, hs, ha, hb⟩ := hG.2 h

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
s : Finset α
hs : G.IsNClique 3 s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ (s : Finset β),
    IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) 3 s ∧
      Membership.mem (α := β) s ((f : (a : α) → β) a : β) ∧ Membership.mem (α := β) s ((f : (a : α) → β) b : β)

Tactic:
⟨s.map f, hs.map, mem_map_of_mem _ ha, mem_map_of_mem _ hb⟩

Premises used: Finset.map, SimpleGraph.IsNClique.map, And.intro, Exists.intro, Finset.mem_map_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
s : Finset α
hs : G.IsNClique 3 s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ (s : Finset β),
    IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) 3 s ∧
      Membership.mem (α := β) s ((f : (a : α) → β) a : β) ∧ Membership.mem (α := β) s ((f : (a : α) → β) b : β)

Tactic:
exact ⟨s.map f, hs.map, mem_map_of_mem _ ha, mem_map_of_mem _ hb⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G) ↔ G.LocallyLinear

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
refine_1 : ∀ (h : LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)), G.LocallyLinear
refine_2 : G.LocallyLinear → LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)
⊢ LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G) ↔ G.LocallyLinear

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)
refine_1 :
  LocallyLinear.{u_2} (α := β)
    (SimpleGraph.map.{u_1, u_2} (V := α) (⇑e.toEmbedding : (a : α) → β)
      (SimpleGraph.comap (⇑e.toEmbedding : (a : α) → β) G))
⊢ G.LocallyLinear

Tactic:
rw [← comap_map_eq e.symm.toEmbedding G, comap_symm, map_symm]

Premises used: SimpleGraph.comap_symm, SimpleGraph.map_symm, Equiv.toEmbedding, Equiv.symm, SimpleGraph.comap_map_eq