mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ∞
h : ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
a : G
ha : a ≠ 1
ha' : IsOfFinOrder a
⊢ n ≤ ↑(orderOf a)

Tactic:
simpa using h (zpowers_ne_bot.2 ha) ha'.finite_zpowers

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
P : Finpartition ⊥
⊢ P = default

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a✝ : α
P✝ : Finpartition a✝
P : Finpartition ⊥
a : α
⊢ a ∈ P.parts ↔ a ∈ default.parts
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
let sneg :
      {x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1} ≃ {x // x ∈ P.parts ∧ #x = #s / #P.parts} := by
    apply (Equiv.refl _).subtypeEquiv
    simp only [Equiv.refl_apply, and_congr_right_iff]
    exact fun _ ha ↦ by rw [hP.card_part_eq_average_iff ha, ne_eq]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ #(P.bind Q).parts = ∑ A ∈ P.parts.attach, #(Q ↑A ⋯).parts

Tactic:
apply card_biUnion

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (↑P.parts.attach).PairwiseDisjoint fun i ↦ ((fun i ↦ Q ↑i ⋯) i).parts
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: case h₂
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := ⋯
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
a : ↥s
c : #↑(f a).fst = #s / #P.parts
⊢ ↑(f a).snd + 1 ≤ #s / #P.parts

Tactic:
exact c ▸ (f a).2.2

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
⊢ (image (fun a ↦ {b ∈ x | s a b}) x).sup id = x

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ a ∈ (image (fun a ↦ {b ∈ x | s a b}) x).sup id ↔ a ∈ x
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
⊢ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}.biUnion id = t

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
hts : t ⊆ s
a : α
⊢ a ∈ {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}.biUnion id ↔ a ∈ t
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
⊢ interedges r s (t.biUnion f) = t.biUnion fun b ↦ interedges r s (f b)

Tactic:
ext a

Goal state after:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a ∈ interedges r s (t.biUnion f) ↔ a ∈ t.biUnion fun b ↦ interedges r s (f b)
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case e_f
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
x✝ : Finset α
⊢ #(interedges r x✝ t) = ∑ y ∈ Q.parts, #(interedges r (x✝, y).1 (x✝, y).2)

Tactic:
rw [card_interedges_finpartition_right]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
⊢ x ∈ A →
    y ∈ A →
      G.Adj x y →
        (G.Adj x y →
            ∀ x_1 ∈ P.parts,
              ∀ x_2 ∈ P.parts,
                x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4) →
          (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
            (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
              ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
intro hx hy h h'

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx : x ∈ A
hy : y ∈ A
h : G.Adj x y
h' :
  G.Adj x y →
    ∀ x_1 ∈ P.parts,
      ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : 1 ≤ ε
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
exact ⟨dum, hdum₁, (le_initialBound ε l).trans hdum₂.ge,
      hdum₂.le.trans (initialBound_le_bound ε l), (dum.isUniform_one G).mono hε₁⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
⊢ edge s t ≤ G ↔ {s(s, t)} \ Sym2.diagSet ⊆ G.edgeSet

Tactic:
by simp [edge]

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

Goal state before:
pp: V : Type u_1
v w : V
⊢ (edge v w).edgeSet = {s(v, w)} \ Sym2.diagSet

Tactic:
by simp [edge]

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

Goal state before:
pp: V : Type u_1
v w : V
⊢ (edge v w).edgeSet ⊆ {s(v, w)}

Tactic:
by simp [edge]

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
S : Set V
uS : u ∈ S
vS : v ∉ S
⊢ ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
induction p with
  | nil => cases vS uS
  | cons a p' ih =>
    rename_i x _
    by_cases h : x ∈ S
    · obtain ⟨d, hd, hcd⟩ := ih h vS
      exact ⟨d, List.Mem.tail _ hd, hcd⟩
    · exact ⟨⟨_, a⟩, List.Mem.head _, uS, h⟩

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w = a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

Tactic:
subst h'
      simp [dropUntil_first]

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
d : G.Dart
h : d ∈ p.darts
⊢ d.symm ∈ p.reverse.darts

Tactic:
by simp [h]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
⊢ G.IsClique (⇑f ⁻¹' t)

Tactic:
rintro x (hx : f x ∈ t) y (hy : f y ∈ t) hne
    obtain ⟨-, u, v, huv, hux, hvy⟩ := h hx hy (by simpa)
    rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy
    rwa [← hux, ← hvy]

Goal state after:
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
hl : i ≤ p.length
⊢ p.getVert i = u → i = 0 ∨ i = p.length

Tactic:
rw [or_iff_not_imp_left]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
hl : i ≤ p.length
⊢ p.getVert i = u → ¬i = 0 → i = p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ Gᶜ.IsClique s ↔ G.IsIndepSet s

Tactic:
isIndepSet_iff,

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ Gᶜ.IsClique s ↔ 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 α
⊢ Gᶜ.IsIndepSet s ↔ G.IsClique s

Tactic:
isIndepSet_iff,

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
⊢ G.FarFromTriangleFree ε

Tactic:
by
  rw [farFromTriangleFree_iff]
  intro H _ hG hH
  rw [← Nat.cast_sub (card_le_card <| edgeFinset_mono hG)]
  exact tris_big.trans
    (Nat.cast_le.2 <| farFromTriangleFree_of_disjoint_triangles_aux htris pd hG hH)

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

Goal state before:
pp: α : 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' ∈ s.powerset | MulDissociated ↑s'}) s'
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Tactic:
simp only [mem_filter, mem_powerset] at hs'

Goal state after:
α : 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'
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ ¬(b = y ∧ c = z)

Tactic:
rintro ⟨rfl, rfl⟩
    exact this (ExplicitDisjoint.inj₀ habc hxyz) rfl rfl

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
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0

Tactic:
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]⟩

Goal state after:
ι : 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, ⋯⟩
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0
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
⊢ #A + 1 + #A.subsetSum = #(insert 0 A) + #A.subsetSum

Tactic:
card_insert_of_notMem fun h => (hA 0 h).false

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
⊢ #A + 1 + #A.subsetSum = #A + 1 + #A.subsetSum
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_2
α : 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
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2 ≤
    ((∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
        ↑(#(chunk hP G ε hU).parts * #(chunk hP G ε hV).parts)) ^
      2

Tactic:
· rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]
          simp

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H1
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m₁ m₂ n : Fin 3 → R),
    ![(m₁ + m₂) 1 * n 2 - (m₁ + m₂) 2 * n 1, (m₁ + m₂) 2 * n 0 - (m₁ + m₂) 0 * n 2,
        (m₁ + m₂) 0 * n 1 - (m₁ + m₂) 1 * n 0] =
      ![m₁ 1 * n 2 - m₁ 2 * n 1, m₁ 2 * n 0 - m₁ 0 * n 2, m₁ 0 * n 1 - m₁ 1 * n 0] +
        ![m₂ 1 * n 2 - m₂ 2 * n 1, m₂ 2 * n 0 - m₂ 0 * n 2, m₂ 0 * n 1 - m₂ 1 * n 0]

Tactic:
intros
    simp_rw [vec3_add, Pi.add_apply]
    apply vec3_eq <;> ring

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H3
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (m n₁ n₂ : Fin 3 → R),
    ![m 1 * (n₁ + n₂) 2 - m 2 * (n₁ + n₂) 1, m 2 * (n₁ + n₂) 0 - m 0 * (n₁ + n₂) 2,
        m 0 * (n₁ + n₂) 1 - m 1 * (n₁ + n₂) 0] =
      ![m 1 * n₁ 2 - m 2 * n₁ 1, m 2 * n₁ 0 - m 0 * n₁ 2, m 0 * n₁ 1 - m 1 * n₁ 0] +
        ![m 1 * n₂ 2 - m 2 * n₂ 1, m 2 * n₂ 0 - m 0 * n₂ 2, m 0 * n₂ 1 - m 1 * n₂ 0]

Tactic:
intros
    simp_rw [vec3_add, Pi.add_apply]
    apply vec3_eq <;> ring

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s < toColex t ↔ ∃ w ∈ t \ s, {a ∈ s | w < a} = {a ∈ t | w < a}

Tactic:
simp only [lt_iff_exists_forall_lt, mem_sdiff, filter_inj, and_assoc]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ a ∈ ofColex (toColex t), a ∉ ofColex (toColex s) ∧ ∀ b ∈ ofColex (toColex s), b ∉ ofColex (toColex t) → b < a) ↔
    ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ (↑n + 1) * ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k)) - (-1) ^ n =
    ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x)) +
      (-1) ^ (n + 1) * ↑((n + 1 + 1).ascFactorial (n + 1 - (n + 1)))

Tactic:
Finset.mul_sum,

Goal state after:
case succ
n : ℕ
hn : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
⊢ ∑ i ∈ Finset.range (n + 1), (↑n + 1) * ((-1) ^ i * ↑((i + 1).ascFactorial (n - i))) - (-1) ^ n =
    ∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n + 1 - x)) +
      (-1) ^ (n + 1) * ↑((n + 1 + 1).ascFactorial (n + 1 - (n + 1)))
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 ![a, b] ∧ LinearIndependent K ![c, d]
⊢ False

Tactic:
← Matrix.of_row (![a, b]),

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 ![c, d]
⊢ False
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)
⊢ Fintype ↥(A.invMulSubgroup h)

Tactic:
simp only [invMulSubgroup, ← coe_mul, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk,
    mem_coe]
  infer_instance

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

Goal state before:
pp: 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
⊢ 0 < K - ψ

Tactic:
linarith [Real.goldenConj_neg]

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

Goal state before:
pp: case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) ↑p ++ []) = count D (List.take (p.firstReturn + 1) ↑p ++ [])

Tactic:
append_nil,

Goal state after:
case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) ↑p) = count D (List.take (p.firstReturn + 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ decide
        (count U (List.take ((range (↑p.nest).length)[(↑p).length + 1] + 1) ↑p.nest) =
          count D (List.take ((range (↑p.nest).length)[(↑p).length + 1] + 1) ↑p.nest)) =
      true ∧
    ∀ (j : ℕ) (hji : j < (↑p).length + 1),
      decide
          (count U (List.take ((range (↑p.nest).length)[j] + 1) ↑p.nest) =
            count D (List.take ((range (↑p.nest).length)[j] + 1) ↑p.nest)) =
        false

pp: p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (range (↑p.nest).length).length

Tactic:
· simp_rw [u, decide_eq_true_eq, getElem_range]
    constructor
    · rw [take_of_length_le (by simp), ← u, p.nest.count_U_eq_count_D]
    · intro j hj
      simp_rw [cons_append, take_succ_cons, count_cons, beq_self_eq_true, ite_true,
        beq_iff_eq, reduceCtorEq, ite_false, take_append,
        show j - p.toList.length = 0 by lia, take_zero, append_nil]
      have := p.count_D_le_count_U j
      simp only [add_zero, decide_eq_false_iff_not, ne_eq]
      lia

Goal state after:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (range (↑p.nest).length).length
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < (↑(p.take (p.firstReturn + 1) ⋯)).length
⊢ count D (List.take i ↑(p.take (p.firstReturn + 1) ⋯)) < count U (List.take i ↑(p.take (p.firstReturn + 1) ⋯))

Tactic:
by
      simp only [take, length_take, lt_min_iff] at ub ⊢
      replace ub := ub.1
      rw [take_take, min_eq_left ub.le]
      rw [show i = i - 1 + 1 by lia] at ub ⊢
      rw [Nat.add_lt_add_iff_right] at ub
      exact count_D_lt_count_U_of_lt_firstReturn ub

Goal state after:
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 ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
i : ℕ
⊢ g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, by grind⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
i : ℕ
h : g i ≠ 0
⊢ i ≠ 0

case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
i : ℕ
h : g i ≠ 0
⊢ i ≤ g i
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ 0 < p ↔ p ≠ 0

Tactic:
ne_comm,

Goal state after:
p : DyckWord
⊢ 0 < p ↔ 0 ≠ p
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
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
⊢ (if Multiset.count i p.parts * i = i * (b + 1) then f i (b + 1) else 0) = 0

Tactic:
suffices Multiset.count i p.parts * i ≠ i * (b + 1) by simp [this]

Goal state after:
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
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
⊢ Multiset.count i p.parts * i ≠ i * (b + 1)
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
congr! 2 with i hi

Goal state after:
case a
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : i ∈ Ioo 0 (n + 1)
⊢ i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
Module: Mathlib.Combinatorics.Enumerative.Schroder

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

Tactic:
rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ]

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

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

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