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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.tail.support ~ p.dropLast.support

Tactic:
cases p with | nil => rfl | cons h p
   =>  _ 

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ (cons h p).tail.support ~ (cons h p).dropLast.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support.tail ~ p.support.dropLast

Tactic:
cases p with | nil => rfl | cons h p
   =>  _ 

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ u
⊢ (cons h p).support.tail ~ (cons h p).support.dropLast
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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) ≤
    ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id)))) *
      (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))

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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))

Tactic:
mul_assoc

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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) ≤
    ↑(#(interedges G.Adj x y)) *
      ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))))

α : 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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
h : completeGraph (Fin n) ⊑ G
this : G.IsNClique (Fintype.card (Fin n)) (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n

Tactic:
Fintype.card_fin

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : completeGraph (Fin n) ⊑ G
this : G.IsNClique n (map (Nonempty.some h).toEmbedding univ)
⊢ ¬G.CliqueFree n
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
ht : p.IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle
⊢ p.IsPath

Tactic:
classical
  match p with
  | .nil => simp
  | .cons hadj p =>
    have hp := isPath_iff_isSubwalk_imp_not_isCycle ht.of_cons |>.mpr (h · · <| ·.cons hadj)
    refine cons_isPath_iff .. |>.mpr ⟨hp, fun hup ↦ h u (p.takeUntil u hup |>.cons hadj) ?_ ?_⟩
    · rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]
      exact (List.prefix_cons_inj u |>.mpr <| p.support_takeUntil_prefix_support hup).isInfix
    · refine cons_isCycle_iff .. |>.mpr ⟨hp.takeUntil hup, fun he ↦ ?_⟩
      exact ht.edges_nodup.notMem <| p.edges_takeUntil_subset_edges hup he

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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(A.sup id)) * ↑(#(B.sup id)) ≤ (1 + ε ^ 5 / 49) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))

Tactic:
refine le_trans ?_ (mul_le_mul_of_nonneg_right (m_add_one_div_m_le_one_add hPα hPε hε₁) ?_)

Goal state after:
case refine_1
α : 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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(A.sup id)) * ↑(#(B.sup id)) ≤ ((↑m + 1) / ↑m) ^ 2 * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))

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
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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 ≤ ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∃ w ∈ p.support, w ∈ q.support ∧ w ≠ u ∧ w ≠ v
w : V
hwp : w ∈ p.support
hwq : w ∈ q.support
hwu : w ≠ u
hwv : w ≠ v
h✝ : p.takeUntil w hwp = q.takeUntil w hwq
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
have := ih _ (hs ▸ length_dropUntil_lt_length hwp hwu) (hp.dropUntil hwp) (hq.dropUntil hwq)
        <| by grind [take_spec]
      grind [isSubwalk_dropUntil, IsSubwalk.trans]

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
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < #(A.sup id) * #(B.sup id)

Tactic:
apply mul_pos <;> rw [Finset.card_pos, sup_eq_biUnion, biUnion_nonempty]

Goal state after:
case ha
α : 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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ A, (id x).Nonempty

case hb
α : 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 y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ∃ x ∈ B, (id x).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
sm : G.IsMaximumClique s
⊢ #s = G.cliqueNum

Tactic:
by
  obtain ⟨sc, sm⟩ := sm
  obtain ⟨t, tc, tcard⟩ := G.exists_isNClique_cliqueNum
  exact eq_of_le_of_not_lt sc.card_le_cliqueNum (by simp [← tcard, sm t tc])

Goal state after:
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}
a : α
a✝¹ : a ∈ ↑X'
b : α
a✝ : b ∈ ↑X'
t : a ≠ b
⊢ Function.onFun Disjoint
    (fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t✝ | G.Adj x y}) ({y ∈ u | G.Adj x y}))) a b

Tactic:
rw [Function.onFun, Finset.disjoint_left]

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}
a : α
a✝¹ : a ∈ ↑X'
b : α
a✝ : b ∈ ↑X'
t : a ≠ b
⊢ ∀ ⦃a_1 : α × α × α⦄,
    a_1 ∈ image (fun x ↦ (a, x)) (G.interedges ({y ∈ t✝ | G.Adj a y}) ({y ∈ u | G.Adj a y})) →
      a_1 ∉ image (fun x ↦ (b, x)) (G.interedges ({y ∈ t✝ | G.Adj b y}) ({y ∈ u | G.Adj b y}))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * ε * ↑(Fintype.card α ^ 2)
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
mul_assoc

Goal state after:
case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : l ≤ Fintype.card α
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ ↑(#P.parts)
k : 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * (ε * ↑(Fintype.card α ^ 2))
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hn : cornersTheoremBound (ε / 9) ≤ n
A : Finset (ℕ × ℕ)
hAn : A ⊆ range n ×ˢ range n
hAε : ε * ↑n ^ 2 ≤ ↑(#A)
⊢ ¬IsCornerFree ↑A

Tactic:
by
  rintro hA
  rw [← coe_subset, coe_product] at hAn
  have : A = Prod.map Fin.val Fin.val ''
      (Prod.map Nat.cast Nat.cast '' A : Set (Fin (2 * n).succ × Fin (2 * n).succ)) := by
    rw [Set.image_image, Set.image_congr, Set.image_id]
    simp only [mem_coe, Nat.succ_eq_add_one, Prod.map_apply, Fin.val_natCast, id_eq, Prod.forall,
      Prod.mk.injEq, Nat.mod_succ_eq_iff_lt]
    rintro a b hab
    have := hAn hab
    simp at this
    lia
  rw [this] at hA
  have := Fin.isAddFreimanIso_Iio two_ne_zero (le_refl (2 * n))
  have := hA.of_image this.isAddFreimanHom Fin.val_injective.injOn <| by
    refine Set.image_subset_iff.2 <| hAn.trans fun x hx ↦ ?_
    simp only [coe_range, Set.mem_prod, Set.mem_Iio] at hx
    exact ⟨Fin.natCast_strictMono (by lia) hx.1, Fin.natCast_strictMono (by lia) hx.2⟩
  rw [← coe_image] at this
  refine corners_theorem (ε / 9) (by positivity) (by simp; lia) _ ?_ this
  calc
    _ = ε / 9 * (2 * n + 1) ^ 2 := by simp
    _ ≤ ε / 9 * (2 * n + n) ^ 2 := by gcongr; simp; unfold cornersTheoremBound at hn; lia
    _ = ε * n ^ 2 := by ring
    _ ≤ #A := hAε
    _ = _ := by
      rw [card_image_of_injOn]
      have : Set.InjOn Nat.cast (range n) :=
        (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono (by simp; lia)
      exact (this.prodMap this).mono hAn

Goal state after:
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)) / 4 ^ #P.parts * (↑(#(star hP G ε hV U)) / 4 ^ #P.parts) * (9 / 4 ^ 2) * ε ^ 2

Tactic:
mul_assoc

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.SubsetSum

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

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
r : ℕ
⊢ Sized r ∅

Tactic:
simp [Sized]

Goal state after:
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
s : Finset α
r : ℕ
⊢ Sized r {s} ↔ #s = r

Tactic:
simp [Sized]

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
⊢ ∃ t ⊆ s, #t = p ∧ ∑ i ∈ t, a i = 0

Tactic:
set N := Fintype.card {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0}
  -- Zero is a common root to `f₁` and `f₂`, so `N` is nonzero
  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]⟩
  have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
  have hs' : 2 * p - 1 = Fintype.card s := by simp [hs]
  -- Chevalley-Warning gives us that `p ∣ n` because the total degrees of `f₁` and `f₂` are at most
  -- `p - 1`, and we have `2 * p - 1 > 2 * (p - 1)` variables.
  have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
  -- Hence, `2 ≤ p ≤ N` and we can make a common root `x ≠ 0`.
  obtain ⟨x, hx⟩ := Fintype.exists_ne_of_one_lt_card ((Fact.out : p.Prime).one_lt.trans_le <|
    Nat.le_of_dvd hN₀ hpN) zero_sol
  -- This common root gives us the required subsequence, namely the `i ∈ s` such that `x i ≠ 0`.
  refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
  · simp +contextual [subset_iff]
  -- From `f₁ x = 0`, we get that `p` divides the number of `a` such that `x a ≠ 0`.
  · rw [card_map]
    refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_
    -- This number is nonzero because `x ≠ 0`.
    · rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
      exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)
    · rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1
    -- And it is at most `2 * p - 1`, so it must be `p`.
    · rw [univ_eq_attach, card_attach, hs]
      exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one
  -- From `f₂ x = 0`, we get that `p` divides the sum of the `a ∈ s` such that `x a ≠ 0`.
  · simpa [f₂, ZMod.pow_card_sub_one, Finset.sum_filter] using x.2.2

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ List.Pairwise (fun x y ↦ x ∈ L ∧ y ∈ L ∧ x - (a + 1) < y - (a + 1)) L

Tactic:
Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y),

Goal state after:
case refine_1
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ List.Pairwise (fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y) L

case refine_1.H
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
haL : ∀ (a' : ℕ), a' ∈ L → a + 1 ≤ a'
⊢ ∀ (a_1 b : ℕ), a_1 ∈ L ∧ b ∈ L ∧ a_1 - (a + 1) < b - (a + 1) ↔ a_1 ∈ L ∧ b ∈ L ∧ a_1 < b
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)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a c : G
ha : ∃ y, y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = a
hc : ∃ y, y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = c
⊢ a * c ∈ A⁻¹ * A

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := ha

Goal state after:
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)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
c : G
hc : ∃ y, y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = c
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ a * b * c ∈ A⁻¹ * A
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ 1 < order P L

Tactic:
← add_lt_add_iff_right 1,

Goal state after:
case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p₁ p₂ p₃ : P
l₁ l₂ l₃ : L
h₂₁ : p₂ ∉ l₁
h₂₂ : p₂ ∈ l₂
h₂₃ : p₂ ∈ l₃
h₃₁ : p₃ ∉ l₁
h₃₂ : p₃ ∈ l₂
h₃₃ : p₃ ∉ l₃
val✝ : Fintype { p // p ∈ l₂ }
⊢ 1 + 1 < order P L + 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 : ¬((crossProduct a) b = 0 ∨ (crossProduct c) d = 0)
⊢ False

Tactic:
not_or,

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 : ¬(crossProduct a) b = 0 ∧ ¬(crossProduct c) d = 0
⊢ 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)
x : G
hx : x ∈ A
⊢ x ∈ ↑A ∧ (fun x1 x2 ↦ x1 * x2) x⁻¹ x = 1

Tactic:
by simp [hx]

Goal state after:
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 (of ![a, b]).row ∧ LinearIndependent K (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
hAB : (Nat.succ 0).succ + (Nat.succ 0).succ ≤ Fintype.card (Fin 3)
⊢ False

Tactic:
Fintype.card_fin

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 (of ![c, d]).row
A : Matrix (Fin 2) (Fin 3) K := of ![a, b]
B : Matrix (Fin 2) (Fin 3) K := of ![c, d]
hAB : (Nat.succ 0).succ + (Nat.succ 0).succ ≤ 3
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
mul_assoc

Goal state after:
m : Multiset ℕ
⊢ (map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣
    m.bell * ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)
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
a b : α
⊢ f a b = g a b

Tactic:
by_cases hab : a ≤ b

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

case neg
𝕜 : Type u_2
α : Type u_5
inst✝¹ : Zero 𝕜
inst✝ : LE α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ f a b = g a b