mathlib-initiative/mathlib-tactics huggingface dataset:
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₂ }
⊢ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
[

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.Configuration

Goal state before:
pp: 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
l : { l // p ∈ l }
⊢ order P L + Fintype.card { x // x = ⟨p, ⋯⟩ } = order P L + Fintype.card { x // ↑x = p }

Tactic:
[

Goal state after:
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
l : { l // p ∈ l }
⊢ order P L + Fintype.card { x // x = ⟨p, ⋯⟩ } = order P L + Fintype.card { x // ↑x = p }
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
⊢ Fintype.card P = order P L ^ 2 + order P L + 1

Tactic:
[

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
⊢ Fintype.card P = order P L ^ 2 + order P L + 1
Module: Mathlib.Combinatorics.Configuration

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

Tactic:
[

Goal state after:
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : ¬((crossProduct a) b = 0 ∨ (crossProduct c) d = 0)
⊢ False
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case «0»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
j : Fin 2
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨0, ⋯⟩) j = 0 ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case «1»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
j : Fin 2
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨1, ⋯⟩) j = 0 ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
⊢ (A * Bᵀ) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

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

Tactic:
[

Goal state after:
case ind
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(catalan d.succ) = ↑d.succ.centralBinom / (↑d.succ + 1)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
[

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ (z * a⁻¹)⁻¹ •> A ⊆ A⁻¹ * A * (A⁻¹ * A)

Tactic:
simp only [← hz, mul_inv_rev, inv_inv, ← mul_assoc]

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⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ (a * a⁻¹ * c⁻¹ * b * a⁻¹) •> A ⊆ A⁻¹ * A * A⁻¹ * 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)

Tactic:
[

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⁻¹ * A) = #(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) * A⁻¹ = A⁻¹ * A

Tactic:
[

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) * A⁻¹ = A⁻¹ * A
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ((↑p).dropLast ++ [U]) = count D ((↑p).dropLast ++ [U])
⊢ False

Tactic:
[

Goal state after:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ((↑p).dropLast ++ [U]) = count D ((↑p).dropLast ++ [U])
⊢ False
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:
[

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⁻¹ * A) = A * A⁻¹
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:
[

Goal state after:
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)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.denest ⋯ = p

Tactic:
[

Goal state after:
p : DyckWord
⊢ p.nest.denest ⋯ = p
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
⊢ f = g

Tactic:
refine DFunLike.coe_injective (funext₂ fun a b ↦ ?_)

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
⊢ f a b = g a b
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✝¹ : AddZeroClass 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (⇑f + ⇑g) a b = 0

Tactic:
[

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddZeroClass 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (⇑f + ⇑g) a b = 0
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
M : Type u_7
inst✝² : Zero 𝕜
inst✝¹ : LE α
inst✝ : SMulZeroClass M 𝕜
c : M
f : IncidenceAlgebra 𝕜 α
a b : α
hab : ¬a ≤ b
⊢ (c • ⇑f) a b = 0

Tactic:
[

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
M : Type u_7
inst✝² : Zero 𝕜
inst✝¹ : LE α
inst✝ : SMulZeroClass M 𝕜
c : M
f : IncidenceAlgebra 𝕜 α
a b : α
hab : ¬a ≤ b
⊢ (c • ⇑f) a b = 0
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 : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (-⇑f) a b = 0

Tactic:
[

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup 𝕜
inst✝ : LE α
f : IncidenceAlgebra 𝕜 α
a b : α
h : ¬a ≤ b
⊢ (-⇑f) a b = 0
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
⊢ (⇑f - ⇑g) a b = 0

Tactic:
[

Goal state after:
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
⊢ (⇑f - ⇑g) a b = 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ∑ x ∈ S, r x = ∑ x ∈ S with (K - 1) * ↑(#A) < ↑(r x), r x + ∑ x ∈ S with ↑(r x) ≤ (K - 1) * ↑(#A), r x

Tactic:
[

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 - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
hk : l = #({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)})
⊢ ∑ x ∈ S, r x = ∑ x ∈ S with (K - 1) * ↑(#A) < ↑(r x), r x + ∑ x ∈ S with ↑(r x) ≤ (K - 1) * ↑(#A), r x
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:
[

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: 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:
[

Goal state after:
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
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
hi : i ≠ 0
⊢ Summable fun j ↦ f i (j + 1) • X ^ (i * (j + 1))

Tactic:
obtain ⟨a, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hi
  apply summable_genFun_term

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

Goal state before:
pp: case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Tactic:
[

Goal state after:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (U :: List.take j (↑p ++ [D])) = count D (U :: List.take j (↑p ++ [D]))) = false

Tactic:
count_cons,

Goal state after:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide
      ((count U (List.take j (↑p ++ [D])) + if (U == U) = true then 1 else 0) =
        count D (List.take j (↑p ++ [D])) + if (U == D) = true then 1 else 0) =
    false
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
⊢ (mu 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a

Tactic:
[

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 𝕜) (toDual a) (toDual b) = (mu 𝕜) b a
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
[

Goal state after:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (range (↑p.nest).length).length
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, (mu 𝕜) x y * g y = ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, f z

Tactic:
[

Goal state after:
𝕜 : 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, (mu 𝕜) x y * g y = ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, f z
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
[

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ (p + q).insidePart = p.insidePart
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
[

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ (p + q).outsidePart = p.outsidePart + q
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.insidePart = p

Tactic:
[

Goal state after:
p : DyckWord
⊢ p.nest.insidePart = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ (↑p.nest).length ≤ (↑p).length + 1 + 1

Tactic:
[

Goal state after:
p : DyckWord
⊢ (↑p.nest).length ≤ (↑p).length + 1 + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ (↑p.nest).length ≤ (↑p).length + 1 + 1

Tactic:
simp_rw [nest, length_append, length_singleton]

Goal state after:
p : DyckWord
⊢ 1 + (↑p).length + 1 ≤ (↑p).length + 1 + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.outsidePart = 0

Tactic:
[

Goal state after:
p : DyckWord
⊢ p.nest.outsidePart = 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.insidePart.nest + p.outsidePart = p

Tactic:
[

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ p.insidePart.nest + p.outsidePart = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
by
  have := semilength_insidePart_add_semilength_outsidePart_add_one h
  lia

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ p.outsidePart.semilength < p.semilength

Tactic:
by
  have := semilength_insidePart_add_semilength_outsidePart_add_one h
  lia

Goal state after:
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
⊢ ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z = ∑ z ≥ x, (mu 𝕜 * zeta 𝕜) x z * f z

Tactic:
[

Goal state after:
𝕜 : 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
⊢ ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z = ∑ z ≥ x, (mu 𝕜 * zeta 𝕜) x z * f z
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = 0
⊢ ↑p <:+: ↑0

Tactic:
mq

Goal state after:
case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑0
mq : m = 0
⊢ ↑p <:+: ↑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
⊢ r' = ↑r

Tactic:
[

Goal state after:
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
⊢ r' = ↑r
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = 0
⊢ p.semilength ≤ semilength 0

Tactic:
mq

Goal state after:
case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ semilength 0
mq : m = 0
⊢ p.semilength ≤ semilength 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : 2 * p.semilength = 2 * q.semilength
⊢ p = q

Tactic:
[

Goal state after:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : 2 * p.semilength = 2 * q.semilength
⊢ p = q
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ ofTree (if p = 0 then BinaryTree.nil else node () p.insidePart.toTree p.outsidePart.toTree) = p

Tactic:
[

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ ofTree (if p = 0 then BinaryTree.nil else node () p.insidePart.toTree p.outsidePart.toTree) = p