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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ Set.InjOn q.getVert {i | i ≤ q.length}

Tactic:
intro n hn m hm hnm

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ∈ {i | i ≤ q.length}
m : ℕ
hm : m ∈ {i | i ≤ q.length}
hnm : q.getVert n = q.getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ G.LocallyLinear

Tactic:
rw [← comap_map_eq e.symm.toEmbedding G, comap_symm, map_symm]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : (SimpleGraph.comap (⇑e) G).LocallyLinear
⊢ (SimpleGraph.map (⇑e.toEmbedding) (SimpleGraph.comap (⇑e.toEmbedding) G)).LocallyLinear
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.comap (⇑e.toEmbedding) G).LocallyLinear

Tactic:
← map_symm

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → (SimpleGraph.map (⇑e.symm.toEmbedding) G).LocallyLinear
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos.inr
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx✝ : x ∈ s
y : α
hy✝ : y ∈ s
hxy : x ≠ y
hx : x ∈ s \ {w}
hy : y ∈ s \ {w}
⊢ (G ⊔ edge v w).Adj x y

Tactic:
exact hw.mono le_sup_left hx hy hxy

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
⊢ Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
intro n hn m hm hnm

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
hn : n ∈ {i | 1 ≤ i ∧ i ≤ p.length}
m : ℕ
hm : m ∈ {i | 1 ≤ i ∧ i ≤ p.length}
hnm : p.getVert n = p.getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
t : Finset β
f : α ↪ β
h' : #t ≤ 1
hn : 1 < #t
⊢ False

Tactic:
exact h'.not_gt hn

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ Set.InjOn p.getVert {i | i ≤ p.length - 1}

Tactic:
intro n hn m hm hnm

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ∈ {i | i ≤ p.length - 1}
m : ℕ
hm : m ∈ {i | i ≤ p.length - 1}
hnm : p.getVert n = p.getVert m
⊢ n = m
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length

Tactic:
by
  refine ⟨fun h ↦ ⟨h.isPath_tail, h.three_le_length⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  cases p with
  | nil => simp_all
  | cons h' p =>
    simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂
    refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩
    have : p.support[0] = p.support[p.length - 1] := by
      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
    have := p.isPath_iff_injective_get_support.mp h₁ this
    lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFreeOn ∅ n ↔ n ≠ 0

Tactic:
by
  simp [CliqueFreeOn, Set.subset_empty_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ Gᶜ.IsClique s ↔ s.Pairwise fun v w ↦ ¬G.Adj v w

Tactic:
isClique_iff

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise Gᶜ.Adj ↔ s.Pairwise fun v w ↦ ¬G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w ↦ ¬Gᶜ.Adj v w) ↔ G.IsClique s

Tactic:
isClique_iff

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w ↦ ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
t : Finset α
tc : Gᶜ.IsClique ↑t
⊢ #t ≤ sSup {n | ∃ s, Gᶜ.IsNClique n s}

Tactic:
exact tc.card_le_cliqueNum

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this✝ : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
this : y₁ - x₂ = y₁ - x₁
⊢ x₁ = x₂

Tactic:
by simpa using this.symm

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

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

Tactic:
simp [S]

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

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
a : M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
hA : ∀ x ∈ A, 0 < x
hAa : ∀ x ∈ A, x < a
ha : 0 < a
disjoint : Disjoint (insert 0 A) (a +ᵥ A.subsetSum)
insert_subset : insert 0 A ⊆ (insert a A).subsetSum
vadd_subset : a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
⊢ #(insert 0 A) + #(a +ᵥ A.subsetSum) = #(insert 0 A ∪ (a +ᵥ A.subsetSum))

Tactic:
by rw [card_union_of_disjoint disjoint]

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

Goal state before:
pp: case bit
b : Bool
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit b n).bitIndices ↔ (bit b n).testBit i = true

Tactic:
cases b <;> cases i

Goal state after:
case bit.false.zero
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
⊢ 0 ∈ (bit false n).bitIndices ↔ (bit false n).testBit 0 = true

case bit.false.succ
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
n✝ : ℕ
⊢ n✝ + 1 ∈ (bit false n).bitIndices ↔ (bit false n).testBit (n✝ + 1) = true

case bit.true.zero
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
⊢ 0 ∈ (bit true n).bitIndices ↔ (bit true n).testBit 0 = true

case bit.true.succ
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
n✝ : ℕ
⊢ n✝ + 1 ∈ (bit true n).bitIndices ↔ (bit true n).testBit (n✝ + 1) = true
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ v = ![v 0, v 1, v 2]

Tactic:
simp [← List.ofFn_inj]

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
⊢ w = ![w 0, w 1, w 2]

Tactic:
simp [← List.ofFn_inj]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : ∀ (a : K), a • D.rep ≠ D'.rep
hD : D = D'
⊢ 1 • D.rep = D'.rep

Tactic:
simp [hD]

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

Goal state before:
pp: case some
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
⊢ (Equiv.swap none (some a)) ((⇑(Equiv.swap none (some a)) ∘ ⇑(optionCongr f)) (some x)) ≠
    (Equiv.swap none (some a)) (some x)

Tactic:
simp only [comp, optionCongr_apply, Option.map_some, swap_apply_self]

Goal state after:
case some
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)
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✝¹ : Finite P
inst✝ : Finite L
p q : P
val✝¹ : Fintype P
val✝ : Fintype 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₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
h : Fintype.card P = Fintype.card L
n : ℕ := lineCount L p₂
hp₂ : lineCount L p₂ = n
hl₁ : pointCount P l₁ = n
hp₃ : lineCount L p₃ = n
hl₃ : pointCount P l₃ = n
hp₁ : lineCount L p₁ = n
hl₂ : pointCount P l₂ = n
this : ∀ (p : P), lineCount L p = n
⊢ lineCount L p = lineCount L q

Tactic:
exact (this p).trans (this q).symm

Goal state after:
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 + 1 = order P L + Fintype.card { x // ↑x = p }

Tactic:
← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })

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: 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 + 1 = order P L + Fintype.card { x // ↑x = p }

Tactic:
rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]

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: 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 ![c, d]
⊢ False

Tactic:
← Matrix.of_row (![c, d])

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 : LinearIndependent K (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ #(treesOfNumNodesEq (n + 1)) = catalan (n + 1)

Tactic:
treesOfNumNodesEq_succ,

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ #((antidiagonal n).biUnion fun ij ↦ pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)) = catalan (n + 1)
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)
H : Subgroup G := A.invMulSubgroup h
⊢ ∃ H x, ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A) ∧ ∀ a ∈ A, ↑A ⊆ a •> ↑H ∧ a •> ↑H = ↑H <• a

Tactic:
refine ⟨H, inferInstance, ?_, fun a ha ↦ ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A)

case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ ↑A ⊆ a •> ↑H

case refine_3
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ a •> ↑H = ↑H <• 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)
⊢ ∃ H x, ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A) ∧ ∀ a ∈ A, ↑A ⊆ a •> ↑H ∧ a •> ↑H = ↑H <• a

Tactic:
let H := invMulSubgroup A h
  refine ⟨H, inferInstance, ?_, fun a ha ↦ ⟨?_, ?_⟩⟩
  · simp only [invMulSubgroup, ← coe_mul, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk,
      mem_coe, ← Nat.card_eq_fintype_card, H]
    rwa [Nat.card_eq_finsetCard, card_inv_mul_of_doubling_lt_three_halves h]
  · rw [invMulSubgroup_eq_inv_mul]
    exact_mod_cast A_subset_aH a ha
  · simpa [H, invMulSubgroup_eq_inv_mul, ← coe_inv, ← coe_mul, ← coe_smul_finset]
      using smul_inv_mul_eq_inv_mul_opSMul h ha

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

Goal state before:
pp: this : Finset.Iic 0 = {0}
⊢ Nat.bell 1 = 1

Tactic:
simp [Nat.bell, this]

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

Goal state before:
pp: this : Finset.Iic 1 = {0, 1}
⊢ Nat.bell 2 = 2

Tactic:
simp [Nat.bell, this]

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

Goal state before:
pp: case left
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (U :: ↑p ++ [D]) = count D (U :: ↑p ++ [D])

Tactic:
← u,

Goal state after:
case left
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U ↑p.nest = count D ↑p.nest
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 (↑p ++ [D])) + 1 = count D (List.take j (↑p ++ [D])) + if False then 1 else 0) = false

Tactic:
ite_false,

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])) + 1 = count D (List.take j (↑p ++ [D])) + 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 α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (∑ x ∈ Icc a b, if x ≤ b then mud a x else 0) = ∑ x ∈ Icc a b, mud a x

Tactic:
by
      congr! with x hx; exact if_pos (mem_Icc.1 hx).2

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

Goal state before:
pp: case e_f
𝕜 : 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 : α
⊢ (mu 𝕜) x y * ∑ z ≥ y, f z = (mu 𝕜) x y * ∑ z ≥ y, (zeta 𝕜) y z * f z

Tactic:
sum_congr rfl fun z hz ↦ ?_

Goal state after:
case e_f
𝕜 : 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 : α
⊢ (mu 𝕜) x y * (Ici y).sum ?m.329 = (mu 𝕜) x y * ∑ z ≥ y, (zeta 𝕜) y z * f z

𝕜 : 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 α := ⋯
y : α
⊢ α → 𝕜

𝕜 : 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 z : α
hz : z ∈ Ici y
⊢ f z = ?m.329 z
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ ((p + q).take ((if False then q.firstReturn else p.firstReturn) + 1) ⋯).denest ⋯ =
    (p.take (p.firstReturn + 1) ⋯).denest ⋯

Tactic:
ite_false,

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ ((p + q).take (p.firstReturn + 1) ⋯).denest ⋯ = (p.take (p.firstReturn + 1) ⋯).denest ⋯
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (p + q).drop ((if False then q.firstReturn else p.firstReturn) + 1) ⋯ = p.drop (p.firstReturn + 1) ⋯ + q

Tactic:
ite_false,

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ (p + q).drop (p.firstReturn + 1) ⋯ = p.drop (p.firstReturn + 1) ⋯ + q
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case inr.intro.calc_1
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)})
ineq : ↑(#A) * ↑(#A) ≤ ((2 - K) * ↑l + (K - 1) * ↑(#S)) * ↑(#A)
this : 0 < #A
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑l

Tactic:
replace ineq := calc
          (#S : ℝ)
      _ ≤ K * #A := ‹_›
      _ ≤ K * ((2 - K) * l + (K - 1) * #S) := by
        gcongr; exact le_of_mul_le_mul_right ineq <| by positivity
      _ = (2 - K) * K * l + (K - 1) * K * #S := by ring

Goal state after:
case inr.intro.calc_1
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)})
this : 0 < #A
ineq : ↑(#S) ≤ (2 - K) * K * ↑l + (K - 1) * K * ↑(#S)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑l
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
ite_false,

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ ofTree (node () p.insidePart.toTree p.outsidePart.toTree) = p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

Tactic:
ite_false,

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ (node () p.insidePart.toTree p.outsidePart.toTree).numNodes = p.semilength
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case neg
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.semilength + p.outsidePart.toTree.numNodes + 1 = p.insidePart.semilength + p.outsidePart.semilength + 1

Tactic:
numNodes_toTree p.outsidePart

Goal state after:
case neg
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.semilength + p.outsidePart.semilength + 1 = p.insidePart.semilength + p.outsidePart.semilength + 1
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ Summable fun n ↦ X ^ ((i + 1) * (n + 1))

Tactic:
pow_mul,

Goal state after:
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
i : ℕ
h✝ : p (i + 1)
⊢ Summable fun n ↦ (X ^ (i + 1)) ^ (n + 1)
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(#(restricted n p))) = genFun fun i c ↦ if p i then 1 else 0

Tactic:
genFun,

Goal state after:
case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(#(restricted n p))) =
    PowerSeries.mk fun n ↦ ∑ p_1, (Multiset.toFinsupp p_1.parts).prod fun i c ↦ if p i then 1 else 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_6
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (PowerSeries.mk fun n ↦ ↑(#(countRestricted n m))) = genFun fun i c ↦ if c < m then 1 else 0

Tactic:
genFun,

Goal state after:
case e'_6
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (PowerSeries.mk fun n ↦ ↑(#(countRestricted n m))) =
    PowerSeries.mk fun n ↦ ∑ p, (Multiset.toFinsupp p.parts).prod fun i c ↦ if c < m then 1 else 0
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) = (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))

Tactic:
rw [map_add, (summable_genFun_term' f hi0).map_tsum _ (WithPiTopology.continuous_coeff _ _)]

Goal state after:
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) =
    (coeff (p.toFinsuppAntidiag i)) 1 +
      ∑' (i_1 : ℕ), (coeff (p.toFinsuppAntidiag i)) (f i (i_1 + 1) • X ^ (i * (i_1 + 1)))