mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ ↑(#(G.cliqueFinset 3))

Tactic:
apply (G.triangle_counting' dst ust dsu usu dtu utu).trans _
  rw [Nat.cast_le]
  refine card_le_card_of_injOn (fun (x, y, z) ↦ {x, y, z}) ?_ ?_
  · rintro ⟨x, y, z⟩
    simp +contextual [is3Clique_triple_iff]
  rintro ⟨x₁, y₁, z₁⟩ h₁ ⟨x₂, y₂, z₂⟩ h₂ t
  simp only [mem_coe, mem_filter, mem_product] at h₁ h₂
  apply triple_eq_triple_of_mem hst hsu htu t <;> tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
a : α
⊢ MulDissociated {a} ↔ a ≠ 1

Tactic:
simp [MulDissociated, ofPred_or, -subset_singleton_iff,
    Finset.coe_subset_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    ∑ x ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x})

Tactic:
← card_disjiUnion

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    #((s * t).disjiUnion (fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ?h)

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ (↑(s * t)).PairwiseDisjoint fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: k n : ℕ
⊢ (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices

Tactic:
induction k with

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

Goal state before:
pp: case composite
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
hk : k ≤ 2 * m - 1
⊢ ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
induction k with

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case pos
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![0, w]

Tactic:
exact fun h ↦ h.ne_zero 0 rfl

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ ofColex (toColex t), a ∉ ofColex (toColex s) ∧ ∀ b ∈ ofColex (toColex s), b ∉ ofColex (toColex t) → b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 <| max'_mem _ _

Goal state after:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ ofColex (toColex t), a ∉ ofColex (toColex s) ∧ ∀ b ∈ ofColex (toColex s), b ∉ ofColex (toColex t) → b < a
u : Finset α := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
hu : u.Nonempty
m : α := u.max' hu
hmt : m ∈ t
hms : m ∉ s
hm : ∀ a ∈ s, a ∉ t → a < m
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a✝ : G
hA : #(A * A) ≤ #A
ha✝ : a✝ ∈ A
smul_A : ∀ {a : G}, a ∈ A → a •> A = A * A
A_smul : ∀ {a : G}, a ∈ A → A <• a = A * A
smul_A_eq_A_smul : ∀ {a : G}, a ∈ A → a •> A = A <• a
mul_mem_A_comm : ∀ {x a : G}, a ∈ A → (x * a ∈ A ↔ a * x ∈ A)
H : Subgroup G := stabilizer G A
a : G
ha : a ∈ A
x : G
hx : a * x ∈ ↑A
⊢ x ∈ ↑H

Tactic:
simpa [← smul_A ha, mul_smul] using! smul_A hx

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ fiber (some a) = {f | fixedPoints ⇑f ⊆ {a}}

Tactic:
by
  ext f
  constructor
  · rw [RemoveNone.mem_fiber]
    rintro ⟨F, F_derangement, F_none, rfl⟩ x x_fixed
    rw [mem_fixedPoints_iff] at x_fixed
    apply_fun some at x_fixed
    rcases Fx : F (some x) with - | y
    · rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
    · exfalso
      rw [removeNone_some F ⟨y, Fx⟩] at x_fixed
      exact F_derangement _ x_fixed
  · intro h_opfp
    use Equiv.Perm.decomposeOption.symm (some a, f)
    constructor
    · intro x
      apply_fun fun x => Equiv.swap none (some a) x
      simp only [Perm.decomposeOption_symm_apply, Perm.coe_mul]
      rcases x with - | x
      · simp
      simp only [comp, optionCongr_apply, Option.map_some, swap_apply_self]
      by_cases x_vs_a : x = a
      · rw [x_vs_a, swap_apply_right]
        apply Option.some_ne_none
      have ne_1 : some x ≠ none := Option.some_ne_none _
      have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
      rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
      intro contra
      exact x_vs_a (h_opfp contra)
    · rw [apply_symm_apply]

Goal state after:
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
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ i ∈ univ ×ˢ univ, lineCount L i.1 = ∑ i ∈ univ ×ˢ univ, pointCount P i.2

Tactic:
Finset.sum_product_right,

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ y, ∑ x, lineCount L (x, y).1 = ∑ i ∈ univ ×ˢ univ, pointCount P i.2
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
⊢ 2 * #A ≤ #(a •> A ∩ b •> A) + #(B * A)

Tactic:
have : #((a • A) ∪ (b • A)) ≤ #(B * A) := by
    gcongr
    rw [union_subset_iff]
    exact ⟨smul_finset_subset_mul ha, smul_finset_subset_mul hb⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
a b : G
ha : a ∈ B
hb : b ∈ B
this : #(a •> A ∪ b •> A) ≤ #(B * A)
⊢ 2 * #A ≤ #(a •> A ∩ b •> A) + #(B * 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
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 c ha hc

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 c : G
ha : a ∈ A⁻¹ * A
hc : c ∈ A⁻¹ * A
⊢ a * c ∈ A⁻¹ * A
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n : ℕ
⊢ ∑ i, catalan ↑i * catalan (n - ↑i) = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

Tactic:
Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n,

Goal state after:
n : ℕ
⊢ ∑ i, catalan ↑i * catalan (n - ↑i) = ∑ k ∈ range n.succ, catalan k * catalan (n - k)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

Tactic:
by_contra h
  simp_rw [not_or, ← ne_eq, crossProduct_ne_zero_iff_linearIndependent] at h
  rw [← Matrix.of_row (![a, b]), ← Matrix.of_row (![c, d])] at h
  let A : Matrix (Fin 2) (Fin 3) K := .of ![a, b]
  let B : Matrix (Fin 2) (Fin 3) K := .of ![c, d]
  have hAB : A * B.transpose = 0 := by
    ext i j
    fin_cases i <;> fin_cases j <;> assumption
  replace hAB := rank_add_rank_le_card_of_mul_eq_zero hAB
  rw [rank_transpose, h.1.rank_matrix, h.2.rank_matrix, Fintype.card_fin, Fintype.card_fin] at hAB
  contradiction

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

Goal state before:
pp: case hz
⊢ #(treesOfNumNodesEq 0) = catalan 0

Tactic:
| hz =>

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)
⊢ #l = #A

Tactic:
rw [hl]

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
⊢ f * 0 = 0

Tactic:
by ext; exact sum_eq_zero fun x _ ↦ mul_zero _

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : LocallyFiniteOrder α
inst✝⁷ : AddCommMonoid 𝕜
inst✝⁶ : Monoid 𝕜
inst✝⁵ : Semiring 𝕝
inst✝⁴ : AddCommMonoid 𝕞
inst✝³ : SMul 𝕜 𝕝
inst✝² : Module 𝕝 𝕞
inst✝¹ : DistribMulAction 𝕜 𝕞
inst✝ : IsScalarTower 𝕜 𝕝 𝕞
f : IncidenceAlgebra 𝕜 α
g : IncidenceAlgebra 𝕝 α
h : IncidenceAlgebra 𝕞 α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ (Icc a b).sigma (Icc a), (f a x.snd • g x.snd x.fst) • h x.fst b =
    ∑ x ∈ (Icc a b).sigma fun a ↦ Icc a b, f a x.fst • g x.fst x.snd • h x.snd b

Tactic:
apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;> aesop (add unsafe le_trans)

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.firstReturn < (↑p).length

Tactic:
by
  have lp := length_pos_of_ne_nil (toList_ne_nil.mpr h)
  rw [← length_range (n := p.toList.length)]
  apply findIdx_lt_length_of_exists
  simp only [mem_range, decide_eq_true_eq]
  use p.toList.length - 1
  exact ⟨by lia, by rw [Nat.sub_add_cancel lp, take_of_length_le (le_refl _),
    p.count_U_eq_count_D]⟩

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (mu' 𝕜) a b = if a = b then 1 else -∑ x ∈ Ioc a b, (mu' 𝕜) x b

Tactic:
rw [mu', coe_mk, muFun'_apply, sum_attach]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ ↑n < (f (i + 1) (m + 1) • X ^ ((i + 1) * (m + 1))).order

Tactic:
PowerSeries.smul_eq_C_mul,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ ↑n < (C (f (i + 1) (m + 1)) * X ^ ((i + 1) * (m + 1))).order
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

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

Tactic:
apply tendsto_order_genFun_term_atTop_nhds_top

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (p + q).insidePart = p.insidePart

Tactic:
by
  simp_rw [insidePart, firstReturn_add, add_eq_zero', h, false_and, dite_false, ite_false,
    DyckWord.ext_iff, take]
  congr 3
  exact take_append_of_le_length (firstReturn_lt_length h)

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

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 =
    p.insidePart.semilength + p.outsidePart.semilength + 1

Tactic:
numNodes_toTree p.insidePart,

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.semilength + p.outsidePart.toTree.numNodes + 1 = p.insidePart.semilength + p.outsidePart.semilength + 1
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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * ↑(#A) < ↑(#(A ∩ z⁻¹ •> A))
hrw : (2 - K) * ↑(#A) ≤ ↑(#(A ∩ w •> A))
⊢ ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) ≤ ↑(#(z⁻¹ •> A ∩ w •> A))

Tactic:
gcongr <;> exact inter_subset_right

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

Goal state before:
pp: n : ℕ
⊢ 0 < 2

Tactic:
by norm_num

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

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

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0

Tactic:
largeSchroder_succ,

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

n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0
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
⊢ 0 < connectivity K S

Tactic:
by
  obtain ⟨A, hA, hSA⟩ := exists_nonempty_isFragment hK hS
  exact (expansion_pos hK hS hA).trans_eq hSA

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_4
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Summable fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)

Tactic:
· exact (hasSum_pow_pentagonal_sub_pentagonalSeries R).summable

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ Nat.cast =O[atTop] fun n ↦ ↑n / 3

pp: ⊢ (fun n ↦ ↑n / 3) =O[atTop] fun n ↦ ↑n / 3 - 2

Tactic:
· simp_rw [div_eq_inv_mul]
        exact (isBigO_refl ..).const_mul_right (by simp)

Goal state after:
⊢ (fun n ↦ ↑n / 3) =O[atTop] fun n ↦ ↑n / 3 - 2
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
⊢ ¬G ≠ ⊥ ↔ ¬V(G).Nonempty

Tactic:
by simp [vertexSet_eq_empty_iff, not_nonempty_iff_eq_empty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
⊢ G ⊓ H = ⊥ ↔ Disjoint V(G) V(H)

Tactic:
← vertexSet_eq_empty_iff,

Goal state after:
α : Type u_1
β : Type u_2
G H : Graph α β
⊢ V(G ⊓ H) = ∅ ↔ Disjoint V(G) V(H)
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : G.Compatible H
⊢ E(G ⊓ H) = E(G) ∩ E(H)

Tactic:
rw [G.edgeSet_inf]
  exact le_antisymm (fun e he ↦ he.1) fun e he ↦ ⟨he, fun _ _ ↦ h.isLink_congr he.1 he.2⟩

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

Goal state before:
pp: case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m

Tactic:
← absorbing_eq_self

Goal state after:
case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N ∩ {m' | m' * m = m}
scaling_eq_self : (fun x ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ (M.IsBasis I X ∧ X ⊆ M.E) ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D

Tactic:
and_iff_left_of_imp IsBasis.subset_ground

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I X ∧ Disjoint X D ↔ M.IsBasis I X ∧ Disjoint X D
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_1
α : 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
⊢ AlmostMono C' → AlmostMono C

Tactic:
refine fun p => ⟨p.line.prod (l'.map some), p.color, fun x => ?_⟩

Goal state after:
case neg.refine_1
α : 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'
x : α
⊢ C (↑(p.line.prod (map some l')) (some x)) = p.color
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
⊢ ∃ B, ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)

Tactic:
by
    choose B hB using fun i ↦ (M i).exists_isBase
    exact ⟨univ.sigma B, by simpa⟩

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
⊢ coeff (m.degree f) f = coeff (m.degree f) ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f) * b)

Tactic:
nth_rewrite 2 [H]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
⊢ coeff (m.degree f) f =
    coeff (m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b)
      ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f) * b)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis I X
hJI : J ⊆ I
h : (M ／ J).IsBasis (I \ J) (X ∩ (M ／ J).E)
⊢ (M ／ J).IsBasis (I \ J) (X \ J)

Tactic:
rwa [contract_ground, ← inter_sdiff_assoc, inter_eq_self_of_subset_left hIX.subset_ground] at h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ (M ／ C).coloops = M.coloops \ C

Tactic:
by
  rw [← dual_delete_dual, dual_coloops, delete_loops_eq, dual_loops]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
this : c ∈ r'.support ∨ c ∈ ((monomial (m.degree f)) (m.leadingCoeff f)).support
⊢ c = m.degree f

Tactic:
Classical.or_iff_not_imp_left

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
hc : c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support
i : ι
hc' : c ∉ r'.support
this : c ∉ r'.support → c ∈ ((monomial (m.degree f)) (m.leadingCoeff f)).support
⊢ c = m.degree f