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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ s.Pairwise fun v w ↦ ¬G.Adj v w

Tactic:
Set.Pairwise

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y

Tactic:
Set.Pairwise

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w ↦ ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj

Tactic:
Set.Pairwise

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ s.Pairwise G.Adj
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ s.Pairwise G.Adj

Tactic:
Set.Pairwise

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → G.Adj x y

Tactic:
Set.Pairwise

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ¬(G.neighborSet v).Pairwise fun v w ↦ ¬G.Adj v w
⊢ False

Tactic:
Set.Pairwise

Goal state after:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ¬∀ ⦃x : α⦄, x ∈ G.neighborSet v → ∀ ⦃y : α⦄, y ∈ G.neighborSet v → x ≠ y → ¬G.Adj x y
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
H : SimpleGraph α
inst✝ : DecidableRel H.Adj
hG : H ≤ G
hH : H.CliqueFree 3
⊢ ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
rw [← Nat.cast_sub (card_le_card <| edgeFinset_mono hG)]

Goal state after:
α : Type u_1
𝕜 : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
H : SimpleGraph α
inst✝ : DecidableRel H.Adj
hG : H ≤ G
hH : H.CliqueFree 3
⊢ ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset - #H.edgeFinset)
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε / 9 * ↑((Fintype.card G + Fintype.card G + Fintype.card G) ^ 2) ≤ ↑(#(triangleIndices A))

Tactic:
simp_rw [card_triangleIndices, mul_comm_div, Nat.cast_pow, Nat.cast_add]

Goal state after:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * ((↑(Fintype.card G) + ↑(Fintype.card G) + ↑(Fintype.card G)) ^ 2 / 9) ≤ ↑(#A)
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
⊢ ε ≤ 1

Tactic:
have := hAε.trans (Nat.cast_le.2 A.card_le_univ)

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : ⌊(triangleRemovalBound (ε / 9) * 27)⁻¹⌋₊ < Fintype.card G
A : Finset (G × G)
hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
hA : IsCornerFree ↑A
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(Fintype.card (G × G))
⊢ ε ≤ 1
Module: Mathlib.Combinatorics.Additive.Energy

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : f (a₁, b₁, c₁) = f (a₂, b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)

Tactic:
simp_rw [f, Prod.ext_iff] at h

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∑ a, (∏ j, x₀ j ^ d ↑j) * a ^ d i = (∏ j, x₀ j ^ d ↑j) * ∑ a, a ^ d i

Tactic:
mul_sum

Goal state after:
K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∑ a, (∏ j, x₀ j ^ d ↑j) * a ^ d i = ∑ i_1, (∏ j, x₀ j ^ d ↑j) * i_1 ^ d i
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_3
α : 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
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
this :
  ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V) * #(star hP G ε hV U)) / ↑(4 * 4) ^ #P.parts * ((3 / 4) ^ 2 * ε ^ 2) ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity x.1 x.2) ^ 2) / ↑(4 * 4) ^ #P.parts
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts

Tactic:
div_pow,

Goal state after:
case refine_3
α : 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
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
this :
  ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V) * #(star hP G ε hV U)) / ↑(4 * 4) ^ #P.parts * (3 ^ 2 / 4 ^ 2 * ε ^ 2) ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity x.1 x.2) ^ 2) / ↑(4 * 4) ^ #P.parts
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : toColex s ≤ toColex t
ht : ∀ b ∈ t, b ≤ a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b ≤ a

Tactic:
· obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›
    exact hbc.trans <| ht _ hct

Goal state after:
Module: Mathlib.Combinatorics.Colex

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

Tactic:
by
  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.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: case inr.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
w : ℙ F (Fin 3 → F)
v : Fin 3 → F
hv : v ≠ 0
h : mk F v hv ≠ w
⊢ (mk F v hv).cross w = w.cross (mk F v hv)

Tactic:
induction w with | h w hw =>
    rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero,
      ← cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ∀ (a : ↑(Equiv.RemoveNone.fiber none)), False
⊢ (a : α) × ↑(Equiv.RemoveNone.fiber (some a)) ≃ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}}

Tactic:
by
      simp_rw [Equiv.RemoveNone.fiber_some]
      rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
this : (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)
⊢ ((φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) / ↑(#S))⁻¹ = (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
by
        have : (#S : ℝ) ≠ 0 := by positivity
        simp [this]

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 𝕜 𝕝
c d : 𝕜
⊢ (algebraMap 𝕜 𝕝) (c * d) • 1 = (algebraMap 𝕜 𝕝) c • 1 * (algebraMap 𝕜 𝕝) d • 1

Tactic:
ext a b
        obtain rfl | h := eq_or_ne a b
        · simp only [one_apply, smul_eq_mul, mul_apply, constSMul_apply, map_mul,
            eq_comm, Icc_self]
          simp
        · simp only [one_apply, mul_one, smul_eq_mul, mul_apply, zero_mul,
            constSMul_apply, ← ite_and, ite_mul, mul_ite, map_mul, mul_zero, if_neg h]
          refine (sum_eq_zero fun x _ ↦ ?_).symm
          exact if_neg fun hx ↦ h <| hx.2.trans hx.1

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ IncidenceAlgebra.prod 1 1 = 1

Tactic:
ext x y; simp [Prod.ext_iff, ← ite_and, and_comm]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝¹⁰ : Ring 𝕜
inst✝⁹ : PartialOrder α
inst✝⁸ : PartialOrder β
inst✝⁷ : LocallyFiniteOrder α
inst✝⁶ : LocallyFiniteOrder β
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : DecidableLE α
inst✝² : DecidableLE β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
⊢ eulerChar 𝕜 (α × β) = eulerChar 𝕜 α * eulerChar 𝕜 β

Tactic:
by simp [eulerChar, ← mu_prod_mu]

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
this : (↑i + 1) * m - 1 + 1 = (↑i + 1) * m
⊢ (if m ∣ (↑i + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑i + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑i + 1)) ^ m

Tactic:
simp [this, pow_mul]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
⊢ HasSum (fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))) (pentagonalSeries R)

Tactic:
by
  have h := hasSum_pentagonalSeries R
  rw [← neg_injective.hasSum_iff (fun x hx ↦ by absurd hx; use -x; simp)] at h
  convert h.nat_add_neg_add_one using 2 with k
  simp_rw [Function.comp_apply, neg_neg, Int.negOnePow_add]
  simp
  ring

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

Goal state before:
pp: n : ℕ
α : Type := Fin (2 * n + 1)
this : Coprime 2 (2 * n + 1)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
have : Fact (IsUnit (2 : Fin (2 * n + 1))) := ⟨by simpa
    using! (ZMod.unitOfCoprime 2 this).isUnit⟩

Goal state after:
n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case calc_2
n : ℕ
⊢ (2 * (n / 6) + 1) * rothNumberNat (n / 6) ≤ ruzsaSzemerediNumberNat (6 * (n / 6) + 3)

Tactic:
exact rothNumberNat_le_ruzsaSzemerediNumberNat _

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
v : α
e : β
f : α → α'
h : G.Inc e v
⊢ (map f G).Inc e (f v)

Tactic:
by
  obtain ⟨w, hw⟩ := h
  exact ⟨f w, hw.map f⟩

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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_const_mul : ∀ (r : M), Continuous fun x ↦ x * r
S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ ∀ t ∈ c, m * m' ∈ t

Tactic:
exact fun t ht => (hcs ht).2.2 m (Set.mem_sInter.mp hm t ht) m' (Set.mem_sInter.mp hm' t ht)

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_5
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : U ∈ S
U_idem : U * U = U
⊢ ∀ᶠ (m : M) in ↑U, m ∈ FP a

Tactic:
convert! Set.mem_iInter.mp hU 0

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case refine_2.htcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋯
⊢ ∀ (i : ℕ), IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}

Tactic:
· intro n
      apply ultrafilter_isClosed_basic

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
⊢ Function.RightInverse (fun n ↦ ⟨(Equiv.symm ↑f) ⟨↑n + #s, ⋯⟩, ⋯⟩) fun x ↦ ⟨↑(↑f ↑x) - #s, ⋯⟩

Tactic:
rintro ⟨n, hn⟩; simp

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hsn : #s ≤ ↑n
⊢ (fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s))
      ((fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩)) n) =
    n

Tactic:
simp [hsn.not_gt, hsn, mem_compl.1 <| Subtype.prop _]

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

Goal state before:
pp: case h
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ I ⊆ univ.sigma Js ∧
    ((∀ (i : ι), (M i).Indep (Js i)) ∧ univ.sigma Js ⊆ X) ∧
      ∀ ⦃t : Set ((i : ι) × α i)⦄,
        (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → univ.sigma Js ⊆ t → t ⊆ univ.sigma Js

Tactic:
refine ⟨?_, ⟨fun i ↦ (hJs i).1.indep, ?_⟩, fun S hS hSX hJS ↦ ?_⟩

Goal state after:
case h.refine_1
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ I ⊆ univ.sigma Js

case h.refine_2
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ univ.sigma Js ⊆ X

case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ S ⊆ univ.sigma Js
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B : Set ((i : ι) × α i)
hB : ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)
⊢ B ⊆ univ.sigma fun i ↦ (M i).E

Tactic:
rw [← univ_sigma_preimage_mk B]
    apply sigma_mono Subset.rfl fun i ↦ (hB i).subset_ground

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

Goal state before:
pp: α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R D B X Y Z K C C₁ C₂ : Set α
inst✝ : M.Finitary
J : Set α
hJ : M.IsBasis' J C
this : (M ／ J).Finitary
⊢ (M ／ C).Finitary

Tactic:
rw [hJ.contract_eq_contract_delete]
    infer_instance

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : ∀ (x : PEmpty.{u_2 + 1} → R), (∀ (i : PEmpty.{u_2 + 1}), x i ∈ S i) → (eval x) P = 0
this : P = C (constantCoeff P)
⊢ P = 0

Tactic:
by
      specialize Heval default (fun i ↦ PEmpty.elim i)
      rw [this, eval_C] at Heval
      rw [this, Heval, C_0]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C D : Set α
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)

Tactic:
by
  rw [delete_eq_delete_iff, contract_ground, sdiff_eq, sdiff_eq, ← inter_inter_distrib_right,
    inter_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case inl
D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
hab : a ≠ b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
⊢ r 0 ≠ r 1

Tactic:
ha0,

Goal state after:
case inl
D : Type u_1
C : Type u_3
inst✝ : PartialOrder C
f : (Fin 2 → D) → C
a b : D
mcf : HasMaxCutPropertyAt f a b
ω : FractionalOperation D 2
symmega : ω.IsSymmetric
r : Fin 2 → D
hab : r 0 ≠ b
rin : ∃ a_1 ∈ ω, (fun i ↦ a_1 (swap ![![a, b], ![b, a]] i)) = r
equ : f ![a, b] = f ![r 0, r 1]
ha0 : a = r 0
hb1 : b = r 1
⊢ r 0 ≠ r 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ {a ∈ Ioo 0 k | a ∈ A} ⊆ Ioo 0 k

Tactic:
exact filter_subset _ _

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case h
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x % m = 1
⊢ x = 1

Tactic:
rcases eq_or_lt_of_le hxm with rfl | hxm'

Goal state after:
case h.inl
x : ℕ
a✝ : 0 < x
hm : x ≠ 1
hm' : x > 0
hxm : x ≤ x
h : x % x = 1
⊢ x = 1

case h.inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x % m = 1
hxm' : x < m
⊢ x = 1
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t₁ t₂ : Finset α
⊢ s ○ (t₁ ∩ t₂) ⊆ s ○ t₁ ∩ s ○ t₂

Tactic:
simpa only [disjSups, product_inter, filter_inter_distrib] using image_inter_subset _ _ _

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ InfIrred (Ici a)

Tactic:
by
  refine ⟨fun h ↦ Ici_ne_top h.eq_top, fun s t hst ↦ ?_⟩
  have := mem_Ici_iff.2 (le_refl a)
  rw [← hst] at this
  exact this.imp (fun ha ↦ le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_left) fun ha ↦
      le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_right

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ ⋯.choose ∧ 2 * #⋯.choose = Fintype.card (Finset α) ∧ (↑⋯.choose).Intersecting

Tactic:
exact Classical.choose_spec (hf j hj).exists_card_eq

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
inst✝ : Finite α
val✝ : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ s ∈ {∅}

Tactic:
by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs

Goal state after: