mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
⊢ ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ := (isCardinalFilteredGenerator_isCardinalPresentable
    (CardinalDirectedPoset κ₁) κ₂).exists_colimitsOfShape (setCardinalLT κ₁ X)
  have : IsCardinalFiltered J κ₁ := .of_le _ h
  have hp (j : J) : HasCardinalLT (p.diag.obj j).obj κ₂ := by
    rw [← CardinalDirectedPoset.isCardinalPresentable_iff _ h]
    exact p.prop_diag_obj j
  -- For each `x : X`, we choose `j : J` in such a way that the singleton
  -- `{x}` belongs to the image of `p.diag.obj j` in `SetCardinalLT κ₁ X`.
  choose j y hy using fun x ↦ Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (forget (CardinalDirectedPoset κ₁)) p.isColimit)
    (SetCardinalLT.singleton κ₁ x)
  dsimp at y hy
  -- The expected cofinal set `A` will be the range of `p.ι.app j'`
  -- where `j' : J` is such that for any `x : X`, there is a map `j x ⟶ j'`
  let j' := IsCardinalFiltered.max j hX
  let y' (x : X) : (p.diag.obj j').obj :=
    p.diag.map (IsCardinalFiltered.toMax j hX x) (y x)
  have hy' (x : X) : p.ι.app j' (y' x) = SetCardinalLT.singleton κ₁ x := by
    rw [← hy, ← p.w (IsCardinalFiltered.toMax j hX x)]
    rfl
  refine ⟨Set.range (p.ι.app j'), (hp j').of_surjective _
    (Set.rangeFactorization_surjective (f := p.ι.app j')), fun ⟨B, hB⟩ ↦ ?_⟩
  let j'' := IsCardinalFiltered.max (fun b ↦ y' b.val) hB
  refine ⟨_, ⟨j'', rfl⟩, fun b hb ↦ ?_⟩
  have : y' b ≤ j'' := (leOfHom (IsCardinalFiltered.toMax (fun b ↦ y' b.val) hB ⟨b, hb⟩) :)
  refine (p.ι.app j').hom.hom.monotone this ?_
  convert Set.mem_singleton b
  exact Subtype.ext_iff.1 (hy' b)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
this :
  ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → ↑(transfiniteIterate (φ Y m) j A)),
    HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
⊢ IsCardinalFiltered (↑(⋃ j, transfiniteIterate (φ Y m) j A)) κ₁

Tactic:
refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_)

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
this :
  ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → ↑(transfiniteIterate (φ Y m) j A)),
    HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
K : Type w
f : K → ↑(⋃ j, transfiniteIterate (φ Y m) j A)
hK : #K < κ₁
⊢ ∃ j, ∀ (k : K), f k ≤ j
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ (Presieve.singleton h).FactorsThruAlong S f

Tactic:
intro W g hg
      cases hg
      refine ⟨Z, i, π, ⟨?_, this⟩⟩
      cases hπ
      rw [Presieve.ofArrows_pUnit]
      exact Presieve.singleton.mk

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ (coherentCoverage C).coverings Y
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

Tactic:
| of Y T hS =>

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
T : Presieve Y
hS : T ∈ (regularCoverage C).coverings Y
⊢ ∃ Y_1 π, EffectiveEpi π ∧ (Sieve.generate T).arrows π

Tactic:
| of Y T hS =>

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)
hc : IsColimit c
i : c.pt ≅ (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim :=
  hc.coconePointUniqueUpToIso (pointwiseIsColimit (G ⋙ sheafToPresheaf (extensiveTopology C) A))
⊢ Presheaf.IsSheaf (extensiveTopology C) c.pt

Tactic:
rw [Presheaf.isSheaf_of_iso_iff i]

Goal state after:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)
hc : IsColimit c
i : c.pt ≅ (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim :=
  hc.coconePointUniqueUpToIso (pointwiseIsColimit (G ⋙ sheafToPresheaf (extensiveTopology C) A))
⊢ Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
x✝¹ : C
x✝ : x✝¹ ⟶ X
hh : Presieve.ofArrows Y π x✝
⊢ S.arrows x✝

Tactic:
cases hh

Goal state after:
case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ S.arrows (π i✝)
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
⊢ F.IsStackFor R.arrows

Tactic:
isStackFor_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
⊢ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
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₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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 : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
        (F.map p.op.toLoc).toFunctor.map ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (φ.hom i₂)) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)

Tactic:
mapComp'_inv_naturality

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
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
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 : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
          (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Cᵒᵖ ⥤ Type u_3
⊢ Nonempty (IsLimit (E.saturate.multifork F)) ↔ Presieve.IsSheafFor F E.presieve₀

Tactic:
by
  rw [Multifork.isLimit_types_iff, Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← Function.Bijective.of_comp_iff' (E.sectionsSaturateEquiv F).symm.bijective]
  rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f (𝒰.f i))
i : (pullback₁ f 𝒰).I₀
⊢ (pullback₁ f 𝒰).f i ≫ f ≫ 𝒰.glueMorphisms (fun i ↦ inv (pullback.snd f (𝒰.f i)) ≫ pullback.fst f (𝒰.f i)) ⋯ =
    (pullback₁ f 𝒰).f i ≫ 𝟙 X

Tactic:
simp [pullback.condition_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : J.IsLocalSite
X✝ : C
R : Sieve X✝
hR : R ∈ J X✝
x : (shrinkCoyoneda.{w, v, u}.obj (op (⊤_ C))).obj X✝
⊢ (ConcreteCategory.hom ((shrinkCoyoneda.{w, v, u}.obj (op (⊤_ C))).map (shrinkCoyonedaObjObjEquiv x)))
      (shrinkCoyonedaObjObjEquiv.symm (𝟙 (unop (op (⊤_ C))))) =
    x

Tactic:
shrinkCoyoneda_obj_map_shrinkCoyonedaObjObjEquiv_symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : J.IsLocalSite
X✝ : C
R : Sieve X✝
hR : R ∈ J X✝
x : (shrinkCoyoneda.{w, v, u}.obj (op (⊤_ C))).obj X✝
⊢ shrinkCoyonedaObjObjEquiv.symm (𝟙 (unop (op (⊤_ C))) ≫ shrinkCoyonedaObjObjEquiv x) = x
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
R : Presieve S
hR₁ : F.IsStackFor R
J : GrothendieckTopology C
hR₂ : Sieve.generate R ∈ J S
inst✝ : F.IsPrestack J
R' : Presieve S
h : R ≤ R'
⊢ F.IsStackFor R'

Tactic:
obtain ⟨ι, _, f, rfl⟩ := R.exists_eq_ofArrows
  obtain ⟨ι', _, f', rfl⟩ := R'.exists_eq_ofArrows
  rw [isStackFor_ofArrows_iff] at hR₁ ⊢
  exact DescentData.isEquivalence_toDescentData_of_sieve_le _ hR₂ (Sieve.generate_mono h)

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
Q : Subfunctor F := K.subsheafify 𝒮
this : ∀ (Z : C), _root_.Small.{max u v, w} (Q.toFunctor.obj (Opposite.op Z))
hQ : Presieve.IsSheaf J Q.toFunctor
x' : Presieve.FamilyOfElements Q.toFunctor S.arrows := fun Z g hg ↦ ⟨x g hg, ⋯⟩
ht₁' : t₁ ∈ Q.obj (Opposite.op X)
ht₂' : t₂ ∈ Q.obj (Opposite.op X)
⊢ t₁ = t₂

Tactic:
have : (⟨t₁, ht₁'⟩ : Q.obj _) = ⟨t₂, ht₂'⟩ :=
      (hQ _ hS).isSeparatedFor x' ⟨_, ht₁'⟩ ⟨_, ht₂'⟩ (.of_mono Q.ι ht₁) (.of_mono Q.ι ht₂)

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
Q : Subfunctor F := K.subsheafify 𝒮
this✝ : ∀ (Z : C), _root_.Small.{max u v, w} (Q.toFunctor.obj (Opposite.op Z))
hQ : Presieve.IsSheaf J Q.toFunctor
x' : Presieve.FamilyOfElements Q.toFunctor S.arrows := fun Z g hg ↦ ⟨x g hg, ⋯⟩
ht₁' : t₁ ∈ Q.obj (Opposite.op X)
ht₂' : t₂ ∈ Q.obj (Opposite.op X)
this : ⟨t₁, ht₁'⟩ = ⟨t₂, ht₂'⟩
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S' : SubmonoidFunctor M'
S : Set (SubmonoidFunctor M)
U V : C
f : U ⟶ V
⊢ ⨆ F ∈ S, F.obj U ≤ ⨆ i ∈ S, Submonoid.comap (MonCat.Hom.hom (M.map f)) (i.obj V)

Tactic:
exact iSup₂_mono fun F _ ↦ F.map f

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

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

Tactic:
isStackFor_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve S
h : (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
⊢ (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
f : X ⟶ Ω
⊢ h.homEquiv f = (Subobject.pullback f).obj h.Ω₀

Tactic:
simpa using! h.homEquiv_comp f (𝟙 _)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
hχ' : IsPullback m ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F) χ' (truth C)
⊢ χ' = χ m

Tactic:
by
  ext X x
  simp only [IsPullback.iff_app, Functor.const_obj_obj, Functor.sieves_obj,
    Functor.isTerminalConst_from_app, truth_app, Types.isPullback_iff,
    Types.isTerminalPUnit_from_apply, and_true, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
    forall_const, forall_and] at hχ'
  obtain ⟨h₁, h₂, h₃⟩ := hχ'
  refine Sieve.ext fun Y f => ?_
  simp only [χ_app, Opposite.op_unop]
  rw [Sieve.mem_iff_pullback_eq_top, ← Quiver.Hom.unop_op f]
  dsimp
  have := ConcreteCategory.congr_hom (Functor.sieves_map C (f.op)) (χ'.app X x)
  rw [← dsimp% this, ← dsimp% NatTrans.naturality_apply χ' f.op x]
  constructor
  · intro h
    obtain ⟨z, hz⟩ := h₃ _ _ h
    use z, hz.symm
  · rintro ⟨a, h⟩
    rw [h]
    simpa using congr($(h₁ (.op Y)) a)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b

Tactic:
have := (hf.bijOn.injOn.mono hAs).bijOn_image (f := f)

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
this : BijOn f A (f '' A)
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b
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 : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this✝ : (map (g ∘ f) s).prod = (map g (map f t)).prod
this : s.prod = (map (g ∘ f) t).prod
x : α
hx : x ∈ t
⊢ (g ∘ f) x = id x

Tactic:
exact h.1 (htA hx)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
a : E
ha : a ∈ frontier s
b : E
hb : b ∈ frontier s
c : E
hc : c ∈ frontier s
habc : a + c = b + b
⊢ (1 / 2) • a + (1 / 2) • c = b

Tactic:
rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by simp), two_smul]

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

Goal state before:
pp: n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : ∑ x, x₁ x.succ * d ^ ↑x = ∑ x, x₂ x.succ * d ^ ↑x ∨ d = 0
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
exact ⟨this, h.resolve_right (pos_of_gt (hx₁ 0)).ne'⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
⊢ CovBySMul N (K * L) A C

Tactic:
have := hAB.nonneg

Goal state after:
M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
this : 0 ≤ K
⊢ CovBySMul N (K * L) A C
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : ℝ
A B : Set G
hA : A.Finite
hB : B.Finite
hB₀ : B.Nonempty
hK : ↑(Nat.card ↑(A * B)) ≤ K * ↑(Nat.card ↑B)
⊢ ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite

Tactic:
by
  lift A to Finset G using hA
  lift B to Finset G using hB
  classical
  obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)
  exact ⟨F, by norm_cast; simp [*]⟩

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * 1.38 ≤ √(log ↑N)

pp: N : ℕ
hN : 4096 ≤ N
⊢ 0 < 1.38

Tactic:
· norm_num [le_sqrt_log hN]

Goal state after:
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 1.38
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / ↑⌈√(log ↑N)⌉₊

pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

pp: case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

pp: case h₁
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹

Tactic:
· grw [ceil_lt_mul]
    · rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]
      · norm_num [le_sqrt_log hN]
      · norm_num1
    · rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
      refine log_pos ?_
      rw [one_lt_cast]
      exact hN.trans_lt' (by norm_num1)
    apply le_sqrt_of_sq_le
    have : (12 : ℕ) * log 2 ≤ log N := by
      rw [← log_rpow zero_lt_two, rpow_natCast]
      exact log_le_log (by positivity) (mod_cast hN)
    refine le_trans ?_ this
    rw [← div_le_iff₀']
    · exact log_two_gt_d9.le.trans' (by norm_num1)
    · norm_num1

Goal state after:
case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

case h₁
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
this : A * A ⊆ A
x✝ : G
hx : x✝ ∈ A
⊢ x✝⁻¹ ∈ A

Tactic:
by rwa [← hA.inv_eq_self, inv_mem_inv]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2

Tactic:
rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
⊢ {x | x.1.Nonempty ∧ x.2.Nonempty}.WellFoundedOn DevosMulRel

Tactic:
refine wellFounded_lt.onFun.wellFoundedOn.prod_lex_of_wellFoundedOn_fiber fun n ↦
    Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber ?_ fun n ↦
      wellFounded_lt.onFun.wellFoundedOn

Goal state after:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
n : ℕ
⊢ ({x | x.1.Nonempty ∧ x.2.Nonempty} ∩ (fun x ↦ #(x.1 * x.2)) ⁻¹' {n}).WellFoundedOn
    ((fun x1 x2 ↦ x1 > x2) on fun x ↦ #x.1 + #x.2)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h✝ : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
i : Fin (m + 1 + 1)
h : ε i = 0
⊢ False

Tactic:
by simpa [h] using hε i

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: G : Type u_1
inst✝ : AddCommMonoid G
x₁ y₁ x₂ y₂ : G
⊢ ¬IsCorner ∅ x₁ y₁ x₂ y₂

Tactic:
simp [isCorner_iff]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
i : Fin m
h : ε i = 0
⊢ False

Tactic:
by simpa [h] using hε i

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

Goal state before:
pp: case h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) ↔ s(x✝, y✝) ∈ ⇑f.sym2Map '' G.edgeSet

Tactic:
Set.mem_image

Goal state after:
case h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
⊢ (∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝) ↔ ∃ x ∈ G.edgeSet, f.sym2Map x = s(x✝, y✝)