mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(P.energy G) + ε ^ 5 / 4 =
    (∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4)) / ↑(#P.parts) ^ 2

Tactic:
by
        rw [coe_energy, add_div, mul_div_cancel_left₀]; positivity

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case hab
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts * (#P.parts - 1)) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) ≤
    ∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts

Tactic:
mul_tsub,

Goal state after:
case hab
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts * #P.parts - #P.parts * 1) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) ≤
    ∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ G.copyCount H = #(image Copy.toSubgraph univ)

Tactic:
rw [copyCount]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : Fintype { f // Injective ⇑f }
inst✝ : DecidableEq G.Subgraph
⊢ #{G' | Nonempty (H ≃g G'.coe)} = #(image Copy.toSubgraph univ)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ G.copyCount ⊥ = 1

Tactic:
rw [copyCount]

Goal state after:
V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ #{G' | Nonempty (⊥ ≃g G'.coe)} = 1
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeFinset - G.copyCount H = #G.edgeFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) }

Tactic:
simp only [edgeFinset, Set.toFinset_card]

Goal state after:
case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ Fintype.card ↑G.edgeSet - G.copyCount H = Fintype.card ↑G.edgeSet - Fintype.card { G' // Nonempty (H ≃g G'.coe) }
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
h✝ : v ≠ w
h : edge v w ≤ G
⊢ (edge v w).Adj v w

Tactic:
by simp_all [edge_adj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n < p.darts.length
⊢ p.darts[n] = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }

Tactic:
by
  rw [p.length_darts] at h
  ext <;> simp [p.getVert_eq_support_getElem (le_of_lt h), p.getVert_eq_support_getElem h]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.reverse.reverse = p✝
⊢ (cons h✝ p✝).reverse.reverse = cons h✝ p✝

Tactic:
simp [ih]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.dropUntil u h).support <:+ p.support

Tactic:
by
  grw [dropUntil_eq_drop, support_copy, drop_support_eq_support_drop_min, List.drop_suffix]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case succ.cons
V : Type u_1
G : SimpleGraph V
u v : V
n k✝ k : ℕ
h : n ≤ k
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
ih : ((cons h✝ p✝).take n).IsSubwalk ((cons h✝ p✝).take k)
⊢ ((cons h✝ p✝).take k).IsSubwalk ((cons h✝ p✝).take (k + 1))

Tactic:
cases k

Goal state after:
case succ.cons.zero
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : n ≤ 0
ih : ((cons h✝ p✝).take n).IsSubwalk ((cons h✝ p✝).take 0)
⊢ ((cons h✝ p✝).take 0).IsSubwalk ((cons h✝ p✝).take (0 + 1))

case succ.cons.succ
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n✝ : ℕ
h : n ≤ n✝ + 1
ih : ((cons h✝ p✝).take n).IsSubwalk ((cons h✝ p✝).take (n✝ + 1))
⊢ ((cons h✝ p✝).take (n✝ + 1)).IsSubwalk ((cons h✝ p✝).take (n✝ + 1 + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3

Tactic:
by
  classical
  simp_rw [is3Clique_iff, isCycle_def]
  exact
    ⟨(fun ⟨_, a, _, _, hab, hac, hbc, _⟩ => ⟨a, cons hab (cons hbc (cons hac.symm nil)), by aesop⟩),
    (fun ⟨_, .cons hab (.cons hbc (.cons hca nil)), _, _⟩ => ⟨_, _, _, _, hab, hca.symm, hbc, rfl⟩)⟩

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

Goal state before:
pp: case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b

Tactic:
conv at hφ => enter [a, b]; rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]

Goal state after:
case neg
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
⊢ ∀ {a b : Fin n}, G.Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
⊢ ∃ w ∈ p.support, w ∈ q.support ∧ ∃ c, c.IsCycle ∧ c.support <+ p.support ++ q.support.reverse.tail

Tactic:
by
  have ⟨u', v', p', q', hp', hq', hcyc⟩ := hp.exists_isCycle_of_ne hq h
  use u', hp'.support_subset p'.start_mem_support, hq'.support_subset q'.start_mem_support
  refine ⟨_, hcyc, ?_⟩
  rw [support_append, support_reverse]
  refine .append ?_ <| .tail <| .reverse ?_
  · exact isSubwalk_iff_support_isInfix.mp hp' |>.sublist
  · exact isSubwalk_iff_support_isInfix.mp hq' |>.sublist

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.bypass.support <+ p.support

Tactic:
by
  induction p with
  | nil => simp!
  | cons _ _ ih =>
    dsimp! only
    split_ifs
    · exact support_dropUntil_suffix_support .. |>.sublist.trans ih |>.cons _
    · simpa

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.bypass.darts <+ p✝.darts
h✝ : u✝ ∈ p✝.bypass.support
⊢ (p✝.bypass.dropUntil u✝ h✝).darts <+ { fst := u✝, snd := v✝, adj := h✝¹ } :: p✝.darts

Tactic:
exact darts_dropUntil_suffix_darts .. |>.sublist.trans ih |>.cons _

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α), x ∈ t → y ∈ t → x ≠ y → s(x, y) ∉ G.edgeFinset \ H.edgeFinset
⊢ H.IsNClique 3 t

Tactic:
simp only [not_and, mem_sdiff, not_not, mem_edgeFinset, mem_edgeSet] at h

Goal state after:
α : Type u_1
G H : SimpleGraph α
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableRel H.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α), x ∈ t → y ∈ t → x ≠ y → G.Adj x y → H.Adj x y
⊢ H.IsNClique 3 t
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:

Tactic:
∑ x, eval x f = ∑ x : σ → K, ∑ d ∈ f.support, f.coeff d * ∏ i, x i ^ d i := by
      simp only [eval_eq']
    _ = ∑ d ∈ f.support, ∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i := sum_comm
    _ = 0 := sum_eq_zero ?_

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ ∀ x ∈ f.support, ∑ x_1, coeff x f * ∏ i, x_1 i ^ x i = 0
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ #𝒜 ≤ #(powersetCard r univ)

Tactic:
exact card_le_card (subset_powersetCard_univ_iff.mpr h𝒜)

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

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

pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ {f | fixedPoints ⇑f ⊆ {a}} → f ∈ fiber (some a)

Tactic:
· 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

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ {f | fixedPoints ⇑f ⊆ {a}} → f ∈ fiber (some 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 : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
this :
  #(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)) + #(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A) =
    #(A ∩ (c * d) •> A) + #(A ∩ (a * b)⁻¹ •> A)
⊢ 0 < ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)))

Tactic:
← Nat.cast_inj (R := ℚ),

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
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
this :
  ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)) + #(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) =
    ↑(#(A ∩ (c * d) •> A) + #(A ∩ (a * b)⁻¹ •> A))
⊢ 0 < ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)))
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
⊢ ↑A⁻¹ * ↑A * (↑A⁻¹ * ↑A) = ↑A⁻¹ * ↑A

Tactic:
← invMulSubgroup_eq_inv_mul _ h,

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
⊢ ↑(A.invMulSubgroup h) * ↑(A.invMulSubgroup h) = ↑(A.invMulSubgroup h)
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⁻¹
⊢ ↑A⁻¹ * ↑A * (↑A⁻¹ * ↑A) = ↑A⁻¹ * ↑A

Tactic:
← invMulSubgroup_eq_inv_mul _ h,

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⁻¹
⊢ ↑(A.invMulSubgroup h) * ↑(A.invMulSubgroup h) = ↑(A.invMulSubgroup h)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A⁻¹ * (↑A * (↑A⁻¹ * ↑A)) = ↑A * ↑A⁻¹

Tactic:
← invMulSubgroup_eq_inv_mul _ h,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A⁻¹ * (↑A * ↑(A.invMulSubgroup h)) = ↑A * ↑A⁻¹
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A⁻¹ * ↑A * ↑(A.invMulSubgroup h) = ↑A * ↑A⁻¹

Tactic:
← invMulSubgroup_eq_inv_mul _ h,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑(A.invMulSubgroup h) * ↑(A.invMulSubgroup h) = ↑A * ↑A⁻¹
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case h
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
⊢ (m.toFinset.erase 0).erase a = ((a ::ₘ m).toFinset.erase 0).erase a

Tactic:
grind [Multiset.toFinset_cons]

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
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹

Tactic:
have const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ)) := by positivity

Goal state after:
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 - ψ))
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) < count U (List.take (i - 1) ↑p) + 1

Tactic:
Nat.lt_add_one_iff

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) ≤ count U (List.take (i - 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < (↑p.nest).length
⊢ count D (List.take i ↑p.nest) < count U (List.take i ↑p.nest)

Tactic:
by
  simp_rw [nest, length_append, length_singleton] at ub ⊢
  rw [take_append_of_le_length (by rw [singleton_append, length_cons]; lia),
    take_append, take_of_length_le (by rw [length_singleton]; lia),
    length_singleton, singleton_append, count_cons_of_ne (by simp), count_cons_self,
    Nat.lt_add_one_iff]
  exact p.count_D_le_count_U _

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✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
⊢ 0 • f = 0

Tactic:
ext; exact sum_eq_zero fun x _ ↦ zero_smul _ _

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

Goal state before:
pp: case H1
m n : ℕ
hn : n ≠ 0
⊢ 0 < n ! ^ m * m !

pp: case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)

Tactic:
· exact Nat.mul_pos (Nat.pow_pos n.factorial_pos) m.factorial_pos

Goal state after:
case H2
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a ≠ b
⊢ (mu' 𝕜) a b = -∑ x ∈ Ioc a b, (mu' 𝕜) x b

Tactic:
mu'_eq_sum_Ioc_of_ne hab

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a ≠ b
⊢ -∑ x ∈ Ioc a b, (mu' 𝕜) x b = -∑ x ∈ Ioc a b, (mu' 𝕜) x b
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
x y : α × β
hxy : x ≤ y
⊢ ((zeta 𝕜).prod (zeta 𝕜)) x y = (zeta 𝕜) x y

Tactic:
simp [hxy, hxy.1, hxy.2]

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

Goal state before:
pp: p q : DyckWord
pq : p ≤ q
⊢ p.semilength ≤ q.semilength

Tactic:
by
  induction pq with
  | refl => rfl
  | tail _ mq ih =>
    rename_i m r _
    rcases eq_or_ne r 0 with rfl | hr
    · rw [insidePart_zero, outsidePart_zero, or_self] at mq
      rwa [mq] at ih
    · rcases mq with hm | hm
      · exact ih.trans (hm ▸ semilength_insidePart_lt hr).le
      · exact ih.trans (hm ▸ semilength_outsidePart_lt hr).le

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

Goal state before:
pp: case refine_3
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
⊢ ∀ (x : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)),
    (if m ∣ (↑x + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑x + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑x + 1)) ^ m

Tactic:
intro i
    have : (i + 1) * m - 1 + 1 = (i + 1) * m := by grind
    simp [this, pow_mul]

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

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

Tactic:
simp at hn

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

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

Tactic:
simp at hn

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
u v : α
f : α → α'
e : β
h : G.IsLink e u v
⊢ (map f G).Adj (f u) (f v)

Tactic:
exact ⟨e, h.map f⟩

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∀ m' ∈ FP (Stream'.drop (n + 1) a), m * m' ∈ FP a

Tactic:
intro m'

Goal state after:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
⊢ m' ∈ FP (Stream'.drop (n + 1) a) → m * m' ∈ FP a
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
⊢ ∀ m' ∈ FP (Stream'.drop (n + 1) a), a.head * m * m' ∈ FP a

Tactic:
intro m'

Goal state after:
case h
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m✝ : M
a : Stream' M
m : M
h✝ : FP a.tail m
n : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n a.tail), m * m' ∈ FP a.tail
m' : M
⊢ m' ∈ FP (Stream'.drop (n + 1) a) → a.head * m * m' ∈ FP a
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ 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}, ⋯⟩
this : ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
⊢ FP (Stream'.corec elem succ ⟨s₀, sU⟩) ⊆ s₀

Tactic:
intro m hm
    exact this _ m hm ⟨s₀, sU⟩ rfl

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

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

Tactic:
delete_eq_self_iff,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ Disjoint C M✶.E ↔ Disjoint C M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ (M✶ ＼ I).Indep J ∧ Disjoint J (X \ I) ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep (J ∪ X \ I)

Tactic:
union_indep_iff_indep_of_subset_coloops hss,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ (M✶ ＼ I).Indep J ∧ Disjoint J (X \ I) ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J
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
this : ∀ ⦃K : Set α⦄, Disjoint K J → M.Indep (K ∪ J) → K ⊆ X → I ⊆ K ∪ J → K ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) (X \ J)

Tactic:
by
    simpa +contextual [IsBasis', (hIX.indep.subset hJI).contract_indep_iff,
      subset_sdiff, maximal_subset_iff, disjoint_sdiff_left,
      union_eq_self_of_subset_right hJI, hIX.indep, sdiff_subset.trans hIX.subset,
      sdiff_subset_iff, subset_antisymm_iff, union_comm J]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
⊢ ∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l

Tactic:
refine ⟨Fintype.card ι, fun C ↦ ?_⟩

Goal state after:
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
⊢ ∃ l, IsMono C l
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
e : σ ≃ τ
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 τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
x : σ → R
hx : ∀ (i : σ), x i ∈ S (e i)
s : τ
⊢ s = e (e.symm s)

Tactic:
simp only [Equiv.apply_symm_apply]

Goal state after: