mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
s : Set (Sym2 V)
⊢ Relation.ReflGen (fromEdgeSet s).Adj = Relation.ReflGen (Sym2.ToRel s)

Tactic:
ext

Goal state after:
V : Type u
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Relation.ReflGen (fromEdgeSet s).Adj x✝¹ x✝ ↔ Relation.ReflGen (Sym2.ToRel s) x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
h : G.IsUniversal u
h' : u ≠ v
⊢ G.Reachable u v

Tactic:
· exact (h h').reachable

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V ↔ ∃ v, ∀ (w : V), G.Reachable v w

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V → ∃ v, ∀ (w : V), G.Reachable v w

case mpr
V : Type u
G : SimpleGraph V
⊢ (∃ v, ∀ (w : V), G.Reachable v w) → G.Preconnected ∧ Nonempty V
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk v = c ↔ G.connectedComponentMk w = c

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk v = c → G.connectedComponentMk w = c

case mpr
V : Type u
G : SimpleGraph V
v w : V
c : G.ConnectedComponent
hadj : G.Adj v w
⊢ G.connectedComponentMk w = c → G.connectedComponentMk v = c
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes ↔ s ∈ c

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes → s ∈ c

case mpr
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ c → s ∈ (mkClasses c ⋯).classes
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ⊆ range'k ∧ #B = r - i ↔ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
constructor

Goal state after:
case mp
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := ⋯
𝒞 : Finset (Finset (Fin n)) := ⋯
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ⊆ range'k ∧ #B = r - i → ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := ⋯
𝒞 : Finset (Finset (Fin n)) := ⋯
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ (∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i) → B ⊆ range'k ∧ #B = r - i
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ g ⋯.some = k ∧ hs.some ⋯.some ∈ s ⋯.some

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ g ⋯.some = k

case right
ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ hs.some ⋯.some ∈ s ⋯.some
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w' ↔ ∃ p, s(v, w) ∉ p.edges

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (G.deleteEdges {s(v, w)}).Reachable v' w' → ∃ p, s(v, w) ∉ p.edges

case mpr
V : Type u
G : SimpleGraph V
v w v' w' : V
⊢ (∃ p, s(v, w) ∉ p.edges) → (G.deleteEdges {s(v, w)}).Reachable v' w'
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n ↔ ∃ C, ∀ (v : V), C v < n

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.Colorable n → ∃ C, ∀ (v : V), C v < n

case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ (∃ C, ∀ (v : V), C v < n) → G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) → ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

case mpr
V : Type u
G : SimpleGraph V
v w : V
⊢ (∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
⊢ (induce s G).Reachable ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
constructor

Goal state after:
V : Type u
G : SimpleGraph V
hG : G.Preconnected
s : Set V
hs : ∀ v ∉ s, (G.neighborSet v).Subsingleton
u : V
hu : u ∈ s
v : V
hv : v ∈ s
p : G.Walk u v
hp : p.IsPath
⊢ (induce s G).Walk ⟨u, hu⟩ ⟨v, hv⟩
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case zero
ι : Type u_4
V : ι → Type u_5
f : (i : ι) → V i
hc : (completeMultipartiteGraph V).CliqueFree 0
⊢ (completeMultipartiteGraph V).Colorable (0 - 1)

Tactic:
exact absurd hc not_cliqueFree_zero

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
ih :
  (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤
    (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s

Tactic:
have : 𝒜 ⊼ ℬ ⊆ powerset (insert a u) := by simpa using infs_subset h𝒜 hℬ

Goal state after:
case insert
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a : α
u : Finset α
hu : a ∉ u
f₁ f₂ f₃ f₄ : Finset α → β
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
ih :
  (∑ s ∈ u.powerset, collapse 𝒜 a f₁ s) * ∑ s ∈ u.powerset, collapse ℬ a f₂ s ≤
    (∑ s ∈ u.powerset ⊼ u.powerset, collapse (𝒜 ⊼ ℬ) a f₃ s) * ∑ s ∈ u.powerset ⊻ u.powerset, collapse (𝒜 ⊻ ℬ) a f₄ s
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hℬ : ℬ ⊆ (insert a u).powerset
this : 𝒜 ⊼ ℬ ⊆ (insert a u).powerset
⊢ (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ h.toWalk.toSubgraph = G.subgraphOfAdj h

Tactic:
ext

Goal state after:
case verts
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝ : V
⊢ x✝ ∈ h.toWalk.toSubgraph.verts ↔ x✝ ∈ (G.subgraphOfAdj h).verts

case Adj
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
x✝¹ x✝ : V
⊢ h.toWalk.toSubgraph.Adj x✝¹ x✝ ↔ (G.subgraphOfAdj h).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons.e_a
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ = G.subgraphOfAdj h✝

Tactic:
ext

Goal state after:
case cons.e_a.verts
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝).verts ↔ x✝ ∈ (G.subgraphOfAdj h✝).verts

case cons.e_a.Adj
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝).Adj x✝¹ x✝ ↔ (G.subgraphOfAdj h✝).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ p.bypass.toSubgraph ≤ p.toSubgraph

Tactic:
constructor

Goal state after:
case left
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ p.bypass.toSubgraph.verts ⊆ p.toSubgraph.verts

case right
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
u v : V
inst✝ : DecidableEq V
⊢ ⊤.edist u v = if u = v then 0 else 1

Tactic:
by_cases h : u = v <;> simp [h]

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

Goal state before:
pp: V : Type u_1
u v : V
⊢ ⊥.dist u v = 0

Tactic:
by_cases h : u = v <;> simp [h]

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

Goal state before:
pp: V : Type u_1
u v : V
inst✝ : DecidableEq V
⊢ ⊤.dist u v = if u = v then 0 else 1

Tactic:
by_cases h : u = v <;> simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this✝ : Nonempty α
this : Nonempty β
⊢ (G □ H).Connected

Tactic:
exact ⟨hG.preconnected.boxProd hH.preconnected⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).Reachable x y ↔ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).Reachable x y → G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2

case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ G.Reachable x.1 y.1 ∧ H.Reachable x.2 y.2 → (G □ H).Reachable x y
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: 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 w' : W
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | Sum.inl ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inl u, Sum.inl v), h⟩) ⋯
      | Sum.inr ⟨e, he⟩ => Sym2.fromRelNdrec e he (fun u v h ↦ ⟨s(Sum.inr u, Sum.inr v), h⟩) ⋯)
    fun x ↦
    match x with
    | ⟨e, he⟩ =>
      Sym2.fromRelNdrec e he
        (fun x x_1 x_2 ↦
          match x, x_1, x_2 with
          | Sum.inl u, Sum.inl v, h => Sum.inl ⟨s(u, v), h⟩
          | Sum.inr u, Sum.inr v, h => Sum.inr ⟨s(u, v), h⟩
          | Sum.inl u, Sum.inr v, h => False.elim ⋯
          | Sum.inr u, Sum.inl v, h => False.elim ⋯)
        ⋯

Tactic:
rintro (⟨⟨u, v⟩, h⟩ | ⟨⟨u, v⟩, h⟩) <;> rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Preconnected ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Preconnected → ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H) → H.Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ (pathGraph n).Adj u v ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u

Tactic:
by simp [pathGraph, hasse]

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) → ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a

case mpr
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a) → ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: case mpr
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a) → ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w

Tactic:
· rintro h v w hvw g hg (rfl | rfl)
    · exact (h g hg v (hvw ·.symm)).symm
    · exact h g hg w hvw

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : Group M
u v : M
⊢ (mulCayley s).Adj u v ↔ u ≠ v ∧ (u⁻¹ * v ∈ s ∨ v⁻¹ * u ∈ s)

Tactic:
by
  simp [mulCayley_adj', ← eq_inv_mul_iff_mul_eq (b := u), ← inv_mul_eq_iff_eq_mul (a := v),
    and_or_left, exists_or]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
s : Set G
⊢ circulantGraph s = circulantGraph (s ∪ -s)

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : AddGroup G
s : Set G
x✝¹ x✝ : G
⊢ (circulantGraph s).Adj x✝¹ x✝ ↔ (circulantGraph (s ∪ -s)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
u v w : V
p : G.Walk u v
q : G.Walk u w
hp : p.IsPath
hq : q.IsPath
hadj : G.Adj v w
hw : w ∈ p.support
⊢ v ∉ q.support

Tactic:
obtain ⟨p₀, p₁, hp₀, hp₁, happend⟩ := hp.mem_support_iff_exists_append.mp hw
  rw [← Subtype.mk.inj <| hG.subsingleton_path u w |>.elim ⟨p₀, hp₀⟩ ⟨q, hq⟩]
  exact fun hxp => (happend ▸ hp).ne_of_mem_support_of_append hadj.symm.ne' hxp
    (p₁.end_mem_support) rfl

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ (G.Connected ∧ ∀ (u v : V) (x y : G.Path u v), x = y) ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

Tactic:
constructor

Goal state after:
case mp
V : Type u_1
G : SimpleGraph V
⊢ (G.Connected ∧ ∀ (u v : V) (x y : G.Path u v), x = y) → Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath

case mpr
V : Type u_1
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath) → G.Connected ∧ ∀ (u v : V) (x y : G.Path u v), x = y
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsAdjMatrix
⊢ A.diag = 0

Tactic:
ext

Goal state after:
α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsAdjMatrix
x✝ : V
⊢ A.diag x✝ = 0 x✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝ : Fintype V
H : SimpleGraph W
m : ℕ
x✝ : ∃ G x, H.Free G ∧ m < #G.edgeFinset
w✝¹ : SimpleGraph V
w✝ : DecidableRel w✝¹.Adj
h : H.Free w✝¹
h' : m < #w✝¹.edgeFinset
⊢ m < #w✝¹.edgeFinset

Tactic:
convert!
    h'

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
⊢ A.compl.IsSymm

Tactic:
ext

Goal state after:
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : A.IsSymm
i✝ j✝ : V
⊢ A.complᵀ i✝ j✝ = A.compl i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
⊢ A.compl.compl = A

Tactic:
ext

Goal state after:
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A : Matrix V V α
hA : A.IsAdjMatrix
i✝ j✝ : V
⊢ A.compl.compl i✝ j✝ = A i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝¹ : Zero α
inst✝ : One α
⊢ adjMatrix α ⊥ = 0

Tactic:
ext

Goal state after:
α : Type u_1
V : Type u_2
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : V
⊢ adjMatrix α ⊥ i✝ j✝ = 0 i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G)ᵀ = adjMatrix α G

Tactic:
ext

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : V
⊢ (adjMatrix α G)ᵀ i✝ j✝ = adjMatrix α G i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
⊢ ⋯.toGraph = G

Tactic:
ext

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ⋯.toGraph.Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Zero α
inst✝¹ : One α
H : SimpleGraph W
inst✝ : DecidableRel H.Adj
f : G ↪g H
⊢ (adjMatrix α H).submatrix ⇑f ⇑f = adjMatrix α G

Tactic:
ext

Goal state after:
α : Type u_1
V : Type u_2
W : Type u_3
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Zero α
inst✝¹ : One α
H : SimpleGraph W
inst✝ : DecidableRel H.Adj
f : G ↪g H
i✝ j✝ : V
⊢ (adjMatrix α H).submatrix (⇑f) (⇑f) i✝ j✝ = adjMatrix α G i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝² : AddGroup α
inst✝¹ : One α
inst✝ : DecidableEq V
⊢ adjMatrix α (completeGraph V) = of 1 - 1

Tactic:
ext

Goal state after:
α : Type u_1
V : Type u_2
inst✝² : AddGroup α
inst✝¹ : One α
inst✝ : DecidableEq V
i✝ j✝ : V
⊢ adjMatrix α (completeGraph V) i✝ j✝ = (of 1 - 1) i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩
p : G.Walk u v
hp :
  p ∈
    Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑⟨x, hx⟩) v) ⊓
      Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑⟨y, hy⟩) v)
⊢ p ∈ ⊥

Tactic:
simp only [inf_eq_inter, mem_inter, mem_map] at hp

Goal state after:
case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩
p : G.Walk u v
hp :
  (∃ a ∈ G.finsetWalkLength n x v, { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } a = p) ∧
    ∃ a ∈ G.finsetWalkLength n y v, { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } a = p
⊢ p ∈ ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t : V
h :
  G.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
hn : ¬G.Adj s t
⊢ G.degree s = G.degree t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G✝ : SimpleGraph V
inst✝¹ : DecidableRel G✝.Adj
r : ℕ
s✝ t✝ : V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
s t : V
hn : ¬G.Adj s t
h : G.degree s ≠ G.degree t
cf : G.CliqueFree (r + 1)
hd : G.degree t < G.degree s
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
classical
  use G.replaceVertex s t, inferInstance, cf.replaceVertex s t
  have := G.card_edgeFinset_replaceVertex_of_not_adj hn
  lia

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h : G.IsTuranMaximal r
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
⊢ ¬G.Adj t u

Tactic:
rw [IsTuranMaximal, IsExtremal] at h

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
h :
  G.CliqueFree (r + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], G'.CliqueFree (r + 1) → #G'.edgeFinset ≤ #G.edgeFinset
hts : ¬G.Adj t s
hsu : ¬G.Adj s u
hst : ¬G.Adj s t
dst : G.degree s = G.degree t
dsu : G.degree s = G.degree u
⊢ ¬G.Adj t u
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ G.degree u = 1

Tactic:
degree_eq_one_iff_existsUnique_adj

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ ∃! w, G.Adj u w
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ G.degree v = 1

Tactic:
degree_eq_one_iff_existsUnique_adj

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ ∃! w, G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), ¬Odd w.length

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.Colorable 2 → ∀ (u : α) (w : G.Walk u u), ¬Odd w.length

case mpr
α : Type u_1
G : SimpleGraph α
⊢ (∀ (u : α) (w : G.Walk u u), ¬Odd w.length) → G.Colorable 2