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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst✝ : Unique ι
X S : C
f : X ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra fun x ↦ f
α : D₁ ⟶ D₂
⊢ (𝟭 (F.DescentDataAsCoalgebra fun x ↦ f)).map α ≫ (isoMk (fun i ↦ eqToIso ⋯) ⋯).hom =
    (isoMk (fun i ↦ eqToIso ⋯) ⋯).hom ≫
      ({ obj := fun D ↦ { A := D.obj default, a := D.hom default default, counit := ⋯, coassoc := ⋯ },
              map := fun {X_1 Y} φ ↦ { f := φ.hom default, h := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun A ↦ { obj := fun x ↦ A.A, hom := fun x x_1 ↦ A.a, counit := ⋯, coassoc := ⋯ },
              map := fun {X_1 Y} φ ↦ { hom := fun i ↦ φ.f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
        α

Tactic:
by
      ext i
      obtain rfl := Subsingleton.elim i default
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
⊢ ∀ (E_1 : Multifork (F.multicospanIndex G)) (m : E_1.pt ⟶ (F.multifork G).pt),
    (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = E_1.ι i) →
      m = Multifork.IsLimit.lift hE (fun a ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯

Tactic:
intro t m hm

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
⊢ m = Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : Over (X i)
q : Z ⟶ Over.mk (𝟙 (X i))
hq : (sieve f f' i).arrows q
⊢ (sieve f f' i).arrows (Over.homMk Z.hom ⋯)

Tactic:
by
      convert! hq
      ext
      simpa using (Over.w q).symm

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ invMap ≫ f.hom.app W ≫ G.obj.map I.f.op = G.obj.map I.f.op

Tactic:
← f.hom.naturality,

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ invMap ≫ F.obj.map I.f.op ≫ f.hom.app (op I.Y) = G.obj.map I.f.op
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ mor w φ (p ≫ f₁) g ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            mor w φ (p ≫ f₂) g ⋯ ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)

Tactic:
mor_eq _ _ _ _ (by grind) (p ≫ q) _ (by grind) rfl,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ D₁.hom (p ≫ q) (p ≫ f₁) (g ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) g (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫ D₂.hom (p ≫ q) (g ≫ p' j) (p ≫ f₁) ⋯ ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            mor w φ (p ≫ f₂) g ⋯ ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ D₁.hom (p ≫ q) (p ≫ f₁) (g ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) g (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫ D₂.hom (p ≫ q) (g ≫ p' j) (p ≫ f₁) ⋯ ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            mor w φ (p ≫ f₂) g ⋯ ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)

Tactic:
mor_eq _ _ _ _ (by grind) (p ≫ q) _ (by grind) rfl,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ D₁.hom (p ≫ q) (p ≫ f₁) (g ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) g (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫ D₂.hom (p ≫ q) (g ≫ p' j) (p ≫ f₁) ⋯ ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            (D₁.hom (p ≫ q) (p ≫ f₂) (g ≫ p' j) ⋯ ⋯ ≫
                pullHom (φ.hom j) g (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫ D₂.hom (p ≫ q) (g ≫ p' j) (p ≫ f₂) ⋯ ⋯) ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).IsPullback ↔ (sq.op.map F.obj).IsPullback

Tactic:
refine Square.IsPullback.iff_of_equiv _ _
    (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
    (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
    (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
    (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv) ?_ ?_ ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₂) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₁₂) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₃) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₁₃) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₂₄) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₂₄) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv)

case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      ⇑(ConcreteCategory.hom (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₃₄) =
    ⇑(ConcreteCategory.hom (sq.op.map F.obj).f₃₄) ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv)
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
this : (pullFunctor F ⋯).Faithful
⊢ (pullFunctor F ⋯).FullyFaithful

Tactic:
have := full_pullFunctor F w hf'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
this✝ : (pullFunctor F ⋯).Faithful
this : (pullFunctor F ⋯).Full
⊢ (pullFunctor F ⋯).FullyFaithful
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₁ : (presheafHom F G).obj (op X)
⊢ ∀ (y₂ : (presheafHom F G).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Tactic:
y₂

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)
⊢ x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
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
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
pb : IsPullback (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
this : IsPullback m.hom ((isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F.obj) χ'.hom (truth J).hom
⊢ IsPullback m.hom ((isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F.obj) (χ'.hom ≫ (closedSieves J).ι)
    (Presheaf.truth C)

Tactic:
simpa using this.paste_horiz pb

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
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
⊢ Nonempty (Abelian.AbelianStruct f₁)

Tactic:
by
    obtain ⟨X₃, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map f₁)
    have : admissibleMorphism ι f₁ := by simp [hA]
    obtain ⟨K, Q, α, β, γ, hT'⟩ := this f₂ f₃ hT
    have := epi_πQ hι hT hT'
    obtain ⟨I, i, δ, hI⟩ := exists_distinguished_triangle_of_epi hι hA (πQ f₂ β)
    have H := someOctahedron (show f₂ ≫ β = ι.map (πQ f₂ β) by simp)
      (rot_of_distTriang _ hT) (rot_of_distTriang _ hT')
      (rot_of_distTriang _ hI)
    obtain ⟨m₁, hm₁⟩ : ∃ (m₁ : X₁ ⟶ I), (shiftFunctor C (1 : ℤ)).map (ι.map m₁) = H.m₁ :=
      ⟨(ι ⋙ shiftFunctor C (1 : ℤ)).preimage H.m₁, Functor.map_preimage (ι ⋙ _) _⟩
    obtain ⟨m₃ : ι.obj I ⟶ (ι.obj K)⟦(1 : ℤ)⟧, hm₃⟩ :
        ∃ m₃, (shiftFunctor C (1 : ℤ)).map m₃ = H.m₃ :=
      ⟨(shiftFunctor C (1 : ℤ)).preimage H.m₃, Functor.map_preimage _ _⟩
    have Hmem : Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃) ∈ distTriang C := by
      rw [rotate_distinguished_triangle, ← Triangle.shift_distinguished_iff _ 1]
      refine isomorphic_distinguished _ H.mem _ ?_
      exact Triangle.isoMk _ _ (-(Iso.refl _)) (Iso.refl _) (Iso.refl _)
    exact ⟨{
      kernelFork := _
      isLimitKernelFork := isLimitKernelFork hι hT hT'
      cokernelCofork := _
      isColimitCokernelCofork := isColimitCokernelCofork hι hT hT'
      image := _
      imageι := _
      imageπ := _
      ι_imageπ := _
      imageι_π := _
      imageIsCokernel := isColimitCokernelCoforkOfDistTriang hι _ _ _ Hmem
      imageIsKernel := isLimitKernelForkOfDistTriang hι _ _ _ hI
      fac := (ι ⋙ shiftFunctor C (1 : ℤ)).map_injective (by simpa [hm₁] using H.comm₂) }⟩

Goal state after:
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ↑(#s)
⊢ ∃ y ∈ t, b ≤ ↑(#({x ∈ s | f x = y}))

Tactic:
simp_rw [cast_card] at hb ⊢
  exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb

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

Goal state before:
pp: x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 2 ≤ x * (1 - 2 / rexp 1)

pp: x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 0 < 2

pp: x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 2 ≠ 0

Tactic:
← div_le_iff₀ this

Goal state after:
x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 2 / (1 - 2 / rexp 1) ≤ x

x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 0 < 2

x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
this : 0 < 1 - 2 / rexp 1
⊢ 2 ≠ 0
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
hC : C.Nonempty
hCA : C ⊆ A
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #C)

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
hC : C.Nonempty
hCA : C ⊆ A
⊢ ↑(#(B ^ m / B ^ n)) * ↑(#C) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A) * ↑(#C)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
⊢ A * A ⊆ A

Tactic:
obtain ⟨x, hx⟩ : ∃ x : G, A * A ⊆ x • A := by
      obtain ⟨K, hK, hKA⟩ := hA.sq_covBySMul
      simp only [Nat.cast_le_one, Finset.card_le_one_iff_subset_singleton,
        Finset.subset_singleton_iff] at hK
      obtain ⟨x, rfl | rfl⟩ := hK
      · simp [hA.nonempty.ne_empty] at hKA
      · rw [Finset.coe_singleton, singleton_smul, sq] at hKA
        use x

Goal state after:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
⊢ A * A ⊆ A
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ A * A ⊆ x • A

Tactic:
by assumption

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : ¬a = ⊥
⊢ P ≤ indiscrete h

Tactic:
· exact fun b hb ↦ ⟨a, mem_singleton_self _, P.le hb⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
⊢ P ≤ if ha : a = ⊥ then (Finpartition.empty α).copy ⋯ else indiscrete ha

Tactic:
split_ifs with h
    · intro x hx
      simpa [h, P.ne_bot hx] using P.le hx
    · exact fun b hb ↦ ⟨a, mem_singleton_self _, P.le hb⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ p ∈ (combine P ha).parts, f p = ∑ i ∈ I, ∑ p ∈ (P i).parts, f p

Tactic:
simp_rw [combine]
  refine Finset.sum_biUnion fun i hi j hj hij => ?_
  rw [Function.onFun, Finset.disjoint_left]
  intro p hpi hpj
  have hp_disj : Disjoint p p := (ha.pairwiseDisjoint hi hj hij).mono ((P i).le hpi) ((P j).le hpj)
  exact (P i).ne_bot hpi (disjoint_self.mp hp_disj)

Goal state after:
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
Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ P.parts.attach.sup Subtype.val = a

Tactic:
rw [Finset.sup_attach (f := fun x => x), ← Function.id_def, P.sup_parts]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ((fun i ↦ Q ↑i ⋯) ⟨b, hb⟩).parts → a_1 ∉ ((fun i ↦ Q ↑i ⋯) ⟨c, hc⟩).parts

Tactic:
rintro d hdb hdc

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
d : α
hdb : d ∈ ((fun i ↦ Q ↑i ⋯) ⟨b, hb⟩).parts
hdc : d ∈ ((fun i ↦ Q ↑i ⋯) ⟨c, hc⟩).parts
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ #({i ∈ ⊥.parts | #i = 0 + 1}) = b

Tactic:
simpa [Finset.filter_true_of_mem] using hs.symm

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ ↑(#A) * (2 * ↑(#A)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Tactic:
by
    rw [mul_left_comm, ← sq]
    convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
      <;> ring

Goal state after: