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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p✝ : G.Walk v✝ u
hp : (cons h p✝).IsCircuit
⊢ G ≠ ⊥

Tactic:
rintro rfl

Goal state after:
V : Type u
u v✝ : V
h : ⊥.Adj u v✝
p✝ : ⊥.Walk v✝ u
hp : (cons h p✝).IsCircuit
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: 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
⊢ p = q

Tactic:
by
  suffices ∀ k : ℕ, p.support[k]? = q.support[k]? by
    exact ext_support <| List.ext_getElem?_iff.mpr this
  intro k
  cases le_or_gt k p.length with
  | inl hk =>
    rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]
    exact congrArg some (h k hk)
  | inr hk =>
    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.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 | 1 ≤ i ∧ i ≤ p.length}

Tactic:
← p.cons_tail_eq hpc.not_nil

Goal state after:
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}
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
⊢ ∑ x ∈ A.product B, ↑↑(#(interedges G.Adj x.1 x.2)) / (↑(↑(#x.1) * ↑(#x.2)) * (↑(#A) * ↑(#B))) ≤
    ∑ x ∈ ((chunk hP G ε hU).ofSubset hA ⋯).parts ×ˢ ((chunk hP G ε hV).ofSubset hB ⋯).parts,
      ↑↑(#(interedges G.Adj x.1 x.2)) * ((1 + ε ^ 5 / 49) / ↑(↑(#(A.sup id)) * ↑(#(B.sup id))))

Tactic:
push_cast

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))) ≤
    ∑ x ∈ ((chunk hP G ε hU).ofSubset hA ⋯).parts ×ˢ ((chunk hP G ε hV).ofSubset hB ⋯).parts,
      ↑(#(interedges G.Adj x.1 x.2)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ #s = n → ((↑s).Subsingleton ↔ n ≤ 1)

Tactic:
rintro rfl

Goal state after:
α : Type u_1
s : Finset α
⊢ (↑s).Subsingleton ↔ #s ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s = ∅ → G.IsClique ↑s

Tactic:
rintro rfl

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ G.IsClique ↑∅
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique ↑(insert a s)

Tactic:
push_cast

Goal state after:
case isClique
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
h : ∀ b ∈ s, G.Adj a b
⊢ G.IsClique (insert a ↑s)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
inst✝ : Nonempty α
hle : 1 ≤ 1
⊢ (SimpleGraph.map (⇑f) G).CliqueFree 1 ↔ G.CliqueFree 1

Tactic:
simp [CliqueFree, show ∃ (_ : β), True from ⟨f (Classical.arbitrary _), trivial⟩]

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

Goal state before:
pp: case mpr
α : Type u_1
G : SimpleGraph α
⊢ G = ⊥ → G.CliqueFree 2

Tactic:
rintro rfl

Goal state after:
case mpr
α : Type u_1
⊢ ⊥.CliqueFree 2
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ ↑{a, b} ⊆ s

Tactic:
push_cast

Goal state after:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ {a, b} ⊆ s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : ↑t ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ ↑(insert a t) ⊆ s

Tactic:
push_cast

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : ↑t ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ insert a ↑t ⊆ s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
n : ℕ
⊢ ↑((SimpleGraph.map (⇑e) G).cliqueFinset n) = ↑(map { toFun := map e.toEmbedding, inj' := ⋯ } (G.cliqueFinset n))

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
n : ℕ
⊢ (SimpleGraph.map (⇑e) G).cliqueSet n = ⇑{ toFun := map e.toEmbedding, inj' := ⋯ } '' G.cliqueSet n
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(↑(#(G.interedges (G.badVertices ε s t) t)) / (↑(#(G.badVertices ε s t)) * ↑(#t))) ≤ ↑(G.edgeDensity s t) - ε

Tactic:
push_cast

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
⊢ ↑(#(G.interedges (G.badVertices ε s t) t)) / (↑(#(G.badVertices ε s t)) * ↑(#t)) ≤ ↑(G.edgeDensity s t) - ε
Module: Mathlib.Data.Finset.CastCard

Goal state before:
pp: α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#s + #t) = ↑(#s) + ↑(#t)

Tactic:
cast_add

Goal state after:
α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#s) + ↑(#t) = ↑(#s) + ↑(#t)
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑(t \ u) ⊆ s

Tactic:
push_cast

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑t \ ↑u ⊆ s
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑(u \ t) ⊆ s

Tactic:
push_cast

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommGroup α
s : Set α
t : Finset α
ht : ↑t ⊆ s
u : Finset α
hu : ↑u ⊆ s
htu : t ≠ u
h : ∏ x ∈ t, x = ∏ x ∈ u, x
⊢ ↑u \ ↑t ⊆ s
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 γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ ↑((graph t).cliqueFinset 3) = ↑(image (⇑toTriangle) t)

Tactic:
push_cast

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ (graph t).cliqueSet 3 = ⇑toTriangle '' ↑t
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₂
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
⊢ ε ^ 4 / 3 ≤ ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / (4 ^ #P.parts * 4 ^ #P.parts) * (9 / 4 ^ 2) * ε ^ 2

Tactic:
←
        _root_.div_mul_div_comm,

Goal state after:
case h₂
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts
Vl : 4 / 5 * ε ≤ ↑(#(star hP G ε hV U)) / 4 ^ #P.parts
⊢ ε ^ 4 / 3 ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts * (↑(#(star hP G ε hV U)) / 4 ^ #P.parts) * (9 / 4 ^ 2) * ε ^ 2
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
⊢ Set.InjOn f ↑(univ ×ˢ t ×ˢ t)

Tactic:
rintro ⟨a₁, b₁, c₁⟩ _ ⟨a₂, b₂, c₂⟩ h₂ h

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : f (a₁, b₁, c₁) = f (a₂, b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤
    ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2

Tactic:
by
      gcongr
      have Ul : 4 / 5 * ε ≤ #(star hP G ε hU V) / _ :=
        eps_le_card_star_div hPα hPε hε₁ hU hV hUVne hUV
      have Vl : 4 / 5 * ε ≤ #(star hP G ε hV U) / _ :=
        eps_le_card_star_div hPα hPε hε₁ hV hU hUVne.symm fun h => hUV h.symm
      rw [show (16 : ℝ) = ↑4 ^ 2 by norm_num, pow_right_comm, sq ((4 : ℝ) ^ _), ←
        _root_.div_mul_div_comm, mul_assoc]
      have : 0 < ε := by sz_positivity
      have UVl := mul_le_mul Ul Vl (by positivity) ?_
      swap
      · -- This seems faster than `exact div_nonneg (by positivity) (by positivity)` and *much*
        -- (tens of seconds) faster than `positivity` on its own.
        apply div_nonneg <;> positivity
      refine le_trans ?_ (mul_le_mul_of_nonneg_right UVl ?_)
      · norm_num
        nlinarith
      · simp [pow_two_nonneg]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ ↑(𝔼 a, ∏ ψ, (c ψ + (d ψ * ψ a).re)) = ↑(∏ ψ, c ψ)

Tactic:
push_cast

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) = ∏ i, ↑(c i)
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:
card_union_of_disjoint disjoint

Goal state after:
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)
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ (↑(Iic (Fintype.card α))).PairwiseDisjoint 𝒜.slice

Tactic:
exact Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h : (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a}
b : α
hb : b ∈ s
⊢ b ≠ a

Tactic:
rintro rfl

Goal state after:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
b : α
hb : b ∈ s
h : (∀ b_1 ∈ s, b_1 ≤ b ∧ (b ∈ s → b_1 = b)) ∧ ¬s = {b}
⊢ False
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
h : ∀ b ∈ s, b < a
⊢ ¬s = {a}

Tactic:
rintro rfl

Goal state after:
case refine_2
α : Type u_1
inst✝ : PartialOrder α
a : α
h : ∀ b ∈ {a}, b < a
⊢ False
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s t u : Finset α
inst✝ : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ (∀ ⦃a : α⦄, a ∈ s \ u ∧ a ∉ t \ u → ∃ b, (b ∈ t \ u ∧ b ∉ s \ u) ∧ a ≤ b) ↔
    ∀ ⦃a : α⦄, a ∈ s ∧ a ∉ t → ∃ b, (b ∈ t ∧ b ∉ s) ∧ a ≤ b

Tactic:
← mem_sdiff,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
s t u : Finset α
inst✝ : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ (∀ ⦃a : α⦄, a ∈ (s \ u) \ (t \ u) → ∃ b ∈ (t \ u) \ (s \ u), a ≤ b) ↔ ∀ ⦃a : α⦄, a ∈ s \ t → ∃ b ∈ t \ s, a ≤ b
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

Goal state after:
case h₀
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 1 * (v 0 * w 1 - v 1 * w 0) - u 2 * (v 2 * w 0 - v 0 * w 2) =
    (u 2 * v 0 - u 0 * v 2) * w 2 - (u 0 * v 1 - u 1 * v 0) * w 1 +
      (v 1 * (u 0 * w 1 - u 1 * w 0) - v 2 * (u 2 * w 0 - u 0 * w 2))

case h₁
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 2 * (v 1 * w 2 - v 2 * w 1) - u 0 * (v 0 * w 1 - v 1 * w 0) =
    (u 0 * v 1 - u 1 * v 0) * w 0 - (u 1 * v 2 - u 2 * v 1) * w 2 +
      (v 2 * (u 1 * w 2 - u 2 * w 1) - v 0 * (u 0 * w 1 - u 1 * w 0))

case h₂
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 2 * w 0 - v 0 * w 2) - u 1 * (v 1 * w 2 - v 2 * w 1) =
    (u 1 * v 2 - u 2 * v 1) * w 1 - (u 2 * v 0 - u 0 * v 2) * w 0 +
      (v 0 * (u 2 * w 0 - u 0 * w 2) - v 1 * (u 1 * w 2 - u 2 * w 1))
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
v : ℙ K V
⊢ v.submodule = K ∙ v.rep

Tactic:
conv_lhs => rw [← v.mk_rep]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ (mk K v.rep ⋯).submodule = K ∙ v.rep
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
a : ℕ
hat : a ∈ ofColex t
has : a ∉ ofColex s
ha : ∀ b ∈ ofColex s, b ∉ ofColex t → b < a
⊢ (fun s ↦ ∑ k ∈ ofColex s, n ^ k) s < (fun s ↦ ∑ k ∈ ofColex s, n ^ k) t

Tactic:
rw [← sum_sdiff_lt_sum_sdiff]

Goal state after:
n : ℕ
hn : 2 ≤ n
s t : Colex (Finset ℕ)
a : ℕ
hat : a ∈ ofColex t
has : a ∉ ofColex s
ha : ∀ b ∈ ofColex s, b ∉ ofColex t → b < a
⊢ ∑ i ∈ ofColex s \ ofColex t, n ^ i < ∑ i ∈ ofColex t \ ofColex s, n ^ i
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Perm α
F : Perm (Option α)
F_derangement : F ∈ derangements (Option α)
F_none : F none = none
right✝ : removeNone F = f
⊢ False

Tactic:
exact F_derangement none F_none

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

Goal state before:
pp: case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)

Tactic:
numDerangements_add_two,

Goal state after:
case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = (n + 1) * (numDerangements n + numDerangements (n + 1))
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ↑(∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))) / ↑n.factorial = s (n + 1)

Tactic:
push_cast

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ (∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x))) / ↑n.factorial = s (n + 1)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n i : ℕ
h : i ≤ n
l₁ : ↑i + 1 ≠ 0
l₂ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)
h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom
h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom
⊢ ↑(i + 1).centralBinom * ↑(n + 1 - (i + 1)).centralBinom * (2 * ↑(i + 1) - ↑(n + 1)) /
        (2 * ↑(n + 1) * (↑(n + 1) + 1)) -
      ↑i.centralBinom * ↑(n + 1 - i).centralBinom * (2 * ↑i - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)

Tactic:
push_cast

Goal state after:
n i : ℕ
h : i ≤ n
l₁ : ↑i + 1 ≠ 0
l₂ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)
h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom
h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom
⊢ ↑(i + 1).centralBinom * ↑(n - i).centralBinom * (2 * (↑i + 1) - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑i.centralBinom * ↑(n + 1 - i).centralBinom * (2 * ↑i - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
⊢ ∀ x ∈ antidiagonal n, #(pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2)) = catalan x.1 * catalan x.2

Tactic:
rintro ⟨i, j⟩ H

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ antidiagonal n
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x ! = (x * (c + 1))!

Tactic:
rw [← Nat.choose_mul_add hx, mul_comm c x, Nat.add_choose_mul_factorial_mul_factorial]

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c + x)! = (x * (c + 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)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
⊢ z ∈ A * A

Tactic:
have : #l = #A := by rw [hl]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this✝ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this : #l = #A
⊢ z ∈ A * A
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
⊢ m.bell * ?m.31 = m.sum ! / ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) * ?m.31

pp: m : Multiset ℕ
⊢ ?m.31 ≠ 0

pp: m : Multiset ℕ
⊢ ℕ

Tactic:
Nat.div_mul_cancel _

Goal state after:
m : Multiset ℕ
⊢ m.bell * ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !

m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣ m.sum !

m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ≠ 0
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.semilength = count D ↑p

Tactic:
by
  rw [← count_U_eq_count_D]; 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✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ (0 * f) a✝¹ b✝ = 0 a✝¹ b✝

Tactic:
exact sum_eq_zero fun x _ ↦ zero_mul _

Goal state after: