mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f s).card = n

Tactic:
card_map

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ s.card = n
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f t).card = n

Tactic:
card_map

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ t.card = n
Module: Mathlib.Combinatorics.Additive.CovBySMul

Goal state before:
pp: M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A₁ A₂ B : Set X
hA : A₁ ⊆ A₂
hAB : CovBySMul M K A₂ B
⊢ CovBySMul M K A₁ B

Tactic:
by simpa using (CovBySMul.of_subset (M := M) hA).trans hAB

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2

Tactic:
refine inter_mul_union_subset_union.trans (union_subset Subset.rfl ?_)
  rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]

Goal state after:
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ ↑(Nat.card ↥(zmultiples ↑(n / n.minFac))) ≤ ↑n.minFac

Tactic:
Nat.card_zmultiples,

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this✝ : Fact (1 < n)
this : ↑(n / n.minFac) ≠ 0
⊢ ↑(addOrderOf ↑(n / n.minFac)) ≤ ↑n.minFac
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
⊢ ↑(#A) * ↑(#(A * A⁻¹ * A)) ≤ ↑(#(A * (A * A⁻¹))) * ↑(#(A * A))

Tactic:
by
      norm_cast; simpa using ruzsa_triangle_inequality_invMul_mul_mul (A * A⁻¹) A A

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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
ε : ℤ
hε : |ε| = 1
⊢ A ^ ε = A

Tactic:
obtain rfl | rfl := eq_or_eq_neg_of_abs_eq hε

Goal state after:
case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
hε : |1| = 1
⊢ A ^ 1 = A

case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
hε : |(-1)| = 1
⊢ A ^ (-1) = A
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ #(induce s G).edgeFinset = #(map (Embedding.subtype fun x ↦ x ∈ s).sym2Map (induce s G).edgeFinset)

Tactic:
card_map

Goal state after:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ #(induce s G).edgeFinset = #(induce s G).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v : ↑s
h : G.neighborSet ↑v ⊆ s
⊢ #((induce s G).neighborFinset v) = #(map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v))

Tactic:
card_map

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
⊢ b ∈ P.parts

Tactic:
· obtain ⟨c, hc, hbc⟩ := hQP hb
        obtain ⟨d, hd, hcd⟩ := hPQ hc
        rwa [hbc.antisymm]
        rwa [Q.disjoint.eq_of_le hb hd (Q.ne_bot hb) (hbc.trans hcd)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
hucard : #u ≠ m * 4 ^ #P.parts + a
⊢ (4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u

Tactic:
by
  have : m * 4 ^ #P.parts ≤ card α / #P.parts := by
    rw [stepBound, ← Nat.div_div_eq_div_mul]
    exact Nat.div_mul_le_self _ _
  rw [Nat.add_sub_of_le this] at hucard
  rw [(hP.card_parts_eq_average hu).resolve_left hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
    Nat.sub_add_cancel a_add_one_le_four_pow_parts_card, ← add_assoc, mul_comm,
    Nat.add_sub_of_le this, card_univ]

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

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

Tactic:
← rpow_natCast 4,

Goal state after:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 100 < 4 ^ ↑(initialBound ε l) * ε ^ 5
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
m_pos : m > 0
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b

Tactic:
induction s using Finset.strongInduction generalizing a b with | H s ih => _

Goal state after:
case inr.H
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case a.calc_2
α : 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 * #P.parts - #P.parts) * (#A / #P.parts + 1) ^ 2 ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2

Tactic:
Nat.mul_sub_right_distrib,

Goal state after:
case a.calc_2
α : 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 * #P.parts * (#A / #P.parts + 1) ^ 2 - #P.parts * (#A / #P.parts + 1) ^ 2 ≤
    (#P.parts * (#A / #P.parts) + #P.parts) ^ 2
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
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)

Tactic:
Nat.mul_sub_right_distrib,

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : #U * #U - 1 * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
⊢ G.maxDegree ≤ (induce s G).maxDegree

Tactic:
refine G.maxDegree_le_of_forall_degree_le _ fun v ↦ ?_

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
s : Set V
inst✝ : DecidablePred fun x ↦ x ∈ s
h : G.support ⊆ s
v : V
⊢ G.degree v ≤ (induce s G).maxDegree
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
⊢ e ∈ G.edgeFinset \ G.incidenceFinset t → ∀ b ∈ image (fun x ↦ s(x, t)) (G.neighborFinset s), e ≠ b

Tactic:
he

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
he : e ∈ G.edgeFinset \ G.incidenceFinset t
⊢ ∀ b ∈ image (fun x ↦ s(x, t)) (G.neighborFinset s), e ≠ b
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
hi : 0 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert 0) ((cons hxy p✝).getVert (0 + 1))

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert (n✝ + 1)) ((cons hxy p✝).getVert (n✝ + 1 + 1))

Tactic:
· simp [getVert, hxy]

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < p✝.length → G.Adj (p✝.getVert i) (p✝.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy p✝).length
⊢ G.Adj ((cons hxy p✝).getVert (n✝ + 1)) ((cons hxy p✝).getVert (n✝ + 1 + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
u v : V
⊢ (G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v

Tactic:
by
  simp [and_assoc]

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

Goal state before:
pp: case refine_2.refine_1
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂.getVert s.length = v

Tactic:
simp [p₂.getVert_eq_support_getElem (by lia : s.length ≤ p₂.length), ← h,
        List.getElem_zero]

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : k ≤ p.length
⊢ p.support[k]? = q.support[k]?

Tactic:
rw [← getVert_eq_support_getElem? p hk, ← getVert_eq_support_getElem? q (hl ▸ hk)]

Goal state after:
case inl
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hl : p.length = q.length
h : ∀ k ≤ p.length, p.getVert k = q.getVert k
k : ℕ
hk : k ≤ p.length
⊢ some (p.getVert k) = some (q.getVert k)
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_3
G : SimpleGraph α
h : BddAbove {n | ∃ s, G.IsNClique n s}
⊢ ∃ s, G.IsNClique G.cliqueNum s

pp: case neg
α : Type u_3
G : SimpleGraph α
h : ¬BddAbove {n | ∃ s, G.IsNClique n s}
⊢ ∃ s, G.IsNClique G.cliqueNum s

Tactic:
· exact Nat.sSup_mem ⟨0, by simp⟩ h

Goal state after:
case neg
α : Type u_3
G : SimpleGraph α
h : ¬BddAbove {n | ∃ s, G.IsNClique n s}
⊢ ∃ s, G.IsNClique G.cliqueNum s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
n : ℕ
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α ↪ β
hn : n ≠ 1
⊢ (SimpleGraph.map (⇑f) G).cliqueSet n = ↑(map { toFun := map f, inj' := ⋯ } (G.cliqueFinset n))

Tactic:
cliqueSet_map hn,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
n : ℕ
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α ↪ β
hn : n ≠ 1
⊢ map f '' G.cliqueSet n = ↑(map { toFun := map f, inj' := ⋯ } (G.cliqueFinset n))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
⊢ 0 ≤ 1 - 2 * (ε / 8)

Tactic:
have : ε / 4 ≤ 1 := ‹ε / 4 ≤ _›.trans (by exact mod_cast G.edgeDensity_le_one _ _)

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
x y z : α
s : Finset α
hX : s ∈ P.parts
Y : Finset α
hY : Y ∈ P.parts
xX : x ∈ s
yY : y ∈ Y
nXY : s ≠ Y
uXY : G.IsUniform (ε / 8) s Y
dXY✝ : ε / 4 ≤ ↑(G.edgeDensity s Y)
Z : Finset α
hZ : Z ∈ P.parts
zZ : z ∈ Z
hX' : s ∈ P.parts
xX' : x ∈ s
nXZ : s ≠ Z
uXZ : G.IsUniform (ε / 8) s Z
dXZ✝ : ε / 4 ≤ ↑(G.edgeDensity s Z)
hY' : Y ∈ P.parts
yY' : y ∈ Y
hZ' : Z ∈ P.parts
zZ' : z ∈ Z
nYZ : Y ≠ Z
uYZ : G.IsUniform (ε / 8) Y Z
dYZ✝ : ε / 4 ≤ ↑(G.edgeDensity Y Z)
dXY : Function.onFun Disjoint id s Y
dXZ : Function.onFun Disjoint id s Z
dYZ : Function.onFun Disjoint id Y Z
that : 2 * (ε / 8) = ε / 4
this : ε / 4 ≤ 1
⊢ 0 ≤ 1 - 2 * (ε / 8)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
hx : x ∈ t
⊢ (graph t).IsNClique 3 (toTriangle x)

Tactic:
simp only [toTriangle_apply, is3Clique_triple_iff, in₀₁_iff, in₀₂_iff, in₁₂_iff]
  exact ⟨⟨_, hx⟩, ⟨_, hx⟩, _, hx⟩

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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 3 / 4 * ε ≤
    |(∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
          (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U))) -
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts|

Tactic:
rw [show (16 : ℝ) = ↑4 ^ 2 by norm_num, pow_right_comm, sq ((4 : ℝ) ^ _)]

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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 3 / 4 * ε ≤
    |(∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) /
          (↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U))) -
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) /
          (4 ^ #P.parts * 4 ^ #P.parts)|
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
⊢ triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
by
  cases isEmpty_or_nonempty α
  · simp [Fintype.card_eq_zero]
  obtain hε | hε := le_or_gt ε 0
  · apply (mul_nonpos_of_nonpos_of_nonneg (triangleRemovalBound_nonpos hε) _).trans <;> positivity
  let l : ℕ := ⌈4 / ε⌉₊
  have hl : 4 / ε ≤ l := le_ceil (4 / ε)
  rcases le_total (card α) l with hl' | hl'
  · calc
      _ ≤ triangleRemovalBound ε * ↑l ^ 3 := by
        gcongr; exact (triangleRemovalBound_pos hε).le
      _ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
      _ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'
  obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G (by positivity : 0 < ε / 8) hl'
  have : 4 / ε ≤ #P.parts := hl.trans (cast_le.2 hP₂)
  have k := regularityReduced_edges_card_aux hε hP₁ hP₄ this
  rw [mul_assoc] at k
  replace k := lt_of_mul_lt_mul_left k zero_le_two
  obtain ⟨t, ht⟩ := hG.cliqueFinset_nonempty' regularityReduced_le k
  exact triangle_removal_aux hε hG.lt_one.le hP₁ hP₃ ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ #(map toTriangle t) = #t

Tactic:
card_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ #t = #t
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ Eₘ[s, t] = ∑ a, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = a}) ^ 2

Tactic:
rw [mulEnergy_eq_sum_sq']

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Mul α
inst✝ : Fintype α
s t : Finset α
⊢ ∑ a ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = a}) ^ 2 = ∑ a, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = a}) ^ 2
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #u * ∑ c ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 = #u * Eₘ[s, t]

Tactic:
rw [mulEnergy_eq_sum_sq']

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

Goal state before:
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

Tactic:
card_map

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
⊢ #{a_1 | ↑x a_1 ≠ 0} = p
Module: Mathlib.Combinatorics.Additive.SubsetSum

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

Tactic:
induction A using induction_on_max with

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s ≤ toColex t ∧ toColex s ≠ toColex t ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
toColex_le_toColex_iff_max'_mem

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t) ∧ toColex s ≠ toColex t ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
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
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
v : { v // v ≠ 0 }
c : f ↑v = 0
⊢ f ↑v = f 0

Tactic:
simp [c]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f ↔ fixedPoints ⇑f = ∅

Tactic:
· rw [Set.eq_empty_iff_forall_notMem]
        exact ⟨fun h x hx => h.2 (h.1 hx ▸ hx), fun h => ⟨fun x hx => (h _ hx).elim, h _⟩⟩

Goal state after:
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 : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
⊢ ↑(#(c⁻¹ •> A ∩ d •> A)) ≤ ↑(#(A ∩ (c * d) •> A))

Tactic:
← card_smul_finset c

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))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
⊢ ↑(#(c •> (c⁻¹ •> A ∩ d •> A))) ≤ ↑(#(A ∩ (c * d) •> A))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
⊢ (↑p).getLast h = D

Tactic:
by_contra f; have s := p.count_U_eq_count_D
  rw [← dropLast_append_getLast h, (dichotomy _).resolve_right f] at s
  simp_rw [dropLast_eq_take, count_append, count_singleton', ite_true, reduceCtorEq, ite_false] at s
  have := p.count_D_le_count_U (p.toList.length - 1); lia

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

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D ([U] ++ List.take (i - [U].length) ↑p) < count U ([U] ++ List.take (i - [U].length) ↑p)

Tactic:
length_singleton,

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D ([U] ++ List.take (i - 1) ↑p) < count U ([U] ++ List.take (i - 1) ↑p)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ ([U] ++ ↑p ++ [D]).dropLast.tail = ↑p

Tactic:
dropLast_concat

Goal state after:
p : DyckWord
⊢ ([U] ++ ↑p).tail = ↑p
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ ((p.take (p.firstReturn + 1) ⋯).denest ⋯).nest + p.drop (p.firstReturn + 1) ⋯ = p

Tactic:
nest_denest,

Goal state after:
p : DyckWord
h : p ≠ 0
⊢ p.take (p.firstReturn + 1) ⋯ + p.drop (p.firstReturn + 1) ⋯ = p