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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : s.Intersecting
⊢ s ≠ {⊥}

pp: case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False

Tactic:
· rintro rfl
    exact intersecting_singleton.1 h rfl

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
h : (s.Pairwise fun a b ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Tactic:
by
  rw [← isLowerSet_compl, ← coe_compl] at h𝒜
  have := h𝒜.card_inter_le_finset hℬ
  rwa [card_compl, Fintype.card_finset, tsub_mul, le_tsub_iff_le_tsub, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
  · grw [inter_subset_right]
  · grw [← Fintype.card_finset, card_le_univ]

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

Goal state before:
pp: case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
⊢ #((cons i s hi).biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi))

Tactic:
have hf₁ : ∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * #(f' j) =
      2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting := by
    rintro j hj
    simp_rw [f', dif_pos hj, ← Fintype.card_finset]
    exact Classical.choose_spec (hf j hj).exists_card_eq

Goal state after:
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
⊢ #((cons i s hi).biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi))
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t

Tactic:
obtain ⟨u, hu, hsu⟩ := hs.2 ht

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
s t : Finset α
ht : t.erase a ⊆ s
hs : (memberSubfamily a 𝒜).Shatters s ∧ (nonMemberSubfamily a 𝒜).Shatters s
ha : a ∉ t
u : Finset α
hu : u ∈ nonMemberSubfamily a 𝒜
hsu : s ∩ u = t.erase a
⊢ ∃ u ∈ 𝒜, insert a s ∩ u = t
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case cons
V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v w✝ : V
hw : w✝ ≠ v
w : V
h✝ : G.Adj v w
p✝ : G.Walk w w✝
⊢ v ∈ G.support

Tactic:
| @cons _ w =>

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

Goal state before:
pp: case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ∈ 𝒞 → toColex t < toColex s ∧ #t = r → t ∈ 𝒞

Tactic:
𝒞,

Goal state after:
case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ∈ powersetCard r range'k → toColex t < toColex s ∧ #t = r → t ∈ powersetCard r range'k
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
A : Finset (Fin n)
hA : A ∈ 𝒜
hAbar : ∃ s, sᶜ ∈ 𝒜 ∧ A ⊆ s ∧ #(s \ A) = n - 2 * r
⊢ False

Tactic:
obtain ⟨C, hC, hAC, _⟩ := hAbar

Goal state after:
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
A : Finset (Fin n)
hA : A ∈ 𝒜
C : Finset (Fin n)
hC : Cᶜ ∈ 𝒜
hAC : A ⊆ C
right✝ : #(C \ A) = n - 2 * r
⊢ False
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)
inst✝ : DecidableRel G.Adj
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ G.neighborFinset w = bipartiteBelow G.Adj s w

Tactic:
rw [isBipartiteWith_neighborFinset' h hw, bipartiteBelow]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v x : V
w : G.Walk u v
hw : w.IsTrail
huv : G.IsEdgeReachable 2 u v
huy : x ∈ w.support
⊢ G.IsEdgeReachable 2 u x

Tactic:
by
  classical
  contrapose huy
  obtain ⟨e, he⟩ := by simpa [isEdgeReachable_two] using huy
  have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦
    he <| (isEdgeReachable_two.1 huv _).trans hvy
  exact fun hy ↦ hw.disjoint_edges_takeUntil_dropUntil hy
    ((w.takeUntil x _).mem_edges_of_not_reachable_deleteEdges he)
    (by simpa using (w.dropUntil x _).reverse.mem_edges_of_not_reachable_deleteEdges he')

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ (∀ ⦃v_1 : V⦄, v_1 ∈ w.support → ∀ ⦃w_1 : V⦄, w_1 ∈ w.support → G.Adj v_1 w_1 → s(v_1, w_1) ∈ w.edges) ↔
    ∀ (x y : V), ¬(G.Adj x y ∧ s(x, y) ∉ w.edges ∧ x ∈ w.support ∧ y ∈ w.support)

Tactic:
grind only

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 ⊕ W}, (H ⊕g G).Adj ((Equiv.sumComm V W) a) ((Equiv.sumComm V W) b) ↔ (G ⊕g H).Adj a b

Tactic:
rintro (u | u) (v | 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
u v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inl u)) ((Equiv.sumComm V W) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)

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
u : V
v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inl u)) ((Equiv.sumComm V W) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)

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' u : W
v : V
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inr u)) ((Equiv.sumComm V W) (Sum.inl v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)

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' u v : W
⊢ (H ⊕g G).Adj ((Equiv.sumComm V W) (Sum.inr u)) ((Equiv.sumComm V W) (Sum.inr v)) ↔
    (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case h
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
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2

Tactic:
have : p.tail.length < p.length := by rw [← p.length_tail_add_one hnp]; lia

Goal state after:
case h
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
this : p.tail.length < p.length
⊢ G.Adj v (p.getVert 1) ∧ G.Adj (p.getVert 1) (p.getVert 2) ∧ ¬G.Adj v (p.getVert 2) ∧ v ≠ p.getVert 2
Module: Mathlib.Combinatorics.SimpleGraph.Prod

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

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

Tactic:
· intro ⟨w⟩
    exact ⟨⟨w.ofBoxProdLeft⟩, ⟨w.ofBoxProdRight⟩⟩

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

Goal state before:
pp: case inl.inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
v₁ v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v₁) (Sum.inl v₂)

pp: case inl.inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
v₁ : V
w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v₁) (Sum.inr w₂)

pp: case inr.inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ : W
v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inl v₂)

pp: case inr.inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inr w₂)

Tactic:
· exact ((hG v₁ v₂).map Embedding.sumInl.toHom).mono le_sup_left

Goal state after:
case inl.inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
v₁ : V
w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v₁) (Sum.inr w₂)

case inr.inl
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ : W
v₂ : V
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inl v₂)

case inr.inr
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
v : V
w : W
hG : G.Preconnected
hH : H.Preconnected
w₁ w₂ : W
⊢ ((G ⊕g H) ⊔ edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inr w₁) (Sum.inr w₂)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ v ∈ t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset

Tactic:
simp only [Finset.mem_biUnion, List.mem_toFinset]

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ v ∈ t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset

pp: case refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ (induce (↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset)) G).Connected

Tactic:
· simp only [Finset.mem_biUnion, List.mem_toFinset]
    exact ⟨v, vt, Walk.end_mem_support _⟩

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ (induce (↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset)) G).Connected
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)
j : V ⊕ V
hj : j ∈ right
⊢ ∃ (_ : j.getRight ⋯ ∈ right.toRight), Sum.inr (j.getRight ⋯) = j

Tactic:
by simp [hj]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
⊢ {p | p.length = 0} = {nil}

Tactic:
by
  simp [Walk.length_eq_zero_iff, ← Walk.eq_nil_iff_nil]

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)
j : V ⊕ V
hj : j ∈ right
⊢ ∃ (_ : j.getLeft ⋯ ∈ right.toLeft), Sum.inl (j.getLeft ⋯) = j

Tactic:
by simp [hj]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this : 3 ≤ p.length
⊢ False

Tactic:
have := Nat.cast_le.mp <| hp.support_nodup.length_le_enatCard.trans h

Goal state after:
V : Type u_1
G : SimpleGraph V
h : ENat.card V ≤ 2
v : V
p : G.Walk v v
hp : p.IsCycle
this✝ : 3 ≤ p.length
this : p.support.tail.length ≤ 2
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₂ ⊑ G
⊢ H₁ ⊑ G

Tactic:
exact h.trans' ⟨e.toCopy⟩

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

Goal state before:
pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₁ ⊑ G
⊢ H₂ ⊑ G

Tactic:
exact h.trans' ⟨e.toCopy⟩

Goal state after:
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
⊢ G.IsExtremal H.Free ↔ H.Free G ∧ #G.edgeFinset = extremalNumber (Fintype.card V) H

Tactic:
rw [IsExtremal, and_congr_right_iff, ← extremalNumber_le_iff]

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.Free G → (extremalNumber (Fintype.card V) H ≤ #G.edgeFinset ↔ #G.edgeFinset = extremalNumber (Fintype.card V) H)
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ ∑ x ∈ (G.neighborSet u).toFinset, ↑(#(G.finsetWalkLength n x v)) = ∑ x, ↑(#(G.finsetWalkLength n (↑x) v))

Tactic:
apply Finset.sum_toFinset_eq_subtype

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

Goal state before:
pp: n r : ℕ
⊢ turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r

Tactic:
SimpleGraph.ext_iff,

Goal state after:
n r : ℕ
⊢ (turanGraph n r).Adj = ⊤.Adj ↔ r = 0 ∨ n ≤ r
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
K : Type u_3
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : Fintype K
⊢ Fintype.card K ^ Fintype.card ↑⊤.edgeSet = Fintype.card K ^ (Fintype.card V).choose 2

Tactic:
by rw [← edgeFinset_card, card_edgeFinset_top_eq_card_choose_two]

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

Goal state before:
pp: case map_rel_iff'.inr
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin #univ
zp :
  ∀ (a b : ↥univ),
    h.finpartition.part ↑a = h.finpartition.part ↑b ↔ ↑(zm a) % #h.finpartition.parts = ↑(zm b) % #h.finpartition.parts
a b : V
this : ¬G.Adj ↑⟨a, ⋯⟩ ↑⟨b, ⋯⟩ ↔ ↑(zm ⟨a, ⋯⟩) % #h.finpartition.parts = ↑(zm ⟨b, ⋯⟩) % #h.finpartition.parts
c : Fintype.card V < r
⊢ ↑(zm ⟨a, ⋯⟩) % r = ↑(zm ⟨b, ⋯⟩) % r ↔ ↑(zm ⟨a, ⋯⟩) % min (Fintype.card V) r = ↑(zm ⟨b, ⋯⟩) % min (Fintype.card V) r

Tactic:
have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x : Quot G.Reachable
hx : x ∈ C
⊢ G.connectedComponentMk x.out ∈ C

Tactic:
simp_all [connectedComponentMk]

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
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
⊢ G.IsTuranMaximal r

Tactic:
obtain ⟨J, _, j⟩ := exists_isTuranMaximal (V := V) hr
  obtain ⟨g⟩ := j.nonempty_iso_turanGraph
  rw [f.card_eq, Fintype.card_fin] at g
  use (turanGraph_cliqueFree (n := n) hr).comap f.isContained,
    fun H _ cf ↦ (f.symm.comp g).card_edgeFinset_eq ▸ j.2 cf

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ a, s ∩ c.supp = {a}

Tactic:
exact exists_inter_eq_singleton hrep h

Goal state after:
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
⊢ G.eccent u ≤ 1

Tactic:
eccent_le_iff

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.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.diam ≠ 0
⊢ Nontrivial α

Tactic:
by
  contrapose! h
  simp [diam, h]

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

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
ediam_eq : G.ediam = e
⊢ G.radius = G.ediam

Tactic:
ediam_eq

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
ediam_eq : G.ediam = e
⊢ G.radius = e
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop (𝓝 H.turanDensity)

Tactic:
have h_tendsto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
    (antitoneOn_extremalNumber_div_choose_two H) (isGLB_turanDensity H).bddBelow

Goal state after:
W : Type u_1
H : SimpleGraph W
h_tendsto :
  Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop
    (𝓝 (sInf ((fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) '' Set.Ici 2)))
⊢ Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop (𝓝 H.turanDensity)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
x✝¹ x✝ : Fin m ⊕ Fin n
hadj : G.Adj x✝¹ x✝
⊢ (SimpleGraph.comap (⇑e₁.toEmbedding) (completeBipartiteGraph V W)).Adj x✝¹ x✝

Tactic:
replace h_le := h_le hadj
        rw [← Embedding.map_adj_iff e₁.toEmbedding, ← comap_adj] at h_le
        exact h_le

Goal state after: