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

Goal state before:
pp: case refine_1.inr
W₁ : Type u_2
W₂ : Type u_3
v : W₁ ⊕ W₂
val✝ : W₂
h : s(Sum.inr val✝, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

Tactic:
cases v

Goal state after:
case refine_1.inr.inl
W₁ : Type u_2
W₂ : Type u_3
val✝¹ : W₂
val✝ : W₁
h : s(Sum.inr val✝¹, Sum.inl val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝¹, Sum.inl val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

case refine_1.inr.inr
W₁ : Type u_2
W₂ : Type u_3
val✝¹ val✝ : W₂
h : s(Sum.inr val✝¹, Sum.inr val✝) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(Sum.inr val✝¹, Sum.inr val✝) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
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
f : G →g G'
g : H →g H'
v : V ⊕ W
val✝ : V
⊢ (G ⊕g H).Adj (Sum.inl val✝) v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝)) (Sum.map (⇑f) (⇑g) v)

Tactic:
cases v

Goal state after:
case inl.inl
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
f : G →g G'
g : H →g H'
val✝¹ val✝ : V
⊢ (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inl val✝))

case inl.inr
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
f : G →g G'
g : H →g H'
val✝¹ : V
val✝ : W
⊢ (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inr val✝))
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
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
f : G →g G'
g : H →g H'
v : V ⊕ W
val✝ : W
⊢ (G ⊕g H).Adj (Sum.inr val✝) v → (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝)) (Sum.map (⇑f) (⇑g) v)

Tactic:
cases v

Goal state after:
case inr.inl
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
f : G →g G'
g : H →g H'
val✝¹ : W
val✝ : V
⊢ (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inl val✝))

case inr.inr
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
f : G →g G'
g : H →g H'
val✝¹ val✝ : W
⊢ (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inr val✝))
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
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
f : G ↪g G'
g : H ↪g H'
v : V ⊕ W
val✝ : V
⊢ Sum.map (⇑f) (⇑g) (Sum.inl val✝) = Sum.map (⇑f) (⇑g) v → Sum.inl val✝ = v

Tactic:
cases v

Goal state after:
case inl.inl
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
f : G ↪g G'
g : H ↪g H'
val✝¹ val✝ : V
⊢ Sum.map (⇑f) (⇑g) (Sum.inl val✝¹) = Sum.map (⇑f) (⇑g) (Sum.inl val✝) → Sum.inl val✝¹ = Sum.inl val✝

case inl.inr
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
f : G ↪g G'
g : H ↪g H'
val✝¹ : V
val✝ : W
⊢ Sum.map (⇑f) (⇑g) (Sum.inl val✝¹) = Sum.map (⇑f) (⇑g) (Sum.inr val✝) → Sum.inl val✝¹ = Sum.inr val✝
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
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
f : G ↪g G'
g : H ↪g H'
v : V ⊕ W
val✝ : W
⊢ Sum.map (⇑f) (⇑g) (Sum.inr val✝) = Sum.map (⇑f) (⇑g) v → Sum.inr val✝ = v

Tactic:
cases v

Goal state after:
case inr.inl
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
f : G ↪g G'
g : H ↪g H'
val✝¹ : W
val✝ : V
⊢ Sum.map (⇑f) (⇑g) (Sum.inr val✝¹) = Sum.map (⇑f) (⇑g) (Sum.inl val✝) → Sum.inr val✝¹ = Sum.inl val✝

case inr.inr
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
f : G ↪g G'
g : H ↪g H'
val✝¹ val✝ : W
⊢ Sum.map (⇑f) (⇑g) (Sum.inr val✝¹) = Sum.map (⇑f) (⇑g) (Sum.inr val✝) → Sum.inr val✝¹ = Sum.inr val✝
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
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
f : G ↪g G'
g : H ↪g H'
v : V ⊕ W
val✝ : V
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } v) ↔
    (G ⊕g H).Adj (Sum.inl val✝) v

Tactic:
cases v

Goal state after:
case inl.inl
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
f : G ↪g G'
g : H ↪g H'
val✝¹ val✝ : V
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝¹))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
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
f : G ↪g G'
g : H ↪g H'
val✝¹ : V
val✝ : W
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝¹))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
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
f : G ↪g G'
g : H ↪g H'
v : V ⊕ W
val✝ : W
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝)) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } v) ↔
    (G ⊕g H).Adj (Sum.inr val✝) v

Tactic:
cases v

Goal state after:
case inr.inl
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
f : G ↪g G'
g : H ↪g H'
val✝¹ : W
val✝ : V
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝¹))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
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
f : G ↪g G'
g : H ↪g H'
val✝¹ val✝ : W
⊢ (G' ⊕g H').Adj ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝¹))
      ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inl
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
f : G ≃g G'
g : H ≃g H'
v : V ⊕ W
val✝ : V
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ((f.sumCongr g.toEquiv) v) ↔ (G ⊕g H).Adj (Sum.inl val✝) v

Tactic:
cases v

Goal state after:
case inl.inl
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
f : G ≃g G'
g : H ≃g H'
val✝¹ val✝ : V
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inl val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
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
f : G ≃g G'
g : H ≃g H'
val✝¹ : V
val✝ : W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inl val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
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
f : G ≃g G'
g : H ≃g H'
v : V ⊕ W
val✝ : W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ((f.sumCongr g.toEquiv) v) ↔ (G ⊕g H).Adj (Sum.inr val✝) v

Tactic:
cases v

Goal state after:
case inr.inl
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
f : G ≃g G'
g : H ≃g H'
val✝¹ : W
val✝ : V
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inr val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inl val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
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
f : G ≃g G'
g : H ≃g H'
val✝¹ val✝ : W
⊢ (G' ⊕g H').Adj ((f.sumCongr g.toEquiv) (Sum.inr val✝¹)) ((f.sumCongr g.toEquiv) (Sum.inr val✝)) ↔
    (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
w₁ : G.Walk x.1 y.1
⊢ (G □ H).Reachable x y

Tactic:
obtain ⟨w₂⟩ := hH x.2 y.2

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Preconnected
hH : H.Preconnected
x y : α × β
w₁ : G.Walk x.1 y.1
w₂ : H.Walk 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.LeftInverse
    (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:
by rintro ⟨⟨u | u, v | v⟩, h⟩ <;> first | contradiction | rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (induce s G).Connected ↔ (⊤.induce s).Connected

Tactic:
rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff']

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

Goal state before:
pp: case inl
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
cG : G.Coloring γ
cH : H.Coloring γ
v : V ⊕ W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝) v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝)) (Sum.elim (⇑cG) (⇑cH) v)

Tactic:
cases v

Goal state after:
case inl.inl
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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : V
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

case inl.inr
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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : V
val✝ : W
huv : (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: case inr
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
cG : G.Coloring γ
cH : H.Coloring γ
v : V ⊕ W
val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝) v
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝)) (Sum.elim (⇑cG) (⇑cH) v)

Tactic:
cases v

Goal state after:
case inr.inl
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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ : W
val✝ : V
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inl val✝))

case inr.inr
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
cG : G.Coloring γ
cH : H.Coloring γ
val✝¹ val✝ : W
huv : (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝)
⊢ (completeGraph γ).Adj (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝¹)) (Sum.elim (⇑cG) (⇑cH) (Sum.inr val✝))
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set M
G : SimpleGraph M
⊢ (fun x ↦ mulCayley x) S ≤ G ↔ S ⊆ (fun x ↦ {g | ∀ (a : M), a * g ≠ a → x.Adj (a * g) a}) G

Tactic:
simp [mulCayley_le_iff, Set.subset_def]

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s ∨ v - u ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
cases h1 with
      | inl h1 => exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩
      | inr h1 => exact Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩

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

Goal state before:
pp: n r : ℕ
hr : 0 < r
⊢ IsEmpty ((completeGraph (Fin (r + 1))).Copy (turanGraph n r))

Tactic:
by_contra! ⟨f⟩

Goal state after:
n r : ℕ
hr : 0 < r
f : (completeGraph (Fin (r + 1))).Copy (turanGraph n r)
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ Odd (Nat.card ↑{c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}) ↔ Odd (Nat.card ↑c'.supp)

Tactic:
cases nonempty_fintype V

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
⊢ Odd (Nat.card ↑{c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}) ↔ Odd (Nat.card ↑c'.supp)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)

Tactic:
cases nonempty_fintype V

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
val✝ : Fintype V
⊢ Odd G.oddComponents.ncard ↔ Odd (Nat.card V)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg
α : 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)
f : Fin r × Fin t ↪ V :=
  {
    toFun := fun x ↦
      match x with
      | (i, j) => ↑((fₜ (fᵣ i)) j),
    inj' := ⋯ }
a✝ b✝ : Fin r × Fin t
hne : (completeEquipartiteGraph r t).Adj a✝ b✝
⊢ G.Adj (f a✝) (f b✝)

Tactic:
refine K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop

Goal state after:
case neg
α : 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)
f : Fin r × Fin t ↪ V :=
  {
    toFun := fun x ↦
      match x with
      | (i, j) => ↑((fₜ (fᵣ i)) j),
    inj' := ⋯ }
a✝ b✝ : Fin r × Fin t
hne : (completeEquipartiteGraph r t).Adj a✝ b✝
⊢ ↑(fᵣ a✝.1) ≠ ↑(fᵣ b✝.1)
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
h : G.Connected
⊢ G.radius ≠ ⊤

Tactic:
obtain ⟨u, v, huv⟩ := G.exists_edist_eq_radius_of_finite

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
h : G.Connected
u v : α
huv : G.edist u v = G.radius
⊢ G.radius ≠ ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ ¬G.radius = ⊤ → ¬G.ediam = ⊤

Tactic:
intro hr

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
hr : ¬G.radius = ⊤
⊢ ¬G.ediam = ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties

Goal state before:
pp: V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property✝ : s ∈ G.end
⊢ False

Tactic:
cases nonempty_fintype V

Goal state after:
case intro
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property✝ : s ∈ G.end
val✝ : Fintype V
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
· refine ⟨univ.map ⟨fun i ↦ univ.map ⟨fun j ↦ f (i, j), fun _ _ h ↦ ?_⟩, fun i₁ i₂ h ↦ ?_⟩,
      ?_, fun h ↦ ?_, fun _ h₁ _ h₂ hne _ h₁' _ h₂' ↦ ?_⟩
    · simpa using f.injective h
    · simp_rw [Finset.ext_iff] at h
      have : NeZero t := ⟨ht⟩
      obtain ⟨_, heq⟩ : ∃ j, f (i₁, j) = f (i₂, 0) := by simpa using h <| f (i₂, 0)
      apply f.injective at heq
      rw [Prod.mk.injEq] at heq
      exact heq.left
    · simp
    · simp_rw [mem_map, mem_univ, Embedding.coeFn_mk, true_and] at h
      replace ⟨_, h⟩ := h
      simp [← h]
    · simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁ h₂
      replace ⟨_, h₁⟩ := h₁
      replace ⟨_, h₂⟩ := h₂
      rw [← h₁] at h₁'
      rw [← h₂] at h₂'
      simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁' h₂'
      replace ⟨_, h₁'⟩ := h₁'
      replace ⟨_, h₂'⟩ := h₂'
      rw [← h₁', ← h₂']
      apply f.toHom.map_adj
      simp_rw [completeEquipartiteGraph_adj]
      contrapose hne with heq
      simp_rw [← h₁, ← h₂, heq]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
x✝ : (Finset V)ᵒᵖ
⊢ ↾ComponentCompl.hom ⋯ = 𝟙 (G.ComponentCompl ↑(Opposite.unop x✝))

Tactic:
by
    ext
    simp [ComponentCompl.hom_refl]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
x✝ Y Z : (Finset V)ᵒᵖ
h : x✝ ⟶ Y
h' : Y ⟶ Z
⊢ ↾ComponentCompl.hom ⋯ = ↾ComponentCompl.hom ⋯ ≫ ↾ComponentCompl.hom ⋯

Tactic:
ext C

Goal state after:
V : Type u
G : SimpleGraph V
K L M : Set V
x✝¹ Y Z : (Finset V)ᵒᵖ
h : x✝¹ ⟶ Y
h' : Y ⟶ Z
C : G.ComponentCompl ↑(Opposite.unop x✝¹)
x✝ : V
⊢ x✝ ∈ ((ConcreteCategory.hom (↾ComponentCompl.hom ⋯)).toFun C).supp ↔
    x✝ ∈ ((ConcreteCategory.hom (↾ComponentCompl.hom ⋯ ≫ ↾ComponentCompl.hom ⋯)).toFun C).supp
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑(#G.edgeFinset * (n - 1)) ≤ ↑((n + 1) * extremalNumber n H)

Tactic:
Nat.cast_le

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset * (n - 1) ≤ (n + 1) * extremalNumber n H
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ ↑(2 * #G.edgeFinset) ≤ ↑(zarankiewicz n n s t)

Tactic:
Nat.cast_le

Goal state after:
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ 2 * #G.edgeFinset ≤ zarankiewicz n n s t
Module: Mathlib.Combinatorics.SimpleGraph.Hall

Goal state before:
pp: case h.inl
V : Type u_1
G : SimpleGraph V
inst✝ : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard
f : ↑p₁ → V
hf₁ : Injective f
hf₂ : ∀ (x : ↑p₁), f x ∈ G.neighborFinset ↑x
this : ∀ (x : ↑p₁), f x ∉ p₁
v : V
h' : v ∈ p₁
⊢ ∃! w, if h : v ∈ p₁ then f ⟨v, h⟩ = w else if h : w ∈ p₁ then f ⟨w, h⟩ = v else False

Tactic:
exact ⟨f ⟨v, h'⟩, by simp_all⟩

Goal state after: