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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
⊢ 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * ε * ↑(Fintype.card α ^ 2)

Tactic:
by
  let A := (P.nonUniforms G (ε / 8)).biUnion fun (U, V) ↦ U ×ˢ V
  let B := P.parts.biUnion offDiag
  let C := (P.sparsePairs G (ε / 4)).biUnion fun (U, V) ↦ G.interedges U V
  calc
    _ = (#((univ ×ˢ univ).filter fun (x, y) ↦
          G.Adj x y ∧ ¬(G.regularityReduced P (ε / 8) (ε / 4)).Adj x y) : ℝ) := by
      rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]
      · norm_cast
        rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]
      · gcongr with xy _
        exact fun hxy ↦ regularityReduced_le hxy
    _ ≤ #(A ∪ B ∪ C) := by gcongr; exact unreduced_edges_subset
    _ ≤ #(A ∪ B) + #C := mod_cast (card_union_le _ _)
    _ ≤ #A + #B + #C := by gcongr; exact mod_cast card_union_le _ _
    _ < 4 * (ε / 8) * card α ^ 2 + _ + _ := by
      gcongr; exact hP.sum_nonUniforms_lt univ_nonempty (by positivity) hPε
    _ ≤ _ + ε / 2 * card α ^ 2 + 4 * (ε / 4) * card α ^ 2 := by
      gcongr
      · exact hP.card_biUnion_offDiag_le hε hP'
      · exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)
    _ = 2 * ε * (card α ^ 2 : ℕ) := by norm_cast; ring

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: case pos
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : ∀ i ∈ s, (eval x) (f i) = 0
i : ι
hi : i ∈ s
⊢ 1 - 0 = 1

Tactic:
sub_zero

Goal state after:
case pos
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : ∀ i ∈ s, (eval x) (f i) = 0
i : ι
hi : i ∈ s
⊢ 1 = 1
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: case pos
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
hx : ∀ i ∈ s, (eval x) (f i) = 0
i : ι
hi : i ∈ s
⊢ 1 - (eval x) (f i) ^ (q - 1) = 1

Tactic:
rw [hx i hi, zero_pow hq.ne', sub_zero]

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0
key : ∑ x, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })
⊢ ∑ x, (eval x) F = 0

Tactic:
apply F.sum_eval_eq_zero

Goal state after:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := ⋯
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ⋯
hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0
key : ∑ x, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })
⊢ F.totalDegree < (q - 1) * Fintype.card σ
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts

Tactic:
by
      have t : (star hP G ε hU V).product (star hP G ε hV U) ⊆
          (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts :=
        product_subset_product star_subset_chunk star_subset_chunk
      have hε : 0 ≤ ε := by sz_positivity
      have sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b := fun a b => rfl
      have := add_div_le_sum_sq_div_card t (fun x => (G.edgeDensity x.1 x.2 : ℝ))
        ((G.edgeDensity U V : ℝ) ^ 2 - ε ^ 5 / ↑25) (show 0 ≤ 3 / 4 * ε by linarith) ?_ ?_
      · simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow, cast_pow, mul_pow,
          div_pow, ← mul_assoc] at this
        norm_num at this
        exact this
      · simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow]
        simpa using edgeDensity_star_not_uniform hPα hPε hε₁ hUVne hUV
      · rw [sp, card_product]
        apply (edgeDensity_chunk_aux hP hPα hPε hU hV).trans
        · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]
          simp

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case false
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit false n).bitIndices.SortedLT

Tactic:
simpa [sortedLT_iff_pairwise, bit_false, bit_true, List.pairwise_map]

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case true
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit true n).bitIndices.SortedLT

Tactic:
simpa [sortedLT_iff_pairwise, bit_false, bit_true, List.pairwise_map]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b✝ : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
b : α
hbu : b ∈ ofColex u
hbt : b ∉ ofColex t
hab : a ≤ b
hbs : b ∈ ofColex s
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
have ⟨c, hcu, hcs, hbc⟩ := trans_aux hst htu hbs hbt

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b✝ : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∈ ofColex t
b : α
hbu : b ∈ ofColex u
hbt : b ∉ ofColex t
hab : a ≤ b
hbs : b ∈ ofColex s
c : α
hcu : c ∈ u
hcs : c ∉ s
hbc : b ≤ c
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : ∃ z, z • u = v
⊢ mk K u hu = mk K v hv

Tactic:
exact ((mk_eq_mk_iff K v u hv hu).2 h).symm

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 - v 2 * w 1 = 0 ∧ v 2 * w 0 - v 0 * w 2 = 0 ∧ v 0 * w 1 - v 1 * w 0 = 0 ∧ ![] = 0
⊢ False

Tactic:
zero_empty,

Goal state after:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 - v 2 * w 1 = 0 ∧ v 2 * w 0 - v 0 * w 2 = 0 ∧ v 0 * w 1 - v 1 * w 0 = 0 ∧ True
⊢ False
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
⊢ ∀ (a : α), f a ≠ a ↔ (e.permCongr f) (e a) ≠ e a

Tactic:
intro b; simp only [ne_eq, permCongr_apply, symm_apply_apply, EmbeddingLike.apply_eq_iff_eq]

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ order P L * order P L + order P L + 1 = order P L ^ 2 + order P L + 1

Tactic:
sq

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L
⊢ order P L * order P L + order P L + 1 = order P L * order P L + order P L + 1
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

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

Tactic:
Nat.cast_mul

Goal state after:
case ind
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ x, ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑d.succ.centralBinom / (↑d.succ + 1)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
A Z : Finset G
hZA : ↑Z ⊆ ↑A
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
hHZA : (fun x ↦ ↑H <• x) '' ↑Z = (fun x ↦ ↑H <• x) '' ↑A
⊢ ∃ Z ⊆ A, ↑H * ↑Z = ↑H * ↑A ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z

Tactic:
refine ⟨Z, mod_cast hZA, ?_, hZinj⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
A Z : Finset G
hZA : ↑Z ⊆ ↑A
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
hHZA : (fun x ↦ ↑H <• x) '' ↑Z = (fun x ↦ ↑H <• x) '' ↑A
⊢ ↑H * ↑Z = ↑H * ↑A
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 * ∏ j ∈ (a ::ₘ m).toFinset.erase 0, (count j (a ::ₘ m))! =
    (a ::ₘ m).sum !
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a)!

Tactic:
← Finset.mul_prod_erase _ _ (a := a) (by simp [*]),

Goal state after:
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))! * ∏ x ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count x (a ::ₘ m))!) =
    (a ::ₘ m).sum !
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) * (a ! * c) = (m.sum + a)!
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.semilength = p.semilength + 1

Tactic:
simp [semilength, nest]

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✝¹ : AddGroup 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ 0 - 0 = 0

Tactic:
sub_zero

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 : α
⊢ { toFun := muFun 𝕜, eq_zero_of_not_le' := ⋯ } a b =
    if a = b then 1 else -∑ x ∈ Ico a b, { toFun := muFun 𝕜, eq_zero_of_not_le' := ⋯ } a x

Tactic:
coe_mk,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ Ico a b, muFun 𝕜 a x
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 : α
⊢ { toFun := fun a b ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := ⋯ } a b =
    if a = b then 1 else -∑ x ∈ Ioc a b, { toFun := fun a b ↦ muFun' 𝕜 b a, eq_zero_of_not_le' := ⋯ } x b

Tactic:
coe_mk,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ Ioc a b, muFun' 𝕜 b x
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
⊢ zeta 𝕜 * mu 𝕜 = 1

Tactic:
rw [mu_eq_mu', zeta_mul_mu']

Goal state after:
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 : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mu 𝕜 = mud
⊢ { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ } (toDual a) (toDual b) = (mu 𝕜) b a

Tactic:
coe_mk,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mu 𝕜 = mud
⊢ (mu 𝕜) (ofDual (toDual b)) (ofDual (toDual a)) = (mu 𝕜) b a
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ y ≥ x, ∑ z ≥ y, 1 x z * f z = f x

Tactic:
by
      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge

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

Goal state before:
pp: p q : DyckWord
h : ↑p <:+ ↑q
⊢ p ≤ q

Tactic:
by
  obtain ⟨r', h⟩ := h
  have hc : (q.toList.take (q.toList.length - p.toList.length)).count U =
      (q.toList.take (q.toList.length - p.toList.length)).count D := by
    have hq := q.count_U_eq_count_D
    rw [← h] at hq ⊢
    rw [count_append, count_append, p.count_U_eq_count_D, Nat.add_right_cancel_iff] at hq
    simp [hq]
  let r : DyckWord := q.take _ hc
  have e : r' = r := by
    simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']
  rw [e] at h; replace h : r + p = q := DyckWord.ext h; rw [← h]; exact le_add_self ..

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ IncidenceAlgebra.prod 1 1 = 1

pp: case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)

Tactic:
one_prod_one

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ 1 = 1

case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ (mu 𝕜).prod (mu 𝕜) = mu 𝕜

Tactic:
refine left_inv_eq_right_inv ?_ zeta_mul_mu
  rw [← zeta_prod_zeta, prod_mul_prod', mu_mul_zeta, mu_mul_zeta, one_prod_one]
  exact fun _ _ _ _ _ _ ↦ Commute.mul_mul_mul_comm (by simp : _ = _) _ _

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
⊢ HasProd (fun i ↦ 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) (genFun f)

Tactic:
by
  rw [HasProd, WithPiTopology.tendsto_iff_coeff_tendsto]
  refine fun d ↦ tendsto_atTop_of_eventually_const (fun s (hs : s ≥ range d) ↦ ?_)
  have : ∏ i ∈ s, ((1 : R⟦X⟧) + ∑' j, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1)))
      = ∏ i ∈ s.map (addRightEmbedding 1), (1 + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) := by simp
  rw [this]
  have hs : Icc 1 d ⊆ s.map (addRightEmbedding 1) := by
    intro i
    suffices 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i by simpa
    intro h1 h2
    refine ⟨i - 1, mem_of_subset hs ?_, ?_⟩ <;> grind
  rw [coeff_genFun, coeff_prod]
  refine (sum_of_injOn toFinsuppAntidiag (toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).symm
  · intro p _
    exact mem_of_subset (finsuppAntidiag_mono hs _) p.toFinsuppAntidiag_mem_finsuppAntidiag
  · exact fun g hg hg' ↦ aux_prod_coeff_eq_zero_of_notMem_range f (by simp) hg (by simpa using hg')
  · exact fun p _ ↦ aux_prod_f_eq_prod_coeff f p hs (by simp)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < ↑((k + 1) * m) + (∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order

Tactic:
refine lt_add_of_lt_of_nonneg ?_ (by simp)

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < ↑((k + 1) * m)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:

Tactic:
(2 * n + 1) * rothNumberNat n
    _ = Fintype.card α * addRothNumber (Iio (⟨n, by lia⟩ : α)) := by
      rw [Fin.addRothNumber_eq_rothNumberNat (by simp), Fintype.card_fin]
    _ ≤ Fintype.card α * addRothNumber (univ : Finset α) := by
      gcongr; exact subset_univ _
    _ ≤ ruzsaSzemerediNumber (Sum α (Sum α α)) := addRothNumber_le_ruzsaSzemerediNumber _
    _ = ruzsaSzemerediNumberNat (6 * n + 3) := by
      simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
      ring_nf

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3)) ≤ ↑(ruzsaSzemerediNumberNat (n + 3))

Tactic:
Nat.mul_div_le

Goal state after:
n : ℕ
⊢ ↑(ruzsaSzemerediNumberNat (n + 3)) ≤ ↑(ruzsaSzemerediNumberNat (n + 3))
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case calc_1
n : ℕ
⊢ n ≤ 2 * 3 * (n / 6) + 2 * 3

Tactic:
← mul_add_one

Goal state after:
case calc_1
n : ℕ
⊢ n ≤ 2 * 3 * (n / 6 + 1)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ (fun n ↦ ↑n ^ 2 * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n ↦
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
sq

Goal state after:
⊢ (fun n ↦ ↑n * ↑n * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n ↦
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
f g : α → α'
h : EqOn f g V(G)
⊢ map f G = map g G

Tactic:
refine Graph.ext (by grind) fun _ _ _ ↦ ⟨fun ⟨_, _, hvw, _, _⟩ ↦ ?_, fun ⟨_, _, hvw, _, _⟩ ↦ ?_⟩
  <;> grind [h hvw.left_mem, h hvw.right_mem, hvw.map]

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

Goal state before:
pp: case ht.refine_2
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
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * (m' * m) = m

Tactic:
eq',

Goal state after:
case ht.refine_2
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
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m = m
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
a : α
h : l.idxFun i = Sum.inl a
⊢ ↑l x i = a

Tactic:
by simp [apply_def, h]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
e : η
h : l.idxFun i = Sum.inr e
⊢ ↑l x i = x e

Tactic:
by simp [apply_def, h]

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

Goal state before:
pp: α : Type u_1
H : Hypergraph α
h : V(H) = ∅ ∧ E(H) = ∅ ∨ V(H).Nonempty ∨ E(H).Nonempty
⊢ H = ⊥ ∨ H.IsNonempty

Tactic:
cases h with

Goal state after: