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

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = (cons h✝ p✝).concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
concat_cons,

Goal state after:
case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = cons h✝ (p✝.concat h')
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').support = p.support ++ p'.support.tail

Tactic:
induction p <;> cases p'

Goal state after:
case nil.nil
V : Type u
G : SimpleGraph V
u v w : V
⊢ (nil.append nil).support = nil.support ++ nil.support.tail

case nil.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w
⊢ (nil.append (cons h✝ p✝)).support = nil.support ++ (cons h✝ p✝).support.tail

case cons.nil
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w
p_ih✝ : ∀ (p' : G.Walk w w), (p✝.append p').support = p✝.support ++ p'.support.tail
⊢ ((cons h✝ p✝).append nil).support = (cons h✝ p✝).support ++ nil.support.tail

case cons.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝¹.append p').support = p✝¹.support ++ p'.support.tail
v✝ : V
h✝ : G.Adj w✝ v✝
p✝ : G.Walk v✝ w
⊢ ((cons h✝¹ p✝¹).append (cons h✝ p✝)).support = (cons h✝¹ p✝¹).support ++ (cons h✝ p✝).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝¹ : G.Adj u' v'
h✝ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : d.edge = s(u', v')
⊢ { fst := u', snd := v', adj := h✝¹ } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts

Tactic:
rw [Dart.edge, Sym2.eq, Sym2.rel_iff'] at h

Goal state after:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝¹ : G.Adj u' v'
h✝ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := u', snd := v', adj := h✝¹ } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ (p.drop n).Nil

Tactic:
← length_eq_zero_iff,

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ (p.drop n).length = 0
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ ((cons h✝ p✝).concat h).dropLast = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
concat_cons,

Goal state after:
case cons
V : Type u
G : SimpleGraph V
t u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : G.Adj w✝ t), (p✝.concat h).dropLast = p✝.copy ⋯ ⋯
h : G.Adj w✝ t
⊢ (cons h✝ (p✝.concat h)).dropLast = (cons h✝ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ p.tail.support = p.support.tail

Tactic:
by
  simp [← p.cons_tail_eq hp]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.getVert i = w ↔ i = p.length

Tactic:
rw [this]

Goal state after:
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
p : G.Walk u w
hp : p.IsPath
hi : i ≤ p.length
this : p.getVert i = w ↔ p.length - i = 0
⊢ p.length - i = 0 ↔ i = p.length
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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
⊢ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) ≤
    (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
conv_lhs => -- Porting note: LHS and RHS need separate treatment to get the desired form
    simp only [SimpleGraph.edgeDensity, edgeDensity, sum_div, Rat.cast_div, div_div]

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
⊢ ∑ x ∈ A.product B, ↑↑(#(interedges G.Adj x.1 x.2)) / (↑(↑(#x.1) * ↑(#x.2)) * (↑(#A) * ↑(#B))) ≤
    (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

Tactic:
simp only [*, true_and] at *
          exact ⟨c, by aesop⟩

Goal state after:
case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
⊢ False

Tactic:
by_cases hi' : i ≥ p.length - 1

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : i ≥ p.length - 1
⊢ False

case neg
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≤ p.length
h' : p.getVert (i - 1) = p.getVert (i + 1)
hl : 3 ≤ p.length
hi' : ¬i ≥ p.length - 1
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}

Tactic:
simp only [*, true_and] at *
          exact ⟨c, by aesop⟩

Goal state after:
case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Tactic:
simp only [*, true_and] at *
          exact ⟨c, by aesop⟩

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

Goal state before:
pp: case hb
α : 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ B, (id x).Nonempty

Tactic:
exact ⟨_, hy, nonempty_of_mem_parts _ (hB hy)⟩

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
this : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b
⊢ a ∈ s'.mulSpan

Tactic:
rw [this]

Goal state after:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
this : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b
⊢ (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b ∈ s'.mulSpan
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
this : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b
⊢ a ∈ s'.mulSpan

Tactic:
rw [this]

Goal state after:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
this : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b
⊢ (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b ∈ s'.mulSpan
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 σ
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }

Tactic:
have hq : 0 < q - 1 := by rw [← Fintype.card_units, Fintype.card_pos_iff]; exact ⟨1⟩

Goal state after:
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
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ (#A).choose 2 ≤ (#(A.erase 0) + 1).choose 2

Tactic:
grw [tsub_le_iff_right.1 <| pred_card_le_card_erase]

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

Goal state before:
pp: ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0

Tactic:
have : NeZero p := inferInstance
  classical
  -- Let `N` be the number of common roots of our polynomials `f₁` and `f₂` (`f s ff` and `f s tt`).
  set N := Fintype.card {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0}
  -- Zero is a common root to `f₁` and `f₂`, so `N` is nonzero
  let zero_sol : {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0} :=
    ⟨0, by simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]⟩
  have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
  have hs' : 2 * p - 1 = Fintype.card s := by simp [hs]
  -- Chevalley-Warning gives us that `p ∣ n` because the total degrees of `f₁` and `f₂` are at most
  -- `p - 1`, and we have `2 * p - 1 > 2 * (p - 1)` variables.
  have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
  -- Hence, `2 ≤ p ≤ N` and we can make a common root `x ≠ 0`.
  obtain ⟨x, hx⟩ := Fintype.exists_ne_of_one_lt_card ((Fact.out : p.Prime).one_lt.trans_le <|
    Nat.le_of_dvd hN₀ hpN) zero_sol
  -- This common root gives us the required subsequence, namely the `i ∈ s` such that `x i ≠ 0`.
  refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
  · simp +contextual [subset_iff]
  -- From `f₁ x = 0`, we get that `p` divides the number of `a` such that `x a ≠ 0`.
  · rw [card_map]
    refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_
    -- This number is nonzero because `x ≠ 0`.
    · rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
      exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)
    · rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1
    -- And it is at most `2 * p - 1`, so it must be `p`.
    · rw [univ_eq_attach, card_attach, hs]
      exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one
  -- From `f₂ x = 0`, we get that `p` divides the sum of the `a ∈ s` such that `x a ≠ 0`.
  · simpa [f₂, ZMod.pow_card_sub_one, Finset.sum_filter] using x.2.2

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

Goal state before:
pp: case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ (2 ^ (1 + k) * n).bitIndices = map (fun x ↦ x + (1 + k)) n.bitIndices

Tactic:
pow_add,

Goal state after:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ (2 ^ 1 * 2 ^ k * n).bitIndices = map (fun x ↦ x + (1 + k)) n.bitIndices
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
c : α
hcu : c ∈ u
hcs : c ∉ s
hbc : b ≤ c
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
exact ⟨c, hcu, hcs, hab.trans hbc⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
replace hst := hst.lt_of_ne <| toColex_inj.not.2 h'

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hst : toColex s < toColex t
⊢ toColex (s.erase a) ≤ toColex (t.erase m)
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))
⊢ 0 < ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)))

Tactic:
have := card_inter_add_card_union (A ∩ (c * d) • A) (A ∩ (a * b)⁻¹ • A)

Goal state after:
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)
⊢ 0 < ↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)))
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
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (c • 0) a✝¹ b✝ = 0 a✝¹ b✝

Tactic:
exact smul_zero _

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ count U (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)

Tactic:
have := findIdx_getElem
    (w := (length_range (n := p.toList.length)).symm ▸ firstReturn_lt_length h)

Goal state after:
p : DyckWord
h : p ≠ 0
this :
  decide
      (count U
          (List.take
            ((range
                  (↑p).length)[findIdx
                  (fun i ↦ decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p)))
                  (range (↑p).length)] +
              1)
            ↑p) =
        count D
          (List.take
            ((range
                  (↑p).length)[findIdx
                  (fun i ↦ decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p)))
                  (range (↑p).length)] +
              1)
            ↑p)) =
    true
⊢ count U (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)
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
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ (k + 1 + 1) * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1))

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ (k + 1) * x ^ 1 * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1))
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
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ (k + 1) * x ^ 1 * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1))

Tactic:
pow_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
k : ℕ
| x ^ k * x ^ 1 * x ^ 1 * ∏ n ∈ Finset.range (k + 1), (1 - x ^ (n + 1))
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 ℕ
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)))
⊢ (coeff d) (∏ b ∈ s, (1 + ∑' (j : ℕ), f (b + 1) (j + 1) • X ^ ((b + 1) * (j + 1)))) = (coeff d) (genFun f)

Tactic:
rw [this]

Goal state after:
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)))
⊢ (coeff d) (∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))) =
    (coeff d) (genFun f)