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

Goal state before:
pp: case in₀₁
α : 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
⊢ ∃ z ∈ t, in₀ a✝¹ ∈ toTriangle z ∧ in₁ b✝ ∈ toTriangle z

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: case in₁₀
α : 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
⊢ ∃ z ∈ t, in₁ b✝ ∈ toTriangle z ∧ in₀ a✝¹ ∈ toTriangle z

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: case in₀₂
α : 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
⊢ ∃ z ∈ t, in₀ a✝¹ ∈ toTriangle z ∧ in₂ c✝ ∈ toTriangle z

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: case in₂₀
α : 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
⊢ ∃ z ∈ t, in₂ c✝ ∈ toTriangle z ∧ in₀ a✝¹ ∈ toTriangle z

Tactic:
exact ⟨_, ‹_›, by simp⟩

Goal state after:
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm✝ : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : 0 < ↑m
⊢ (↑m + 1) * (↑m - 1) ≤ ↑m * ↑m

Tactic:
linarith

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

Goal state before:
pp: case in₁₂
α : 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
⊢ ∃ z ∈ t, in₁ b✝ ∈ toTriangle z ∧ in₂ c✝ ∈ toTriangle z

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: case in₂₁
α : 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
⊢ ∃ z ∈ t, in₂ c✝ ∈ toTriangle z ∧ in₁ b✝ ∈ toTriangle z

Tactic:
exact ⟨_, ‹_›, by simp⟩

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : DecidableEq G
A B : Finset G
inst✝ : Fintype G
⊢ σₘ[A, B] ≤ A.dens⁻¹

Tactic:
rw [dens, inv_div, mulConst]; gcongr; exact card_le_univ _

Goal state after:
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
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ 0 ≤ 3 / 4 * ε

Tactic:
linarith

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

pp: case neg
α : 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
        exact ⟨c, hcu, hcs, hab.trans hbc⟩

Goal state after:
case neg
α : 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
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : 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}
w : α
⊢ w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w

Tactic:
simp [u, and_assoc]

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
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
x a : G
ha : a ∈ A
⊢ a •> (x * a) ∈ a •> A ↔ a * x ∈ A

Tactic:
smul_A_eq_A_smul ha,

Goal state after:
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
x a : G
ha : a ∈ A
⊢ a •> (x * a) ∈ A <• a ↔ a * x ∈ A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

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

Tactic:
linarith

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

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

Tactic:
linarith

Goal state after:
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝² x✝¹ : V
x✝ : ⊥.toSimpleGraphInclusive.Adj x✝² x✝¹
left✝ : x✝² ≠ x✝¹
h : ⊥.Adj x✝² x✝¹ ∨ ⊥.Adj x✝¹ x✝²
⊢ ⊥.Adj x✝² x✝¹

Tactic:
tauto

Goal state after:
Module: Mathlib.Combinatorics.Digraph.Orientation

Goal state before:
pp: V : Type u_1
x✝² x✝¹ : V
x✝ : ⊥.toSimpleGraphStrict.Adj x✝² x✝¹
left✝ : x✝² ≠ x✝¹
h : ⊥.Adj x✝² x✝¹ ∧ ⊥.Adj x✝¹ x✝²
⊢ ⊥.Adj x✝² x✝¹

Tactic:
tauto

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

Goal state before:
pp: ι : Sort u_1
V : Type u_2
G✝ : Digraph V
a b : V
G : Digraph V
v w : V
x✝ : (Digraph.completeDigraph V).Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
tauto

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✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ 1 < order P L

Tactic:
rw [← add_lt_add_iff_right 1, ← pointCount_eq _ l₂, pointCount, Nat.card_eq_fintype_card,
    Fintype.two_lt_card_iff]

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
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))
this : ↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) ≤ ↑(#A)
⊢ 0 < ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)))

Tactic:
linarith

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 * A)) < 2 * ↑(#A)

Tactic:
linarith

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

Tactic:
by
  rw [invMulSubgroup_eq_inv_mul, eq_comm]
  norm_cast
  exact mul_inv_eq_inv_mul_of_doubling_lt_two (by qify at h ⊢; linarith)

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h.h.h.h
K : Type u_3
inst✝ : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K d hd)
hbd : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K d hd)
⊢ Projectivization.mk K a ha = Projectivization.mk K b hb ∨ Projectivization.mk K c hc = Projectivization.mk K d hd

Tactic:
| h d hd =>

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

Goal state before:
pp: case U
⊢ U = U ∨ U = D

Tactic:
tauto

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

Goal state before:
pp: case D
⊢ D = U ∨ D = D

Tactic:
tauto

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

Goal state before:
pp: case nil
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
h : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h = U

Tactic:
tauto

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

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + if False then 1 else 0
⊢ False

Tactic:
ite_false

Goal state after:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + 0
⊢ False
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case nil
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
h : { toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1
      (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h']

Tactic:
tauto

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

Goal state before:
pp: case cons.cons
s head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: head✝ :: tail✝) = count D (s :: head✝ :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i (s :: head✝ :: tail✝)) ≤ count U (take i (s :: head✝ :: tail✝))
h :
  { toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
      count_D_le_count_U := count_D_le_count_U✝ } ≠
    0
h' :
  ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
        count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
⊢ take 1
      (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h']

Tactic:
tauto

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
⊢ 0 < φ - K

Tactic:
linarith

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

Goal state before:
pp: case nil
q : DyckWord
i : ℕ
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i []) ≤ count U (List.take i [])
hn : { toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ List.take 1 ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h]

Tactic:
tauto

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

Goal state before:
pp: case cons
q : DyckWord
i : ℕ
head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (head✝ :: tail✝) = count D (head✝ :: tail✝)
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i (head✝ :: tail✝)) ≤ count U (List.take i (head✝ :: tail✝))
h :
  ↑{ toList := head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
⊢ List.take 1
      ↑{ toList := head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
          count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h]

Tactic:
tauto

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

Goal state before:
pp: case nil
q : DyckWord
i : ℕ
count_U_eq_count_D✝ : count U [] = count D []
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i []) ≤ count U (List.take i [])
hn : { toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D✝, count_D_le_count_U := count_D_le_count_U✝ }).length -
          1 -
        1 +
      1

Tactic:
tauto

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

Goal state before:
pp: case cons.cons
q : DyckWord
i : ℕ
s head✝ : DyckStep
tail✝ : List DyckStep
count_U_eq_count_D✝ : count U (s :: head✝ :: tail✝) = count D (s :: head✝ :: tail✝)
count_D_le_count_U✝ :
  ∀ (i : ℕ), count D (List.take i (s :: head✝ :: tail✝)) ≤ count U (List.take i (s :: head✝ :: tail✝))
hn :
  { toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
      count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h :
  ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
        count_D_le_count_U := count_D_le_count_U✝ } ≠
    []
l1 :
  List.take 1
      ↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
          count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
              count_D_le_count_U := count_D_le_count_U✝ }).head
        h]
⊢ (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
            count_D_le_count_U := count_D_le_count_U✝ }).length -
      1 =
    (↑{ toList := s :: head✝ :: tail✝, count_U_eq_count_D := count_U_eq_count_D✝,
                count_D_le_count_U := count_D_le_count_U✝ }).length -
          1 -
        1 +
      1

Tactic:
tauto

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this✝¹ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
this✝ : (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)
this : ↑(#S) ≠ 0
⊢ ((φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) / ↑(#S))⁻¹ = (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
simp [this]

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

Goal state before:
pp: case e'_6.U
p : DyckWord
⊢ (U == U) = decide ¬(U == D) = true

Tactic:
tauto

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

Goal state before:
pp: case e'_6.D
p : DyckWord
⊢ (D == U) = decide ¬(D == D) = true

Tactic:
tauto

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ ∃ x < (↑p).length, count U (List.take (x + 1) ↑p) = count D (List.take (x + 1) ↑p)

Tactic:
use p.toList.length - 1

Goal state after:
case h
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ (↑p).length - 1 < (↑p).length ∧
    count U (List.take ((↑p).length - 1 + 1) ↑p) = count D (List.take ((↑p).length - 1 + 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:

Tactic:
_ = (∑ a ∈ p.parts.toFinset, p.parts.count a * a) * p.parts.bell := by
    rw [succ_eq_add_one, mul_eq_mul_right_iff]
    left
    simpa [smul_eq_mul, p.parts_sum] using Finset.sum_multiset_count p.parts
  _ = ∑ a ∈ p.parts.toFinset, a * (p.parts.count a * p.parts.bell) := by grind [Finset.sum_mul]
  _ = ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell) := by
    congr! 1 with a ha
    have ha0 : a ≠ 0 := by grind
    have hsum : (p.parts.erase a).sum + a = n + 1 := by
      simpa [p.parts_sum, add_comm] using congrArg Multiset.sum (cons_erase (mem_dedup.mp ha))
    grind [Nat.add_one_mul_choose_eq, cons_erase, bell_cons_mul_count]
  _ = _ := by rw [Finset.mul_sum]

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

Goal state before:
pp: case a
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
p : (n + 1).Partition
a✝ : p ∈ Finset.univ
⊢ ∑ a, n.choose (↑a - 1) * (p.parts.erase ↑a).bell = p.parts.bell

Tactic:
bell_eq_sum_erase p

Goal state after:
case a
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
p : (n + 1).Partition
a✝ : p ∈ Finset.univ
⊢ ∑ a, n.choose (↑a - 1) * (p.parts.erase ↑a).bell = ∑ a ∈ p.parts.toFinset, n.choose (a - 1) * (p.parts.erase a).bell
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 < (C (f (i + 1) (m + 1)) * X ^ ((i + 1) * (m + 1))).order

Tactic:
← le_order_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))).order + (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
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
this : g x ≠ 0
⊢ (coeff (g x)) 1 = 0

Tactic:
simp [this]

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
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
i : ℕ
this : g x ≠ x * (i + 1)
⊢ (if g x = x * (i + 1) then 1 else 0) = 0

Tactic:
simp [this]

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
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
x : ℕ
hx : x ∉ s
this : g x = 0
⊢ x ∣ g x

Tactic:
simp [this]

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

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i b : ℕ
hn : b ∈ range (m - 1)
this : b + 1 < m
⊢ X ^ ((i + 1) * (b + 1)) = (if b + 1 < m then 1 else 0) • X ^ ((i + 1) * (b + 1))

Tactic:
simp [this]

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

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

Tactic:
rw [eq_sub_iff_add_eq, show 1 - x ^ (2 * k + 3) = 0 - aux k 0 x by simp [aux]]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ ∑' (n : ℕ), powMulProdOneSubPow k n x + x ^ (3 * k + 5) * ∑' (n : ℕ), powMulProdOneSubPow (k + 1) n x = 0 - aux k 0 x