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

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b = m ∨ b ∉ t
⊢ b < w

Tactic:
obtain rfl | hbt := hbt

Goal state after:
case inr.inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
hbs : m ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
⊢ m < w

case inr.inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
b : α
hbs : b ∈ ofColex { val := s.val.erase a, nodup := ⋯ }
hbt : b ∉ t
⊢ b < w
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a
a : α
ha : p a
hfa : f ⟨a, ha⟩ = ⟨a, ha⟩
⊢ ↑(f ⟨a, ha⟩) = a

Tactic:
hfa

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: ⊢ catalan 0 = 1

Tactic:
by rw [catalan]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
      · refine sum_congr rfl fun i _ => ?_
        rw [gosper_trick i.is_le, mul_div]
      · rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
            sum_range_sub, Nat.succ_eq_add_one]
        rw [gosper_catalan_sub_eq_central_binom_div d]
        norm_cast

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p)) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p))

Tactic:
have ub : min (1 + i) (p.toList.length - 1) < p.toList.length :=
      (min_le_right _ p.toList.length.pred).trans_lt (Nat.pred_lt ((length_pos_iff.mpr h).ne'))

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
ub : min (1 + i) ((↑p).length - 1) < (↑p).length
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p)) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p).length - 1)) ↑p))
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
simp [count_replicate]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ofTree p.toTree = p

Tactic:
by
  by_cases h : p = 0
  · simp [h, toTree, ofTree]
  · rw [toTree]
    simp_rw [h, ite_false, ofTree]
    rw [ofTree_toTree p.insidePart, ofTree_toTree p.outsidePart]
    exact nest_insidePart_add_outsidePart h

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
⊢ expansion K S ∅ = 0

Tactic:
by
  simp [expansion]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
x' y' : α
⊢ G.IsLink e x' y' ↔ s(x, y) = s(x', y')

Tactic:
rw [h.isLink_iff, Sym2.eq_iff]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ H.deleteEdges F ≤ G.deleteEdges F

Tactic:
simp_rw [← restrict_edgeSet_sdiff_eq_deleteEdges]
  refine (restrict_mono_left h (E(H) \ F)).trans (G.restrict_mono_right ?_)
  exact sdiff_subset_sdiff_left h.edgeSet_mono

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.Inc e x
⊢ H.Inc e x

Tactic:
by
  obtain ⟨y, hy⟩ := h
  exact ⟨y, hy.of_compatible hGH heH⟩

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y u v : α
edgeSet : Set β
⊢ x = u ∧ y = v ∨ x = v ∧ y = u → ((∃ x, x ∈ edgeSet) ↔ edgeSet.Nonempty)

Tactic:
exact fun _ ↦ Iff.rfl

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.succ
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
hι : ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
specialize hι C'

Goal state after:
case pos.succ
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hι : (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C' l
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M✶ ＼ I ＼ (X \ I) = M✶ ＼ I ／ (X \ I)

Tactic:
ext_iff_indep

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ (M✶ ＼ I ＼ (X \ I)).E = (M✶ ＼ I ／ (X \ I)).E ∧
    ∀ ⦃I_1 : Set α⦄, I_1 ⊆ (M✶ ＼ I ＼ (X \ I)).E → ((M✶ ＼ I ＼ (X \ I)).Indep I_1 ↔ (M✶ ＼ I ／ (X \ I)).Indep I_1)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
⊢ M ／ C ↾ R = (M ↾ (R ∪ C)) ／ C

Tactic:
refine ext_indep (by simp [h.sdiff_eq_right]) fun I (hI : I ⊆ R) ↦ ?_

Goal state after:
α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
I : Set α
hI : I ⊆ R
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : ¬coeff n.some (((optionEquivLeft R σ) P).coeff (n none)) = 0
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)

Tactic:
optionEquivLeft_coeff_some_coeff_none,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : ¬coeff n P = 0
hn : n none = m ∧ n.some = e
⊢ e i ≤ P.support.sup fun m ↦ m (Option.some i)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.vertices ≠ []
⊢ p.vertices.head h = a

Tactic:
induction p with
  | nil => simp only [vertices_nil, head_cons]
  | cons p' _ ih => simp [head_append_of_ne_nil (vertices_ne_nil p'), ih]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: case succ
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
p : Path a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = n + 1
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)

Tactic:
have h_pos : 0 < p.length := by simp [h_len]
    obtain ⟨c, p', e, rfl⟩ := (length_ne_zero_iff_eq_cons p).mp h_pos.ne'
    by_cases hc_in_S : c ∈ S
    · have p'_len : p'.length = n := by simp_all
      obtain ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂, hp'⟩ :=
        ih p' S ha_not_in_S hc_in_S p'_len
      refine ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂.comp e.toPath, ?_⟩
      simp [hp', comp_toPath_eq_cons]
    · refine ⟨c, hc_in_S, b, hb_in_S, e, p', Path.nil, ?_⟩
      simp [comp_toPath_eq_cons]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ : V
pPrev : Path a b✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
e : b✝ ⟶ v
hv : v ∈ (pPrev.cons e).vertices
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
exact ⟨pPrev.cons e, Path.nil, by simp [comp_nil], by simp [vertices_nil]⟩

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∩ ℬ) = memberSubfamily a 𝒜 ∩ memberSubfamily a ℬ

Tactic:
unfold memberSubfamily

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ image (fun s ↦ s.erase a) ({s ∈ 𝒜 ∩ ℬ | a ∈ s}) =
    image (fun s ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∩ image (fun s ↦ s.erase a) ({s ∈ ℬ | a ∈ s})
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
⊢ memberSubfamily a (image (insert a) 𝒜) = 𝒜

Tactic:
by
  ext s
  simp only [mem_memberSubfamily, mem_image]
  refine ⟨?_, fun hs ↦ ⟨⟨s, hs, rfl⟩, h𝒜 _ hs⟩⟩
  rintro ⟨⟨t, ht, hts⟩, hs⟩
  rwa [← insert_erase_invOn.2.injOn (h𝒜 _ ht) hs hts]

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
ha : SupPrime a
⊢ a ≠ ⊥

Tactic:
rintro rfl; exact not_supPrime_bot ha

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
h : a ∈ 𝓒 u v s
ha : a ∉ s
⊢ Disjoint v a

Tactic:
by
  rw [mem_compression] at h
  obtain h | ⟨-, b, hb, hba⟩ := h
  · cases ha h.1
  unfold compress at hba
  split_ifs at hba
  · rw [← hba]
    exact disjoint_sdiff_self_right
  · cases ne_of_mem_of_not_mem hb ha hba

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∉ A
h : insert i A ∈ ↑(∂⁺ 𝒜)
⊢ #(insert i A) = r + 1

Tactic:
card_insert_of_notMem hi,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∉ A
h : insert i A ∈ ↑(∂⁺ 𝒜)
⊢ #A + 1 = r + 1
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 β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∈ 𝒜
⊢ f t ≤ f s + f t

pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t

Tactic:
· exact le_add_of_nonneg_left <| hf _

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
h✝ : s ∉ 𝒜
⊢ f t ≤ 0 + f t
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case a
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
this : 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))
s : Finset α
hs : s ∈ 𝒜
⊢ (Fintype.card α).choose #s ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
· exact choose_le_middle _ _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
⊢ C.toSimpleGraph.spanningCoe.Adj v w ↔ v ∈ C.supp ∧ G.Adj v w

Tactic:
apply Iff.intro

Goal state after:
case mp
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
⊢ C.toSimpleGraph.spanningCoe.Adj v w → v ∈ C.supp ∧ G.Adj v w

case mpr
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
⊢ v ∈ C.supp ∧ G.Adj v w → C.toSimpleGraph.spanningCoe.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
h : v ∈ C.supp
hadj : G.Adj v w
⊢ ∃ a, ∃ (_ : a ∈ ↑C), ∃ a_1, G.Adj a a_1 ∧ a = v ∧ ∃ (_ : a_1 ∈ ↑C), a_1 = w

Tactic:
exact ⟨v, h, w, hadj, rfl, (C.mem_supp_congr_adj hadj).mp h, rfl⟩

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

Goal state before:
pp: case inr.inl
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∉ P.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
exact ⟨(P.toDeleteEdges {s(x, y)} (by grind)).reverse⟩

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

Goal state before:
pp: V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
⊢ Injective ⇑C

Tactic:
exact Hom.injective_of_top_hom C

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

Goal state before:
pp: V : Type u_4
inst✝ : Infinite V
⊢ ⊤.chromaticNumber = ⊤

Tactic:
by_contra hc

Goal state after:
V : Type u_4
inst✝ : Infinite V
hc : ¬⊤.chromaticNumber = ⊤
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
this : G.Coloring ↥(Finset.univ.erase b)
⊢ G.Colorable (card V - 1)

Tactic:
simpa using Coloring.colorable this

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

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    (∑ i ∈ u.powerset, if i ∈ 𝒜 then f i else 0) + ∑ x ∈ u.powerset, if insert a x ∈ 𝒜 then f (insert a x) else 0

pp: case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ Set.InjOn (insert a) ↑u.powerset

Tactic:
← sum_add_distrib

Goal state after:
case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    ∑ x ∈ u.powerset, ((if x ∈ 𝒜 then f x else 0) + if insert a x ∈ 𝒜 then f (insert a x) else 0)

case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ Set.InjOn (insert a) ↑u.powerset
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst✝ : Fintype ↑(G.neighborSet u)
h : G.IsEdgeReachable k u v
huv : u ≠ v
hh : ↑(Fintype.card ↑(G.incidenceSet u)) < ↑k
⊢ False

Tactic:
Set.coe_fintypeCard

Goal state after:
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst✝ : Fintype ↑(G.neighborSet u)
h : G.IsEdgeReachable k u v
huv : u ≠ v
hh : (G.incidenceSet u).encard < ↑k
⊢ False
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

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

Tactic:
have := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
    (mul_nonneg hμ₀ hg.le) (fun a b ↦ ?_) univ univ

Goal state after:
case inr.inr.refine_2
α : 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
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
this : (∑ a, g a) * ∑ a, (μ * f) a ≤ (∑ a ∈ univ ⊼ univ, f a) * ∑ a ∈ univ ⊻ univ, (μ * g) a
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * g a

case inr.inr.refine_1
α : 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
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ u ≠ v

Tactic:
simp +decide [← G.edist_eq_zero_iff.not (b := u = v), h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
hnadj : ¬G.Adj u v
⊢ ¬1 = G.dist u v

Tactic:
by_contra hc

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
hnadj : ¬G.Adj u v
hc : 1 = G.dist u v
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Metric

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

Tactic:
rw [dist, ENat.toNat_eq_iff, ENat.natCast_one, edist_eq_one_iff_adj]
  decide

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:
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:
ext ((v | w) | u) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a₁ a₂✝ : α
b₁ b₂✝ : β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
w : (G □ H).Walk (a₁, b₁) (a₂✝, b₂✝)
b₂ : β
a₂ : α
v✝ : α × β
x : (G □ H).Adj (a₁, b₁) v✝
w' : (G □ H).Walk v✝ (a₂, b₂)
⊢ (cons x w').length = (cons x w').ofBoxProdLeft.length + (cons x w').ofBoxProdRight.length

Tactic:
next c =>
    unfold ofBoxProdLeft ofBoxProdRight
    rw [length_cons, length_boxProd w']
    have disj : (G.Adj a₁ c.1 ∧ b₁ = c.2) ∨ (H.Adj b₁ c.2 ∧ a₁ = c.1) := by simp_all
    rcases disj with h₁ | h₂
    · simp only [h₁, and_self, ↓reduceDIte, length_cons, Or.by_cases]
      rw [add_comm, add_comm w'.ofBoxProdLeft.length 1, add_assoc]
      congr <;> simp [h₁.2.symm]
    · simp only [h₂, add_assoc, Or.by_cases]
      congr <;> simp [h₂.2.symm]

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:
ext ((v | w) | u) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯

Tactic:
let : Fintype ((G □ H).neighborSet x) := SimpleGraph.boxProdFintypeNeighborSet _

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
this : Fintype ↑((G □ H).neighborSet x) := boxProdFintypeNeighborSet x
⊢ (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case hle
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Preconnected
tconn : (⊤.induce t).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Adj v w

Tactic:
simp [hv, hw, ha]

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ mulCayley s ≤ G ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a

Tactic:
rw [SimpleGraph.le_iff_adj]

Goal state after:
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), (mulCayley s).Adj v w → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a