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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
| fun x ↦ #(G.neighborFinset ↑x)

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
v : ↥s
| #(G.neighborFinset ↑v)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
⊢ ∀ x ∈ s ∪ t, x ∉ G.support.toFinset → G.degree x = 0

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
v : V
⊢ v ∈ s ∪ t → v ∉ G.support.toFinset → G.degree v = 0
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ w ∈ (G.connectedComponentMk v).supp

Tactic:
simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]

Goal state after:
case h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ G.Reachable w v
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
⊢ G.neighborSet w ⊆ (between s sᶜ G).neighborSet w ∪ sᶜ

Tactic:
intro v

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
⊢ v ∈ G.neighborSet w → v ∈ (between s sᶜ G).neighborSet w ∪ sᶜ
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ⊔ g b)

Tactic:
← inf_eq_inter,

Goal state after:
case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ⊓ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ⊔ g b)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #G.bipartiteDoubleCover.edgeFinset =
    #{x |
        match x with
        | (x, y) => G.Adj x y}

Tactic:
eq_comm

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #{x |
        match x with
        | (x, y) => G.Adj x y} =
    #G.bipartiteDoubleCover.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑p.length + ↑q.length

Tactic:
← Nat.cast_add,

Goal state after:
case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ ↑(p.length + q.length)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
⊢ G.dist u v ≠ 0

Tactic:
simp [h, hne]

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

Goal state before:
pp: α : 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
hf : Monotone f
hg : Monotone g
hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)
⊢ (∑ a, μ a * f a) * ∑ a, μ a * g a ≤ (∑ a, μ a) * ∑ a, μ a * (f a * g a)

Tactic:
refine four_functions_theorem_univ (μ * f) (μ * g) μ _ (mul_nonneg hμ₀ hf₀) (mul_nonneg hμ₀ hg₀)
    hμ₀ (mul_nonneg hμ₀ <| mul_nonneg hf₀ hg₀) (fun a b ↦ ?_)
  dsimp
  rw [mul_mul_mul_comm, ← mul_assoc (μ (a ⊓ b))]
  exact mul_le_mul (hμ _ _) (mul_le_mul (hf le_sup_left) (hg le_sup_right) (hg₀ _) <| hf₀ _)
    (mul_nonneg (hf₀ _) <| hg₀ _) <| mul_nonneg (hμ₀ _) <| hμ₀ _

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length + 1 =
    w'.ofBoxProdLeft.length + 1 +
      (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length

Tactic:
add_comm,

Goal state after:
case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
c : α × β
x : (G □ H).Adj (a₁, b₁) c
w' : (G □ H).Walk c (a₂, b₂)
h₁ : G.Adj a₁ c.1 ∧ b₁ = c.2
⊢ 1 + (w'.ofBoxProdLeft.length + w'.ofBoxProdRight.length) =
    w'.ofBoxProdLeft.length + 1 +
      (if h : H.Adj c.2 c.2 ∧ a₁ = c.1 then cons ⋯ w'.ofBoxProdRight else ⋯ ▸ w'.ofBoxProdRight).length
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
a₁ a₂ : α
w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)
⊢ G.Reachable a₁ a₂

Tactic:
exact ⟨w.ofBoxProdLeft⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ y.1 ∈ G.neighborFinset x.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ y.2 ∈ H.neighborFinset x.2 ↔
    (Equiv.refl (α × β)) y ∈ (G □ H).neighborSet x

Tactic:
mem_neighborFinset,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
V₁ : Type u_5
V₂ : Type u_6
W : Type u_7
W₁ : Type u_8
W₂ : Type u_9
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝¹ : Fintype ↑(G.neighborSet x.1)
inst✝ : Fintype ↑(H.neighborSet x.2)
y : α × β
⊢ G.Adj x.1 y.1 ∧ y.2 = x.2 ∨ y.1 = x.1 ∧ H.Adj x.2 y.2 ↔ (Equiv.refl (α × β)) y ∈ (G □ H).neighborSet x
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
  · intro ⟨w⟩
    exact ⟨⟨w.ofBoxProdLeft⟩, ⟨w.ofBoxProdRight⟩⟩
  · intro ⟨⟨w₁⟩, ⟨w₂⟩⟩
    exact ⟨(w₁.boxProdLeft _ _).append (w₂.boxProdRight _ _)⟩

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

Goal state before:
pp: n : ℕ
v w : Fin (n + 2)
⊢ v = w + 1 ∨ w = v + 1 ↔ w + 1 = v ∨ w = v + 1

Tactic:
eq_comm

Goal state after:
n : ℕ
v w : Fin (n + 2)
⊢ w + 1 = v ∨ w = v + 1 ↔ w + 1 = v ∨ w = v + 1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∀ {v : V},
    v ∈ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset) →
      ∃ s' ⊆ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset),
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
intro v

Goal state after:
case refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
⊢ v ∈ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset) →
    ∃ s' ⊆ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset),
      ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ ↑(G.finsetWalkLength n u v) ↔ p ∈ {p | p.length = n}

Tactic:
coe_finsetWalkLength_eq

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ {p | p.length = n} ↔ p ∈ {p | p.length = n}
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

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

Tactic:
· 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✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1} ∪ s ∩ {1})

Tactic:
rw [mulCayley_union]

Goal state after:
M : Type u_1
s : Set M
inst✝ : MulOneClass M
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
⊢ G.IsAcyclic

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
⊢ ∀ (c : G.Walk v v), ¬c.IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

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

Tactic:
intro v

Goal state after:
case mp
V : Type u_1
G : SimpleGraph V
hc : G.Connected
hu : ∀ (u v : V) (x y : G.Path u v), x = y
v : V
⊢ ∀ (w : V), ∃! p, p.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case mpr.refine_1
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ G.Preconnected

Tactic:
intro v

Goal state after:
case mpr.refine_1
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v : V
⊢ ∀ (v_1 : V), G.Reachable v v_1
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: α : Type u_1
V : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i j : V
⊢ ¬A i j = 1 ↔ A i j = 0

Tactic:
obtain h | h := h.zero_or_one i j <;> simp [h]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ Function.Injective fun v ↦ ⟨↑v, ⋯⟩

Tactic:
rintro v w

Goal state after:
n : ℕ
h : 2 ≤ n
v w : Fin 2
⊢ (fun v ↦ ⟨↑v, ⋯⟩) v = (fun v ↦ ⟨↑v, ⋯⟩) w → v = w
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
⊢ ∃ F, H ≤ F ∧ F ≤ G ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable

Tactic:
obtain ⟨F, hF⟩ := G.exists_maximal_isAcyclic_of_le_isAcyclic hH_le hH_isAcyclic
  grind [maximal_isAcyclic_iff_reachable_eq, Maximal]

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
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
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
v : V
⊢ v ∈ (G.replaceVertex s t).neighborFinset u ↔ v ∈ G.neighborFinset u \ {t}

Tactic:
mem_neighborFinset,

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
s t u : V
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
h : G.Adj t u
cf : G.CliqueFree (r + 1)
nst : s ≠ t
ntu : t ≠ u
this : ¬(G.replaceVertex s t).Adj s u
l1 : (G.replaceVertex s t).degree s = G.degree s
v : V
⊢ (G.replaceVertex s t).Adj u v ↔ v ∈ G.neighborFinset u \ {t}
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
⊢ z ∈ {v}ᶜ

Tactic:
Set.mem_compl_iff,

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
⊢ z ∉ {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.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ fp.part t = fp.part s ↔ fp.part s = fp.part t

Tactic:
eq_comm

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s t : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ fp.part s = fp.part t ↔ fp.part s = fp.part t
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
⊢ ∃ x, True

Tactic:
use ((pwu.append pux).toPath.val.induce {v}ᶜ ?_).copy (SetCoe.ext rfl) (SetCoe.ext rfl)
  /- Each path between vertex u and another vertex in G.induce {v}ᶜ
  is contained in G.induce {v}ᶜ. -/
  intro z hz
  rw [Set.mem_compl_iff, Set.mem_singleton_iff]
  obtain ⟨pwz, pzx, p_eq_pwzx⟩ := mem_support_iff_exists_append.mp hz
  /- Prove vertex v is not in the path formed from the concatenated walks
  by showing that vertex u must then be passed twice. -/
  by_contra
  subst_vars
  refine List.nodup_iff_forall_not_duplicate.mp (pwu.append pux).toPath.nodup_support u ?_
  rw [p_eq_pwzx, support_append, List.duplicate_iff_two_le_count, List.count_append]
  have := List.one_le_count_iff.mpr (pwz.getVert_mem_support (pwz.length - 1))
  simp only [hu _ (pwz.adj_penultimate (not_nil_of_ne (by aesop))).symm] at this
  have := List.one_le_count_iff.mpr (pzx.snd_mem_tail_support (not_nil_of_ne (by aesop)))
  rw [hu _ (pzx.adj_snd (not_nil_of_ne (by aesop)))] at this
  lia

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Finite V
inst✝ : Nontrivial V
hconn : G.Connected
T : SimpleGraph V
left✝ : T ≤ G
T_isTree : T.IsTree
hT : T.Connected
isAcyclic✝ : T.IsAcyclic
this : Fintype V
⊢ ∃ v, (induce {v}ᶜ G).Connected

Tactic:
classical
  obtain ⟨v, hv⟩ := T_isTree.exists_vert_degree_one_of_nontrivial
  exact ⟨v, (hT.induce_compl_singleton_of_degree_eq_one hv).mono (by tauto)⟩

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
this : G.Adj w₁ w₂
⊢ G.Adj
      (match a✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match b✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a✝ = b✝ ∧ ¬↑a✝ + 1 = ↑b✝ ∧ ¬↑b✝ + 1 = ↑a✝

Tactic:
have := h.adj.symm

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
this✝ : G.Adj w₁ w₂
this : G.Adj w₂ w₁
⊢ G.Adj
      (match a✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂)
      (match b✝ with
      | 0 => w₁
      | 1 => v
      | 2 => w₂) ↔
    ¬a✝ = b✝ ∧ ¬↑a✝ + 1 = ↑b✝ ∧ ¬↑b✝ + 1 = ↑a✝
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v → ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

pp: case mpr
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ (∃ n, (G.finsetWalkLength (↑n) u v).Nonempty) → G.Reachable u v

Tactic:
· intro r
    refine r.elim_path fun p => ?_
    refine ⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩
    simp [mem_finsetWalkLength_iff]

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ (∃ n, (G.finsetWalkLength (↑n) u v).Nonempty) → G.Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
| fun v ↦ (completeEquipartiteGraph r t).degree v

Tactic:
intro v

Goal state after:
r t : ℕ
v : Fin r × Fin t
| (completeEquipartiteGraph r t).degree v
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case injective'
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
hF : ∀ {c₁ c₂ : Fin n} {v₁ : ↑(C.colorClass c₁)} {v₂ : ↑(C.colorClass c₂)}, c₁ = c₂ → (F c₁) v₁ = (F c₂) v₂ → ↑v₁ = ↑v₂
⊢ Injective ⇑{ toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ }

Tactic:
intro v

Goal state after:
case injective'
α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
this : ∀ (c : Fin n), Nonempty (↑(C.colorClass c) ↪ Fin t)
F : (c : Fin n) → ↑(C.colorClass c) ↪ Fin t
hF : ∀ {c₁ c₂ : Fin n} {v₁ : ↑(C.colorClass c₁)} {v₂ : ↑(C.colorClass c₂)}, c₁ = c₂ → (F c₁) v₁ = (F c₂) v₂ → ↑v₁ = ↑v₂
v : α
⊢ ∀ ⦃a₂ : α⦄,
    { toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ } v =
        { toFun := fun v ↦ (C v, (F (C v)) ⟨v, ⋯⟩), map_rel' := ⋯ } a₂ →
      v = a₂
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case inj'
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
⊢ ∀ ⦃a₂ : Fin r × Fin t⦄,
    (fun x ↦
            match x with
            | (i, j) => ↑((fₜ (fᵣ i)) j))
          (i₁, j₁) =
        (fun x ↦
            match x with
            | (i, j) => ↑((fₜ (fᵣ i)) j))
          a₂ →
      (i₁, j₁) = a₂

Tactic:
(i₂, j₂)

Goal state after:
case inj'
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
⊢ (fun x ↦
          match x with
          | (i, j) => ↑((fₜ (fᵣ i)) j))
        (i₁, j₁) =
      (fun x ↦
          match x with
          | (i, j) => ↑((fₜ (fᵣ i)) j))
        (i₂, j₂) →
    (i₁, j₁) = (i₂, j₂)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
u : α
h : ∀ (v : α), ∃ w, ¬G.Reachable v w
⊢ G.eccent u = ⊤

Tactic:
obtain ⟨v, h⟩ := h u

Goal state after:
α : Type u_1
G : SimpleGraph α
u : α
h✝ : ∀ (v : α), ∃ w, ¬G.Reachable v w
v : α
h : ¬G.Reachable u v
⊢ G.eccent u = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
u : α
⊢ ∀ (i : α), ⊤.edist u i ≤ 1

Tactic:
intro v

Goal state after:
α : Type u_1
inst✝ : Nontrivial α
u v : α
⊢ ⊤.edist u v ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
⊢ ∀ (v : α), G.edist u v ≤ 1

Tactic:
intro v

Goal state after:
case mpr
α : Type u_1
G : SimpleGraph α
u : α
hall : ∀ (v : α), u ≠ v → G.Adj u v
v : α
⊢ G.edist u v ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
n : ℕ
⊢ #(turanGraph n 0).edgeFinset = (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

pp: case inr
n r : ℕ
hr : r > 0
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2

Tactic:
· rw [Nat.mod_zero, tsub_self, zero_mul, Nat.zero_div, zero_add]
    have := card_edgeFinset_top_eq_card_choose_two (V := Fin n)
    rw [Fintype.card_fin] at this; convert! this; exact turanGraph_zero

Goal state after:
case inr
n r : ℕ
hr : r > 0
⊢ #(turanGraph n r).edgeFinset = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inr.inr.e_a.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) * (r - 1)

Tactic:
add_comm,

Goal state after:
case inr.inr.e_a.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 * r + n' % r) * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk vnL
⊢ s K = G.componentComplMk ⋯

Tactic:
by
  rw [← sec h, hs]
  apply ComponentCompl.hom_mk _ (le_of_op_hom h)

Goal state after: