mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
| (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
rw [SimpleGraph.edgeDensity_def, SimpleGraph.interedges, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl), ofSubset_parts,
      ofSubset_parts]
    simp only [cast_sum, sum_div, mul_sum, Rat.cast_sum, Rat.cast_div,
      mul_div_left_comm ((1 : ℝ) - _)]

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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
| ∑ x ∈ A ×ˢ B, ↑↑(#(interedges G.Adj x.1 x.2)) * ((1 - ε ^ 5 / 50) / ↑(↑(#(A.sup id)) * ↑(#(B.sup id))))
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'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts ↔
    ∃ a ∈ p.darts, a.edge = s(u', v')

Tactic:
refine ⟨fun h ↦ by grind [Dart.edge], fun 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')
⊢ { 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
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
x✝ : i + 1 ≠ 0
⊢ p.getVert (i + 1) ∈ p.support.tail

Tactic:
rw [← getVert_tail, ← p.support_tail_of_not_nil hp]
    exact getVert_mem_support ..

Goal state after:
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
| (1 + ε ^ 5 / 49) * ↑(edgeDensity G.Adj (A.biUnion id) (B.biUnion id))

Tactic:
edgeDensity,

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
| (1 + ε ^ 5 / 49) * ↑(↑(#(interedges G.Adj (A.biUnion id) (B.biUnion id))) / (↑(#(A.biUnion id)) * ↑(#(B.biUnion id))))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
c : G.Walk v v
hu : u ∈ c.support
⊢ (c.rotate u hu).IsTrail ↔ c.IsTrail

Tactic:
by
  rw [isTrail_def, isTrail_def, (c.rotate_edges u hu).perm.nodup_iff]

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ p.edges.Disjoint q.edges

Tactic:
grind [IsPath.disjoint_edges_of_disjoint_support, List.Disjoint.symm]

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

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ ↑(#A) = ↑(#(image (fun x ↦ ↑x) A))

Tactic:
rw [card_image_of_injOn]
      exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by
        simp; lia

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}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ 𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ) * (starRingEnd ℂ) (ψ a) =
    𝔼 i, ((∏ ψ ∈ u, d ψ) * ∏ i_1 ∈ u, i_1 i) * ((∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ)) * ∏ i_1 ∈ t \ u, i_1 (-i))

Tactic:
← prod_mul_distrib,

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ 𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ) * (starRingEnd ℂ) (ψ a) =
    𝔼 i, (∏ x ∈ u, d x * x i) * ∏ x ∈ t \ u, (starRingEnd ℂ) (d x) * x (-i)
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: case insert
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A✝ : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : (∀ x ∈ A, 0 < x) → (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ insert a A, 0 < x
A_pos' : ∀ x ∈ A, 0 < x
⊢ (#A + 1).choose (2 - 1) + (#A + 1).choose 2 < #(insert a A).subsetSum

Tactic:
Nat.choose_one_right,

Goal state after:
case insert
M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A✝ : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : M
A : Finset M
A_lt_a : ∀ x ∈ A, x < a
ih : (∀ x ∈ A, 0 < x) → (#A + 1).choose 2 < #A.subsetSum
A_pos : ∀ x ∈ insert a A, 0 < x
A_pos' : ∀ x ∈ A, 0 < x
⊢ #A + 1 + (#A + 1).choose 2 < #(insert a A).subsetSum
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄, x ∈ ⋃ i, f i → #x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → #x = r

Tactic:
Set.mem_iUnion,

Goal state after:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄, (∃ i, x ∈ f i) → #x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → #x = r
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case cons
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L

Tactic:
have h' : ∃ (L₀ : List ℕ), L₀.SortedLT ∧ L = L₀.map (· + a + 1) := by
    refine ⟨L.map (· - (a+1)), ?_, ?_⟩
    · rwa [sortedLT_iff_pairwise, pairwise_map, Pairwise.and_mem,
        Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ← Pairwise.and_mem]
      simp only [and_congr_right_iff]
      exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]
    have h' : ∀ x ∈ L, ((fun x ↦ x + a + 1) ∘ (fun x ↦ x - (a + 1))) x = x := fun x hx ↦ by
      simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]
    simp [List.map_congr_left h']

Goal state after:
case cons
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
h' : ∃ L₀, L₀.SortedLT ∧ L = map (fun x ↦ x + a + 1) L₀
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L
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]

pp: case H2
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

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]

pp: case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![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:
case H2
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

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]

case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]
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]

pp: case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![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:
case H4
R : Type u_1
inst✝ : CommRing R
⊢ ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ (crossProduct v) w + (crossProduct w) v = 0

Tactic:
rw [add_eq_zero_iff_eq_neg, cross_anticomm]

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

Goal state before:
pp: n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ↑n ∣ ∑ i ∈ t, i.1
⊢ (Multiset.map Prod.fst t.val).card = n ∧ ↑n ∣ (Multiset.map Prod.fst t.val).sum

Tactic:
by simpa using ht

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

Goal state before:
pp: n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ∑ i ∈ t, i.1 = 0
⊢ (Multiset.map Prod.fst t.val).card = n ∧ (Multiset.map Prod.fst t.val).sum = 0

Tactic:
by simpa using ht

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

Goal state before:
pp: case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ a, a • w = v

Tactic:
refine ⟨Units.mk0 a fun c => hv.symm ?_, ha⟩

Goal state after:
case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv✝ : v ≠ 0
hv : ∃ x, ¬v ⬝ᵥ x = 0
⊢ ∃ w, ¬(mk F v hv✝).orthogonal w

Tactic:
obtain ⟨w, hw⟩ := hv

Goal state after:
case h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : ¬v ⬝ᵥ w = 0
⊢ ∃ w, ¬(mk F v hv).orthogonal w
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![![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,
        ![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,
        ![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]
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
· simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![![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,
        ![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,
        ![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]
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
· simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case «2»
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ ![![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,
        ![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,
        ![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]
      ((fun i ↦ i) ⟨2, ⋯⟩) =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
· simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i ∈ s, lineCount L i.1 + ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 + ∑ i ∈ sᶜ, pointCount P i.2
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
⊢ ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2

Tactic:
step2,

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i ∈ s, pointCount P i.2 + ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 + ∑ i ∈ sᶜ, pointCount P i.2
step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2
⊢ ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q ↦ ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq ↦ ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card { q // q ≠ p } + 1 = Fintype.card P

Tactic:
apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } := ⋯
⊢ Fintype.card { q // q ≠ p } = Fintype.card P - Nat.succ 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> A⁻¹ * A

Tactic:
exact subset_mul_right _ (by simp [← inv_smul_mem_iff, inv_mem_inv ha])

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 : 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
this✝ : #r = #A
this : #(l ∪ r) < 2 * #A
⊢ (l ∩ r).Nonempty

Tactic:
rw [← card_pos]

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
this✝ : #r = #A
this : #(l ∪ r) < 2 * #A
⊢ 0 < #(l ∩ r)
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
⊢ f = g

Tactic:
by
  refine DFunLike.coe_injective (funext₂ fun a b ↦ ?_)
  by_cases hab : a ≤ b
  · exact h _ _ hab
  · rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le hab]

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

Goal state before:
pp: ⊢ insidePart 0 = 0

Tactic:
by simp [insidePart]

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : CommRing α
inst✝ : Fact (IsUnit 2)
⊢ Fintype.card α * addRothNumber univ ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Tactic:
obtain ⟨s, -, hscard, hs⟩ := addRothNumber_spec (univ : Finset α)
  have := noAccidental hs
  rw [← hscard, ← card_triangleIndices, ← card_triangles]
  exact (locallyLinear hs).le_ruzsaSzemerediNumber

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case refine_2
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ↑b ≤ 12 * ↑((b - 3) / 6)

Tactic:
exact ⟨15, fun x hx ↦ by norm_cast; lia⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Semigroup

Goal state before:
pp: case hts
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := ⋯
N : Set M
hN : Minimal (fun x ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x ↦ x * m) '' N ⊆ N

Tactic:
· rintro _ ⟨m', hm', rfl⟩
        exact N_mul _ hm' _ hm

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

Goal state before:
pp: α : Type u_1
e f : Set α
H : Hypergraph α
h : H.EAdj e f
⊢ ∃ x ∈ V(H), x ∈ e ∧ x ∈ f

Tactic:
obtain ⟨x, hx⟩ := h.2.2
  exact ⟨x, mem_vertexSet_of_mem_edgeSet h.1 hx.1, hx⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ M.IsCircuit C → (C ⊆ M.E ∧ Disjoint C D ↔ Disjoint C D)

Tactic:
and_iff_right_iff_imp

Goal state after:
α : Type u_1
M : Matroid α
D C : Set α
⊢ M.IsCircuit C → Disjoint C D → C ⊆ M.E
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.succ.inr
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h✝ : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
h : ∃ l, IsMono C' l
⊢ (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
exact Or.inr (mono_of_mono h)

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
⊢ (M j).IsBase (Sigma.mk j ⁻¹' insert ⟨i, f⟩ (B₁ \ {⟨i, e⟩}))

Tactic:
rw [← union_singleton, preimage_union, preimage_sdiff]

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ \ Sigma.mk j ⁻¹' {⟨i, e⟩} ∪ Sigma.mk j ⁻¹' {⟨i, f⟩})
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hIX : M.IsBasis' I X
hJI : J ⊆ I
⊢ (M ／ J).IsBasis' (I \ J) X

Tactic:
simpa [isBasis'_iff_isBasis_inter_ground, inter_sdiff_assoc, ← sdiff_inter_distrib_right] using
    (hIX.contract_isBasis'_sdiff_sdiff_of_subset hJI).isBasis_inter_ground

Goal state after: