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

Goal state before:
pp: case mp
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ x.IsAmalgamation y →
    ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))

pp: case mpr
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ (∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))) →
    x.IsAmalgamation y

Tactic:
· intro h Y g hg
    rw [← h g hg]
    dsimp
    rw [presheafHom_map_app_op_mk_id]

Goal state after:
case mpr
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ (∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))) →
    x.IsAmalgamation y
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case left.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac : a ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄ = a ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map a.op

Tactic:
rfl

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

Goal state before:
pp: case mpr
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
H : x (W.hom ≫ g) ⋯ = (ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)
⊢ (x g hg).app (op (Over.mk W.hom)) = (x g hg).app (op W)

Tactic:
rfl

Goal state after:
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₂
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op

Tactic:
let φ : Over.mk f.left ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk f.left

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) ⋯
⊢ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case right.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op

Tactic:
rfl

Goal state after:
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
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j : Under (op X)
⊢ f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom) =
    f ≫ end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j

Tactic:
rfl

Goal state after:
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
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j : (Over X)ᵒᵖ
⊢ g.app (op (Over.mk (Under.mk (unop j).hom.op).hom.unop)) = g.app j

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
X Y : C
f : X ⟶ Y
inst✝ : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)
j : Over X
⊢ uncurry
      (y ≫
        enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G) ((Under.map f.op).obj (Under.mk j.hom.op))) =
    uncurry (y ≫ enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G) (Under.mk (f.op ≫ j.hom.op)))

Tactic:
rfl

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f' i₁).op.toLoc ≫ f₁.op.toLoc = q.op.toLoc

Tactic:
grind

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (p.op.toLoc ≫ (f' i₁).op.toLoc) ≫ f₁.op.toLoc = p.op.toLoc ≫ q.op.toLoc

Tactic:
grind

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f' i₂).op.toLoc ≫ f₂.op.toLoc = q.op.toLoc

Tactic:
grind

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (p.op.toLoc ≫ (f' i₂).op.toLoc) ≫ f₂.op.toLoc = p.op.toLoc ≫ q.op.toLoc

Tactic:
grind

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f (α i₁)).op.toLoc ≫ (p' i₁).op.toLoc = p.op.toLoc ≫ (f' i₁).op.toLoc

Tactic:
grind

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
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f (α i₂)).op.toLoc ≫ (p' i₂).op.toLoc = p.op.toLoc ≫ (f' i₂).op.toLoc

Tactic:
grind

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ (ConcreteCategory.hom (⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber.map (Over.mk f).hom)) y =
    ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd

Tactic:
rfl

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
x✝ : ι''
⊢ (p' (β x✝)).op.toLoc ≫ (q' x✝).op.toLoc = (r' x✝).op.toLoc

Tactic:
grind

Goal state after:
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)
⊢ ∃ (h : Presieve.FamilyOfElements.Compatible fun x x_1 hr ↦ y✝ x_1 hr), ⋯.choose = t✝

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ Presieve.IsSheaf J (Functor.closedSieves K.toGrothendieck).toFunctor

Tactic:
rw [H.isSheaf_type_iff]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
⊢ ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor (Functor.closedSieves K.toGrothendieck).toFunctor R
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
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (p' (β k₁)).op.toLoc ≫ (q' k₁).op.toLoc = (r' k₁).op.toLoc

Tactic:
grind

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
x✝ : discretePresieve δ g
x : ε
h✝ : ∀ (y : ε), y = x
this : (ConcreteCategory.hom f₁) (Classical.choose hf₁) = (ConcreteCategory.hom f₂) (Classical.choose hf₂)
⊢ (ConcreteCategory.hom (S.map (g ≫ g₁ ≫ ↾fun x ↦ PUnit.unit).op))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂))) =
    (ConcreteCategory.hom (S.map (g ≫ g₂ ≫ ↾fun x ↦ PUnit.unit).op))
      (f ((ConcreteCategory.hom f₂) (Classical.choose hf₂)))

Tactic:
rfl

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom (↾fun x ↦ (ConcreteCategory.hom (S.map ((↾fun x_1 ↦ x) ≫ f).op)) s)) x =
    (ConcreteCategory.hom (f ≫ ↾fun x ↦ (ConcreteCategory.hom (S.map (↾fun x_1 ↦ x).op)) s)) x

Tactic:
rfl

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
U V : C
f : U ⟶ V
⊢ Submonoid.map (MonCat.Hom.hom (M.map f)) (S.obj U) ≤ S.obj V

Tactic:
grw [Submonoid.map_le_iff_le_comap, S.map f]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M M' M'' : C ⥤ MonCat
p : M ⟶ M'
S'' : SubmonoidFunctor M''
p' : M' ⟶ M''
⊢ comap (p ≫ p') S'' = comap p (comap p' S'')

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (S.toBiprod F n₀) 2 3 ⋯ =
    (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)

Tactic:
rfl

Goal state after:
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 : ℤ
h : n + -n = 0
⊢ (commShiftIso F.op n).hom.app X =
    (F.map ((shiftFunctorOpIso C n (-n) h).hom.app X).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop X)).op ≫ (shiftFunctorOpIso D n (-n) h).inv.app (op (F.obj (unop X)))

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
⊢ ∃ n, P.triangEnvelopeIter n ((shiftFunctor C a).obj X)

Tactic:
exact ⟨n, IsStableUnderShiftBy.le_shift _ hn⟩

Goal state after:
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
n : ℤ
hnm : n + -n = 0
⊢ (iso C n).hom.app X =
    ((shiftFunctorOpIso C (-n) n ⋯).hom.app (op X)).op ≫ (shiftFunctorOpIso Cᵒᵖ n (-n) hnm).inv.app (op (op X))

Tactic:
rfl

Goal state after:
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
n : ℤ
hnm : n + -n = 0
⊢ (iso C n).inv.app X =
    (shiftFunctorOpIso Cᵒᵖ n (-n) hnm).hom.app (op (op X)) ≫ ((shiftFunctorOpIso C (-n) n ⋯).inv.app (op X)).op

Tactic:
rfl

Goal state after:
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ᵒᵖᵒᵖ
n : ℤ
hnm : n + -n = 0
⊢ (iso C n).hom.app X =
    ((shiftFunctorOpIso Cᵒᵖ n (-n) hnm).hom.app X).unop.unop ≫ ((shiftFunctorOpIso C (-n) n ⋯).inv.app (unop X)).unop

Tactic:
rfl

Goal state after:
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ᵒᵖᵒᵖ
n : ℤ
hnm : n + -n = 0
⊢ (iso C n).inv.app X =
    ((shiftFunctorOpIso C (-n) n ⋯).hom.app (unop X)).unop ≫ ((shiftFunctorOpIso Cᵒᵖ n (-n) hnm).inv.app X).unop.unop

Tactic:
rfl

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

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
hs : ThreeGPFree s
c d : α
h : c * d = c * c
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → c * c_1 = b * b → c = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c_1 : α⦄, c_1 ∈ s → b * c_1 = c * c → b = c
hd : d = c ∨ d ∈ s
⊢ c = c

Tactic:
rfl

Goal state after:
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝² : DecidableEq β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : α → Finset β
h₁ : s.Nonempty
h₂ : ∀ j ∈ s, 0 < #(f j)
k : ℕ := s.inf' h₁ fun j ↦ #(f j)
hk : k = s.inf' h₁ fun j ↦ #(f j)
h₃ : ∀ a ∈ s, ∀ x ∈ f a, #{j | j ∈ s ∧ x ∈ f j} ≤ k
x : β
a✝ : x ∈ s.biUnion f
⊢ #{j | j ∈ s ∧ x ∈ f j} ≤ k

Tactic:
grind

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

Goal state before:
pp: case refine_1
α : 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 : IsMulFreimanHom n B C g
hf : IsMulFreimanHom 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
h : s.prod = t.prod
⊢ ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B

Tactic:
simpa using fun a h ↦ hf.mapsTo (hsA h)

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n✝ : ℕ
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ (map (⇑f) s).prod = (map (⇑f) t).prod

Tactic:
rw [← map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero]),
        h, map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero])]

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

Goal state before:
pp: case zero
d k : ℕ
⊢ Fintype.card (Fin 0 → ℕ) = rothNumberNat 1

Tactic:
rfl

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

Goal state before:
pp: N : ℕ
hN : 64 ≤ N
⊢ 3 ≤ nValue N

Tactic:
rw [nValue, ← lt_iff_add_one_le, lt_ceil, cast_two]

Goal state after:
N : ℕ
hN : 64 ≤ N
⊢ 2 < √(log ↑N)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case refine_1.refine_2
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
x✝¹ : b₁ ∈ ↑B
b₂ : G
x✝ : b₂ ∈ ↑B
h : (fun b ↦ (a / b, c / b)) b₁ = (fun b ↦ (a / b, c / b)) b₂
⊢ b₁ = b₂

Tactic:
exact div_right_injective (Prod.ext_iff.1 h).1

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(C * B)

Tactic:
by
  simpa using ruzsa_triangle_inequality_mulInv_mulInv_mulInv A B⁻¹ C

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

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
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))
⊢ rexp (-2 * √(log ↑N)) ≤ ↑N ^ (-(2 / ↑n))

Tactic:
rw [← le_log_iff_exp_le (rpow_pos_of_pos hN₀ _), log_rpow hN₀, ← le_div_iff₀, mul_div_assoc,
      div_sqrt, neg_mul, neg_le_neg_iff, div_mul_eq_mul_div, div_le_iff₀ hn]

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))
⊢ 2 * √(log ↑N) ≤ 2 * ↑n

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))
⊢ 0 < √(log ↑N)