mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case base
n : ℕ
⊢ nil ∈ treesOfNumNodesEq n ↔ nil.numNodes = n

pp: case ind
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
n : ℕ
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq n ↔ (node () x✝ y✝).numNodes = n

Tactic:
<;>

Goal state after:
case base
n : ℕ
⊢ nil ∈ treesOfNumNodesEq n ↔ nil.numNodes = n

case ind
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
n : ℕ
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq n ↔ (node () x✝ y✝).numNodes = n
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case base.zero
⊢ nil ∈ treesOfNumNodesEq 0 ↔ nil.numNodes = 0

pp: case base.succ
n✝ : ℕ
⊢ nil ∈ treesOfNumNodesEq (n✝ + 1) ↔ nil.numNodes = n✝ + 1

pp: case ind.zero
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq 0 ↔ (node () x✝ y✝).numNodes = 0

pp: case ind.succ
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
n✝ : ℕ
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq (n✝ + 1) ↔ (node () x✝ y✝).numNodes = n✝ + 1

Tactic:
<;>

Goal state after:
case base.zero
⊢ nil ∈ treesOfNumNodesEq 0 ↔ nil.numNodes = 0

case base.succ
n✝ : ℕ
⊢ nil ∈ treesOfNumNodesEq (n✝ + 1) ↔ nil.numNodes = n✝ + 1

case ind.zero
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq 0 ↔ (node () x✝ y✝).numNodes = 0

case ind.succ
x✝ y✝ : BinaryTree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ x✝.numNodes = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ y✝.numNodes = n
n✝ : ℕ
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq (n✝ + 1) ↔ (node () x✝ y✝).numNodes = n✝ + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

pp: case D
⊢ D = U ∨ D = D

Tactic:
<;>

Goal state after:
case U
⊢ U = U ∨ U = D

case D
⊢ D = U ∨ D = D
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

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

Tactic:
<;>

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

case cons.nil.D
bal : count U [D] = count D [D]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (take i [D]) ≤ count U (take i [D])
h : { toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ 0
h' : ↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
⊢ take 1 (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).dropLast =
    [(↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h']
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = [(↑p).head h'] ++ (↑p).dropLast.tail ++ [D]

Tactic:
head_eq_U

Goal state after:
p : DyckWord
h : p ≠ 0
h' : ↑p ≠ []
this : take 1 (↑p).dropLast = [(↑p).head h']
⊢ U :: (↑p).dropLast.tail ++ [D] = [U] ++ (↑p).dropLast.tail ++ [D]
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i ↑p) = count D (List.take i ↑p)
k : ℕ
⊢ count D (List.take k (List.take i ↑p)) ≤ count U (List.take k (List.take i ↑p))

Tactic:
rw [take_take]; exact p.count_D_le_count_U (min k i)

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]

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

Goal state after:
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]

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]
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq :
  count D [(↑p).head h] + count D (List.drop 1 (List.take j ↑p)) <
    count U [(↑p).head h] + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))

Tactic:
head_eq_U

Goal state after:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : ↑p ≠ []
l1 : List.take 1 ↑p = [(↑p).head h]
l3 : (↑p).length - 1 = (↑p).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p).length - 1)
ub : j < (↑p).length
lb : 0 < j
eq : count D [U] + count D (List.drop 1 (List.take j ↑p)) < count U [U] + count U (List.drop 1 (List.take j ↑p))
⊢ count D (List.drop 1 (List.take j ↑p)) ≤ count U (List.drop 1 (List.take j ↑p))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

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

Tactic:
<;>

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

case e'_6.D
p : DyckWord
⊢ (D == U) = decide ¬(D == D) = true
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
take_of_length_le (le_refl _),

Goal state after:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ count U ↑p = count D ↑p
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1

Tactic:
rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]

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

Goal state before:
pp: case inl
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
⊢ f x.1 y.1 * g x.2 y.2 = 0

pp: case inr
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.2 ≤ y.2
⊢ f x.1 y.1 * g x.2 y.2 = 0

Tactic:
<;>

Goal state after:
case inl
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
⊢ f x.1 y.1 * g x.2 y.2 = 0

case inr
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.2 ≤ y.2
⊢ f x.1 y.1 * g x.2 y.2 = 0
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

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

Tactic:
rcases k with (_ | _) | _

Goal state after:
case ofNat.zero
⊢ ↑(pentagonal (Int.ofNat 0)) = Int.ofNat 0 * (3 * Int.ofNat 0 - 1) / 2

case ofNat.succ
n✝ : ℕ
⊢ ↑(pentagonal (Int.ofNat (n✝ + 1))) = Int.ofNat (n✝ + 1) * (3 * Int.ofNat (n✝ + 1) - 1) / 2

case negSucc
a✝ : ℕ
⊢ ↑(pentagonal (Int.negSucc a✝)) = Int.negSucc a✝ * (3 * Int.negSucc a✝ - 1) / 2
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: case ofNat.zero
⊢ ↑(pentagonal (Int.ofNat 0)) = Int.ofNat 0 * (3 * Int.ofNat 0 - 1) / 2

pp: case ofNat.succ
n✝ : ℕ
⊢ ↑(pentagonal (Int.ofNat (n✝ + 1))) = Int.ofNat (n✝ + 1) * (3 * Int.ofNat (n✝ + 1) - 1) / 2

pp: case negSucc
a✝ : ℕ
⊢ ↑(pentagonal (Int.negSucc a✝)) = Int.negSucc a✝ * (3 * Int.negSucc a✝ - 1) / 2

Tactic:
<;>

Goal state after:
case ofNat.zero
⊢ ↑(pentagonal (Int.ofNat 0)) = Int.ofNat 0 * (3 * Int.ofNat 0 - 1) / 2

case ofNat.succ
n✝ : ℕ
⊢ ↑(pentagonal (Int.ofNat (n✝ + 1))) = Int.ofNat (n✝ + 1) * (3 * Int.ofNat (n✝ + 1) - 1) / 2

case negSucc
a✝ : ℕ
⊢ ↑(pentagonal (Int.negSucc a✝)) = Int.negSucc a✝ * (3 * Int.negSucc a✝ - 1) / 2
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

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

pp: case inr
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
h✝ : x - y = 0
⊢ x = y

Tactic:
<;>

Goal state after:
case inl
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
h✝ : 3 * (x + y) - 1 = 0
⊢ x = y

case inr
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
h✝ : x - y = 0
⊢ x = y
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
⊢ ↑(#A) - K * ↑(#A) ≤ ↑(#(A * S)) - K * ↑(#A)

Tactic:
have := card_le_card_mul_right hS (s := A)

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hS : S.Nonempty
this : #A ≤ #(A * S)
⊢ ↑(#A) - K * ↑(#A) ≤ ↑(#(A * S)) - K * ↑(#A)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : 0 < expansion K S A
⊢ A.Nonempty

Tactic:
by by_contra! rfl; simp at hA

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 ∈ range d

pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 + 1 = i

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 ∈ range d

case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 + 1 = i
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
          (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
        ⊥.largeSchroder * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ < n + 1

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0

Tactic:
<;>

Goal state after:
n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
          (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
        ⊥.largeSchroder * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ < n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ n + 1 - i ≠ 0

pp: case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0

Tactic:
<;>

Goal state after:
case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ n + 1 - i ≠ 0

case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case zero
⊢ stirlingFirst 0 0 = 1

pp: case succ
n✝ : ℕ
a✝ : n✝.stirlingFirst n✝ = 1
⊢ (n✝ + 1).stirlingFirst (n✝ + 1) = 1

Tactic:
<;>

Goal state after:
case zero
⊢ stirlingFirst 0 0 = 1

case succ
n✝ : ℕ
a✝ : n✝.stirlingFirst n✝ = 1
⊢ (n✝ + 1).stirlingFirst (n✝ + 1) = 1
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case zero
⊢ stirlingSecond 0 0 = 1

pp: case succ
n✝ : ℕ
a✝ : n✝.stirlingSecond n✝ = 1
⊢ (n✝ + 1).stirlingSecond (n✝ + 1) = 1

Tactic:
<;>

Goal state after:
case zero
⊢ stirlingSecond 0 0 = 1

case succ
n✝ : ℕ
a✝ : n✝.stirlingSecond n✝ = 1
⊢ (n✝ + 1).stirlingSecond (n✝ + 1) = 1
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : CommRing α
s✝ : Finset α
x : α × α × α
s : Finset α
⊢ Function.Injective fun xa ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)

Tactic:
by
      rintro ⟨x, a⟩ ⟨y, b⟩ h
      simp only [Prod.ext_iff] at h
      obtain rfl := h.1
      obtain rfl := add_right_injective _ h.2.1
      rfl

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

Goal state before:
pp: case refine_5.h₁
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ n + 1 ≤ k + 1

pp: case refine_5.h₂
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ 2 ≤ 3 * k + 4

Tactic:
<;>

Goal state after:
case refine_5.h₁
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ n + 1 ≤ k + 1

case refine_5.h₂
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ 2 ≤ 3 * k + 4
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z

pp: case inr.inr
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z

Tactic:
<;>

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z

case inr.inr
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: case vertexSet_mono
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (V(noEdge ∅ β) ⊆ V(G)) IsSubgraph.vertexSet_mono._autoParam

pp: case isLink_mono
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, (noEdge ∅ β).IsLink e x y → G.IsLink e x y) IsSubgraph.isLink_mono._autoParam

Tactic:
<;>

Goal state after:
case vertexSet_mono
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (V(noEdge ∅ β) ⊆ V(G)) IsSubgraph.vertexSet_mono._autoParam

case isLink_mono
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, (noEdge ∅ β).IsLink e x y → G.IsLink e x y) IsSubgraph.isLink_mono._autoParam
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.Inc e = G₂.Inc f → G₁.IsLink e = G₂.IsLink f

pp: case mpr
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.IsLink e = G₂.IsLink f → G₁.Inc e = G₂.Inc f

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.Inc e = G₂.Inc f → G₁.IsLink e = G₂.IsLink f

case mpr
α : Type u_1
β : Type u_2
e f : β
G₁ G₂ : Graph α β
⊢ G₁.IsLink e = G₂.IsLink f → G₁.Inc e = G₂.Inc f
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ H.restrict F ≤ G.restrict F

Tactic:
refine (Compatible.of_le_le (G := G) (restrict_le.trans h) (by simp)).le_iff.mpr ⟨?_, ?_⟩
  · simpa using h.vertexSet_mono
  simp [inter_subset_left.trans h.edgeSet_mono]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y

pp: case inr
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y

case inr
α : Type u_1
β : Type u_2
y : α
e : β
G : Graph α β
h' : G.Inc e y
h : G.IsLoopAt e y
⊢ y = y
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ y✝ : α
e✝ : β
G✝ H : Graph α β
F✝ F₀ : Set β
X : Set α
G : Graph α β
F : Set β
e : β
x y : α
⊢ (G.restrict (E(G) \ F)).IsLink e x y ↔ G.IsLink e x y ∧ e ∉ F

Tactic:
simp only [restrict_isLink, mem_sdiff, and_comm, and_congr_left_iff, and_iff_left_iff_imp]
    exact fun h _ ↦ h.edge_mem

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

Goal state before:
pp: case hV
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
x✝ : α
⊢ x✝ ∈ V(G.copy hV hE h_isLink) ↔ x✝ ∈ V(G)

pp: case h
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e✝ : β
x✝ y✝ : α
⊢ (G.copy hV hE h_isLink).IsLink e✝ x✝ y✝ ↔ G.IsLink e✝ x✝ y✝

Tactic:
<;>

Goal state after:
case hV
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
x✝ : α
⊢ x✝ ∈ V(G.copy hV hE h_isLink) ↔ x✝ ∈ V(G)

case h
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e✝ : β
x✝ y✝ : α
⊢ (G.copy hV hE h_isLink).IsLink e✝ x✝ y✝ ↔ G.IsLink e✝ x✝ y✝
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case hV
α : Type u_1
β : Type u_2
u v x✝ : α
⊢ x✝ ∈ V(banana u v ∅) ↔ x✝ ∈ V(noEdge {u, v} β)

pp: case h
α : Type u_1
β : Type u_2
u v : α
e✝ : β
x✝ y✝ : α
⊢ (banana u v ∅).IsLink e✝ x✝ y✝ ↔ (noEdge {u, v} β).IsLink e✝ x✝ y✝

Tactic:
<;>

Goal state after:
case hV
α : Type u_1
β : Type u_2
u v x✝ : α
⊢ x✝ ∈ V(banana u v ∅) ↔ x✝ ∈ V(noEdge {u, v} β)

case h
α : Type u_1
β : Type u_2
u v : α
e✝ : β
x✝ y✝ : α
⊢ (banana u v ∅).IsLink e✝ x✝ y✝ ↔ (noEdge {u, v} β).IsLink e✝ x✝ y✝