mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ 𝒞.χ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow = 𝒞.χ i

Tactic:
refine (𝒞.uniq _ (?_ : IsPullback _ (𝒞.χ₀ _) _ _)).symm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ IsPullback ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
    (𝒞.χ₀ (underlying.obj ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject))) (𝒞.χ i) 𝒞.truth
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ : GrothendieckTopology C
F G : Sheaf J✝ (Type (max u v))
J : GrothendieckTopology C
⊢ Presheaf.IsSheaf J (closedSieves J).toFunctor

Tactic:
rw [CategoryTheory.isSheaf_iff_isSheaf_of_type]
    exact CategoryTheory.classifier_isSheaf J

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
⊢ ∀ {X Y : C} (x : Retract X Y), P.triangEnvelope Y → P.triangEnvelope X

Tactic:
by
    intro X Y r hY
    rw [prop_triangEnvelope_iff] at hY ⊢
    obtain ⟨n, hn⟩ := hY
    exact ⟨n, IsStableUnderRetracts.of_retract r hn⟩

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

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B
hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁
k : (Triangle.mk α β γ).obj₃ ⟶ ι.obj B
hk : x₁ = (Triangle.mk α β γ).mor₂ ≫ k
⊢ ∃ k, πQ f₂ β ≫ k = x₂

Tactic:
exact ⟨ι.preimage k, ι.map_injective (by cat_disch)⟩

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d✝ k N : ℕ
x : Fin n → ℕ
d : ℕ
⊢ ∑ x, 0 = 0

Tactic:
sum_const_zero

Goal state after:
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 B : Set X
⊢ CovBySMul M K A B → 0 ≤ K

Tactic:
rintro ⟨F, hF, -⟩

Goal state after:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A B : Set X
F : Finset M
hF : ↑(#F) ≤ K
⊢ 0 ≤ K
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case refine_1
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)

pp: case refine_2
n d : ℕ
⊢ #(range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))

Tactic:
· rw [mem_range, Nat.lt_succ_iff]
    exact sum_sq_le_of_mem_box hx

Goal state after:
case refine_2
n d : ℕ
⊢ #(range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log (2 ^ ↑6)

Tactic:
log_rpow zero_lt_two,

Goal state after:
N : ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < ↑6 * log 2
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
have hn₂ : 2 < n := three_le_nValue <| hN.trans' <| by norm_num1

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 4 < log (2 ^ ↑6)

Tactic:
log_rpow zero_lt_two,

Goal state after:
⊢ 4 < ↑6 * log 2
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ log (2 ^ ↑12) < 16

Tactic:
log_rpow zero_lt_two,

Goal state after:
⊢ ↑12 * log 2 < 16
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)

Tactic:
have hB' : B ∈ B.powerset.erase ∅ := mem_erase_of_ne_of_mem hB.ne_empty (mem_powerset_self _)

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ (A ^ m)⁻¹ ∩ (B ^ n)⁻¹ = A ^ m ∩ B ^ n

Tactic:
← inv_pow,

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ A⁻¹ ^ m ∩ B⁻¹ ^ n = A ^ m ∩ B ^ n
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#((B ^ m)⁻¹ / (B ^ n)⁻¹)) ≤ (↑(#(A / B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
← inv_pow,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#(B⁻¹ ^ m / (B ^ n)⁻¹)) ≤ (↑(#(A / B)) / ↑(#A)) ^ (m + n) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#(B⁻¹ ^ m / (B ^ n)⁻¹)) ≤ (↑(#(A / B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
← inv_pow,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ ↑(#(B⁻¹ ^ m / B⁻¹ ^ n)) ≤ (↑(#(A / B)) / ↑(#A)) ^ (m + n) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
x : Finset α × Finset α
⊢ mulETransformLeft 1 x = x

Tactic:
by simp [mulETransformLeft]

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

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

Tactic:
smul_inv_smul

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ x.1 * x.2 ⊆ x.1 * x.2
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2

Tactic:
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]

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

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
K : ℝ
m : ℕ
hm : 3 ≤ m
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA : ↑(#(∅ ^ 3)) ≤ K * ↑(#∅)
⊢ ↑(#(List.map (fun i ↦ ∅ ^ ε i) (finRange m)).prod) ≤ K ^ (3 * (m - 2)) * ↑(#∅)

Tactic:
simp [hm₀, hε₀]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
⊢ LeftInverse (Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom)
    (Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom)

Tactic:
rintro ⟨e, h⟩

Goal state after:
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
⊢ Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom (Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom ⟨e, h⟩) =
    ⟨e, h⟩
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
⊢ RightInverse (Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom)
    (Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom)

Tactic:
rintro ⟨e, h⟩

Goal state after:
V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G : SimpleGraph V
G' : SimpleGraph W
u v : V
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
⊢ Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom (Hom.mapEdgeSet (RelIso.toRelEmbedding f.symm).toRelHom ⟨e, h⟩) =
    ⟨e, h⟩
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
⊢ G.incidenceFinset v = {e ∈ G.edgeFinset | v ∈ e}

Tactic:
by
  ext ⟨⟨⟩⟩
  simp [mk'_mem_incidenceSet_iff]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
hc : #p = #s / #P.parts + 1
⊢ #p = #s / #P.parts + 1 ↔
    ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm ⟨p, property✝⟩))) <
      #s % #P.parts

Tactic:
simp [hc]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
hc : ¬#p = #s / #P.parts + 1
⊢ #p = #s / #P.parts + 1 ↔
    ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a ↦ #↑a = #s / #P.parts + 1).symm ⟨p, property✝⟩))) <
      #s % #P.parts

Tactic:
simp [hc]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n : ℤ
inst✝ : t.IsLE X n
i : EInt
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n

Tactic:
by
  induction i using WithBotTop.rec with
  | bot => exact isLE_of_isZero _ (by simp) _
  | coe _ => dsimp; infer_instance
  | top => dsimp; infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ x₁ ∈ x, ∃ x₂ ∈ x, s x₁ x₂
⊢ ⊥ ∉ image (fun a ↦ {b ∈ x | s a b}) x

Tactic:
simpa [filter_eq_empty_iff]

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4

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

Tactic:
· exact log_pos (by simp)

Goal state after:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < 100 / ε ^ 5
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t})
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ id ({i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t})
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R

Tactic:
rw [id, mem_filter] at hz1 hz2

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
⊢ interedges r (s.biUnion f) t = s.biUnion fun a ↦ interedges r (f a) t

Tactic:
ext
  simp only [mem_biUnion, mem_interedges_iff, exists_and_right, ← and_assoc]

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

Goal state before:
pp: case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
· rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]
    apply G.nonuniformWitnesses_spec fun i => h₂ i.symm

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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx :
  x ∈
    {u ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty}.biUnion id \
      (star hP G ε hU V).biUnion id
⊢ x ∈
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id

Tactic:
star,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx :
  x ∈
    {u ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty}.biUnion id \
      {A ∈ (chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}.biUnion id
⊢ x ∈
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case map_rel_iff'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
⊢ ∀ {a b : ↑A'.verts}, (Subgraph.map f.toHom A').Adj (f.toHom ↑a) (f.toHom ↑b) ↔ A'.Adj ↑a ↑b

Tactic:
Subgraph.map_adj,

Goal state after:
case map_rel_iff'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
⊢ ∀ {a b : ↑A'.verts}, Relation.Map A'.Adj (⇑f.toHom) (⇑f.toHom) (f.toHom ↑a) (f.toHom ↑b) ↔ A'.Adj ↑a ↑b
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
hn : ¬G.Adj s t
⊢ G.incidenceFinset t ⊆ G.edgeFinset

Tactic:
simp [incidenceFinset, incidenceSet_subset]

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

Goal state before:
pp: case e_a.e_a
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) = G.degree s

Tactic:
rw [card_image_of_injective, card_neighborFinset_eq_degree]

Goal state after:
case e_a.e_a.H
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hn : ¬G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ Function.Injective fun x ↦ s(x, t)
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
ha : G.Adj s t
⊢ G.incidenceFinset t ⊆ G.edgeFinset

Tactic:
simp [incidenceFinset, incidenceSet_subset]

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

Goal state before:
pp: case e_a.e_a
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ #G.edgeFinset + #(image (fun x ↦ s(x, t)) (G.neighborFinset s)) = #G.edgeFinset + G.degree s

Tactic:
rw [card_image_of_injective, card_neighborFinset_eq_degree]

Goal state after:
case e_a.e_a.H
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
ha : G.Adj s t
inc : G.incidenceFinset t ⊆ G.edgeFinset
⊢ Function.Injective fun x ↦ s(x, t)
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
⊢ G.Adj v w

Tactic:
grind [adj_congr_of_sym2]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ ↑p.support = {u} + ↑p.support.tail

Tactic:
cases p <;> rfl

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

Goal state before:
pp: case zero
V : Type u_1
G : SimpleGraph V
v : V
n k : ℕ
u : V
p : G.Walk u v
⊢ (p.drop (0 + 1)).IsSubwalk (p.drop 0)

Tactic:
exact p.drop_zero ▸ (p.isSubwalk_rfl.copy rfl rfl p.getVert_zero.symm rfl).tail

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

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

Tactic:
← takeUntil_append_of_mem_left _ (p.dropUntil w hw) hx,

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).tail = p.copy ⋯ ⋯

Tactic:
cases p <;> rfl

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

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

Tactic:
simp only [ht, true_or, iff_true]
    exact IsClique.of_subsingleton <| card_le_one.1 ht

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : G.Walk u v
f : G →g G'
h : (Walk.map f p).IsPath
⊢ Set.InjOn ⇑f {w | w ∈ p.support}

Tactic:
intro u

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ v : V
p : G.Walk u✝ v
f : G →g G'
h : (Walk.map f p).IsPath
u : V
⊢ u ∈ {w | w ∈ p.support} → ∀ ⦃x₂ : V⦄, x₂ ∈ {w | w ∈ p.support} → f u = f x₂ → u = x₂
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
n : ℕ
h : 2 ≤ n
⊢ ⊥.CliqueFree n

Tactic:
intro t ht

Goal state after:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : ⊥.IsNClique n t
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
n : ℕ
h : 2 ≤ n
⊢ ⊥.CliqueFree n

Tactic:
by
  intro t ht
  have := le_trans h (isNClique_bot_iff.1 ht).1
  contradiction

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

Goal state before:
pp: n : ℕ
ι : Type u_3
inst✝ : Fintype ι
V : ι → Type u_4
hc : Fintype.card ι < n
f : (completeGraph (Fin n)).Copy (completeMultipartiteGraph V)
⊢ Fintype.card ι < Fintype.card (Fin n)

Tactic:
simp [hc]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 2
a b : α
hab : G.Adj a b
⊢ G.IsClique ↑{a, b}

Tactic:
simpa [hab.ne]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
x✝ : a ≠ b
hab : G.Adj a b
⊢ G.IsClique ↑{a, b}

Tactic:
simpa [hab.ne]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
⊢ Gᶜ.IsMaximumClique s ↔ G.IsMaximumIndepSet s

Tactic:
by
  simp [isMaximumIndepSet_iff, isMaximumClique_iff]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
⊢ Gᶜ.IsMaximumIndepSet s ↔ G.IsMaximumClique s

Tactic:
by
  simp [isMaximumIndepSet_iff, isMaximumClique_iff]

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

Goal state before:
pp: ε : ℝ
hε₁ : ε ≤ 1
⊢ triangleRemovalBound ε ≤ (1 - ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3

Tactic:
by
  simp [triangleRemovalBound, hε₁]

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

Goal state before:
pp: case right
α : 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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B)) ≤
    ε ^ 5 / 50

Tactic:
sub_le_iff_le_add,

Goal state after:
case right
α : 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
⊢ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ε ^ 5 / 50 + (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑(#A) * ↑(#B))