mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
rw [← log_le_log_iff (mul_pos (cast_pos.2 (zero_lt_two.trans_le hN)) (exp_pos _)) zero_lt_one,
    log_one, log_mul (cast_pos.2 (zero_lt_two.trans_le hN)).ne' (exp_pos _).ne', log_exp, neg_mul, ←
    sub_eq_add_neg, sub_nonpos, ←
    div_le_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 <| one_lt_two.trans_le hN), div_sqrt,
    sqrt_le_left zero_le_four, log_le_iff_le_exp (cast_pos.2 (zero_lt_two.trans_le hN))]
  norm_num1
  apply le_trans _ four_zero_nine_six_lt_exp_sixteen.le
  exact mod_cast hN'

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(A ^ (n + 2))) ≤ ↑(#(F ^ (n + 1) * A))

Tactic:
gcongr; exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by lia)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
y : EInt
a : ℤ
f : WithBotTop.coe a ⟶ y
⊢ WithBotTop.rec (𝟭 C) t.truncGE 0 (WithBotTop.coe a) ⟶ WithBotTop.rec (𝟭 C) t.truncGE 0 y

Tactic:
induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | top => exact 0

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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ ↑(#(A * C)) ≤ ↑(#(A * B)) / ↑(#B) * ↑(#(B * C))

Tactic:
mul_comm _ B

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ ↑(#(A * C)) ≤ ↑(#(B * A)) / ↑(#B) * ↑(#(B * C))
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ (s •> A).convolution B x = A.convolution B (s⁻¹ * x)

Tactic:
by
  nth_rw 1 [← inv_inv x, ← inv_inv (s⁻¹ * x)]
  rw [← inv_inv B, ← card_smul_inter, ← card_smul_inter, mul_inv_rev, inv_inv, smul_smul]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommMonoid G
A : Set (G × G)
hA : A.Subsingleton
_x₁ _y₁ _x₂ _y₂ : G
hxyd : IsCorner A _x₁ _y₁ _x₂ _y₂
⊢ _x₁ = _x₂

Tactic:
by simpa using hA hxyd.fst_fst_mem hxyd.snd_fst_mem

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#A) * ↑(#(A⁻¹ * (A * A))) ≤ ↑(#(A * A)) * ↑(#(A * (A * A)))

Tactic:
norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul A A (A * A)

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

Goal state before:
pp: case h.mp
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) → ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)

Tactic:
intro ⟨a, b, hadj, ha, hb⟩

Goal state after:
case h.mp
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
a b : V
hadj : G.Adj a b
ha : f a = x✝
hb : f b = y✝
⊢ ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case h.mp
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) → ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)

Tactic:
intro ⟨a, b, hadj, ha, hb⟩
    use s(a, b), hadj
    rw [Embedding.sym2Map_apply, Sym2.map_mk, ha, hb]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
v : V
f : G ≃g G'
⊢ ⇑f '' G.neighborSet v = G'.neighborSet (f v)

Tactic:
by
  rw [← f.toEmbedding.preimage_neighborSet]
  apply Equiv.image_preimage

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
by
  rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩
  have hk : 0 < k := by
    have hh : Finset.Nonempty {v : V | Odd (G.degree v)} := by
      use v
      rw [mem_filter_univ]
      exact h
    rwa [← card_pos, hg, ← two_mul, mul_pos_iff_of_pos_left] at hh
    exact zero_lt_two
  have hc : (fun w : V => w ≠ v ∧ Odd (G.degree w)) = fun w : V => Odd (G.degree w) ∧ w ≠ v := by
    ext w
    rw [and_comm]
  simp only [hc]
  rw [← filter_filter, filter_ne', card_erase_of_mem]
  · refine ⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩
    lia
  · rwa [mem_filter_univ]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
H : SimpleGraph V
inst✝ : Fintype ↑(H.neighborSet v)
hle : G ≤ H
⊢ G.degree v ≤ H.degree v

Tactic:
simp_rw [← card_neighborSet_eq_degree]
  exact Set.card_le_card fun v hv => hle hv

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
ha : IsAtom a
P : Finpartition a
⊢ P = indiscrete ⋯

Tactic:
by
    have h : ∀ b ∈ P.parts, b = a := fun _ hb ↦
      (ha.le_iff.mp <| P.le hb).resolve_left (P.ne_bot hb)
    ext b
    refine Iff.trans ⟨h b, ?_⟩ mem_singleton.symm
    rintro rfl
    obtain ⟨c, hc⟩ := P.parts_nonempty ha.1
    simp_rw [← h c hc]
    exact hc

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
let el := {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : ↥({p ∈ P.parts | #p = #s / #P.parts + 1}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts + 1}) :=
  {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.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)
⊢ { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts }

Tactic:
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:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5

Tactic:
exact div_pos (by simp) (pow_pos hε 5)

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

Goal state before:
pp: ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
⊢ |x| ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|

Tactic:
by rwa [abs_of_nonneg hx]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 ≤ (#A + #P.parts) ^ 2

Tactic:
gcongr; apply Nat.mul_div_le

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∑ A ∈ P.parts.attach, #(chunk hP G ε ⋯).parts = stepBound #P.parts

Tactic:
chunk,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∑ A ∈ P.parts.attach,
      #(if hUcard : #↑A = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts) then equitabilise ⋯
          else equitabilise ⋯).parts =
    stepBound #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inr.inr.zero
α : 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
this : Nonempty α
⊢ 0 ≤ ↑(dum.energy G)

Tactic:
exact mod_cast dum.energy_nonneg G

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(P.energy G) + ε ^ 5 / 4 =
    (∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4)) / ↑(#P.parts) ^ 2

Tactic:
rw [coe_energy, add_div, mul_div_cancel_left₀]

Goal state after:
case ha
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(#P.parts) ^ 2 ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∉ G.incidenceSet x ↔ x ∉ x✝

Tactic:
incidenceSet,

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∉ {e | e ∈ G.edgeSet ∧ x ∈ e} ↔ x ∉ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset - G.copyCount ⊥ ≤ #(G.killCopies ⊥).edgeFinset

pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
⊢ #G.edgeFinset - G.copyCount H ≤ #(G.killCopies H).edgeFinset

Tactic:
· simp [← card_edgeSet]

Goal state after:
case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
⊢ #G.edgeFinset - G.copyCount H ≤ #(G.killCopies H).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
hadj : v = w ∨ G.Adj v w
v' w' : V
hvw' : (edge v w).Adj v' w'
⊢ G.Adj v' w'

Tactic:
grind [adj_symm]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
⊢ #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1

Tactic:
rw [G.edgeFinset_sup_edge hn h, card_cons]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
⊢ (p.dropUntil w h).length = p.length - List.idxOf w p.support

Tactic:
by
  simp [dropUntil_eq_drop]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
| ((p.takeUntil w hw).append (p.dropUntil w hw)).getVert n

Tactic:
getVert_append

Goal state after:
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
| if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
  else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).reverse.IsPath
⊢ q.reverse.IsPath

Tactic:
rw [reverse_append] at h

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (q.reverse.append p.reverse).IsPath
⊢ q.reverse.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.support.tail

Tactic:
rw [mem_support_iff] at hy

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x = v ∨ x ∈ q.support.tail
hq : ¬q.Nil
⊢ x ∈ q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : 0 < n
h : (p.drop 1).IsPath
⊢ (p.drop n).IsPath

Tactic:
rw [← Nat.add_sub_of_le hn, drop_add_eq]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : 0 < n
h : (p.drop 1).IsPath
⊢ (((p.drop (Nat.succ 0)).drop (n - Nat.succ 0)).copy ⋯ ⋯).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ Set.InjOn p.getVert {i | i ≤ p.length}

Tactic:
intro n

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
n : ℕ
⊢ n ∈ {i | i ≤ p.length} → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {i | i ≤ p.length} → p.getVert n = p.getVert x₂ → n = x₂
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
⊢ Set.InjOn q.getVert {i | i ≤ q.length}

Tactic:
intro n

Goal state after:
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
⊢ n ∈ {i | i ≤ q.length} → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {i | i ≤ q.length} → q.getVert n = q.getVert x₂ → n = x₂
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ u :: (cons h p).tail.support ~ u :: (cons h p).dropLast.support

Tactic:
List.perm_comm,

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ u :: (cons h p).dropLast.support ~ u :: (cons h p).tail.support
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
hpc : (cons ⋯ p.tail).IsCycle
⊢ Set.InjOn p.getVert {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
intro n

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc✝ : p.IsCycle
hpc : (cons ⋯ p.tail).IsCycle
n : ℕ
⊢ n ∈ {i | 1 ≤ i ∧ i ≤ p.length} → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {i | 1 ≤ i ∧ i ≤ p.length} → p.getVert n = p.getVert x₂ → n = x₂
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 | i ≤ p.length - 1}

Tactic:
intro n

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
⊢ n ∈ {i | i ≤ p.length - 1} → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ {i | i ≤ p.length - 1} → p.getVert n = p.getVert x₂ → n = x₂
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
hn : 1 < n
t : Finset β
f : α ↪ β
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) ∧ #t = n → ∃ s, G.IsNClique n s ∧ map f s = t

Tactic:
rintro ⟨⟨s, hs, rfl⟩, rfl⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
hs : G.IsClique ↑s
hn : 1 < #(map f s)
⊢ ∃ s_1, G.IsNClique (#(map f s)) s_1 ∧ map f s_1 = map f s
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)) ≤ ↑(#s) * ε + ↑(#s) * ε

Tactic:
rw [Nat.cast_add]

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.Additive.Dissociation

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
⊢ Pi.single a 1 b = -1 ∨ Pi.single a 1 b = 0 ∨ Pi.single a 1 b = 1

Tactic:
by obtain rfl | hab := eq_or_ne a b <;> simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s ^ 2 * #t ^ 2 = (#s * #t) ^ 2

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ x ∈ s ×ˢ t, x.1 * x.2 ∈ s * t

Tactic:
mul_pow

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #s ^ 2 * #t ^ 2 = #s ^ 2 * #t ^ 2

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ x ∈ s ×ˢ t, x.1 * x.2 ∈ s * t
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / A)) * ↑(#(A / A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
by rw [← divConst_mul_card]; ring

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

Goal state before:
pp: case refine_1
ι : 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
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0} ⊆ s

pp: case refine_2
ι : 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
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ #(Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}) = p

pp: case refine_3
ι : 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
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ ∑ i ∈ Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}, a i = 0

Tactic:
· simp +contextual [subset_iff]

Goal state after:
case refine_2
ι : 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
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ #(Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}) = p

case refine_3
ι : 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
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ ∑ i ∈ Finset.map { toFun := Subtype.val, inj' := ⋯ } {a_1 | ↑x a_1 ≠ 0}, a i = 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u✝ : Finset α
a✝ b : α
s t u : Colex (Finset α)
hst : s ≤ t
htu : t ≤ u
a : α
has : a ∈ ofColex s
hau : a ∉ ofColex u
hat : a ∉ ofColex t
⊢ ∃ b ∈ ofColex u, b ∉ ofColex s ∧ a ≤ b

Tactic:
· exact trans_aux hst htu has hat

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

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

Tactic:
by
  simp_rw [cross_apply, vec3_add]
  apply vec3_eq <;> dsimp <;> ring

Goal state after: