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

Goal state before:
pp: 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
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
⊢ F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map (Over.Hom.left φ ≫ Z₁.hom).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))

Tactic:
Over.w f

Goal state after:
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
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
⊢ F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (functorEnrichedHom A F G ⋙ coyoneda.obj (op M))

Tactic:
by
  rw [Presieve.isSheaf_iff_of_nat_equiv
    (functorEnrichedHomCoyonedaObjEquiv M F G)
    (fun _ _ _ _ ↦ functorEnrichedHomCoyonedaObjEquiv_naturality _ _)]
  rw [← isSheaf_iff_isSheaf_of_type]
  exact Presheaf.IsSheaf.hom (F ⊗ (Functor.const _).obj M) G hG

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)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Tactic:
· intro y₁ y₂ hy₁ hy₂
    rw [PresheafHom.isAmalgamation_iff _ _ hx] at hy₁ hy₂
    apply NatTrans.ext
    ext ⟨Y : Over X⟩
    apply (hG Y.hom).hom_ext
    rintro ⟨Z : Over Y.left, hZ⟩
    dsimp
    let φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom
    refine (y₁.naturality φ.op).symm.trans (Eq.trans ?_ (y₂.naturality φ.op))
    rw [(hy₁ _ _ hZ), ← ((hy₂ _ _ hZ))]

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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
⊢ ∀ ⦃Y : C⦄ (q_1 : Y ⟶ S'') ⦃i₁ i₂ : ι''⦄ (f₁ : Y ⟶ X'' i₁) (f₂ : Y ⟶ X'' i₂) (hf₁ : f₁ ≫ f'' i₁ = q_1)
    (hf₂ : f₂ ≫ f'' i₂ = q_1),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β i₁)).op.toLoc (q' i₁).op.toLoc (r' i₁).op.toLoc ⋯)).symm.app
              (D.obj (α (β i₁)))).hom ≫
        ((pullFunctor F ⋯).obj D).hom q_1 f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w ⋙ pullFunctor F w').obj D).hom q_1 f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β i₂)).op.toLoc (q' i₂).op.toLoc (r' i₂).op.toLoc ⋯)).symm.app
              (D.obj (α (β i₂)))).hom

Tactic:
intro Y s k₁ k₂ f₁ f₂ hf₁ hf₂
      dsimp
      rw [pullFunctorObjHom_eq _ _ _ _ _ (s ≫ r) _ _ rfl,
        pullFunctorObjHom_eq _ _ _ _ _ (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂)]
      dsimp
      rw [pullFunctorObjHom_eq _ _ _ _ _ (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂)
        rfl (by simp [w', reassoc_of% hf₁, reassoc_of% hf₂]) (by
          simp [reassoc_of% w', reassoc_of% hf₁, hr])]
      dsimp
      simp only [Category.assoc]
      rw [mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc _ _ _ _ _ _ _
        (by grind) rfl rfl, mapComp'₀₂₃_hom_app _ _ _ _ _ _ _ _ rfl rfl]

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

Goal state before:
pp: X : Type u
⊢ yonedaEquiv
      (yoneda'.map
            ((NatIso.ofComponents
                    (fun _α ↦
                      { hom := ↾fun x ↦ ↾fun x_1 ↦ x, inv := ↾fun f ↦ (TypeCat.Hom.hom f) PUnit.unit, hom_inv_id := ⋯,
                        inv_hom_id := ⋯ })
                    ⋯).hom.app
              X) ≫
          (NatIso.ofComponents (fun S ↦ equivYoneda' S) ⋯).symm.hom.app (yoneda'.obj X)).hom =
    yonedaEquiv (𝟙 (yoneda'.obj X)).hom

Tactic:
dsimp [yoneda', yonedaEquiv, equivYoneda, evalEquiv]

Goal state after:
X : Type u
⊢ typesGlue (yoneda.obj X) ⋯ X ⇑(ConcreteCategory.hom (𝟙 X ≫ ↾fun x ↦ ↾fun x_1 ↦ x)) = 𝟙 X
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
w✝³ : Type (max u v)
w✝² : w✝³ → C
f : (i : w✝³) → w✝² i ⟶ S
w✝¹ : Type (max u v)
w✝ : w✝¹ → C
f' : (i : w✝¹) → w✝ i ⟶ S
h : Sieve.generate (Presieve.ofArrows w✝² f) = Sieve.generate (Presieve.ofArrows w✝ f')
⊢ Nonempty (F.toDescentData fun f_1 ↦ f_1.obj.hom).FullyFaithful ↔
    Nonempty (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful

Tactic:
apply DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
w✝³ : Type (max u v)
w✝² : w✝³ → C
f : (i : w✝³) → w✝² i ⟶ S
w✝¹ : Type (max u v)
w✝ : w✝¹ → C
f' : (i : w✝¹) → w✝ i ⟶ S
h : Sieve.generate (Presieve.ofArrows w✝² f) = Sieve.generate (Presieve.ofArrows w✝ f')
⊢ (Sieve.ofArrows (fun f_1 ↦ f_1.obj.left) fun f_1 ↦ f_1.obj.hom) =
    Sieve.ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

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
⊢ Nonempty (F.toDescentData fun f_1 ↦ f_1.obj.hom).FullyFaithful ↔ Nonempty (F.toDescentData f).FullyFaithful

Tactic:
apply DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
⊢ (Sieve.ofArrows (fun f_1 ↦ f_1.obj.left) fun f_1 ↦ f_1.obj.hom) = Sieve.ofArrows X f
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ CommSq 𝒞.truth eΩ₀.hom eΩ.hom t

Tactic:
simp [ht]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ CommSq t eΩ₀.inv eΩ.inv 𝒞.truth

Tactic:
simp [ht]

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case e
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ m ≫ χ m = (isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J

pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback ((sheafToPresheaf J (Type (max u v))).map m)
    ((sheafToPresheaf J (Type (max u v))).map ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    ((sheafToPresheaf J (Type (max u v))).map (χ m)) ((sheafToPresheaf J (Type (max u v))).map (truth J))

Tactic:
· ext : 1
    simp only [Ω_obj, ObjectProperty.FullSubcategory.comp_hom, χ_hom, terminal_obj, truth_hom,
      ← cancel_mono (closedSieves J).ι, Category.assoc, Subfunctor.lift_ι]
    exact Presheaf.comp_χ_eq m.hom

Goal state after:
case H
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback ((sheafToPresheaf J (Type (max u v))).map m)
    ((sheafToPresheaf J (Type (max u v))).map ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    ((sheafToPresheaf J (Type (max u v))).map (χ m)) ((sheafToPresheaf J (Type (max u v))).map (truth J))
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
⊢ ∀ (P : A) (g : P ⟶ K), g ≫ ιK f₃ α = 0 → g = 0

Tactic:
intro B

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
⊢ ∀ (g : B ⟶ K), g ≫ ιK f₃ α = 0 → g = 0
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
⊢ ∀ (R : A) (g : Q ⟶ R), πQ f₂ β ≫ g = 0 → g = 0

Tactic:
intro B

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
⊢ ∀ (g : Q ⟶ B), πQ f₂ β ≫ g = 0 → g = 0
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
inst✝² : Preadditive A
inst✝¹ : ι.Full
inst✝ : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
⊢ HasKernel f₁

Tactic:
obtain ⟨X₃, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map f₁)
  obtain ⟨K, Q, α, β, γ, hT'⟩ := hf₁ f₂ f₃ hT
  exact hasKernel hι hT hT'

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 : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ (map g t).card = n

Tactic:
simp [ht]

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
i : 2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
⊢ (↑N ^ (↑(nValue N))⁻¹) ^ ↑(nValue N) ≤ ↑N

Tactic:
rw [← rpow_mul (cast_nonneg _), inv_mul_cancel₀, rpow_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
⊢ ↑(#(A * A)) ≤ K * ↑(#A)

Tactic:
by simpa [sq] using hA.card_pow_le (n := 2)

Goal state after:
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ∞
⊢ n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)

Tactic:
by simp [minOrder]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph W
⊢ SimpleGraph.map (⇑f) (SimpleGraph.comap (⇑f) G) ≤ G

Tactic:
rw [map_le_iff_le_comap]

Goal state after:
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
⊢ SimpleGraph.map (⇑f) G ≤ G'

Tactic:
rw [map_le_iff_le_comap]

Goal state after:
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'
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
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v w : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w

Tactic:
obtain rfl | hvw := eq_or_ne v w

Goal state after:
case inl
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
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v : V
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding v) ↔ G.Adj v v

case inr
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
H : SimpleGraph W
f✝ : G ↪g G'
G'' : SimpleGraph X
G''' : SimpleGraph Y
f : Gᶜ ↪g Hᶜ
v w : V
hvw : v ≠ w
⊢ H.Adj (f.toEmbedding v) (f.toEmbedding w) ↔ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = Fintype.card V - 1 - G.degree v

Tactic:
← card_neighborSet_union_compl_neighborSet G v,

Goal state after:
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset - G.degree v
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts.Nonempty ↔ a ≠ ⊥

Tactic:
by
  contrapose!; exact parts_eq_empty_iff

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P ∈
    image
      (fun ps ↦
        if h : ps.sup id = s ∧ ⊥ ∉ ps ∧ ps.SupIndep id then
          { parts := ps, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
        else ⊤)
      s.powerset.powerset

Tactic:
refine mem_image.mpr ⟨P.parts, ?_, ?_⟩
    · rw [mem_powerset]; intro p hp; rw [mem_powerset]; exact P.le hp
    · simp [P.supIndep, P.sup_parts, P.bot_notMem, -bot_eq_empty]

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

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

Tactic:
exact mem_part_ofSetSetoid_iff_rel univ

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 (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity s t|

Tactic:
edgeDensity_comm _ s

Goal state after:
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 (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity t s|
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ P.sparsePairs G ε ⊆ P.parts.offDiag

Tactic:
apply filter_subset

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

Goal state before:
pp: case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts = ∅
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      ↑(#(increment hP G ε).parts) ^ 2 ≤
    ↑((increment hP G ε).energy G)

Tactic:
coe_energy

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      ↑(#(increment hP G ε).parts) ^ 2 ≤
    (∑ uv ∈ (increment hP G ε).parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#(increment hP G ε).parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
h✝ : Nonempty V
v : V
h : G.maxDegree = G.degree v
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
grind [degree_le_maxDegree H (f v), f.degree_le v]

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
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {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
⊢ ∀ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts, #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m

Tactic:
intro B

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
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {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
B : Finset α
⊢ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts → #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) = a * m + b * (m + 1)

Tactic:
rw [h, ← (P.equitabilise h).sum_card_parts]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #({u ∈ (equitabilise h).parts | #u = m}) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i