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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁴ : α
b✝¹ : β
c✝¹ : γ
a✝³ : (a✝⁴, b✝¹, c✝¹) ∈ t
a✝² : α
c✝ : γ
a✝¹ : (a✝², b✝¹, c✝) ∈ t
b✝ : β
a✝ : (a✝⁴, b✝, c✝) ∈ t
⊢ {in₀ ?m.3588, in₁ ?m.3591, in₂ ?m.3594} = {in₁ b✝¹, in₀ a✝⁴, in₂ c✝}

Tactic:
by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁴ : α
b✝¹ : β
c✝¹ : γ
a✝³ : (a✝⁴, b✝¹, c✝¹) ∈ t
b✝ : β
c✝ : γ
a✝² : (a✝⁴, b✝, c✝) ∈ t
a✝¹ : α
a✝ : (a✝¹, b✝, c✝¹) ∈ t
⊢ {in₀ ?m.3745, in₁ ?m.3748, in₂ ?m.3751} = {in₀ a✝⁴, in₂ c✝¹, in₁ b✝}

Tactic:
by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁴ : α
b✝¹ : β
c✝¹ : γ
a✝³ : (a✝⁴, b✝¹, c✝¹) ∈ t
a✝² : α
b✝ : β
a✝¹ : (a✝², b✝, c✝¹) ∈ t
c✝ : γ
a✝ : (a✝⁴, b✝, c✝) ∈ t
⊢ {in₀ ?m.3902, in₁ ?m.3905, in₂ ?m.3908} = {in₂ c✝¹, in₀ a✝⁴, in₁ b✝}

Tactic:
by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
this : 0 ≤ ε
⊢ (↑(G.edgeDensity U V) - ε ^ 5 / 50) ^ 2 ≤
    ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2

Tactic:
by
      gcongr
      have rflU := Subset.refl (chunk hP G ε hU).parts
      have rflV := Subset.refl (chunk hP G ε hV).parts
      refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
      · rw [biUnion_parts, biUnion_parts]
      · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
        norm_cast

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁴ : α
b✝¹ : β
c✝¹ : γ
a✝³ : (a✝⁴, b✝¹, c✝¹) ∈ t
a✝² : α
c✝ : γ
a✝¹ : (a✝², b✝¹, c✝) ∈ t
b✝ : β
a✝ : (a✝², b✝, c✝¹) ∈ t
⊢ {in₀ ?m.4059, in₁ ?m.4062, in₂ ?m.4065} = {in₁ b✝¹, in₂ c✝¹, in₀ a✝²}

Tactic:
by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁴ : α
b✝¹ : β
c✝¹ : γ
a✝³ : (a✝⁴, b✝¹, c✝¹) ∈ t
a✝² : α
b✝ : β
a✝¹ : (a✝², b✝, c✝¹) ∈ t
c✝ : γ
a✝ : (a✝², b✝¹, c✝) ∈ t
⊢ {in₀ ?m.4216, in₁ ?m.4219, in₂ ?m.4222} = {in₂ c✝¹, in₁ b✝¹, in₀ a✝²}

Tactic:
by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).EdgeDisjointTriangles

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ s, (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
· unfold EdgeDisjointTriangles
    convert! map_toTriangle_disjoint t
    rw [cliqueSet_eq_image, coe_map]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ s, (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
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}) =
    #((s * t).disjiUnion (fun x ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯)

Tactic:
· congr
    aesop (add unsafe mul_mem_mul)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u}) ^ 2 ≤ #u * Eₘ[s, t]

Tactic:
calc
    _ = (∑ c ∈ u, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 := by
        rw [← sum_card_fiberwise_eq_card_filter]
    _ ≤ #u * ∑ c ∈ u, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c} ^ 2 := by
        simpa using sum_mul_sq_le_sq_mul_sq (R := ℕ) _ 1 _
    _ ≤ #u * ∑ c ∈ s * t, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c} ^ 2 := by
        refine mul_le_mul_right (sum_le_sum_of_ne_zero ?_) _
        aesop (add simp [filter_eq_empty_iff]) (add unsafe mul_mem_mul)
    _ = #u * Eₘ[s, t] := by rw [mulEnergy_eq_sum_sq']

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: 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
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ (∏ j, x₀ j ^ d ↑j) * ∑ a, a ^ d i = 0

Tactic:
rw [sum_pow_lt_card_sub_one K _ hi, mul_zero]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: ⊢ (fun N ↦ ↑(rothNumberNat N)) =o[atTop] fun N ↦ ↑N

Tactic:
by
  simp only [isLittleO_iff, eventually_atTop, RCLike.norm_natCast]
  refine fun ε hε ↦ ⟨cornersTheoremBound (ε / 3), fun n hn ↦ ?_⟩
  obtain ⟨A, hs₁, hs₂, hs₃⟩ := rothNumberNat_spec n
  rw [← hs₂, ← not_lt]
  exact fun hδn ↦ roth_3ap_theorem_nat ε hε hn _ hs₁ hδn.le hs₃

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b ↦ bif b then f₂ else f₁
⊢ p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }

Tactic:
have : (∑ b : Bool, (F b).totalDegree) < Fintype.card σ := (add_comm _ _).trans_lt h

Goal state after:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f₁ f₂ : MvPolynomial σ K
h : f₁.totalDegree + f₂.totalDegree < Fintype.card σ
F : Bool → MvPolynomial σ K := fun b ↦ bif b then f₂ else f₁
this : ∑ b, (F b).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f₁ = 0 ∧ (eval x) f₂ = 0 }
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
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ 16 ^ #P.parts = ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))

Tactic:
rw [card_product, cast_mul, card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ←
      cast_mul, ← mul_pow]

Goal state after:
α : 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
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ 16 ^ #P.parts = ↑((4 * 4) ^ #P.parts)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
⊢ toColex (cons a s ha) ≤ toColex (cons b s hb) ↔ a ≤ b

Tactic:
by
  obtain rfl | hab := eq_or_ne a b
  · simp
  classical
  rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
    singleton_le_singleton]

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)

Tactic:
simp_rw [cross_apply, vec3_add]
  apply vec3_eq <;> dsimp <;> ring

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
obtain hwa | haw := (ne_of_mem_of_not_mem ha hws).symm.lt_or_gt

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
hwa : w < a
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
⊢ toColex (s.erase a) ≤ toColex (t.erase m)
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 = 0 ∧ v 1 = 0 ∧ v 2 = 0 ∧ ![] = 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 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : True → -w 0 = 0 ∧ v 0 = 0
h21 : True → -w 1 = 0 ∧ v 1 = 0
h22 : True → -w 2 = 0 ∧ v 2 = 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 = 0 ∧ v 1 = 0 ∧ v 2 = 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 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : True → -w 0 = 0 ∧ v 0 = 0
h21 : True → -w 1 = 0 ∧ v 1 = 0
h22 : True → -w 2 = 0 ∧ v 2 = 0
⊢ False
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : x ∈ fixedPoints ⇑(removeNone F)
⊢ x ∈ {a}

Tactic:
rw [mem_fixedPoints_iff] at x_fixed

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = some a
x : α
x_fixed : (removeNone F) x = x
⊢ x ∈ {a}
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: V : Type u_1
adj adj' : V → V → Bool
h : (fun v w ↦ adj v w = true) = fun v w ↦ adj' v w = true
v w : V
⊢ adj v w = adj' v w

Tactic:
simpa only [eq_iff_iff, Bool.coe_iff_coe] using congr($h v w)

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝ : Nontrivial L
this : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
⊢ ∃ p ∈ l₁, p ∈ l₂

Tactic:
have : ∀ q : { q // q ∈ l₂ }, p ≠ q := fun q hq => hl₂ ((congr_arg (· ∈ l₂) hq).mpr q.2)

Goal state after:
case neg
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
l₁ l₂ : L
hl : l₁ ≠ l₂
f : L → P
left✝ : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
this✝¹ : Nontrivial L
this✝ : Nontrivial P
h₁ : ∀ (p : P), 0 < lineCount L p
h₂ : ∀ (l : L), 0 < pointCount P l
p : P
hl₁ : p ∈ l₁
hl₂ : p ∉ l₂
key' : Fintype.card { q // q ∈ l₂ } = Fintype.card { l // p ∈ l }
this : ∀ (q : { q // q ∈ l₂ }), p ≠ ↑q
⊢ ∃ p ∈ l₁, p ∈ l₂
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:
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: case inr
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c d : 𝕜
a b : α
a✝ : a ≤ b
h : a ≠ b
x : α
x✝ : x ∈ Icc a b
⊢ (if x = b ∧ a = x then (algebraMap 𝕜 𝕝) c * (algebraMap 𝕜 𝕝) d else 0) = 0

Tactic:
exact if_neg fun hx ↦ h <| hx.2.trans hx.1

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

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

Tactic:
u,

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

Goal state before:
pp: case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ p.firstReturn < (↑(p + q)).length

Tactic:
u,

Goal state after:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ p.firstReturn < (↑p ++ ↑q).length
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
u,

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ (mu 𝕜 * zeta 𝕜) a b = ∑ x ∈ Icc a b, (mu 𝕜) a x

Tactic:
mul_apply

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, (mu 𝕜) a x
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ (zeta 𝕜 * mu' 𝕜) a b = ∑ x ∈ Icc a b, (mu' 𝕜) x b

Tactic:
mul_apply

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (mu' 𝕜) x b = ∑ x ∈ Icc a b, (mu' 𝕜) x b
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (↑p.nest).length

Tactic:
u,

Goal state after:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (U :: ↑p ++ [D]).length
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✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x ≤ y
⊢ f x.1 y.1 * g x.2 y.2 = 0

Tactic:
Prod.le_def,

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬(x.1 ≤ y.1 ∧ x.2 ≤ y.2)
⊢ f x.1 y.1 * g x.2 y.2 = 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
⊢ p ≤ q

Tactic:
rw [e] at h

Goal state after:
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
h : ↑r ++ ↑p = ↑q
e : r' = ↑r
⊢ p ≤ q
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ofTree p.toTree = p

Tactic:
by_cases h : p = 0
  · simp [h, toTree, ofTree]
  · rw [toTree]
    simp_rw [h, ite_false, ofTree]
    rw [ofTree_toTree p.insidePart, ofTree_toTree p.outsidePart]
    exact nest_insidePart_add_outsidePart h

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

Goal state before:
pp: k : ℤ
⊢ 2 * ↑(pentagonal (-k)) = k * (3 * k + 1)

Tactic:
grind [two_mul_natCast_pentagonal]

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

Goal state before:
pp: x y : ℤ
h : pentagonal x = pentagonal y
⊢ (3 * (x + y) - 1) * (x - y) = 0

Tactic:
grind [two_mul_natCast_pentagonal]

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

Goal state before:
pp: case hfg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) =
    if i * Multiset.count i p.parts = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0

Tactic:
simp [Nat.sub_add_cancel (Multiset.one_le_count_iff_mem.mpr hi)]

Goal state after:
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:
simp_rw [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.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ E(H) \ F ⊆ E(G) \ F

Tactic:
exact sdiff_subset_sdiff_left h.edgeSet_mono

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

Goal state before:
pp: α : Type u_1
β : Type u_4
G : Graph α β
⊢ map id G = G

Tactic:
ext a b c <;> simp

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

Goal state before:
pp: case refine_1.inr
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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ (⋂₀ c).Nonempty

Tactic:
convert!
      @IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ _ _ hcnemp.coe_sort
        ((↑) : c → Set M) ?_ ?_ ?_ ?_

Goal state after:
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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ⋂₀ c = ⋂ i, ↑i

case refine_1.inr.convert_1
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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ Directed (fun x1 x2 ↦ x1 ⊇ x2) Subtype.val

case refine_1.inr.convert_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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), (↑i).Nonempty

case refine_1.inr.convert_3
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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), IsCompact ↑i

case refine_1.inr.convert_4
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}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ∀ (i : ↑c), IsClosed ↑i
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M ＼ D).IsCocircuit (K \ D)

Tactic:
by
  rw [isCocircuit_def, dual_delete]
  exact hK.isCircuit.contract_isCircuit hD

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sum' M).Finitary

Tactic:
by
  have := Finitary.sigma h
  rw [Matroid.sum']
  infer_instance

Goal state after: