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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
hst : toColex s < toColex t
⊢ False

pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
hst : toColex s = toColex t
⊢ False

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
hts : toColex t < toColex s
⊢ False

Tactic:
· exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
hst : toColex s = toColex t
⊢ False

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
hts : toColex t < toColex s
⊢ False
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
⊢ #s ≤ #(s.biUnion t)

Tactic:
suffices #(s.biUnion t)ᶜ ≤ #sᶜ by
      -- Rephrase in terms of complements (uses `h`)
      rw [Finset.card_compl, Finset.card_compl, tsub_le_iff_left] at this
      replace := h.trans this
      rwa [← add_tsub_assoc_of_le s.card_le_univ, le_tsub_iff_left (le_add_left s.card_le_univ),
        add_le_add_iff_right] at this

Goal state after:
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: n : ℕ
⊢ ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)

Tactic:
intro a

Goal state after:
n : ℕ
a : Fin (n + 1)
⊢ card ↑{a}ᶜ = card (Fin n)
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case zero
⊢ ↑(numDerangements (0 + 1)) = (↑0 + 1) * ↑(numDerangements 0) - (-1) ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case zero
⊢ ↑(numDerangements 0) = ∑ k ∈ Finset.range (0 + 1), (-1) ^ k * ↑((k + 1).ascFactorial (0 - k))

Tactic:
| zero =>

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
⊢ ∀ {a b : G}, a ∈ A⁻¹ * A → b ∈ A⁻¹ * A → a * b ∈ A⁻¹ * A

Tactic:
intro a

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
⊢ ∀ {b : G}, a ∈ A⁻¹ * A → b ∈ A⁻¹ * A → a * b ∈ A⁻¹ * A
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
⊢ lineCount L p = lineCount L q

Tactic:
have hp₁ : lineCount L p₁ = n := (HasLines.lineCount_eq_pointCount h h₁₃).trans hl₃

Goal state after:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₁₂ : p₁ ∉ l₂
h₁₃ : p₁ ∉ l₃
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
⊢ lineCount L p = lineCount L q
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)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
⊢ ∀ (a b : G), a ∈ A → b ∈ A → ∃ y ∈ A, ∃ z, (∃ y ∈ A, y⁻¹ = z) ∧ y * z = a * b⁻¹

Tactic:
intro a

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
a : G
⊢ ∀ (b : G), a ∈ A → b ∈ A → ∃ y ∈ A, ∃ z, (∃ y ∈ A, y⁻¹ = z) ∧ y * z = a * b⁻¹
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)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ (A⁻¹ * A).Nonempty

Tactic:
simp [h₀]

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

Goal state before:
pp: case zero
⊢ ↑(catalan 0) = ↑(Nat.centralBinom 0) / (↑0 + 1)

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
⊢ ↑(catalan n) = ↑n.centralBinom / (↑n + 1)

Tactic:
induction n using Nat.caseStrongRecOn with
  | zero => simp
  | ind d hd =>
    simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]
    trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) *
                            (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
    · congr
      ext1 x
      have m_le_d : x.val ≤ d := by lia
      have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
      rw [hd _ m_le_d, hd _ d_minus_x_le_d]
      norm_cast
    · 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.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
⊢ a⁻¹ •> z •> A⁻¹ ⊆ A⁻¹ * (A * (A * A⁻¹))

Tactic:
simp only [← mul_assoc, smul_smul]

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
⊢ (a⁻¹ * z) •> A⁻¹ ⊆ A⁻¹ * A * A * A⁻¹
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e_a
m : Multiset ℕ
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!

Tactic:
← Finset.prod_mul_distrib

Goal state after:
case e_a
m : Multiset ℕ
⊢ ∏ x ∈ m.toFinset.erase 0,
      x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take i [U]) + count D (List.take (i - [U].length) ↑p) +
      count D (List.take (i - ([U] ++ ↑p).length) [D]) ≤
    count U (List.take i [U]) + count U (List.take (i - [U].length) ↑p) +
      count U (List.take (i - ([U] ++ ↑p).length) [D])

Tactic:
rw [← add_rotate (count D _), ← add_rotate (count U _)]

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take (i - ([U] ++ ↑p).length) [D]) + count D (List.take i [U]) +
      count D (List.take (i - [U].length) ↑p) ≤
    count U (List.take (i - ([U] ++ ↑p).length) [D]) + count U (List.take i [U]) +
      count U (List.take (i - [U].length) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
hc : 0 < a ! * c
hq : (a ::ₘ m).bell * (map (fun j ↦ j !) (a ::ₘ m)).prod * ((count a (a ::ₘ m))! * rest) = (a ::ₘ m).sum !
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a)!

Tactic:
simpa [c, Nat.factorial_succ, add_comm, mul_assoc, mul_left_comm] using hq

Goal state after:
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)})
⊢ ↑(#(A ×ˢ A⁻¹)) = ∑ z ∈ S, ↑(r z)

Tactic:
norm_cast
          exact card_eq_sum_card_fiberwise fun xy hxy ↦
            mul_mem_mul (mem_product.mp hxy).1 (mem_product.mp hxy).2

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

Goal state before:
pp: case succ
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
⊢ ∑ i ≤ n, n.choose i * (n - i).bell = ∑ p, p.parts.bell

Tactic:
calc
  _ = ∑ i ≤ n, ∑ q : (n - i).Partition, n.choose i * q.parts.bell := by
    congr! with i
    simp [ih (n - i) _, Finset.mul_sum]
  _ = ∑ i ≤ n, ∑ p : {p : (n + 1).Partition // (i + 1 : ℕ) ∈ p.parts},
      choose n i * (p.1.parts.erase (i + 1)).bell := by
    congr! with i hi
    have : i ≤ n := Finset.mem_Iic.mp hi
    have h1 : 1 ≤ (i + 1 : ℕ) := by lia
    have h2 : (i + 1 : ℕ) ≤ n + 1 := by lia
    have hsub : n + 1 - (i + 1 : ℕ) = n - i := by lia
    exact hsub ▸ (Fintype.sum_equiv (Partition.partitionWithPartEquiv h1 h2) _ _ (fun _ ↦ rfl)).symm
  _ = ∑ x : Σ p : (n + 1).Partition, p.parts.toFinset,
      choose n (x.2.1 - 1) * (x.1.parts.erase x.2.1).bell := by
    rw [← Nat.range_succ_eq_Iic, Finset.sum_range, ← Fintype.sum_sigma']
    refine Fintype.sum_equiv (sigmaPartitionWithPartEquiv n) _ _ ?_
    simp [sigmaPartitionWithPartEquiv]
  _ = ∑ p : (n + 1).Partition, ∑ a : p.parts.toFinset, choose n (a - 1) * (p.parts.erase a).bell :=
    Fintype.sum_sigma' fun (p : (n + 1).Partition) (a : p.parts.toFinset) ↦
      choose n (a - 1) * (p.parts.erase a.1).bell
  _ = _ := by
    congr! with p
    rw [bell_eq_sum_erase p]
    exact p.parts.toFinset.sum_coe_sort (fun a ↦ choose n (a - 1) * (p.parts.erase a).bell)

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

Goal state before:
pp: case pos.refine_1
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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
⊢ (coeff (g x)) 1 = 0

pp: case pos.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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
i : ℕ
⊢ (coeff (g x)) (f x (i + 1) • X ^ (x * (i + 1))) = 0

Tactic:
· suffices g x ≠ 0 by simp [this]
      contrapose hprod
      simp [hprod]

Goal state after:
case pos.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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
i : ℕ
⊢ (coeff (g x)) (f x (i + 1) • X ^ (x * (i + 1))) = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ Function.Injective fun i ↦ (↑i + 1) * m - 1

Tactic:
intro a

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
⊢ ∀ ⦃a₂ : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)⦄,
    (fun i ↦ (↑i + 1) * m - 1) a = (fun i ↦ (↑i + 1) * m - 1) a₂ → a = a₂
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
⊢ expansion K S (A ∩ B) = connectivity K S

Tactic:
have := expansion_submodularity (S := S) (A := A) (B := B) (K := K)

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
this : expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
⊢ expansion K S (A ∩ B) = connectivity K S
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case zero
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (0 + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (0 + 1) * x ^ ((0 + 1) * (3 * 0 + 4) / 2) * ∑' (n : ℕ), powMulProdOneSubPow 0 n x

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ 2 * (n + 3).smallSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder

Tactic:
by
      rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia

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

Goal state before:
pp: case zero
⊢ (0 + 1).stirlingFirst 0 = (0 + 1).choose 2

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ (0 + 1).stirlingFirst 1 = 0!

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ (0 + 1).stirlingSecond 1 = 1

Tactic:
| zero =>

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
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha : a ∈ n⁻¹ •> ↑N
⊢ a⁻¹ ∈ n⁻¹ •> ↑N

Tactic:
by
      rw [← coe_smul_finset, mem_coe] at *
      apply smul_mem_smul_finset (a := a⁻¹) at ha
      rw [smul_eq_mul, inv_mul_cancel] at ha
      have : (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty := ⟨1, by simpa using! ⟨one_mem_carrier, ha⟩⟩
      simpa only [← (hN.smul_finset n⁻¹).eq_of_inter_nonempty hK.le hS
        ((hN.smul_finset n⁻¹).smul_finset a⁻¹) this] using! self_mem_smul_carrier a⁻¹

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

Goal state before:
pp: case zero
⊢ (0 + 1).stirlingSecond 0 = (0 + 1).choose 2

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e✝ f : β
X Y : Set α
G : SimpleGraph α
e : Sym2 α
⊢ e ∈ G.edgeSet ↔ ∃ x y, e = s(x, y) ∧ e ∈ G.edgeSet

Tactic:
induction e with

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
this✝² : Semigroup M' := { mul := fun p q ↦ ⟨↑p * ↑q, ⋯⟩, mul_assoc := ⋯ }
this✝¹ : CompactSpace M'
this✝ : Nonempty M'
this : ∀ (p : M'), Continuous fun x ↦ x * p
⊢ ∃ m ∈ s, m * m = m

Tactic:
obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this

Goal state after:
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
s : Set M
snemp : s.Nonempty
s_compact : IsCompact s
s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s
M' : Type (max 0 u_1) := { m // m ∈ s }
this✝² : Semigroup M' := { mul := fun p q ↦ ⟨↑p * ↑q, ⋯⟩, mul_assoc := ⋯ }
this✝¹ : CompactSpace M'
this✝ : Nonempty M'
this : ∀ (p : M'), Continuous fun x ↦ x * p
m : M
hm : m ∈ s
idem : ⟨m, hm⟩ * ⟨m, hm⟩ = ⟨m, hm⟩
⊢ ∃ m ∈ s, m * m = m
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
hlm : ↑l = ↑m
i : ι
⊢ l.idxFun i = m.idxFun i

Tactic:
simp only [funext_iff] at hlm

Goal state after:
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
⊢ l.idxFun i = m.idxFun i
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
x✝ : α ⊕ η
hl : l.idxFun i = x✝
⊢ x✝ = m.idxFun i

Tactic:
cases hl : idxFun l i with

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

Tactic:
cases h : l.idxFun ie.1

Goal state after:
case none
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
h : l.idxFun ie.1 = none
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

case some
η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
val✝ : η → α
h : l.idxFun ie.1 = some val✝
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
⊢ M ＼ D = M ↔ Disjoint D M.E

Tactic:
rw [← restrict_compl, restrict_eq_self_iff, sdiff_eq_left, disjoint_comm]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.zero
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = 0) ∨ ∃ l, IsMono C l

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
⊢ ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p

Tactic:
intro a

Goal state after:
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
⊢ ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ FP (Stream'.drop 0 a) ⊆ FP a

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ a.get 0 ∈ FP a

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
he : M.Dep {e}
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.Dep {e}

Tactic:
exact he.of_isMinor (by simpa) hNM

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
inst✝ : DecidableEq X
s : Finset X
⊢ (prefixed s).dens = (↑((Fintype.card X).choose #s))⁻¹

Tactic:
simp [dens, card_prefixed, Nat.cast_choose _ s.card_le_univ]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_3
α : 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 α) → κ
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 : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
⊢ ∀ (p : AlmostMono C),
    p = { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ∨
        p ∈ Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines →
      ↑p.line none = Sum.elim s.focus (↑(map some l') none)

Tactic:
Multiset.mem_map

Goal state after:
case neg.refine_3
α : 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 α) → κ
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 : ColorFocused C'
sr : s.lines.card = r
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
⊢ ∀ (p : AlmostMono C),
    (p = { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ∨
        ∃ a ∈ s.lines, { line := a.line.prod (map some l'), color := a.color, has_color := ⋯ } = p) →
      ↑p.line none = Sum.elim s.focus (↑(map some l') none)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsNonloop e
⊢ (M ／ {e}).Indep I ↔ e ∉ I ∧ M.Indep (insert e I)

Tactic:
by
  simp [he.indep.contract_indep_iff]

Goal state after: