mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ₁.ev i j a b =
    γ₁.ev i j a b * ((ConcreteCategory.hom (G.map b.op)) (α⁻¹ j) * (ConcreteCategory.hom (G.map b.op)) (α j))

Tactic:
Cochain₀.inv_apply,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ₁.ev i j a b =
    γ₁.ev i j a b * ((ConcreteCategory.hom (G.map b.op)) (α j)⁻¹ * (ConcreteCategory.hom (G.map b.op)) (α j))
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
X✝ Y✝ : Cᵒᵖ ⥤ A
x✝¹ : X✝ ⟶ Y✝
x✝ : Cᵒᵖ ⥤ A
⊢ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x X✝ ⊗ₘ Φ.toPresheafFiber X x x✝) ⋯ ≫
      Φ.presheafFiber.map x✝¹ ▷ Φ.presheafFiber.obj x✝ =
    Φ.presheafFiber.map (x✝¹ ▷ x✝) ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x Y✝ ⊗ₘ Φ.toPresheafFiber X x x✝) ⋯

Tactic:
ext
    simp [tensorHom_def', ← comp_whiskerRight, ← whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case hunique
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₁.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
hy₂ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : Over X
⊢ ∀ (j : (Sieve.pullback Y.hom S).arrows.categoryᵒᵖ),
    y₁.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app j =
      y₂.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app j

Tactic:
rintro ⟨Z : Over Y.left, hZ⟩

Goal state after:
case hunique
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₁.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
hy₂ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : Over X
Z : Over Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
⊢ y₁.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app (op { obj := Z, property := hZ }) =
    y₂.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app (op { obj := Z, property := hZ })
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
⊢ IsSheaf J (presheafHom F G)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]
  intro X S hS
  exact presheafHom_isSheafFor F G S
    (fun _ _ => ((Presheaf.isSheaf_iff_isLimit J G).1 hG _ (J.pullback_stable _ hS)).some)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Map

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
J : GrothendieckTopology C
Φ : J.Point
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsCocontinuous J K
X : D
R : Sieve X
hR : R ∈ K X
U : C
f : F.obj U ⟶ X
V : C
g : V ⟶ U
hg : (Sieve.functorPullback F (Sieve.pullback f R)).arrows g
v : Φ.fiber.obj V
⊢ ∃ Y g_1, ∃ (_ : R.arrows g_1), ∃ v_1 q a, a ≫ g_1 = F.map ↑q ≫ f

Tactic:
exact ⟨_, F.map g ≫ f, hg, Φ.fiber.elementsMk _ v, ⟨g, rfl⟩, 𝟙 _, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
S : Sieve X
hS :
  ∀ (Φ : (pointsBot C).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map a).app (op X))) (shrinkYonedaObjObjEquiv.symm b) =
    shrinkYonedaObjObjEquiv.symm (𝟙 X)
⊢ shrinkYonedaObjObjEquiv.symm (b ≫ a) = shrinkYonedaObjObjEquiv.symm (𝟙 X)

Tactic:
by
        rw [← hb, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve S
h : (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
⊢ (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful

Tactic:
exact .ofFullyFaithful _

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Types

Goal state before:
pp: α : Type u
f g : MonoOver α
t : f ⟶ g
⊢ Set.range ⇑(hom f.obj.hom) ⊆ Set.range ⇑(hom g.obj.hom)

Tactic:
rintro a ⟨x, rfl⟩
            exact ⟨t.hom.1 x, congr_hom t.hom.w x⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S₀ : C
S : Over S₀
R : Sieve S
hF :
  ∀ ⦃S₀_1 : C⦄ (M N : ↑(F.obj { as := op S₀_1 })) (a : S.left ⟶ S₀_1),
    Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk a)).symm ((Sieve.overEquiv S) R)).arrows
M N : ↑(F.obj { as := op S₀ })
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows

Tactic:
obtain ⟨S, a, rfl⟩ := S.mk_surjective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S₀ : C
M N : ↑(F.obj { as := op S₀ })
S : C
a : S ⟶ S₀
R : Sieve (Over.mk a)
hF :
  ∀ ⦃S₀_1 : C⦄ (M N : ↑(F.obj { as := op S₀_1 })) (a_1 : (Over.mk a).left ⟶ S₀_1),
    Presieve.IsSheafFor (F.presheafHom M N)
      ((Sieve.overEquiv (Over.mk a_1)).symm ((Sieve.overEquiv (Over.mk a)) R)).arrows
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows
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
a : ℤ
X : C
⊢ P.triangEnvelope X ≤ P.triangEnvelope.shift a X

Tactic:
hX

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 : ObjectProperty C
a : ℤ
X : C
hX : P.triangEnvelope X
⊢ P.triangEnvelope.shift a X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖᵒᵖ
⊢ (iso C 0).hom.app X = (Functor.CommShift.isoZero (unopUnop C) ℤ).hom.app X

Tactic:
simp [iso_hom_app _ 0 0, shiftFunctorZero_op_inv_app,
      shiftFunctorZero_op_hom_app]

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₁ : B ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
k' : (shiftFunctor C 1).obj (ι.obj B) ⟶ (shiftFunctor C 1).obj (ι.obj K)
hk' : (shiftFunctor C 1).map (ι.map x₁) = k' ≫ α ≫ f₃
⊢ ∃ k, k ≫ ιK f₃ α = x₁

Tactic:
refine ⟨(ι ⋙ shiftFunctor C (1 : ℤ)).preimage k',
      (ι ⋙ shiftFunctor C (1 : ℤ)).map_injective ?_⟩

Goal state after:
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₁ : B ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
k' : (shiftFunctor C 1).obj (ι.obj B) ⟶ (shiftFunctor C 1).obj (ι.obj K)
hk' : (shiftFunctor C 1).map (ι.map x₁) = k' ≫ α ≫ f₃
⊢ (ι ⋙ shiftFunctor C 1).map ((ι ⋙ shiftFunctor C 1).preimage k' ≫ ιK f₃ α) = (ι ⋙ shiftFunctor C 1).map x₁
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 (g ∘ f) s).prod = (map (g ∘ f) t).prod ↔ s.prod = t.prod

Tactic:
rw [← map_map, ← map_map]
    rw [hg.map_prod_eq_map_prod _ _ (by rwa [card_map]) (by rwa [card_map]),
      hf.map_prod_eq_map_prod hsA htA hs ht]
    · simpa using fun a h ↦ hf.bijOn.mapsTo (hsA h)
    · simpa using fun a h ↦ hf.bijOn.mapsTo (htA h)

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

Goal state before:
pp: k n✝¹ n✝ : ℕ
⊢ ∀ x ∈ image (⇑(map (2 * (n✝ + 1) - 1))) (sphere (n✝¹ + 1) (n✝ + 1) k), x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

pp: k n✝¹ n✝ : ℕ
⊢ Set.InjOn ⇑(map (2 * (n✝ + 1) - 1)) ↑(sphere (n✝¹ + 1) (n✝ + 1) k)

Tactic:
· simp only [mem_image, and_imp, forall_exists_index,
      sphere, mem_filter]
    rintro _ x hx _ rfl
    exact (map_le_of_mem_box hx).trans_lt sum_lt

Goal state after:
k n✝¹ n✝ : ℕ
⊢ Set.InjOn ⇑(map (2 * (n✝ + 1) - 1)) ↑(sphere (n✝¹ + 1) (n✝ + 1) k)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hd
N : ℕ
hN : 4096 ≤ N
⊢ 1 < ↑N

Tactic:
one_lt_cast

Goal state after:
case hd
N : ℕ
hN : 4096 ≤ N
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hd
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈√(log ↑N)⌉₊

Tactic:
rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
      refine log_pos ?_
      rw [one_lt_cast]
      exact hN.trans_lt' (by norm_num1)

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

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < ↑N

Tactic:
one_lt_cast

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

Goal state before:
pp: case h₂
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < ↑N

Tactic:
one_lt_cast

Goal state after:
case h₂
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < N
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x y : G
⊢ Set.LeftInvOn (fun ab' ↦ x •> ab'.1) (fun z ↦ (x⁻¹ * z, z⁻¹ * y)) ↑(x •> A ∩ y •> B)

Tactic:
by simp [Set.LeftInvOn]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ Set.LeftInvOn (fun ab ↦ (ab.1, ab.2⁻¹)) (fun ab ↦ (ab.1, ab.2⁻¹)) ↑({ab ∈ A ×ˢ B | ab.1 * ab.2⁻¹ = x})

Tactic:
by simp [Set.LeftInvOn]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ Set.RightInvOn (fun ab ↦ (ab.1, ab.2⁻¹)) (fun ab ↦ (ab.1, ab.2⁻¹)) ↑({ab ∈ A ×ˢ B⁻¹ | ab.1 * ab.2 = x})

Tactic:
by simp [Set.LeftInvOn]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
e₁ e₂ : ↑(G.neighborSet v)
h : G.dartOfNeighborSet v e₁ = G.dartOfNeighborSet v e₂
⊢ ↑e₁ = ↑e₂

Tactic:
by
    injection h with h'
    convert! congr_arg Prod.snd h'

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ x ∈ G.support.toFinsetᶜ, G.degree x = 0

Tactic:
intro v

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ v ∈ G.support.toFinsetᶜ → G.degree v = 0
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap f G'

Tactic:
intro v

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst✝ : Subsingleton V
v : V
⊢ ∀ ⦃w : V⦄, G.Adj v w → (SimpleGraph.comap f G').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1

Tactic:
intro v

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
v : V
⊢ v ∈ {x | ↑(G.degree x) ≠ 0} → ↑(G.degree v) = 1
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
⊢ Injective ⇑f

Tactic:
intro v

Goal state after:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
v : V
⊢ ∀ ⦃a₂ : V⦄, f v = f a₂ → v = a₂
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)

Tactic:
intro v

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
v : V
⊢ Gᶜ.degree v = Fintype.card V - 1 - k
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
v : V
⊢ Gᶜ.degree v = Fintype.card V - 1 - k

Tactic:
rw [degree_compl, h v]

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.maxDegree = 0
⊢ ∀ (v : V), G.IsIsolated v

Tactic:
intro v

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G.maxDegree = 0
v : V
⊢ G.IsIsolated v
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z :
  #({x ∈ P.parts | #x = #s / #P.parts + 1}) * (#s / #P.parts) + #({x ∈ P.parts | #x = #s / #P.parts + 1}) * 1 +
      #({p ∈ P.parts | ¬#p = #s / #P.parts + 1}) * (#s / #P.parts) =
    #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z :
  #({p ∈ P.parts | ¬#p = #s / #P.parts + 1}) * (#s / #P.parts) +
      (#({x ∈ P.parts | #x = #s / #P.parts + 1}) * (#s / #P.parts) + #({x ∈ P.parts | #x = #s / #P.parts + 1}) * 1) =
    #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
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
p : Subtype Pr
⊢ p ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts ↔ ↑p ∈ P.parts

Tactic:
by simp [toSubtype]

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
⊢ IsIso (t.eTruncGEπ ⊥)

Tactic:
by
  dsimp [eTruncGEπ]
  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
⊢ ∀ x₁ ∈ x, ∃ x₂ ∈ x, s x₁ x₂

Tactic:
intro x _

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x✝ : Finset α
inst✝ : DecidableRel ⇑s
x : α
a✝ : x ∈ x✝
⊢ ∃ x₂ ∈ x✝, s x x₂
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
h : a ≤ b
X : C
⊢ IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))

Tactic:
by
  induction b using WithBotTop.rec with
  | bot =>
    obtain rfl : a = ⊥ := by simpa using h
    infer_instance
  | coe b =>
    induction a using WithBotTop.rec with
    | bot => infer_instance
    | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X
    | top => simp at h
  | top => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ a ∈ (image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset).sup id

Tactic:
rw [mem_sup]
        refine
          ⟨{i ∈ s | ∀ t ∈ F, t ∈ {u ∈ F | a ∈ u} ↔ i ∈ t},
            mem_image_of_mem _ (mem_powerset.2 <| filter_subset _ _),
            mem_filter.2 ⟨ha, fun t ht ↦ ?_⟩⟩
        rw [mem_filter]
        exact and_iff_right ht

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 : EInt
X : C
⊢ IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X))

Tactic:
rw [← eTruncLT_obj_map_eTruncLTι_app]

Goal state after:
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 : EInt
X : C
⊢ IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app 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 β
⊢ #({e ∈ s ×ˢ t | r e.1 e.2}) + #({e ∈ s ×ˢ t | ¬r e.1 e.2}) = #(s ×ˢ t)

Tactic:
← card_union_of_disjoint,

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ #({e ∈ s ×ˢ t | r e.1 e.2} ∪ {e ∈ s ×ˢ t | ¬r e.1 e.2}) = #(s ×ˢ t)

α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ Disjoint ({e ∈ s ×ˢ t | r e.1 e.2}) ({e ∈ s ×ˢ t | ¬r e.1 e.2})
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
⊢ G.IsUniform ε {a} {b} ↔ 0 < ε

Tactic:
refine ⟨IsUniform.pos, fun hε s' hs' t' ht' hs ht ↦ ?_⟩

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(#{a}) * ε ≤ ↑(#s')
ht : ↑(#{b}) * ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁

Tactic:
have hst : (#s₂ : ℚ) * #t₂ ≠ 0 := by simp [hs₂.ne_empty, ht₂.ne_empty]

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : ↑(#s₂) * ↑(#t₂) ≠ 0
⊢ ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁)) * edgeDensity r s₂ t₂ ≤ edgeDensity r s₁ t₁
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(⋯.choose, ⋯.choose).1)

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.1

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

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
this : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}
⊢ #({e ∈ s ×ˢ t | G.Adj e.1 e.2}) + #({e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}) = #(s ×ˢ t)

Tactic:
← card_union_of_disjoint,

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
this : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}
⊢ #({e ∈ s ×ˢ t | G.Adj e.1 e.2} ∪ {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}) = #(s ×ˢ t)

α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
this : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2}
⊢ Disjoint ({e ∈ s ×ˢ t | G.Adj e.1 e.2}) ({e ∈ s ×ˢ t | ¬G.Adj e.1 e.2})