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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ 0 < p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ 0 < p.length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ ↑k ≠ ⊤

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ ↑k ≠ ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ 1 ≠ ⊤

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ 1 ≠ ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i' ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i' ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
hl : p.getVert i' = p.getVert i
right✝ : p.getVert (i' + 1) = v
⊢ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ≤ p.length
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (a ⊓ b) * g (b ⊔ a))

Tactic:
inf_comm

Goal state after:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ μ b * (f b * g a) ≤ μ (b ⊔ a) * (f (b ⊓ a) * g (b ⊔ a))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i - 1 ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i - 1 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i + 1 ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ i + 1 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ i ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ 0 ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ 0 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ i + 1 ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ i + 1 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this : p.tail.tail.length < p.tail.length
⊢ p.tail.length < p.tail.length + 1

Tactic:
;

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : p.length = G.dist v w
hl : 1 < G.dist v w
hnp : ¬p.Nil
this : p.tail.tail.length < p.tail.length
⊢ p.tail.length < p.tail.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ 0 ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ 0 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
v : V
⊢ v ∈ p.toSubgraph.neighborSet u ↔ v ∈ {p.snd, p.penultimate}

Tactic:
simp_all only [Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
    SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
⊢ (∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) ↔
    v = p.snd ∨ v = p.penultimate
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (Walk.boxProdLeft H b (cons' x y z h w)).ofBoxProdLeft = cons' x y z h w

Tactic:
rw [Walk.boxProdLeft, map_cons, ofBoxProdLeft, Or.by_cases, dif_pos, ← Walk.boxProdLeft]
    · simp [ofBoxProdLeft_boxProdLeft]
    · exact ⟨h, rfl⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i' ≤ p.length - 1

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i' ≤ p.length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i ≤ p.length - 1

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i ≤ p.length - 1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ 1 ≤ i' + 1 ∧ i' + 1 ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ 1 ≤ i' + 1 ∧ i' + 1 ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ 1 ≤ i ∧ i ≤ p.length

Tactic:
;

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ 1 ≤ i ∧ i ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
⊢ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Tactic:
toSubgraph_reverse _

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
⊢ p.toSubgraph.verts = p.toSubgraph.verts
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
⊢ H.Preconnected

Tactic:
by
  classical
  rintro b₁ b₂
  obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
  exact ⟨w.ofBoxProdRight⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤)
⊢ G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤)
⊢ G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
⊢ ((Walk.map (G.boxProdLeft H x.2).toHom wG).append (Walk.map (G.boxProdRight H y.1).toHom wH)).length =
    wG.length + wH.length

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
⊢ ((Walk.map (G.boxProdLeft H x.2).toHom wG).append (Walk.map (G.boxProdRight H y.1).toHom wH)).length =
    wG.length + wH.length
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hH : H.Connected
hG : G.Preconnected
nonempty✝ : Nonempty V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected

Tactic:
;

Goal state after:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hH : H.Connected
hG : G.Preconnected
nonempty✝ : Nonempty V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
x✝ : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable (max n n)

Tactic:
;

Goal state after:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
x✝ : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable (max n n)
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n✝ : ℕ
⊢ DecidableRel
    (match n✝ + 2 with
      | 0 => ⊥
      | 1 => ⊥
      | n.succ.succ => { Adj := fun a b ↦ a - b = 1 ∨ b - a = 1, symm := ⋯, loopless := ⋯ }).Adj

Tactic:
;

Goal state after:
n✝ : ℕ
⊢ DecidableRel
    (match n✝ + 2 with
      | 0 => ⊥
      | 1 => ⊥
      | n.succ.succ => { Adj := fun a b ↦ a - b = 1 ∨ b - a = 1, symm := ⋯, loopless := ⋯ }).Adj
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ¬H ⊑ G
⊢ ¬extremalNumber (Fintype.card V) H < #G.edgeFinset

Tactic:
;

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ¬H ⊑ G
⊢ ¬extremalNumber (Fintype.card V) H < #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
⊢ (A ⊙ A) i j = A i j

Tactic:
;

Goal state after:
α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
⊢ (A ⊙ A) i j = A i j
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
this : A i j = 0 ∨ A i j = 1
⊢ (A ⊙ A) i j = A i j

Tactic:
;

Goal state after:
α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
this : A i j = 0 ∨ A i j = 1
⊢ (A ⊙ A) i j = A 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 B : Matrix V V α
hA : A.IsAdjMatrix
hB : B.IsAdjMatrix
i j : V
h :
  (fun i j ↦ if i = j then 0 else if A i j = 0 then 1 else 0) = fun i j ↦
    if i = j then 0 else if B i j = 0 then 1 else 0
⊢ A i j = B i j

Tactic:
;

Goal state after:
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
inst✝¹ : Zero α
inst✝ : One α
A B : Matrix V V α
hA : A.IsAdjMatrix
hB : B.IsAdjMatrix
i j : V
h :
  (fun i j ↦ if i = j then 0 else if A i j = 0 then 1 else 0) = fun i j ↦
    if i = j then 0 else if B i j = 0 then 1 else 0
⊢ A i j = B 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
i✝ j✝ : V
⊢ (if i✝ = j✝ then 0 else if ¬i✝ = j✝ → A i✝ j✝ = 0 → 1 = 0 then 1 else 0) = A i✝ j✝

Tactic:
;

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
⊢ (if i✝ = j✝ then 0 else if ¬i✝ = j✝ → A i✝ j✝ = 0 → 1 = 0 then 1 else 0) = A i✝ j✝
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

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

Tactic:
;

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✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
H : SimpleGraph V
inst✝ : DecidableRel H.Adj
h : IsCompl G H
this : Gᶜ = H
⊢ adjMatrix α G + adjMatrix α H = adjMatrix α G + adjMatrix α Gᶜ

Tactic:
;

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
H : SimpleGraph V
inst✝ : DecidableRel H.Adj
h : IsCompl G H
this : Gᶜ = H
⊢ adjMatrix α G + adjMatrix α H = adjMatrix α G + adjMatrix α Gᶜ
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
inst✝ : DecidableRel Gᶜ.Adj
h : IsCompl G Gᶜ
⊢ adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α G + adjMatrix α Gᶜ

Tactic:
;

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : AddZeroClass α
inst✝¹ : One α
inst✝ : DecidableRel Gᶜ.Adj
h : IsCompl G Gᶜ
⊢ adjMatrix α G + adjMatrix α Gᶜ = adjMatrix α G + adjMatrix α Gᶜ
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : 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✝

Tactic:
;

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: α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i ↦ adjMatrix α G i v) = adjMatrix α G v

Tactic:
;

Goal state after:
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
v : V
vec : V → α
⊢ (fun i ↦ adjMatrix α G i v) = adjMatrix α G v
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.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

Tactic:
;

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