mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData f
i₁ i₂ i₃ : ι
⊢ pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁
        (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
      pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁
      (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯

Tactic:
by
    rw [pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₂₃,
      pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₃,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,
      D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p, D.hom_comp]
    all_goals cat_disch

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h✝ :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
X : Over S₀
b : X ⟶ Over.mk a
Y : Over S
c : Y ⟶ Over.mk (𝟙 S)
d : X ⟶ (Over.map a).obj Y
h : ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows c
fac :
  (Over.forget S₀).map (b ≫ (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv) =
    (Over.forget S₀).map (d ≫ (Over.map a).map c)
⊢ ((Sieve.overEquiv (Over.mk a)).symm R).arrows b

Tactic:
dsimp at fac

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h✝ :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
X : Over S₀
b : X ⟶ Over.mk a
Y : Over S
c : Y ⟶ Over.mk (𝟙 S)
d : X ⟶ (Over.map a).obj Y
h : ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows c
fac : Over.Hom.left b ≫ 𝟙 S = Over.Hom.left d ≫ Over.Hom.left c
⊢ ((Sieve.overEquiv (Over.mk a)).symm R).arrows b
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
    (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
      ∃ x₁,
        (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃

Tactic:
· simp only [Functor.const_obj_obj, Functor.sieves_obj, χ_app, Opposite.op_unop,
      TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, truth_app, Functor.isTerminalConst_from_app,
      Types.isTerminalPUnit_from_apply, and_true, forall_const]
    intro p hp
    simpa [eq_comm] using! congr($(hp).arrows (𝟙 _))

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

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  (F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁)) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
⊢ Triangle.mk (G.map T.mor₁) (G.map T.mor₂) (G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁) ∈
    distinguishedTriangles

Tactic:
have h₂' : g ≫ (G.commShiftIso (1 : ℤ)).inv.app T.obj₁ =
        adj.homEquiv _ _ h ≫ G.map T.mor₃ := by
      apply (adj.homEquiv _ _).symm.injective
      simp only [Functor.comp_obj, homEquiv_counit, Functor.id_obj, Functor.map_comp, assoc,
        homEquiv_unit, counit_naturality, counit_naturality_assoc, left_triangle_components_assoc,
        ← h₂, adj.shift_counit_app, Iso.hom_inv_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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  (F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁)) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
⊢ Triangle.mk (G.map T.mor₁) (G.map T.mor₂) (G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁) ∈
    distinguishedTriangles
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
⊢ ∀ (P : C) (g : P ⟶ Z), g ≫ (adj.homEquiv Z T.obj₃) h = 0 → g = 0

Tactic:
intro _

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
⊢ ∀ (g : P✝ ⟶ Z), g ≫ (adj.homEquiv Z T.obj₃) h = 0 → g = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: case refine_1
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 c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
      (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X) ≫
        (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
← cancel_epi ((t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X)),

Goal state after:
case refine_1
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 c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
        (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X) ≫
          (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
⊢ mulRothNumber B ≤ mulRothNumber A

Tactic:
have hfsA : Set.SurjOn f A s := hf'.surjOn.mono Subset.rfl (coe_subset.2 hsB)

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanHom 2 (↑A) (↑B) f
hf' : Set.BijOn f ↑A ↑B
s : Finset β
hsB : s ⊆ B
hcard : #s = mulRothNumber B
hs : ThreeGPFree ↑s
hsA : invFunOn f ↑A '' ↑s ⊆ ↑A
hfsA : Set.SurjOn f ↑A ↑s
⊢ mulRothNumber B ≤ mulRothNumber A
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a * b = c * d → f a * f b = f c * f d
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 2 → t.card = 2 → s.prod = t.prod → (map f s).prod = (map f t).prod

Tactic:
by aesop (add simp card_eq_two)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, f a * f b = f c * f d ↔ a * b = c * d
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 2 → t.card = 2 → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)

Tactic:
by aesop (add simp card_eq_two)

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

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * ↑(dValue N)) ^ nValue N ≤ ↑N

Tactic:
suffices i : (2 * dValue N : ℝ) ≤ (N : ℝ) ^ (nValue N : ℝ)⁻¹ by
    rw [← rpow_natCast]
    apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans
    rw [← rpow_mul (cast_nonneg _), inv_mul_cancel₀, rpow_one]
    rw [cast_ne_zero]
    apply (nValue_pos hN).ne'

Goal state after:
N : ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
⊢ ∀ y ∈ {x | x.1.Nonempty ∧ x.2.Nonempty},
    (∀ z ∈ {x | x.1.Nonempty ∧ x.2.Nonempty}, DevosMulRel z y → min (minOrder α) ↑(#z.1 + #z.2 - 1) ≤ ↑(#(z.1 * z.2))) →
      min (minOrder α) ↑(#y.1 + #y.2 - 1) ≤ ↑(#(y.1 * y.2))

Tactic:
rintro ⟨s, t⟩ ⟨hs, ht⟩ ih

Goal state after:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : (s, t).1.Nonempty
ht : (s, t).2.Nonempty
ih :
  ∀ z ∈ {x | x.1.Nonempty ∧ x.2.Nonempty}, DevosMulRel z (s, t) → min (minOrder α) ↑(#z.1 + #z.2 - 1) ≤ ↑(#(z.1 * z.2))
⊢ min (minOrder α) ↑(#(s, t).1 + #(s, t).2 - 1) ≤ ↑(#((s, t).1 * (s, t).2))
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
hv : v ∉ G.support.toFinset
⊢ v ∉ G.support

Tactic:
Set.mem_toFinset

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
hv : v ∉ G.support
⊢ v ∉ G.support
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
⊢ (SimpleGraph.induce u G).IsCompleteBetween (u ↓∩ s) (u ↓∩ t)

Tactic:
intro _

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁✝ : ↑u
⊢ v₁✝ ∈ u ↓∩ s → ∀ ⦃v₂ : ↑u⦄, v₂ ∈ u ↓∩ t → (SimpleGraph.induce u G).Adj v₁✝ v₂
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ 0 < G.degree v ↔ ∃ w, G.Adj v w

Tactic:
by
  simp only [degree, card_pos, Finset.Nonempty, mem_neighborFinset]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
⊢ G.minDegree ≤ H.minDegree

Tactic:
cases isEmpty_or_nonempty V
  · simp
  · apply le_minDegree_of_forall_le_degree
    exact fun v ↦ (G.minDegree_le_degree v).trans (G.degree_le_of_le hle)

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

Goal state before:
pp: case refine_1
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ (G.commonNeighbors v w).toFinset

Tactic:
Set.mem_toFinset

Goal state after:
case refine_1
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ w ∉ G.commonNeighbors v w
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
⊢ (↑P.parts).PairwiseDisjoint f

Tactic:
intro _

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
x✝ : α
⊢ x✝ ∈ ↑P.parts → ∀ ⦃y : α⦄, y ∈ ↑P.parts → x✝ ≠ y → (Disjoint on f) x✝ y
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ Disjoint (id b) (P.parts.sup id)

Tactic:
rwa [sup_parts, disjoint_comm]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
⊢ a ∈ P.part b → ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p

Tactic:
intro h
    have : b ∈ s := P.part_nonempty.1 ⟨a, h⟩
    refine ⟨_, ?_, h, ?_⟩ <;> simp [this]

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 : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
⊢ ∀ a ∈ x, ∀ a_2 ∈ x, ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a x_3 → x_3 ∈ x → s a_2 x_3 → (s a x_1 ↔ s a_2 x_1)

Tactic:
intro _

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
a✝ : α
⊢ a✝ ∈ x → ∀ a ∈ x, ∀ x_1 ∈ x, ∀ x_3 ∈ x, s a✝ x_3 → x_3 ∈ x → s a x_3 → (s a✝ x_1 ↔ s a x_1)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
a : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
b : α
⊢ b ∈ (ofSetSetoid s x).part a ↔ a ∈ x ∧ b ∈ x ∧ s a b

Tactic:
suffices (∃ a₁ ∈ x, (b ∈ x ∧ s a₁ b) ∧ a ∈ x ∧ s a₁ a) ↔ a ∈ x ∧ b ∈ x ∧ s a b by
    simpa [mem_part_iff_exists, ofSetSetoid_parts]
  exact ⟨
    fun ⟨c, _, ⟨hb, hcb⟩, ⟨ha, hca⟩⟩ ↦ ⟨ha, hb, s.trans' (s.symm' hca) hcb⟩,
    fun h ↦ ⟨a, ⟨h.1, ⟨⟨h.2.1, h.2.2⟩, ⟨h.1, s.refl _⟩⟩⟩⟩
  ⟩

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 s' : Finset α
hs : Disjoint s s'
t : Finset β
⊢ Disjoint (interedges r s t) (interedges r s' t)

Tactic:
rw [Finset.disjoint_left] at hs ⊢

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s' t
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 α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s' t

Tactic:
intro _

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
⊢ a✝ ∈ interedges r s t → a✝ ∉ interedges r s' t
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 t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s t'

Tactic:
intro _

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
⊢ a✝ ∈ interedges r s t → a✝ ∉ interedges r s t'
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
hab : b ≤ a
X : C
⊢ (t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X) ≫
      (t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X)) =
    𝟙 ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))

Tactic:
by
  simp [eTruncLT_obj_map_eTruncLTι_app]

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
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncLT.obj b').map
          ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
            (t.eTruncGE.obj a').map ((t.eTruncLTι b).app X)) ≫
        (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)

Tactic:
Functor.map_comp_assoc,

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 b : EInt
hab : a ≤ b
a' b' : EInt
hab' : a' ≤ b'
φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')
X : C
⊢ (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X)) ≫
        (t.eTruncLT.obj b').map ((t.eTruncGE.obj a').map ((t.eTruncLTι b).app X)) ≫
          (t.eTruncLTGEIsoGELT a' b').hom.app X =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)) ≫
      (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X) ≫
        (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
obtain ⟨dum, hdum₁, hdum₂⟩ :=
    exists_equipartition_card_eq (univ : Finset α) (initialBound_pos _ _).ne' htα

Goal state after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
⊢ ∀ x_1 ∈ G.edgeFinset, x_1 ∉ G.incidenceFinset x ↔ x ∉ x_1

Tactic:
intro _

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
⊢ x✝ ∈ G.edgeFinset → (x✝ ∉ G.incidenceFinset x ↔ x ∉ x✝)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → G.Subgraph
x✝¹ x✝ : V
⊢ (⨅ a, ⨆ b, f a b).Adj x✝¹ x✝ ↔ (⨆ g, ⨅ a, f a (g a)).Adj x✝¹ x✝

Tactic:
simp [Classical.skolem]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ⊆ H.verts
h₁ : S ⊆ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
M : G.Subgraph
h : v ∈ M.verts
⊢ M' ≤ M

Tactic:
constructor <;> simp [h, M']

Goal state after: