mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
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 α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∉ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ t) * f₄ (insert a s ∪ t) + f₃ (insert a (s ∩ t)) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ t) + f₃ (insert a (s ∩ t))) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
insert_union,

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
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 α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∉ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₃ (s ∩ t) * f₄ (insert a (s ∪ t)) + f₃ (insert a (s ∩ t)) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ t) + f₃ (insert a (s ∩ t))) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
h : G = ⊥
⊢ ∀ {a b : V}, ⊥.Adj a b → (completeGraph (Fin 1)).Adj (0 a) (0 b)

Tactic:
by simp

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

Goal state before:
pp: case inl
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ #𝒜 ≤ (n - 1).choose (r - 1)

pp: case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
⊢ #𝒜 ≤ (n - 1).choose (r - 1)

Tactic:
· convert! Nat.zero_le _
    rw [Finset.card_eq_zero, eq_empty_iff_forall_notMem]
    refine fun A HA ↦ h𝒜 HA HA ?_
    rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b]
    exact h₂ HA

Goal state after:
case inr
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
⊢ #𝒜 ≤ (n - 1).choose (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
C : G.Coloring α
⊢ card α ≤ card (Fin (card α))

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p : (G.deleteEdges {s(v, w)}).Walk v' w'
⊢ G.deleteEdges {s(v, w)} ≤ G

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ n ≤ card (Fin n)

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : card α ≤ sInf {n' | G.Colorable n'}
C : G.Coloring α
i : α
hi : ∀ (a : V), C a ≠ i
D : G.Coloring { a // a ≠ i } := { toFun := fun v ↦ ⟨C v, ⋯⟩, map_rel' := ⋯ }
⊢ card { a // a ≠ i } = card (Fin (card α - 1))

Tactic:
by simp

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

Goal state before:
pp: V : Type u
inst✝ : Nonempty V
⊢ ⊥.Colorable 1

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Finset V
h : G.IsClique ↑s
⊢ s.card ≤ Nat.card ↥s

Tactic:
by simp

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

Goal state before:
pp: V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι✝ : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
ι : Type u_4
V : ι → Type u_5
⊢ ∀ {v w : (i : ι) × V i}, (completeMultipartiteGraph V).Adj v w → v.fst ≠ w.fst

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
hadj : G.Adj v w
⊢ w ∈ t

Tactic:
apply h.mem_of_adj at hadj
  have nhv : v ∉ t := Set.disjoint_left.mp h.disjoint hv
  simpa [hv, nhv] using hadj

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet w)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ Disjoint (G.neighborFinset w) t

Tactic:
by
  rw [neighborFinset_def, ← disjoint_coe, Set.coe_toFinset]
  exact isBipartiteWith_neighborSet_disjoint' h hw

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

Goal state before:
pp: case refine_2.inr
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk : k ≠ 0
h : ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeReachable k u v
s : Set (Sym2 V)
hs : s.encard < ↑(k + 1)
e : Sym2 V
he : e ∈ s
⊢ (G.deleteEdges s).Reachable u v

Tactic:
rw [← Set.insert_sdiff_self_of_mem he, Set.insert_eq, ← deleteEdges_deleteEdges]
    refine h e <| ENat.add_lt_add_iff_right ENat.one_ne_top |>.mp ?_
    rwa [Set.encard_sdiff_singleton_add_one he]

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

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

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).toSubgraph = G.subgraphOfAdj h

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ (Subtype.val ∘ ⇑fα) (s₁.getLeft hs₁) ∈ ↑left

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isLeft = true
hs₂ : s₂.isRight = true
⊢ (Subtype.val ∘ ⇑fβ) (s₂.getRight hs₂) ∈ ↑right

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ (Subtype.val ∘ ⇑fα) (s₂.getLeft hs₂) ∈ ↑left

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
f : α ⊕ β ↪ V := { toFun := Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ), inj' := ⋯ }
s₁ s₂ : α ⊕ β
hs₁ : s₁.isRight = true
hs₂ : s₂.isLeft = true
⊢ (Subtype.val ∘ ⇑fβ) (s₁.getRight hs₁) ∈ ↑right

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝ : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
⊢ #(map { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } univ) = Fintype.card α

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝ : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
⊢ #(map { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } univ) = Fintype.card β

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ x✝ : V
w✝¹ : α
left✝¹ : w✝¹ ∈ univ
hl : { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } w✝¹ = x✝¹
w✝ : β
left✝ : w✝ ∈ univ
hr : { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } w✝ = x✝
⊢ (completeBipartiteGraph α β).Adj (Sum.inl w✝¹) (Sum.inr w✝)

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
x✝ : Infinite V
⊢ 4 * G.edgeSet.encard ≤ ENat.card V ^ 2

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val✝¹ val✝ : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inl val✝¹) (Sum.inr val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val✝¹ val✝ : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inr val✝¹) (Sum.inl val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun w ↦ ↑w.length) = G.edist v u

Tactic:
← Set.image_univ,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf ((fun w ↦ ↑w.length) '' Set.univ) = G.edist v u
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v

Tactic:
by
  by_cases huv : u = v
  · simp [huv]
  · simp only [huv, or_false]
    have h : 0 < G.edist u v := edist_pos_of_ne huv
    rw [(Order.one_le_iff_pos.mpr h).ge_iff_eq']
    exact edist_eq_one_iff_adj

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
⊢ G.dist v v = 0

Tactic:
by simp

Goal state after:
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
u v : V
⊢ (fun u ↦ Sum.inl u) u = (fun u ↦ Sum.inl u) v → u = v

Tactic:
by simp

Goal state after:
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
⊢ ∀ {a b : V},
    (G ⊕g H).Adj ({ toFun := fun u ↦ Sum.inl u, inj' := ⋯ } a) ({ toFun := fun u ↦ Sum.inl u, inj' := ⋯ } b) ↔ G.Adj a b

Tactic:
by simp

Goal state after:
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' u v : W
⊢ (fun u ↦ Sum.inr u) u = (fun u ↦ Sum.inr u) v → u = v

Tactic:
by simp

Goal state after:
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
⊢ ∀ {a b : W},
    (G ⊕g H).Adj ({ toFun := fun u ↦ Sum.inr u, inj' := ⋯ } a) ({ toFun := fun u ↦ Sum.inr u, inj' := ⋯ } b) ↔ H.Adj a b

Tactic:
by simp

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 β
G : SimpleGraph V
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
⊢ ∀ {a b : V × (W₁ ⊕ W₂)},
    (G □ H₁ ⊕g G □ H₂).Adj ((Equiv.prodSumDistrib V W₁ W₂) a) ((Equiv.prodSumDistrib V W₁ W₂) b) ↔
      (G □ (H₁ ⊕g H₂)).Adj a b

Tactic:
by simp

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 β
G₁ : SimpleGraph V₁
G₂ : SimpleGraph V₂
H : SimpleGraph W
⊢ ∀ {a b : (V₁ ⊕ V₂) × W},
    (G₁ □ H ⊕g G₂ □ H).Adj ((Equiv.sumProdDistrib V₁ V₂ W) a) ((Equiv.sumProdDistrib V₁ V₂ W) b) ↔
      ((G₁ ⊕g G₂) □ H).Adj a b

Tactic:
by simp

Goal state after:
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
e : Sym2 V
he : e ∈ G.edgeSet
⊢ ∀ (a b : V) (h : G.Adj a b), ⟨s(Sum.inl a, Sum.inl b), h⟩ = ⟨s(Sum.inl b, Sum.inl a), ⋯⟩

Tactic:
by simp

Goal state after:
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
e : Sym2 W
he : e ∈ H.edgeSet
⊢ ∀ (a b : W) (h : H.Adj a b), ⟨s(Sum.inr a, Sum.inr b), h⟩ = ⟨s(Sum.inr b, Sum.inr a), ⋯⟩

Tactic:
by simp

Goal state after:
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
⊢ ¬(G ⊕g H).Adj (Sum.inl v) (Sum.inr w)

Tactic:
by simp

Goal state after:
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
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
hs : ∀ (x : V ⊕ W), x ∉ Set.range Sum.inl ↔ x ∈ Set.range Sum.inr
⊢ Sum.inl v ∈ Set.range Sum.inl

Tactic:
by simp

Goal state after:
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
p : (G ⊕g H).Walk (Sum.inl v) (Sum.inr w)
hs : ∀ (x : V ⊕ W), x ∉ Set.range Sum.inl ↔ x ∈ Set.range Sum.inr
⊢ Sum.inr w ∉ Set.range Sum.inl

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
s t : Set V
sconn : (H.induce s).Preconnected
tconn : (H.induce t).Preconnected
sintert : (s ⊓ t).Nonempty
⊢ (H.induce s ⊔ H.induce t).verts = (H.induce (s ∪ t)).verts

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
⊢ a ∈ ↑{a, b, c}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
⊢ b ∈ ↑{a, b, c}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this : (hasse α).Adj a b
⊢ b ∈ ↑{a, b, c}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this : (hasse α).Adj a b
⊢ c ∈ ↑{a, b, c}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this✝ : (hasse α).Adj a b
this : (hasse α).Adj b c
⊢ a ∈ ↑{a, b, c}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
hc : (hasse α).IsClique ↑{a, b, c}
hcard : {a, b, c}.card = 3
this✝ : (hasse α).Adj a b
this : (hasse α).Adj b c
⊢ c ∈ ↑{a, b, c}

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ left.toLeft
j : V
hj : j ∈ left.toLeft
⊢ Sum.inl i = Sum.inl j → i = j

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ 3 ≤ (cycle n).length

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ right.toRight
j : V
hj : j ∈ right.toRight
⊢ Sum.inr i = Sum.inr j → i = j

Tactic:
by simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
⊢ ∃ t', t ⊆ t' ∧ (induce (↑t') G).Connected

Tactic:
classical
  obtain ⟨u, ut⟩ := tn
  refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
  · simp only [Finset.mem_biUnion, List.mem_toFinset]
    exact ⟨v, vt, Walk.end_mem_support _⟩
  · apply G.induce_connected_of_patches u
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
                 Set.mem_ofPred_eq, Walk.start_mem_support, exists_prop, and_true]
      exact ⟨u, ut⟩
    intro v hv
    simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
    obtain ⟨w, wt, hw⟩ := hv
    refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
    · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
      exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
    · simp only [Set.mem_ofPred_eq, Walk.start_mem_support, exists_true_left]
      refine ⟨hw, Walk.connected_induce_support _ _ _⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n✝ : ℕ
u v : V
n : ℕ
w : ↑(G.neighborSet u)
x✝¹ x✝ : G.Walk (↑w) v
⊢ (fun p ↦ Walk.cons ⋯ p) x✝¹ = (fun p ↦ Walk.cons ⋯ p) x✝ → x✝¹ = x✝

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ left.toRight
j : V
hj : j ∈ left.toRight
⊢ Sum.inr i = Sum.inr j → i = j

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ right.toLeft
j : V
hj : j ∈ right.toLeft
⊢ Sum.inl i = Sum.inl j → i = j

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ∀ ⦃v w : V ⊕ V⦄,
    G.bipartiteDoubleCover.Adj v w →
      v ∈ {v | v.isLeft = true} ∧ w ∈ {w | w.isRight = true} ∨ v ∈ {w | w.isRight = true} ∧ w ∈ {v | v.isLeft = true}

Tactic:
by simp

Goal state after: