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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
⊢ (if h : a ∈ upperClosure ↑s then {b ∈ s | b ≤ a}.inf' ⋯ (⇑e ∘ id) else ⊥) =
    if h : a ∈ upperClosure ↑s then {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id else ⊥

Tactic:
congr with h

Goal state after:
case e_t
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeInf α
inst✝⁴ : SemilatticeInf β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE β
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
e : α ≃o β
s : Finset α
a : α
this : e a ∈ upperClosure ↑(map e.toEmbedding s) ↔ a ∈ upperClosure ↑s
h : a ∈ upperClosure ↑s
⊢ {b ∈ s | b ≤ a}.inf' ⋯ (⇑e ∘ id) = {b ∈ map e.toEmbedding s | b ≤ e a}.inf' ⋯ id
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t

Tactic:
by
  simp only [shadow, mem_sup, mem_image]

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: case neg
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : ¬SupIrred a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
not_supIrred

Goal state after:
case neg
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
ih : ∀ y < a, ∃ s, s.sup id = y ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
ha : IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t
⊢ a ∉ upperClosure ↑(s ⊻ t)

Tactic:
rwa [coe_sups, upperClosure_sups]

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
⊢ Disjoint s (map { toFun := compl, inj' := ⋯ } s)

Tactic:
Finset.disjoint_left

Goal state after:
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
⊢ ∀ ⦃a : α⦄, a ∈ s → a ∉ map { toFun := compl, inj' := ⋯ } s
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ ↑s ∧ ⊥ᶜ ∉ ↑s
⊢ (↑{⊤}).Intersecting

Tactic:
by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
⊢ False

Tactic:
have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left sdiff_subset

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
⊢ False
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
· exact (disjoint_right.1 disj (max'_mem _ hU) <| heq.symm ▸ max'_mem _ _).elim

Goal state after:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ k ≤ 𝒜.vcDim, (Fintype.card α).choose k

Tactic:
simp_rw [← card_univ, ← card_powersetCard]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ x ≤ 𝒜.vcDim, #(powersetCard x univ)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
inst✝² : Nontrivial V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.Preconnected
⊢ 0 < G.minDegree

Tactic:
obtain ⟨v, hv⟩ := G.exists_minimal_degree_vertex
  rw [hv]
  exact h.degree_pos_of_nontrivial v

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Colorable 1 ↔ G = ⊥

Tactic:
by
  refine ⟨fun ⟨C⟩ ↦ eq_bot_iff_forall_not_adj.mpr fun u v h ↦ ?_, fun h ↦ h ▸ ⟨0, by simp⟩⟩
  exact C.map_rel h <| Subsingleton.elim ..

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

Goal state before:
pp: 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 ↑𝒞
⊢ #(∂^[i] 𝒞) ≤ #(∂^[i] 𝒜)

Tactic:
refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩

Goal state after:
case refine_1
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 ↑𝒞
⊢ #𝒞 ≤ #𝒜

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 ∈ 𝒞
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (extend (⇑f) (⇑C) (const β default) (f w✝¹)) (extend (⇑f) (⇑C) (const β default) b)

Tactic:
f.injective.extend_apply,

Goal state after:
case map_rel'
V : Type u
G : SimpleGraph V
n : ℕ
β : Type u_3
f : V ↪ β
inst✝ : NeZero n
C : G.Coloring (Fin n)
a b : β
left✝ : a ≠ b
w✝¹ w✝ : V
hadj : G.Adj w✝¹ w✝
ha : f w✝¹ = a
hb : f w✝ = b
⊢ (completeGraph (Fin n)).Adj (C w✝¹) (extend (⇑f) (⇑C) (const β default) b)
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
⊢ m ∈ {n | G.Colorable n} → Nat.succ 0 ≤ m

Tactic:
hm

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
⊢ Nat.succ 0 ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
⊢ Nat.succ 0 ≤ m

Tactic:
by_contra h'

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Nonempty V
n : ℕ
hc : G.Colorable n
m : ℕ
hm : m ∈ {n | G.Colorable n}
h' : ¬Nat.succ 0 ≤ m
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
h : G.chromaticNumber ≠ ⊤
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
rw [chromaticNumber_ne_top_iff_exists] at h

Goal state after:
V : Type u
G : SimpleGraph V
h : ∃ n, G.Colorable n
⊢ G.Colorable G.chromaticNumber.toNat
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case neg
α : 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 ∉ 𝒜
⊢ (0 + 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
simp_rw [add_zero, zero_mul]

Goal state after:
case neg
α : 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 ∉ 𝒜
⊢ 0 ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
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:
by
  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.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
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G →g G'
g : H →g H'
h : I →g I'
⊢ (f.sum (g.sum h)).comp Iso.sumAssoc.toHom = Iso.sumAssoc.toHom.comp ((f.sum g).sum h)

Tactic:
by
  ext ((v | w) | u) <;> 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
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ↪g G'
g : H ↪g H'
h : I ↪g I'
⊢ (f.sum (g.sum h)).comp Iso.sumAssoc.toEmbedding = Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)

Tactic:
by
  ext ((v | w) | u) <;> 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
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
f : G ≃g G'
g : H ≃g H'
h : I ≃g I'
⊢ sumAssoc.comp ((f.sumCongr g).sumCongr h) = (f.sumCongr (g.sumCongr h)).comp sumAssoc

Tactic:
by
  ext ((v | w) | u) <;> simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ u ∈ (⊤.induce {u, v} ⊓ H).verts

Tactic:
simp [uH]

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

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

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

Tactic:
· calc (G □ H).edist x y ≤ w_app.length := by exact edist_le _
          _ = wG.length + wH.length := by exact_mod_cast w_len
          _ = G.edist x.1 y.1 + H.edist x.2 y.2 := by simp only [hwG, hwH]

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

Goal state before:
pp: n : ℕ
v : Fin (n + 2)
⊢ ((cycleGraph (n + 2)).neighborFinset v).card = {v - 1, v + 1}.card

Tactic:
cycleGraph_neighborFinset

Goal state after:
n : ℕ
v : Fin (n + 2)
⊢ {v - 1, v + 1}.card = {v - 1, v + 1}.card
Module: Mathlib.Combinatorics.SimpleGraph.Hasse

Goal state before:
pp: α : Type u_1
β : Type u_2
V : Type u_3
inst✝ : DecidableEq V
G : SimpleGraph V
u v : V
w : G.Walk u v
hw : w.IsPath
⊢ Function.RightInverse (fun v_1 ↦ ⟨List.idxOf (↑v_1) w.support, ⋯⟩) ⇑w.pathGraphHomToSubgraph

Tactic:
by grind [pathGraphHomToSubgraph, RelHom.coeFn_mk]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ (u v : V), Subsingleton (G.Path u v)

Tactic:
refine ⟨fun h u v ↦ ⟨fun p q ↦ ?_⟩, fun h v c hc ↦ ?_⟩

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
u v : V
p q : G.Path u v
⊢ p = q

case refine_2
V : Type u_1
G : SimpleGraph V
h : ∀ (u v : V), Subsingleton (G.Path u v)
v : V
c : G.Walk v v
hc : c.IsCycle
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : Fintype V
R : Type u_3
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ ↑(extremalNumber (Fintype.card V) H) ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → ↑(#G.edgeFinset) ≤ m

Tactic:
← Nat.le_floor_iff h

Goal state after:
V : Type u_1
W : Type u_2
inst✝³ : Fintype V
R : Type u_3
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ extremalNumber (Fintype.card V) H ≤ ⌊m⌋₊ ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ ⌊m⌋₊
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : Minimal Connected G
x✝² x✝¹ : V
x✝ : G.Adj x✝² x✝¹
hbr : ¬G.IsBridge s(x✝², x✝¹)
⊢ G.deleteEdges {s(x✝², x✝¹)} < G

Tactic:
simpa [deleteEdges, ← edgeSet_ssubset_edgeSet]

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

Goal state before:
pp: case right
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
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
⊢ #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u

Tactic:
have l3 : 0 < G.degree u := by rw [G.degree_pos_iff_exists_adj u]; use t, h.symm

Goal state after:
case right
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
l2 : (G.replaceVertex s t).degree u = G.degree u - 1
l3 : 0 < G.degree u
⊢ #G.edgeFinset < #G.edgeFinset + (G.replaceVertex s t).degree s - (G.replaceVertex s t).degree u
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 : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
use G.replaceVertex v w, inferInstance, cf.replaceVertex v w

Goal state after:
case right
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := ⋯
large : Finset V
hl : large ∈ fp.parts
small : Finset V
hs : small ∈ fp.parts
ineq : #small + 1 < #large
w : V
hw : w ∈ large
v : V
hv : v ∈ small
cf : G.CliqueFree (r + 1)
⊢ #G.edgeFinset < #(G.replaceVertex v w).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
⊢ G.IsCompleteMultipartite ↔ ∃ ι V, ∃ (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V)

Tactic:
constructor <;> intro h
  · exact ⟨_, _, fun _ ↦ ⟨_, h.setoid.refl _⟩, ⟨h.iso⟩⟩
  · obtain ⟨_, _, _, ⟨e⟩⟩ := h
    refine ⟨fun _ _ _ h1 h2 ↦ ?_⟩
    rw [← e.map_rel_iff] at *
    exact completeMultipartiteGraph.isCompleteMultipartite _ |>.trans _ _ _ h1 h2

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
K : G.ConnectedComponent
hrep : Represents s G.oddComponents
⊢ Even (K.supp \ s).ncard

Tactic:
by
  by_cases h : Even K.supp.ncard
  · simpa [hrep.ncard_sdiff_of_notMem
      (by simpa [Set.ncard_image_of_injective, ← Nat.not_odd_iff_even] using h)] using h
  · have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
    rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by lia)]
    simpa [Nat.even_sub] using Nat.not_even_iff_odd.mp h

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
⊢ G.ediam = 0

Tactic:
by
  simp [ediam_def]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
⊢ completeEquipartiteGraph (r + 1) t ⊑ G ↔ ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

Tactic:
rw [completeEquipartiteGraph_isContained_iff]
    refine ⟨fun ⟨K'⟩ ↦ ?_, fun ⟨K, s, hs, hadj⟩ ↦ ?_⟩
    · obtain ⟨parts, hparts_sub, hparts_card⟩ := K'.parts.exists_subset_card_eq (Nat.pred_le _)
      let K : G.CompleteEquipartiteSubgraph r t := by
        refine ⟨parts, ?_, fun h ↦ K'.card_mem_parts (hparts_sub h),
          fun _ h₁ _ h₂ hne ↦ K'.isCompleteBetween (hparts_sub h₁) (hparts_sub h₂) hne⟩
        rw [hparts_card, K'.card_parts.resolve_right ht]
        exact .inl (Nat.pred_succ r)
      obtain ⟨s, nhs_mem, hs⟩ : ∃ s ∉ K.parts, insert s K.parts = K'.parts := by
        refine exists_eq_insert_iff.mpr ⟨hparts_sub, ?_⟩
        rw [K.card_parts.resolve_right ht, K'.card_parts.resolve_right ht]
      have hs_mem : s ∈ K'.parts := by simp [← hs]
      exact ⟨K, s, K'.card_mem_parts hs_mem,
        fun _ h ↦ K'.isCompleteBetween (hparts_sub h) hs_mem (ne_of_mem_of_not_mem h nhs_mem)⟩
    · refine ⟨K.parts.cons s ?_, ?_, ?_, ?_⟩
      · intro hs_mem
        obtain ⟨v, hv⟩ : s.Nonempty := by
          rw [← Finset.card_pos, hs]
          exact Nat.pos_of_ne_zero ht
        exact G.irrefl <| hadj s hs_mem hv hv
      · rw [Finset.card_cons, K.card_parts.resolve_right ht]
        exact .inl rfl
      · simp_rw [mem_cons, forall_eq_or_imp]
        exact ⟨hs, fun p ↦ K.card_mem_parts⟩
      · rw [coe_cons]
        have : Std.Symm G.IsCompleteBetween := by simp [symm_def, isCompleteBetween_comm]
        exact K.isCompleteBetween.insert_of_symm fun p hp _ ↦ hadj p hp |>.symm

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (fun n ↦ ↑(extremalNumber n H) / ↑(n.choose 2)) atTop (𝓝 H.turanDensity)
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)

Tactic:
apply Tendsto.const_mul (1 / turanDensity H : ℝ) at hπ

Goal state after:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ :
  Tendsto (fun x ↦ 1 / H.turanDensity * (↑(extremalNumber x H) / ↑(x.choose 2))) atTop
    (𝓝 (1 / H.turanDensity * H.turanDensity))
⊢ (fun n ↦ ↑(extremalNumber n H)) ~[atTop] fun n ↦ H.turanDensity * ↑(n.choose 2)