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

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ a, f a = p
⊢ ∑ p ∈ map { toFun := f, inj' := hf₁ } univ, lineCount L p < ∑ p, lineCount L p

Tactic:
refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le

Goal state after:
case refine_1
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ a, f a = p
⊢ p ∉ map { toFun := f, inj' := hf₁ } univ

case refine_2
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
p : P
hp : ¬∃ a, f a = p
⊢ 0 < lineCount L p
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
l : L
q : P
hq : q ∉ l
⊢ lineCount L q = pointCount P l

Tactic:
by
      cases nonempty_fintype P
      cases nonempty_fintype L
      exact HasLines.lineCount_eq_pointCount (card_points_eq_card_lines P L) hq

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this✝¹ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this✝ : #l = #A
this : #r = #A
⊢ #(l ∪ r) < 2 * #A

Tactic:
refine (card_le_card lr).trans_lt ?_

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this✝¹ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this✝ : #l = #A
this : #r = #A
⊢ #(a •> (A⁻¹ * A)) < 2 * #A
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take ((range (↑p).length)[0] + 1) ↑p) = count D (List.take ((range (↑p).length)[0] + 1) ↑p)) =
        true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)

pp: p : DyckWord
h : p ≠ 0
⊢ 0 < (range (↑p).length).length

Tactic:
getElem_range

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ ¬(decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
      ∀ (j : ℕ) (hji : j < 0),
        decide
            (count U (List.take ((range (↑p).length)[j] + 1) ↑p) =
              count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
          false)

p : DyckWord
h : p ≠ 0
⊢ 0 < (range (↑p).length).length
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
hi : i < p.firstReturn
ne : count U (List.take ((range (↑p).length)[i] + 1) ↑p) ≠ count D (List.take ((range (↑p).length)[i] + 1) ↑p)
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)

Tactic:
getElem_range

Goal state after:
p : DyckWord
i : ℕ
hi : i < p.firstReturn
ne : count U (List.take (i + 1) ↑p) ≠ count D (List.take (i + 1) ↑p)
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n : ℕ
⊢ (n + 1).bell = ∑ i ≤ n, n.choose i * (n - i).bell

Tactic:
Nat.bell

Goal state after:
n : ℕ
⊢ ∑ i ≤ n, n.choose i * (n - i).bell = ∑ i ≤ n, n.choose i * (n - i).bell
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ count U (List.take ((range (↑p ++ ↑q).length)[p.firstReturn] + 1) (↑p ++ ↑q)) =
      count D (List.take ((range (↑p ++ ↑q).length)[p.firstReturn] + 1) (↑p ++ ↑q)) ∧
    ∀ (j : ℕ) (hji : j < p.firstReturn),
      decide
          (count U (List.take ((range (↑p ++ ↑q).length)[j] + 1) (↑p ++ ↑q)) =
            count D (List.take ((range (↑p ++ ↑q).length)[j] + 1) (↑p ++ ↑q))) =
        false

Tactic:
getElem_range

Goal state after:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q)) ∧
    ∀ j < p.firstReturn,
      decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (List.take ((range (U :: ↑p ++ [D]).length)[(↑p).length + 1] + 1) (U :: ↑p ++ [D])) =
      count D (List.take ((range (U :: ↑p ++ [D]).length)[(↑p).length + 1] + 1) (U :: ↑p ++ [D])) ∧
    ∀ (j : ℕ) (hji : j < (↑p).length + 1),
      decide
          (count U (List.take ((range (U :: ↑p ++ [D]).length)[j] + 1) (U :: ↑p ++ [D])) =
            count D (List.take ((range (U :: ↑p ++ [D]).length)[j] + 1) (U :: ↑p ++ [D]))) =
        false

Tactic:
getElem_range

Goal state after:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) =
      count D (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) ∧
    ∀ j < (↑p).length + 1,
      decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i : ℕ
⊢ Filter.Tendsto (fun j ↦ (f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))).order) Filter.atTop (nhds ⊤)

Tactic:
refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n : ℕ
⊢ ∀ (b : ℕ), n ≤ b → ↑n < (f (i + 1) (b + 1) • X ^ ((i + 1) * (b + 1))).order
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
this : 0 < #A
⊢ K * ↑(#A) ≤ K * ((2 - K) * ↑l + (K - 1) * ↑(#S))

Tactic:
gcongr; exact le_of_mul_le_mul_right ineq <| by positivity

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ ∀ {i : ℕ}, i ∈ Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ } → 0 < i

pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ (Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ }).sum = d

pp: case refine_4
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ { parts := Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ },
        parts_pos := ?refine_2, parts_sum := ?refine_3 }.toFinsuppAntidiag =
    g

Tactic:
· suffices ∀ i, g i ≠ 0 → i ≠ 0 by simpa [Nat.pos_iff_ne_zero]
    exact fun i h ↦ ((hgne0 i).mp h).1

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ (Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ }).sum = d

case refine_4
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ { parts := Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ },
        parts_pos := ⋯, parts_sum := ?refine_3 }.toFinsuppAntidiag =
    g
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: case succ
n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
⊢ Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)

Tactic:
have : k < n + 1 := by simp at hk; lia

Goal state after:
case succ
n : ℕ
x✝ : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
this : k < n + 1
⊢ Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
⊢ G.IsLink e x y ↔ G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y

Tactic:
refine ⟨fun h ↦ ⟨h.inc_left, h.inc_right, fun z h' ↦ h'.eq_or_eq_of_isLink h⟩, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
⊢ (G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y) → G.IsLink e x y
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ (C ∩ M✶.E))✶ = M ／ C

Tactic:
delete_inter_ground_eq,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ C)✶ = M ／ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
⊢ (M ／ C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C

Tactic:
by
  rw [isCocircuit_def, dual_contract, delete_isCircuit_iff]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = M ／ C ↾ R \ C

Tactic:
contract_restrict_eq_restrict_contract _ disjoint_sdiff_right

Goal state after:
α : Type u_1
R C : Set α
M : Matroid α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Hdeg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := ⋯
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
⊢ ∀ (i : σ), degreeOf i r < #(S i)

Tactic:
intro i
    rw [degreeOf_eq_sup, Finset.sup_lt_iff (by simp [Sne i])]
    aesop (add simp [Alon.degree_P])

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
n : ℕ
hn : n ≤ p.length
⊢ ∃ v p₁ p₂, p = p₁.comp p₂ ∧ p₁.length = n

Tactic:
by
  induction p generalizing n with
  | nil =>
    obtain ⟨rfl⟩ : n = 0 := by simpa using hn
    exact ⟨a, Path.nil, Path.nil, by simp, rfl⟩
  | @cons _ c p' e ih =>
    rw [length_cons] at hn
    rcases (Nat.le_succ_iff).1 hn with h | rfl
    · obtain ⟨d, p₁, p₂, hp, hl⟩ := ih h
      exact ⟨d, p₁, p₂.cons e, by simp [hp], hl⟩
    · exact ⟨c, p'.cons e, Path.nil, by simp, by simp⟩

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
b v : V
p : Path v b
hv : v ∈ nil.vertices
⊢ ¬v ∈ nil.vertices.tail

Tactic:
simp only [vertices_nil, tail_cons, not_mem_nil, not_false_eq_true]

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
  rw [filter_inter_distrib, image_inter_of_injOn _ _ ((erase_injOn' _).mono _)]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ s, ↑(#((𝒜 ∪ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
      ∑ s, ↑(#((𝒜 ⊼ ℬ).truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ∑ s, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
      ∑ s, ↑(#(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))

Tactic:
← sum_add_distrib,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ x,
      (↑(#((𝒜 ∪ ℬ).truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) +
        ↑(#((𝒜 ⊼ ℬ).truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x))) =
    ∑ s, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
      ∑ s, ↑(#(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ x,
      (↑(#((𝒜 ∪ ℬ).truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) +
        ↑(#((𝒜 ⊼ ℬ).truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x))) =
    ∑ s, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) +
      ∑ s, ↑(#(ℬ.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s))

Tactic:
← sum_add_distrib,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ x,
      (↑(#((𝒜 ∪ ℬ).truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) +
        ↑(#((𝒜 ⊼ ℬ).truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x))) =
    ∑ x,
      (↑(#(𝒜.truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) +
        ↑(#(ℬ.truncatedSup x)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ s, ↑(#((𝒜 ∪ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s, ↑(#((𝒜 ⊻ ℬ).truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) =
    ∑ s, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s, ↑(#(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
← sum_add_distrib,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ x,
      (↑(#((𝒜 ∪ ℬ).truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)) +
        ↑(#((𝒜 ⊻ ℬ).truncatedInf x)) / (↑(#x) * ↑((card α).choose #x))) =
    ∑ s, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s, ↑(#(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ x,
      (↑(#((𝒜 ∪ ℬ).truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)) +
        ↑(#((𝒜 ⊻ ℬ).truncatedInf x)) / (↑(#x) * ↑((card α).choose #x))) =
    ∑ s, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s, ↑(#(ℬ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
← sum_add_distrib,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∑ x,
      (↑(#((𝒜 ∪ ℬ).truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)) +
        ↑(#((𝒜 ⊻ ℬ).truncatedInf x)) / (↑(#x) * ↑((card α).choose #x))) =
    ∑ x,
      (↑(#(𝒜.truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)) +
        ↑(#(ℬ.truncatedInf x)) / (↑(#x) * ↑((card α).choose #x)))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
⊢ ∑ s ∈ 𝒜, (↑((card α).choose #s))⁻¹ = ∑ s ∈ 𝒜, ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
h𝒜₀ : ∅ ∉ 𝒜
s : Finset α
hs : s ∈ 𝒜
⊢ (↑((card α).choose #s))⁻¹ = ↑(#(𝒜.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s))
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : 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 ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
by
  rw [collapse_eq ha, ← hts, if_pos ht]
  split_ifs
  · exact le_add_of_nonneg_left <| hf _
  · rw [zero_add]

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
i : ι
x : α
hx : x ∈ s i
⊢ f i x = g x

Tactic:
rw [hg, piecewise_apply, hs.mem_iff_index_eq.mp hx]

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 α
inst✝² : Nonempty (G.Coloring α)
inst✝¹ : Infinite α
inst✝ : Nonempty V
⊢ Infinite (G.Coloring α)

Tactic:
have ⟨C⟩ := ‹Nonempty <| G.Coloring α›
  have ⟨v⟩ := ‹Nonempty V›
  let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C
  refine Infinite.of_injective f fun a b h ↦ ?_
  have := congrFun (congrArg RelHom.toFun h) v
  dsimp [f, Iso.completeGraph] at this
  grind

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

Goal state before:
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:
refine le_of_not_gt fun size ↦ ?_

Goal state after:
case inr
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) < #𝒜
⊢ False
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
β : Type u_5
f : α ≃ β
C : G.Coloring α
v : V
⊢ ((G.recolorOfEmbedding f.symm.toEmbedding) ((G.recolorOfEmbedding f.toEmbedding) C)) v = C v

Tactic:
apply Equiv.symm_apply_apply

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
⊢ ∃ p, s(v, w) ∉ p.edges

Tactic:
by_contra! hb

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
⊢ ∃ C, ¬Surjective ⇑C

Tactic:
refine ⟨G.recolorOfCardLE (by simpa using h.le) C, fun hC ↦ ?_⟩

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
hC : Surjective ⇑((G.recolorOfCardLE ⋯) C)
⊢ False
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]
    exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _

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

Goal state before:
pp: V : Type u
⊢ ⊤.chromaticNumber = ENat.card V

Tactic:
cases finite_or_infinite V

Goal state after:
case inl
V : Type u
h✝ : Finite V
⊢ ⊤.chromaticNumber = ENat.card V

case inr
V : Type u
h✝ : Infinite V
⊢ ⊤.chromaticNumber = ENat.card V
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber < 1 ↔ G = ⊥ ∧ Nonempty V

Tactic:
Order.lt_one_iff_nonpos,

Goal state after:
V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber ≤ 1 ∧ ¬G.chromaticNumber ≤ 0 ↔ G = ⊥ ∧ Nonempty V
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
⊢ (_root_.completeBipartiteGraph α β).Copy G

Tactic:
by
  have : Nonempty (α ↪ left) := by
    rw [← card_coe] at card_left
    exact Function.Embedding.nonempty_of_card_le card_left.symm.le
  let fα : α ↪ left := Classical.arbitrary (α ↪ left)
  have : Nonempty (β ↪ right) := by
    rw [← card_coe] at card_right
    exact Function.Embedding.nonempty_of_card_le card_right.symm.le
  let fβ : β ↪ right := Classical.arbitrary (β ↪ right)
  let f : α ⊕ β ↪ V := by
    refine ⟨Sum.elim (Subtype.val ∘ fα) (Subtype.val ∘ fβ), fun s₁ s₂ ↦ ?_⟩
    match s₁, s₂ with
    | .inl p₁, .inl p₂ => simp
    | .inr p₁, .inl p₂ =>
      simpa using (h (fα p₂).prop (fβ p₁).prop).ne'
    | .inl p₁, .inr p₂ =>
      simpa using (h (fα p₁).prop (fβ p₂).prop).symm.ne'
    | .inr p₁, .inr p₂ => simp
  refine ⟨⟨f.toFun, fun {s₁ s₂} hadj ↦ ?_⟩, f.injective⟩
  rcases hadj with ⟨hs₁, hs₂⟩ | ⟨hs₁, hs₂⟩
  all_goals dsimp [f]
  · rw [← Sum.inl_getLeft s₁ hs₁, ← Sum.inr_getRight s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr]
    exact h (by simp) (by simp)
  · rw [← Sum.inr_getRight s₁ hs₁, ← Sum.inl_getLeft s₂ hs₂,
      Sum.elim_inl, Sum.elim_inr, adj_comm]
    exact h (by simp) (by simp)

Goal state after: