mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ (((∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) +
        ∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      ∑ i ∈ range (n + r), ∑ w ∈ range r, if i % r ≠ (n + w) % r then 1 else 0) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
sum_range_add,

Goal state after:
n r : ℕ
⊢ ((∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) +
        ∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
        ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a
n r : ℕ
⊢ (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) = ∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0

pp: case e_a
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
        ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
;

Goal state after:
case e_a
n r : ℕ
⊢ (∑ x ∈ range n, ∑ w ∈ range n, if x % r ≠ w % r then 1 else 0) = ∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0

case e_a
n r : ℕ
⊢ (∑ x ∈ range r, ∑ w ∈ range n, if (n + x) % r ≠ w % r then 1 else 0) +
      ((∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
        ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a
n r : ℕ
⊢ (((∑ y ∈ range n, ∑ x ∈ range r, if (n + x) % r ≠ y % r then 1 else 0) +
        ∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
;

Goal state after:
case e_a
n r : ℕ
⊢ (((∑ y ∈ range n, ∑ x ∈ range r, if (n + x) % r ≠ y % r then 1 else 0) +
        ∑ x ∈ range n, ∑ w ∈ range r, if x % r ≠ (n + w) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a
n r : ℕ
⊢ ((2 * ∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
;

Goal state after:
case e_a
n r : ℕ
⊢ ((2 * ∑ x ∈ range n, ∑ x_1 ∈ range r, if x % r ≠ (n + x_1) % r then 1 else 0) +
      ∑ x ∈ range r, ∑ w ∈ range r, if (n + x) % r ≠ (n + w) % r then 1 else 0) =
    2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:

Tactic:
G.edist v w
      ≤ G.edist v u + G.edist u w := G.edist_triangle
    _ = G.edist u v + G.edist u w := by rw [edist_comm]
    _ ≤ G.eccent u + G.eccent u := add_le_add edist_le_eccent edist_le_eccent
    _ = 2 * G.eccent u := (two_mul _).symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : Subsingleton α
⊢ G.diam = 0

Tactic:
simp [diam, h]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ ENat.toNat 0 = 0

Tactic:
;

Goal state after:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ ENat.toNat 0 = 0
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a.e_a.e_a.a
n r x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ (∑ x ∈ range r, if x✝ % r ≠ (n + x) % r then 1 else 0) = r - 1

Tactic:
;

Goal state after:
case e_a.e_a.e_a.a
n r x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ (∑ x ∈ range r, if x✝ % r ≠ (n + x) % r then 1 else 0) = r - 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
| r

Tactic:
;

Goal state after:
n r : ℕ
| r
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case e_a.e_a.a
n r x✝ : ℕ
a✝ : x✝ ∈ range r
⊢ (∑ w ∈ range r, if (n + x✝) % r ≠ (n + w) % r then 1 else 0) = r - 1

Tactic:
;

Goal state after:
case e_a.e_a.a
n r x✝ : ℕ
a✝ : x✝ ∈ range r
⊢ (∑ w ∈ range r, if (n + x✝) % r ≠ (n + w) % r then 1 else 0) = r - 1
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : G.radius = 0
⊢ Subsingleton α

pp: case refine_3
α : Type u_1
G : SimpleGraph α
x✝ : Nonempty α ∧ Subsingleton α
left✝ : Nonempty α
right✝ : Subsingleton α
⊢ G.radius = 0

Tactic:
· contrapose! h
    simp [radius_ne_zero_of_nontrivial]

Goal state after:
case refine_3
α : Type u_1
G : SimpleGraph α
x✝ : Nonempty α ∧ Subsingleton α
left✝ : Nonempty α
right✝ : Subsingleton α
⊢ G.radius = 0
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
n : ℕ
this : #⊤.edgeFinset = n.choose 2
⊢ #(turanGraph n 0).edgeFinset = n.choose 2

Tactic:
;

Goal state after:
case inl
n : ℕ
this : #⊤.edgeFinset = n.choose 2
⊢ #(turanGraph n 0).edgeFinset = n.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n : ℕ
this : #⊤.edgeFinset = n.choose 2
⊢ turanGraph n 0 = ⊤

Tactic:
;

Goal state after:
n : ℕ
this : #⊤.edgeFinset = n.choose 2
⊢ turanGraph n 0 = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
⊢ G.center = Set.univ

Tactic:
by
  rw [Set.eq_univ_iff_forall]
  intro u
  rw [mem_center_iff, eccent_eq_zero_of_subsingleton u, eq_comm, radius_eq_zero_iff]
  tauto

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inl
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : n < r
this : #⊤.edgeFinset = n.choose 2
⊢ #(turanGraph n r).edgeFinset = n.choose 2

Tactic:
;

Goal state after:
case inr.inl
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : n < r
this : #⊤.edgeFinset = n.choose 2
⊢ #(turanGraph n r).edgeFinset = n.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : n < r
this : #⊤.edgeFinset = n.choose 2
⊢ r = 0 ∨ n ≤ r

Tactic:
;

Goal state after:
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : n < r
this : #⊤.edgeFinset = n.choose 2
⊢ r = 0 ∨ n ≤ r
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
e : ↑G.end
K : (Finset V)ᵒᵖ
⊢ (ComponentCompl.supp (↑e K)).Infinite

Tactic:
refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)
  change Opposite.unop K ⊆ Opposite.unop (Opposite.op L) at h
  exact ⟨e.val (Opposite.op L), (e.prop (CategoryTheory.opHomOfLE h))⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w u✝ : ↑Kᶜ
a✝ : Walk.nil.IsPath
⊢ f ⋯ = f ⋯

Tactic:
;

Goal state after:
case nil
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w u✝ : ↑Kᶜ
a✝ : Walk.nil.IsPath
⊢ f ⋯ = f ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : (induce Kᶜ G).Adj u v
q : (induce Kᶜ G).Walk v w
ih : q.IsPath → f ⋯ = f ⋯
⊢ (Walk.cons a q).IsPath → f ⋯ = f ⋯

Tactic:
;

Goal state after:
case cons
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : (induce Kᶜ G).Adj u v
q : (induce Kᶜ G).Walk v w
ih : q.IsPath → f ⋯ = f ⋯
⊢ (Walk.cons a q).IsPath → f ⋯ = f ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : (induce Kᶜ G).Adj u v
q : (induce Kᶜ G).Walk v w
ih : q.IsPath → f ⋯ = f ⋯
h' : (Walk.cons a q).IsPath
⊢ f ⋯ = f ⋯

Tactic:
;

Goal state after:
case cons
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : (induce Kᶜ G).Adj u v
q : (induce Kᶜ G).Walk v w
ih : q.IsPath → f ⋯ = f ⋯
h' : (Walk.cons a q).IsPath
⊢ f ⋯ = f ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' * (r - 1) + r.choose 2 + n' % r * (n' / r) * (r - 1) + r.choose 2 * (n' / r) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2

Tactic:
;

Goal state after:
case inr.inr.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' * (r - 1) + r.choose 2 + n' % r * (n' / r) * (r - 1) + r.choose 2 * (n' / r) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) + r.choose 2 =
    r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1) + r.choose 2

Tactic:
;

Goal state after:
case inr.inr.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) + r.choose 2 =
    r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1) + r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' * (r - 1) + n' % r * (n' / r) * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r) + n' % r * (n' / r) * (r - 1)

Tactic:
;

Goal state after:
case inr.inr.e_a.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' * (r - 1) + n' % r * (n' / r) * (r - 1) = n' % r * (r - 1) + r * (r - 1) * (n' / r) + n' % r * (n' / r) * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 - (n % r) ^ 2 * (r - 1) ≤ (r - 1) * n ^ 2

pp: n r : ℕ
⊢ (n % r) ^ 2 * (r - 1) ≤ n ^ 2 * (r - 1)

Tactic:
;

Goal state after:
n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 - (n % r) ^ 2 * (r - 1) ≤ (r - 1) * n ^ 2

n r : ℕ
⊢ (n % r) ^ 2 * (r - 1) ≤ n ^ 2 * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case h₁.inl
n : ℕ
⊢ (n % 0 - 1) * 0 ≤ (0 - 1) * (n % 0)

pp: case h₁.inr
n r : ℕ
hr : r > 0
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)

Tactic:
;

Goal state after:
case h₁.inl
n : ℕ
⊢ (n % 0 - 1) * 0 ≤ (0 - 1) * (n % 0)

case h₁.inr
n r : ℕ
hr : r > 0
⊢ (n % r - 1) * r ≤ (r - 1) * (n % r)
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: case inl.inl
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v : α
t : Finset α
C : G.Coloring (Fin (r + 1))
x : α
hcx : C x = C v
y : α
hcy : C y = C v
h : Set.SurjOn (⇑C) (insert x ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert y ↑t) Set.univ
hw : G.IsFiveWheelLike r k v x y s t
⊢ False

Tactic:
;

Goal state after:
case inl.inl
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v : α
t : Finset α
C : G.Coloring (Fin (r + 1))
x : α
hcx : C x = C v
y : α
hcy : C y = C v
h : Set.SurjOn (⇑C) (insert x ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert y ↑t) Set.univ
hw : G.IsFiveWheelLike r k v x y s t
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = v
⊢ (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) w ∧ ∀ (y : V), (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) y → y = w

Tactic:
;

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = v
⊢ (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) w ∧ ∀ (y : V), (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) y → y = w
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
this : Fintype α
⊢ Finite α

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
this : Fintype α
⊢ Finite α
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
h : p.IsHamiltonian
⊢ Finite α

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
h : p.IsHamiltonian
⊢ Finite α
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = w
⊢ (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) v ∧ ∀ (y : V), (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) y → y = v

Tactic:
;

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v✝ : V
h✝ : v✝ = w
⊢ (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) v ∧ ∀ (y : V), (fun w_1 ↦ (G.subgraphOfAdj h).Adj v✝ w_1) y → y = v
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
h : p.IsHamiltonianCycle
⊢ Finite α

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
h : p.IsHamiltonianCycle
⊢ Finite α
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
hG : G.IsHamiltonian
v u : α
p : G.Walk u u
hp : p.IsHamiltonianCycle
⊢ ∃ p, p.IsHamiltonianCycle

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
hG : G.IsHamiltonian
v u : α
p : G.Walk u u
hp : p.IsHamiltonianCycle
⊢ ∃ p, p.IsHamiltonianCycle
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i

pp: case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
x✝ : ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i
e : Sym2 V
he : e ∈ M.edgeSet
hv : v ∈ ↑e
⊢ v ∈ M.verts

Tactic:
· have ⟨u, he, _⟩ := h hv
    exact ⟨s(v, u), he, Sym2.mem_mk_left ..⟩

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
x✝ : ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i
e : Sym2 V
he : e ∈ M.edgeSet
hv : v ∈ ↑e
⊢ v ∈ M.verts
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
a b : α
h : s(a, b) ∈ G.edgeSet
⊢ ∑ a_1, incMatrix R G a_1 s(a, b) = 2

Tactic:
rw [mem_edgeSet] at h

Goal state after:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝³ : NonAssocSemiring R
inst✝² : DecidableEq α
inst✝¹ : DecidableRel G.Adj
e : Sym2 α
inst✝ : Fintype α
a b : α
h : G.Adj a b
⊢ ∑ a_1, incMatrix R G a_1 s(a, b) = 2
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i j : V
| if G.Adj i j then x i * x i - x i * x j else 0

Tactic:
;

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
i j : V
| if G.Adj i j then x i * x i - x i * x j else 0
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| ∑ i, ∑ j, if G.Adj j i then x i * x i - x i * x j else 0

Tactic:
;

Goal state after:
V : Type u_1
R : Type u_2
inst✝⁴ : Fintype V
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : DecidableEq V
inst✝¹ : Field R
inst✝ : CharZero R
x : V → R
| ∑ i, ∑ j, if G.Adj j i then x i * x i - x i * x j else 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
this : (p.toSubgraph.neighborSet v).ncard = 2
⊢ Nonempty (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Tactic:
rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _),
    ← Set.cast_ncard (finite_neighborSet_toSubgraph p),
    hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [this]),
    this]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.snd = w'

Tactic:
by
  apply hp.snd_of_toSubgraph_adj
  rw [Walk.mem_support_iff_exists_getVert] at hw'
  obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
  by_cases hn : n = 0 ∨ n = p.length
  · aesop
  have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
    refine @Classical.ofNonempty _ ?_
    rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
        hp.ncard_neighborSet_toSubgraph_internal_eq_two (by lia) (by lia),
        hcyc (Set.nonempty_of_mem hadj.symm)]
  rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
  exact hadj.symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.LineGraph

Goal state before:
pp: case mk
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
val✝ : Sym2 V
a✝ : V × V
h : Quot.mk (Sym2.Rel V) a✝ ∈ G.edgeSet
⊢ Sym2.map ⇑f ↑⟨Quot.mk (Sym2.Rel V) a✝, h⟩ ∈ G'.edgeSet

Tactic:
;

Goal state after:
case mk
V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G.Copy G'
val✝ : Sym2 V
a✝ : V × V
h : Quot.mk (Sym2.Rel V) a✝ ∈ G.edgeSet
⊢ Sym2.map ⇑f ↑⟨Quot.mk (Sym2.Rel V) a✝, h⟩ ∈ G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg.inl.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w ↔ ¬G'.Adj u x

Tactic:
simp only [hnadj, not_false_eq_true, iff_true]

Goal state after:
case neg.inl.inr
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v w w' : V
hww' : w ≠ w'
hl : G.Adj v w
h2 : (v = u ∧ w' = x ∨ v = x ∧ w' = u) ∧ v ≠ w'
⊢ G'.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case e'_2.e'_5
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v : V
⊢ k = #(G.neighborFinset v)

Tactic:
simp [h.regular v]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Trails

Goal state before:
pp: case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ w✝ : V
huv : G.Adj u✝ x
p : G.Walk x w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w✝ → x ≠ x ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, x) ∉ p.edges
this : u✝ ≠ x
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
;

Goal state after:
case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ w✝ : V
huv : G.Adj u✝ x
p : G.Walk x w✝
ih : Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges) ↔ x ≠ w✝ → x ≠ x ∧ x ≠ w✝
ht : p.IsTrail ∧ s(u✝, x) ∉ p.edges
this : u✝ ≠ x
⊢ Even (List.countP (fun e ↦ decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Nonempty V
inst✝ : Finite V
⊢ ENat.card V - 1 + 1 ≤ ENat.card V

Tactic:
ENat.card_eq_coe_natCard

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Nonempty V
inst✝ : Finite V
⊢ ↑(Nat.card V) - 1 + 1 ≤ ↑(Nat.card V)
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: x✝ : ℕ × ℕ
⊢ x✝ ∈ ↑⊥ ↔ x✝ ∈ ∅

Tactic:
;

Goal state after:
x✝ : ℕ × ℕ
⊢ x✝ ∈ ↑⊥ ↔ x✝ ∈ ∅
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
j : ℕ
c : ℕ × ℕ
⊢ c ∈ μ.col j ↔ c ∈ μ ∧ c.2 = j

Tactic:
simp [col]

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ.col j ↔ (i, j) ∈ μ

Tactic:
simp [col]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2

Tactic:
;

Goal state after:
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2