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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k]? = some p₁.support[i]

Tactic:
rw [getElem?_pos _ _ <| by grind, Option.some_inj]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
⊢ p₂.support[i + k] = p₁.support[i]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : u✝ = u
h' : u = u✝
⊢ List.count u (h'✝ ▸ nil).support = 1

Tactic:
subst_vars

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u✝ ∈ p✝.support), List.count u✝ (p✝.takeUntil u✝ h).support = 1
a✝ : List.Mem u✝ p✝.support
h' : u✝ = u✝
⊢ List.count u✝ (⋯ ▸ nil).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : ¬u✝ = u
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1

Tactic:
subst_vars

Goal state after:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
h'✝ : ¬u✝ = u
h' : ¬u = u✝
⊢ List.count u (cons h✝ (p✝.takeUntil u ⋯)).support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ q.support <:+ (p.append q).support

Tactic:
by
  simp [support_append_eq_support_dropLast_append]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).darts = p.darts

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).darts = p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
⊢ u ∈ p.support

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
v w u✝ : V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
⊢ (p.copy hv hw).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).takeUntil u h = (p.takeUntil u ⋯).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
⊢ (p.copy hv hw).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
x u✝ : V
q : G.Walk u✝ w
hx✝ : x ∈ nil.support
hx : x = u✝
⊢ (nil.append q).takeUntil x ⋯ = nil.takeUntil x hx✝

Tactic:
subst_vars

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
q : G.Walk u✝ w
hx : u✝ ∈ nil.support
⊢ (nil.append q).takeUntil u✝ ⋯ = nil.takeUntil u✝ hx
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).edges = p.edges

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).edges = p.edges
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
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
⊢ w ∉ (p.takeUntil x ⋯).support

Tactic:
← takeUntil_takeUntil p hw hx

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
⊢ w ∉ ((p.takeUntil w hw).takeUntil x hx).support
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).IsTrail ↔ p.IsTrail

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsTrail ↔ p.IsTrail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).IsPath ↔ p.IsPath

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).IsPath ↔ p.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u u' : V
p : G.Walk u u
hu : u = u'
⊢ (p.copy hu hu).IsCircuit ↔ p.IsCircuit

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCircuit ↔ p.IsCircuit
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u u' : V
p : G.Walk u u
hu : u = u'
⊢ (p.copy hu hu).IsCycle ↔ p.IsCycle

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' : V
p : G.Walk u' u'
⊢ (p.copy ⋯ ⋯).IsCycle ↔ p.IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).Nil = p.Nil

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).Nil = p.Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
i : ℕ
h : u = w
h' : v = x
⊢ (p.copy h h').getVert i = p.getVert i

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
w x : V
i : ℕ
p : G.Walk w x
⊢ (p.copy ⋯ ⋯).getVert i = p.getVert i
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.tail.getVert i ∈ p.support.tail

Tactic:
← p.support_tail_of_not_nil hp

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
i : ℕ
x✝ : i + 1 ≠ 0
⊢ p.tail.getVert i ∈ p.tail.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ ¬G.IsClique s ↔ ∃ v w, v ≠ w ∧ ¬G.Adj ↑v ↑w

Tactic:
by
  aesop (add simp [isClique_iff, Set.Pairwise])

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ #t ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
obtain (ht | ht) := le_or_gt #t 1
  · simp only [ht, true_or, iff_true]
    exact IsClique.of_subsingleton <| card_le_one.1 ht
  rw [isClique_map_finset_iff_of_nontrivial, ← not_lt]
  · simp [ht]
  exact Finset.one_lt_card_iff_nontrivial.mp ht

Goal state after:
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
⊢ (cons h p).support.tail ~ (cons h p).support.dropLast

Tactic:
simpa using support_tail_perm_support_dropLast <| p.cons h

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:
refine ⟨?_, by aesop⟩

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 α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ #(s.erase a) = n - 1

Tactic:
card_erase_of_mem ha,

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ #s - 1 = n - 1
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔ ∃ u w, w.IsCycle ∧ w.length = 3

Tactic:
isCycle_def

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ (∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔
    ∃ u w, (w.IsTrail ∧ w ≠ nil ∧ w.support.tail.Nodup) ∧ w.length = 3
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).bypass = p.bypass.copy hu hv

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).bypass = p.bypass.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ G.badVertices ε s t, ↑(#({y ∈ t | G.Adj x y})) ≤ #(G.badVertices ε s t) • ((↑(G.edgeDensity s t) - ε) * ↑(#t))

Tactic:
exact sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2.le

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v✝ w v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s

Tactic:
subst_vars

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
⊢ toDeleteEdges s (p.copy hu hv) h = (toDeleteEdges s p ⋯).copy hu hv

Tactic:
subst_vars

Goal state after:
V : Type u
G : SimpleGraph V
u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ toDeleteEdges s (p.copy ⋯ ⋯) h = (toDeleteEdges s p ⋯).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ b, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ b, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ a, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case in₂₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ a, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ↑(#(star hP G ε hU V)) * (↑m + 1) * ((1 - (↑m)⁻¹) / (4 ^ #P.parts * ↑m)) ≤ ↑(#(star hP G ε hU V)) / 4 ^ #P.parts

Tactic:
rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      linarith

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
⊢ (∃ x ∈ t, toTriangle x = s) → (graph t).IsNClique 3 s

Tactic:
· rintro ⟨x, hx, rfl⟩
    exact toTriangle_is3Clique hx

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

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : A ⊆ range n
hAε : ε * ↑n ≤ ↑(#A)
⊢ ¬ThreeAPFree ↑A

Tactic:
by
  rintro hA
  rw [← coe_subset, coe_range] at hAn
  have : A = Fin.val '' (Nat.cast '' A : Set (Fin (2 * n).succ)) := by
    rw [Set.image_image, Set.image_congr, Set.image_id]
    simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]
    rintro a ha
    have := hAn ha
    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 <| Set.image_subset_iff.2 <|
      hAn.trans fun x hx ↦ Fin.natCast_strictMono (by lia) <| by
        simpa only [coe_range, Set.mem_Iio] using hx
  rw [← coe_image] at this
  refine roth_3ap_theorem (ε / 3) (by positivity) (by simp; lia) _ ?_ this
  calc
    _ = ε / 3 * (2 * n + 1) := by simp
    _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; lia
    _ = ε * n := by ring
    _ ≤ #A := hAε
    _ = _ := by
      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}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) =
    ∑ x, 𝔼 i, (∏ ψ ∈ x, (d ψ * ψ i + (starRingEnd ℂ) (d ψ * ψ i)) / 2) * ∏ ψ ∈ xᶜ, ↑(c ψ)

Tactic:
← expect_sum_comm,

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
⊢ 𝔼 i, ∏ x, (↑(c x) + ↑(d x * x i).re) =
    𝔼 i, ∑ j, (∏ ψ ∈ j, (d ψ * ψ i + (starRingEnd ℂ) (d ψ * ψ i)) / 2) * ∏ ψ ∈ jᶜ, ↑(c ψ)
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
D D' : ℙ K V
h : D ≠ D'
a : K
hD : a • D.rep = D'.rep
this : a ≠ 0
⊢ ∃ a, a • D.rep = D'.rep

Tactic:
by refine ⟨(Ne.isUnit this).unit, by simp [← hD]⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ #(s.erase a) ≤ #(t.erase m)

Tactic:
card_erase_of_mem ha,

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
hwt : m ∈ t
hws : m ∉ s
hw : ∀ ⦃a : α⦄, m < a → (a ∈ s ↔ a ∈ t)
haw : a < m
this : t.erase m ⊆ s.erase a
⊢ #s - 1 ≤ #(t.erase m)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
⊢ IsInitSeg (initSeg s) #s

Tactic:
refine ⟨fun t ht => (mem_initSeg.1 ht).1.symm, fun t₁ t₂ ht₁ ht₂ ↦ mem_initSeg.2 ⟨ht₂.2.symm, ?_⟩⟩
  rw [mem_initSeg] at ht₁
  exact ht₂.1.le.trans ht₁.2

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ fiber (some a) = {f | fixedPoints ⇑f ⊆ {a}}

Tactic:
ext f

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ f ∈ fiber (some a) ↔ f ∈ {f | fixedPoints ⇑f ⊆ {a}}
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
contra : f x = x
⊢ False

Tactic:
exact x_vs_a (h_opfp contra)

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h.h.h
K : Type u_3
inst✝ : Field K
d : ℙ K (Fin 3 → K)
a : Fin 3 → K
ha : a ≠ 0
had : (Projectivization.mk K a ha).orthogonal d
b : Fin 3 → K
hb : b ≠ 0
hbd : (Projectivization.mk K b hb).orthogonal d
c : Fin 3 → K
hc : c ≠ 0
hac : (Projectivization.mk K a ha).orthogonal (Projectivization.mk K c hc)
hbc : (Projectivization.mk K b hb).orthogonal (Projectivization.mk K c hc)
⊢ Projectivization.mk K a ha = Projectivization.mk K b hb ∨ Projectivization.mk K c hc = d

Tactic:
induction d with

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
· trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
      · refine sum_congr rfl fun i _ => ?_
        rw [gosper_trick i.is_le, mul_div]
      · rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
            sum_range_sub, Nat.succ_eq_add_one]
        rw [gosper_catalan_sub_eq_central_binom_div d]
        norm_cast

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

Goal state before:
pp: case e_a
m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
      ((map (fun j ↦ j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    ∏ i ∈ m.toFinset, (i * count i m)!

pp: case e_a
m : Multiset ℕ
⊢ ∑ k ∈ m.toFinset, k * count k m = m.sum

Tactic:
· rw [mul_comm, mul_assoc, ← Finset.prod_mul_distrib, Finset.prod_multiset_map_count]
    suffices this : _ by
      by_cases hm : 0 ∈ m.toFinset
      · rw [← Finset.prod_erase_mul _ _ hm]
        rw [← Finset.prod_erase_mul _ _ hm]
        simp only [factorial_zero, one_pow, mul_one, zero_mul]
        exact this
      · nth_rewrite 1 [← Finset.erase_eq_of_notMem hm]
        nth_rewrite 3 [← Finset.erase_eq_of_notMem hm]
        exact this
    rw [← Finset.prod_mul_distrib]
    congr! 1 with x hx
    rw [← mul_assoc, bell_mul_eq_lemma]
    simp only [Finset.mem_erase, ne_eq, mem_toFinset] at hx
    simp only [ne_eq, hx.1, not_false_eq_true]

Goal state after:
case e_a
m : Multiset ℕ
⊢ ∑ k ∈ m.toFinset, k * count k m = m.sum
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.nest.denest ⋯ = p

Tactic:
simp_rw [nest, denest, DyckWord.ext_iff, dropLast_concat]; rfl

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
⊢ (algebraMap 𝕜 𝕝) 1 • 1 = 1

Tactic:
by
      ext; simp only [mul_boole, one_apply, smul_eq_mul, constSMul_apply, map_one]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ ↑n < (f (i + 1) (m + 1) • X ^ ((i + 1) * (m + 1))).order

Tactic:
grw [PowerSeries.smul_eq_C_mul, ← le_order_mul]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ ↑n < (C (f (i + 1) (m + 1))).order + (X ^ ((i + 1) * (m + 1))).order
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
⊢ ↑p <:+: ↑r

Tactic:
· have : [U] ++ r.insidePart ++ [D] ++ r.outsidePart = r :=
        DyckWord.ext_iff.mp (nest_insidePart_add_outsidePart hr)
      grind

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

Goal state before:
pp: case tail
p q b✝ c✝ : DyckWord
a✝ : Relation.ReflTransGen (fun p q ↦ p = q.insidePart ∨ p = q.outsidePart) p b✝
mq : b✝ = c✝.insidePart ∨ b✝ = c✝.outsidePart
ih : p.semilength ≤ b✝.semilength
⊢ p.semilength ≤ c✝.semilength

Tactic:
| tail _ mq ih =>

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
⊢ ∏' (i : ℕ), (1 - X ^ ((i + 1) * m)) = (∏' (i : ℕ), ∑ j ∈ range m, X ^ ((i + 1) * j)) * ∏' (i : ℕ), (1 - X ^ (i + 1))

Tactic:
← (multipliable_powerSeriesMk_card_countRestricted R m).tprod_mul
    (multipliable_one_sub_X_pow _)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
⊢ ∏' (i : ℕ), (1 - X ^ ((i + 1) * m)) = ∏' (b : ℕ), (∑ j ∈ range m, X ^ ((b + 1) * j)) * (1 - X ^ (b + 1))
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs✝ : s ⊇ range d
this :
  ∏ i ∈ s, (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) =
    ∏ i ∈ Finset.map (addRightEmbedding 1) s, (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
p : d.Partition
a✝ : p ∈ ↑univ
⊢ p.toFinsuppAntidiag ∈ ↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d)

Tactic:
exact mem_of_subset (finsuppAntidiag_mono hs _) p.toFinsuppAntidiag_mem_finsuppAntidiag

Goal state after: