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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ h.toWalk.length = 1

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
hadj : G.Adj u v
⊢ p.support <:+ (cons hadj p).support

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
hadj : G.Adj u v
⊢ p.support ⊆ (cons hadj p).support

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
h : i < p.darts.length
⊢ p.darts[i].edge = p.edges[i]

Tactic:
getElem_edges_eq_edge_getElem_darts

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
h : i < p.darts.length
⊢ p.darts[i].edge = p.darts[i].edge
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).length = p.length

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).support = p.support

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).edges = p.edges

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).edgeSet = p.edgeSet

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).reverse = mapLe h p.reverse

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ mapLe h (p.append q) = (mapLe h p).append (mapLe h q)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support = p.support.dropLast.concat v

Tactic:
by
  simp

Goal state after:
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
hadj : G.Adj v w
⊢ p.support <+: (p.concat hadj).support

Tactic:
by
  simp

Goal state after:
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
hadj : G.Adj v w
⊢ p.support ⊆ (p.concat hadj).support

Tactic:
by
  simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ edges.card ≤ G.edgeFinset.card

Tactic:
have : edges ⊆ G.edgeFinset := by
    intro e h
    refine mem_edgeFinset.mpr ?_
    apply w.edges_subset_edgeSet
    simpa [edges] using h

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this✝ : edges.card = w.length
this : edges ⊆ G.edgeFinset
⊢ edges.card ≤ G.edgeFinset.card
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath → p.IsPath ∧ u ∉ p.support

Tactic:
simp +contextual [isPath_def]

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ p.IsPath ∧ u ∉ p.support → (cons h p).IsPath

Tactic:
simp +contextual [isPath_def]

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
⊢ p.IsPath ↔ p = nil

Tactic:
by
  simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
⊢ ¬p.Nil

Tactic:
grind [not_nil_iff_lt_length, hc.three_le_length, length_cons]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : p.length < k
⊢ p.support[k]? = q.support[k]?

Tactic:
replace hk : p.length + 1 ≤ k := hk
    have ht : q.length + 1 ≤ k := hl ▸ hk
    rw [← length_support, ← List.getElem?_eq_none_iff] at hk ht
    rw [hk, ht]

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

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : t ∈ Set.range ⇑φ
⊢ completeGraph (Fin n) ⊑ G

Tactic:
obtain ⟨x, hx⟩ := mt

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : ε ^ 5 / 50 ≤ ↑(G.edgeDensity U V)
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
    ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2

Tactic:
rw [← sub_nonneg] at hGε

Goal state after:
case inr
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
    ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this✝ :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ ↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) ≤ 2 * (↑(#s) * ε)

Tactic:
two_mul

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this✝ :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
this : 0 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ ↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) ≤ ↑(#s) * ε + ↑(#s) * ε
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ↑(#(star hP G ε hU V)) * (↑m + 1) * ((1 - (↑m)⁻¹) / ↑(#U)) ≤
    ↑(#(star hP G ε hU V)) * (↑m + 1) * ((1 - (↑m)⁻¹) / (4 ^ #P.parts * ↑m))

Tactic:
gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU

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 : 1 < triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G)
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
hε₁ : ε ≤ 1
this : NoAccidental (triangleIndices A)
⊢ triangleRemovalBound (ε / 9) * 27 * ↑(Fintype.card G) * ↑(Fintype.card G) ^ 2 ≤ 1 * ↑(Fintype.card G) ^ 2

Tactic:
have h₁ := (farFromTriangleFree_graph hAε).le_card_cliqueFinset
  rw [card_triangles, card_triangleIndices] at h₁
  convert! h₁.trans (Nat.cast_le.2 <| card_le_univ _) using 1 <;> simp <;> ring

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
⊢ ∀ (a : { j // j ≠ i } → K), ∑ x, ∏ j, ↑x j ^ d j = 0

Tactic:
intro x₀

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
⊢ ∑ x, ∏ j, ↑x j ^ d j = 0
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
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
⊢ 2 * p - 1 = Fintype.card ↥s

Tactic:
simp [hs]

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

Goal state before:
pp: case refine_1
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ #(ℬ.biUnion fun x ↦ x) = m * n

Tactic:
card_biUnion (h𝒜disj.mono hℬ𝒜),

Goal state after:
case refine_1
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ∑ u ∈ ℬ, #u = m * n
Module: Mathlib.Combinatorics.Compactness

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x

Tactic:
let instTop (a : α) : TopologicalSpace (β a) := ⊥

Goal state after:
α : Type u_1
β : α → Type u_2
inst✝ : ∀ (a : α), Finite (β a)
g : Finset α → (a : α) → β a
instTop : (a : α) → TopologicalSpace (β a) := fun a ↦ ⊥
⊢ ∃ χ, ∀ (s : Finset α), ∃ t, s ⊆ t ∧ ∀ x ∈ s, χ x = g t x
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum

Tactic:
obtain ⟨t, hts, ht⟩ := Int.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)
  exact ⟨t.1.map Prod.fst, Multiset.map_fst_le_of_subset_toEnumFinset hts, by simpa using ht⟩

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 -
        u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1,
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 -
        u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2,
      u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 -
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0] =
    ![![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 2 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 1 +
        (v 1 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2 -
          v 2 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1),
      ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 0 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 2 +
        (v 2 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0 -
          v 0 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 2),
      ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 1 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 0 +
        (v 0 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 1 -
          v 1 * ![u 1 * w 2 - u 2 * w 1, u 2 * w 0 - u 0 * w 2, u 0 * w 1 - u 1 * w 0] 0)]

Tactic:
apply vec3_eq <;> dsimp <;> ring

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

Goal state before:
pp: n : ℕ
⊢ ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n

Tactic:
by
  induction n with
  | zero => rfl
  | succ n hn =>
    simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]
    ring

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ #(A * A) < 2 * #A

Tactic:
by qify at h ⊢; linarith

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

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

Tactic:
by
  simp_rw [nest, denest, DyckWord.ext_iff, dropLast_concat]; rfl

Goal state after:
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✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
a b : α
hab : a ≤ b
⊢ (c • f) a b =
    ({ toFun := fun c ↦ (algebraMap 𝕜 𝕝) c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } c * f) a b

Tactic:
simp [if_pos hab, constSMul_apply, Algebra.smul_def]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
⊢ mu 𝕜 * zeta 𝕜 = 1

Tactic:
ext a b
  calc
    _ = ∑ x ∈ Icc a b, mu 𝕜 a x := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).2]
    _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu_right ..

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
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))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
⊢ 1 - ∑' (i : ℕ), x ^ (i + 1) * ∏ j < i, (1 - x ^ (j + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x

Tactic:
Nat.Iio_eq_range,

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))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
⊢ 1 - ∑' (i : ℕ), x ^ (i + 1) * ∏ x_1 ∈ Finset.range i, (1 - x ^ (x_1 + 1)) =
    1 - x - x ^ 2 * ∑' (n : ℕ), powMulProdOneSubPow 0 n x
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
⊢ (n + 1).stirlingFirst (k + 1) = 0

Tactic:
rw [stirlingFirst_succ_succ, stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt_succ hk),
      stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt hk), mul_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ x ∈ V(H) ↔ y ∈ V(H)

Tactic:
refine ⟨fun hin ↦ ?_, fun hin ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
⊢ y ∈ V(H)

case refine_2
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α : Type u_2
ι : Type u_3
l : Line (η → α) ι
a : η → α
ie : ι × η
⊢ ↑l.toSubspace a ie = ↑l a ie.1 ie.2

Tactic:
cases h : l.idxFun ie.1 <;> simp [toSubspace, h, coe_apply, Subspace.coe_apply]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₁ ＼ (D₂ \ D₁)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
⊢ (M ＼ {e}).Indep I ↔ M.Indep I ∧ e ∉ I

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I (X ∩ Dᶜ ∩ M.E) ∧ Disjoint (X ∩ Dᶜ ∩ M.E) D ↔ M.IsBasis' I (X \ D)

Tactic:
← sdiff_eq,

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I (X \ D ∩ M.E) ∧ Disjoint (X \ D ∩ M.E) D ↔ M.IsBasis' I (X \ D)
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X ∩ Dᶜ ∩ M.E) ∩ (Dᶜ ∩ M.E) = M.closure (X \ D) \ D

Tactic:
← sdiff_eq,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D ∩ M.E) ∩ (Dᶜ ∩ M.E) = M.closure (X \ D) \ D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) ∩ Dᶜ ∩ M.E = M.closure (X \ D) \ D

Tactic:
← sdiff_eq,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) \ D ∩ M.E = M.closure (X \ D) \ D
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ (M✶ ／ X)✶ = M ＼ X

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ (M ／ X ＼ Y)✶ = M✶ ＼ X ／ Y

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ (M ＼ X ／ Y)✶ = M✶ ／ X ＼ Y

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ C₁ ／ (C₂ \ C₁)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ ¬(Disjoint J I ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint J I ↔ Disjoint J I ∧ ¬M.Indep (J ∪ I) ∧ J ∪ I ⊆ M.E

Tactic:
disjoint_comm,

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ∪ I ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ Disjoint D X ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
disjoint_comm,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ Disjoint X D ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree f)

pp: case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
· exact fun b ↦ le_trans (H'.2.1 b) (degree_sub_LTerm_le f)

Goal state after:
case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support, ∀ (i : ι), ¬m.degree (b i) ≤ c