mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x✝ : F.obj (Opposite.op X)
Z✝ : C
R✝ : Presieve Z✝
hR : R✝ ∈ K.coverings Z✝
y✝ : Presieve.FamilyOfElements F R✝
hy : y✝.Compatible
hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), K.SubsheafClosure 𝒮 W (y✝ r hr)
t✝ : F.obj (Opposite.op Z✝)
ht : y✝.IsAmalgamation t✝
x : ⦃W : C⦄ → (r : W ⟶ Z✝) → R✝ r → Witness K ι W
hx : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), Witness.eval hF ι t (x r hr) = some (y✝ r hr)
⊢ Witness.eval hF ι t (Witness.amalgamate hR x) = some t✝

Tactic:
simp [Witness.eval, hx]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
x✝ : F.obj (Opposite.op X)
Z✝ : C
R✝ : Presieve Z✝
hR : R✝ ∈ K.coverings Z✝
y✝ : Presieve.FamilyOfElements F R✝
hy : y✝.Compatible
hmem : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), K.SubsheafClosure 𝒮 W (y✝ r hr)
t✝ : F.obj (Opposite.op Z✝)
ht : y✝.IsAmalgamation t✝
x : ⦃W : C⦄ → (r : W ⟶ Z✝) → R✝ r → Witness K ι W
hx : ∀ ⦃W : C⦄ (r : W ⟶ Z✝) (hr : R✝ r), Witness.eval hF ι t (x r hr) = some (y✝ r hr)
⊢ ∃ (h : Presieve.FamilyOfElements.Compatible fun x x_1 hr ↦ y✝ x_1 hr), ⋯.choose = t✝
Module: Mathlib.CategoryTheory.Sites.PreservesLimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
K : Type u_1
inst✝ : Category.{v_1, u_1} K
F : K ⥤ C
⊢ PreservesLimit F J.yoneda

Tactic:
have : PreservesLimitsOfShape K (J.yoneda ⋙ sheafToPresheaf J (Type v)) :=
      preservesLimitsOfShape_of_natIso (yonedaCompSheafToPresheaf J).symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
K : Type u_1
inst✝ : Category.{v_1, u_1} K
F : K ⥤ C
this : PreservesLimitsOfShape K (J.yoneda ⋙ sheafToPresheaf J (Type v))
⊢ PreservesLimit F J.yoneda
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Sheaf typesGrothendieckTopology (Type u)
⊢ { hom := (equivYoneda S.obj ⋯).hom } ≫ { hom := (equivYoneda S.obj ⋯).inv } = 𝟙 S

Tactic:
ext1; apply (equivYoneda S.1 S.2).hom_inv_id

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
F G : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ F.obj U✝ ⊔ G.obj U✝ ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (F.obj V✝ ⊔ G.obj V✝)

Tactic:
by grw [F.map i, G.map i, (Submonoid.monotone_comap).le_map_sup]

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 Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ (P.shiftClosure ℤ).binaryProductsClosure ≤ Q

Tactic:
binaryProductsClosure_le_iff,

Goal state after:
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 Q : ObjectProperty C
inst✝¹ : Q.IsStableUnderRetracts
inst✝ : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ P.shiftClosure ℤ ≤ Q
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
        (commShiftIso F n).inv.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
          (commShiftIso F n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
            (shiftFunctor D n).map ((commShiftIso F.op n).inv.app X).unop ≫
              ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((commShiftIso F.op n).hom.app X).unop ≫
        (shiftFunctor D n).map ((commShiftIso F.op n).inv.app X).unop ≫
          ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app ((shiftFunctor C n).obj (unop X))).op ≫
        ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X))).op ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op =
    (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop (op ((shiftFunctor C n).obj (unop X))))).op ≫
        (shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop (op ((shiftFunctor C n).obj (unop X)))))) ≫
          (shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj ((shiftFunctor C n).obj (unop X)))) ≫
            ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X)).op.unop).op ≫
              ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app ((shiftFunctor C n).obj (unop X))).op ≫
        ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X))).op ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op =
    (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop (op ((shiftFunctor C n).obj (unop X))))).op ≫
        ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X)).op.unop).op ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
b : E
hb : b ∈ frontier s
⊢ ∀ ⦃c : E⦄, c ∈ frontier s → a + c = b + b → a = b

Tactic:
c

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
b : E
hb : b ∈ frontier s
c : E
⊢ c ∈ frontier s → a + c = b + b → a = b
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber (map (mulRightEmbedding a) s) = mulRothNumber s

Tactic:
← mulLeftEmbedding_eq_mulRightEmbedding,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber (map (mulLeftEmbedding a) s) = mulRothNumber s
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
⊢ Set.InjOn ⇑(map d) {x | ∀ (i : Fin n), x i < d}

Tactic:
intro x₁ hx₁ x₂ hx₂ h
  induction n with
  | zero => simp [eq_iff_true_of_subsingleton]
  | succ n ih =>
    ext i
    have x := (map_eq_iff hx₁ hx₂).1 h
    exact Fin.cases x.1 (congr_fun <| ih (fun _ => hx₁ _) (fun _ => hx₂ _) x.2) i

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

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ addRothNumber (Iio k) ≤ rothNumberNat ↑k

Tactic:
suffices h : Set.BijOn (Nat.cast : ℕ → Fin n.succ) (range k) (Iio k : Finset (Fin n.succ)) by
    exact (AddHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h
  refine ⟨?_, (CharP.natCast_injOn_Iio _ n.succ).mono (by simp), ?_⟩
  · simpa using! fun x ↦ natCast_strictMono (is_le k)
  simp only [Set.SurjOn, coe_Iio, Set.subset_def, Set.mem_Iio, Set.mem_image, lt_def, coe_range]
  exact fun x hx ↦ ⟨x, hx, by simp⟩

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

Goal state before:
pp: N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑N

Tactic:
exact (cast_le.2 hN).trans' (by norm_num1)

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

Goal state before:
pp: case refine_1.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ ↑B
⊢ (fun b ↦ (a / b, c / b)) b ∈
    bipartiteAbove
      (fun b x ↦
        match x with
        | (a, c) => a / c = b)
      ((A / B) ×ˢ (C / B)) (a / c)

Tactic:
mem_bipartiteAbove

Goal state after:
case refine_1.refine_1
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
a : G
ha : a ∈ A
c : G
hc : c ∈ C
hx : a / c ∈ A / C
b : G
hb : b ∈ ↑B
⊢ (fun b ↦ (a / b, c / b)) b ∈ (A / B) ×ˢ (C / B) ∧
    match (fun b ↦ (a / b, c / b)) b with
    | (a_1, c_1) => a_1 / c_1 = a / c
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
⊢ (↑s).EquitableOn f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
Set.equitableOn_iff_exists_le_le_add_one

Goal state after:
α : Type u_1
s : Finset α
f : α → ℕ
⊢ (∃ b, ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1) ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset ≠ ∅ ↔ G ≠ ⊥

Tactic:
edgeFinset_eq_empty.ne

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G ≠ ⊥ ↔ G ≠ ⊥
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
⊢ map (Embedding.subtype fun x ↦ x ∈ s) ((induce s G).neighborFinset v) = G.neighborFinset ↑v

Tactic:
classical
  rwa [← Set.toFinset_subset_toFinset, ← neighborFinset_def, ← inter_eq_left,
    ← map_neighborFinset_induce v] at h

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : u ⊆ Finset.map (↑e).toEmbedding P.parts
x✝¹ : β
hb : x✝¹ ∈ Finset.map (↑e).toEmbedding P.parts
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
⊢ x✝ ≤ ⊥

Tactic:
rw [← map_symm_subset] at hu
    simp only [mem_map_equiv] at hb
    have := P.supIndep hu hb (by simp [hbu]) (map_rel e.symm hx) ?_
    · rw [← e.symm.map_bot] at this
      exact e.symm.map_rel_iff.mp this
    · convert! e.symm.map_rel_iff.mpr hxu
      rw [map_finset_sup, sup_map]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝¹ : Lattice (Subtype Pr) := Subtype.lattice Prsup Prinf
this✝ : OrderBot (Subtype Pr) := Subtype.orderBot Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ∀ ⦃x y : α⦄, Pr x → Pr y → Pr (x ⊔ y)

Tactic:
exact Prsup

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
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι j).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)

Tactic:
dsimp [eTruncLTι]
  rw [show homOfLE le_top = f ≫ homOfLE le_top by rfl]
  induction j using WithBotTop.rec with simp [truncLT_map_truncLTι_app]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
hr : b \ a = ⊥
⊢ P.parts ⊆ (⋯ ▸ P).parts

Tactic:
cases le_antisymm (sdiff_eq_bot_iff.mp hr) hab

Goal state after:
case pos.refl
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a : α
P : Finpartition a
hab : a ≤ a
hr : a \ a = ⊥
⊢ P.parts ⊆ (⋯ ▸ P).parts
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
a : ↥s
c : #↑(f a).fst = #s / #P.parts
⊢ z a < #P.parts * (↑(f a).snd + 1)

Tactic:
simp only [z, mul_add_one]; gcongr; exact gl a

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ (atomise s F).parts → x ⊆ t → ∀ x_1 ∈ x, ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x

Tactic:
mem_atomise,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    (x.Nonempty ∧ ∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = x) →
      x ⊆ t → ∀ x_1 ∈ x, ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ #(interedges r s t) + #(interedges (fun x y ↦ ¬r x y) s t) = #s * #t

Tactic:
by
  classical
  rw [← card_product, interedges, interedges, ← card_union_of_disjoint, filter_union_filter_not_eq]
  exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

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
inst✝ : IsTriangulated C
a b : EInt
⊢ IsIso (t.eTruncLTGELTSelfToLTGE a b)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]
  intro X
  induction b using WithBotTop.rec with
  | bot => simp [isIsoZero_iff_source_target_isZero]
  | coe b =>
    induction a using WithBotTop.rec with
    | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X)))
    | coe a =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
      constructor
      all_goals exact Functor.map_isZero _ (Functor.zero_obj _)
  | top => simpa using inferInstanceAs (IsIso (𝟙 _))

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s : Finset α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t)

Tactic:
← P.biUnion_parts,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
s : Finset α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ #(interedges r (P.parts.biUnion id) t) = ∑ a ∈ P.parts, #(interedges r a t)
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)

Tactic:
← P.biUnion_parts,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(interedges r s (P.parts.biUnion id)) = ∑ b ∈ P.parts, #(interedges r s b)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
⊢ {x ∈ A ×ˢ A |
      match x with
      | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y} ⊆
    ((P.nonUniforms G (ε / 8)).biUnion fun x ↦
          match x with
          | (U, V) => U ×ˢ V) ∪
        P.parts.biUnion offDiag ∪
      (P.sparsePairs G (ε / 4)).biUnion fun x ↦
        match x with
        | (U, V) => G.interedges U V

Tactic:
rintro ⟨x, y⟩
  simp only [mem_filter, regularityReduced_adj, not_and, not_exists,
    not_le, mem_biUnion, mem_union, mem_product, Prod.exists, mem_offDiag, and_imp,
    or_assoc, and_assoc, P.mk_mem_nonUniforms, Finpartition.mk_mem_sparsePairs, mem_interedges_iff]
  intro hx hy h h'
  replace h' := h' h
  obtain ⟨U, hU, hx⟩ := P.exists_mem hx
  obtain ⟨V, hV, hy⟩ := P.exists_mem hy
  obtain rfl | hUV := eq_or_ne U V
  · exact Or.inr (Or.inl ⟨U, hU, hx, hy, G.ne_of_adj h⟩)
  by_cases h₂ : G.IsUniform (ε / 8) U V
  · exact Or.inr <| Or.inr ⟨U, V, hU, hV, hUV, h' _ hU _ hV hx hy hUV h₂, hx, hy, h⟩
  · exact Or.inl ⟨U, V, hU, hV, hUV, h₂, hx, hy⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
Ui Vj : Finset α
⊢ (Ui, Vj) ∈ P.parts.offDiag.attach.biUnion (distinctPairs hP G ε) → (Ui, Vj) ∈ (increment hP G ε).parts.offDiag

Tactic:
simp only [distinctPairs, increment, mem_offDiag, bind_parts, mem_biUnion, Prod.exists,
    mem_product, mem_attach, true_and, Subtype.exists, and_imp,
    mem_offDiag, forall_exists_index, Ne]

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
Ui Vj : Finset α
⊢ ∀ (x x_1 : Finset α) (x_2 : x ∈ P.parts ∧ x_1 ∈ P.parts ∧ ¬x = x_1),
    Ui ∈ (chunk hP G ε ⋯).parts →
      Vj ∈ (chunk hP G ε ⋯).parts →
        (∃ a, ∃ (h : a ∈ P.parts), Ui ∈ (chunk hP G ε ⋯).parts) ∧
          (∃ a, ∃ (h : a ∈ P.parts), Vj ∈ (chunk hP G ε ⋯).parts) ∧ ¬Ui = Vj
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
⊢ G.killCopies H = G

Tactic:
obtain rfl | hH := eq_or_ne H ⊥

Goal state after:
case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
hHG : ⊥.Free G
⊢ G.killCopies ⊥ = G

case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hHG : H.Free G
hH : H ≠ ⊥
⊢ G.killCopies H = G
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ H.Free (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some}))

Tactic:
Free,

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ ¬H ⊑ G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset - G.copyCount H ≤ #(G.killCopies H).edgeFinset

Tactic:
obtain rfl | hH := eq_or_ne H ⊥

Goal state after:
case inl
V : Type u_1
W : Type u_2
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset - G.copyCount ⊥ ≤ #(G.killCopies ⊥).edgeFinset

case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
⊢ #G.edgeFinset - G.copyCount H ≤ #(G.killCopies H).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ Fintype ↑(edge s t).edgeSet

Tactic:
edge

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ Fintype ↑(fromEdgeSet {s(s, t)}).edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ ↑m / (↑m + 1) = (↑m + 1 - 1) / (↑m + 1)

Tactic:
add_sub_cancel_right

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ ↑m / (↑m + 1) = ↑m / (↑m + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
a v✝ w✝ : V
h✝ : G.Adj a v✝
p : G.Walk v✝ w✝
ih : ∀ (h : w ∈ p.support), (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support
h : w ∈ (cons h✝ p).support
h' : w ≠ a
⊢ ((cons h✝ p).dropUntil w h).support = (((cons h✝ p).drop (List.idxOf w (cons h✝ p).support)).copy ⋯ ⋯).support

Tactic:
· rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil]
      grind

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
h'' : (s(u✝, v✝) == s(u, x)) = true
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
simp only [beq_iff_eq, Sym2.eq, Sym2.rel_iff'] at h''
          obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''
          · exact (h' rfl).elim
          · cases p' <;> simp!

Goal state after: