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

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) ≫ pullback.fst f g =
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.fst f g

pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) ≫ pullback.snd f g =
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.snd f g

Tactic:
<;>

Goal state after:
case h₀
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) ≫ pullback.fst f g =
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.fst f g

case h₁
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) ≫ pullback.snd f g =
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.snd f g
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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ IsPullback (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ pullback.fst (𝒰.f i ≫ f) g)
    (pullback.lift fst snd h ≫ pullback.fst f g) (𝒰.f i)

Tactic:
simpa using .of_hasPullback _ _

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

Goal state before:
pp: case fst
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ (↑(S.toPullbackObj P x)).1 = (↑(S.toPullbackObj P y)).1

pp: case snd
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ (↑(S.toPullbackObj P x)).2 = (↑(S.toPullbackObj P y)).2

Tactic:
<;>

Goal state after:
case fst
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ (↑(S.toPullbackObj P x)).1 = (↑(S.toPullbackObj P y)).1

case snd
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ (↑(S.toPullbackObj P x)).2 = (↑(S.toPullbackObj P y)).2
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
H : K.Generates J
F : Cᵒᵖ ⥤ Type w
h : Presieve.IsSheaf J F
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows

Tactic:
exact h _ (H.le_toPrecoverage _ hR)

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
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
f₂ : Y ⟶ X'' k₂
hf₁ : f₁ ≫ f'' k₁ = s
hf₂ : f₂ ≫ f'' k₂ = s
⊢ (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₁)).op.toLoc (q' k₁).op.toLoc (r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₁)))) ≫
      pullFunctorObjHom ⋯ D (f₁ ≫ f'' k₁) f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom w' (pullFunctorObj w D) (f₁ ≫ f'' k₁) f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₂))))

Tactic:
rw [pullFunctorObjHom_eq _ _ _ _ _ (s ≫ r) _ _ rfl,
        pullFunctorObjHom_eq _ _ _ _ _ (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂)]

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
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
⊢ (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₁)).op.toLoc (q' k₁).op.toLoc (r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₁)))) ≫
      (F.mapComp' (r' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ r' k₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj ((α ∘ β) k₁)) ≫
        D.hom (s ≫ r) (f₁ ≫ r' k₁) (f₂ ≫ r' k₂) ⋯ ⋯ ≫
          (F.mapComp' (r' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ r' k₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj ((α ∘ β) k₂)) =
    ((F.mapComp' (q' k₁).op.toLoc f₁.op.toLoc (f₁ ≫ q' k₁).op.toLoc ⋯).inv.toNatTrans.app
          ((pullFunctorObj w D).obj (β k₁)) ≫
        (pullFunctorObj w D).hom (s ≫ q) (f₁ ≫ q' k₁) (f₂ ≫ q' k₂) ⋯ ⋯ ≫
          (F.mapComp' (q' k₂).op.toLoc f₂.op.toLoc (f₂ ≫ q' k₂).op.toLoc ⋯).hom.toNatTrans.app
            ((pullFunctorObj w D).obj (β k₂))) ≫
      (F.map f₂.op.toLoc).toFunctor.map
        ((F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α (β k₂))))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case e'_2.refine_1
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
⊢ ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows ≤
    Presieve.ofArrows (fun i ↦ Over.mk i.obj.hom) fun i ↦ Over.homMk i.obj.hom ⋯

Tactic:
rintro X f (hf : R.arrows f.left)
    obtain ⟨X, g, rfl⟩ := Over.mk_surjective X
    obtain rfl : f = Over.homMk g := by ext; simpa using Over.w f
    exact Presieve.ofArrows.mk (ι := R.arrows.category) ⟨Over.mk g, hf⟩

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
⊢ HasSubobjectClassifier C → (Subobject.presheaf C).IsRepresentable

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
⊢ (Subobject.presheaf C).IsRepresentable → HasSubobjectClassifier C

Tactic:
<;>

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
⊢ HasSubobjectClassifier C → (Subobject.presheaf C).IsRepresentable

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
⊢ (Subobject.presheaf C).IsRepresentable → HasSubobjectClassifier C
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: case commfst
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m

pp: case commsnd
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)) ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω₀)).hom =
    (e.counitIso.app F).hom ≫ e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F))

pp: case commf
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (𝒞₁.χ (e.inverse.map m)) ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω)).hom =
    (e.counitIso.app G).hom ≫ e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

pp: case commg
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map 𝒞₁.truth ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω)).hom =
    (Iso.refl (e.functor.obj 𝒞₁.Ω₀)).hom ≫ e.functor.map 𝒞₁.truth

Tactic:
<;>

Goal state after:
case commfst
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m

case commsnd
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)) ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω₀)).hom =
    (e.counitIso.app F).hom ≫ e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F))

case commf
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (𝒞₁.χ (e.inverse.map m)) ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω)).hom =
    (e.counitIso.app G).hom ≫ e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

case commg
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map 𝒞₁.truth ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω)).hom =
    (Iso.refl (e.functor.obj 𝒞₁.Ω₀)).hom ≫ e.functor.map 𝒞₁.truth
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 : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
Z : C
f' : Z ⟶ Y
hf' :
  (Sieve.pullback f
        ((ConcreteCategory.hom
            (↾fun x ↦
              {
                arrows := fun Y f ↦
                  ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                downward_closed := ⋯ }))
          x)).arrows
    f'
⊢ (ConcreteCategory.hom (G.map f'.op)) ((ConcreteCategory.hom (G.map f.op)) x) =
    (ConcreteCategory.hom (G.map (f.op ≫ f'.op))) x

Tactic:
Functor.map_comp_apply

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
Z : C
f' : Z ⟶ Y
hf' :
  (Sieve.pullback f
        ((ConcreteCategory.hom
            (↾fun x ↦
              {
                arrows := fun Y f ↦
                  ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                downward_closed := ⋯ }))
          x)).arrows
    f'
⊢ (ConcreteCategory.hom (G.map f'.op)) ((ConcreteCategory.hom (G.map f.op)) x) =
    (ConcreteCategory.hom (G.map f'.op)) ((ConcreteCategory.hom (G.map f.op)) x)
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 : ℤ
⊢ P.triangEnvelope ≤ P.triangEnvelope.shift a

Tactic:
intro X hX

Goal state after:
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
hX : P.triangEnvelope X
⊢ P.triangEnvelope.shift a X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Heart

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
t : TStructure C
H : Type u'
inst✝² : Category.{v', u'} H
inst✝¹ : Preadditive H
inst✝ : t.Heart H
X : H
⊢ t.heart (t.ιHeart.obj X)

Tactic:
by
  rw [← t.essImage_ιHeart H]
  exact t.ιHeart.obj_mem_essImage X

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

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

pp: case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
⊢ b = c

Tactic:
<;>

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

case inr
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree s
ha : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
ha' : ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a
b c : α
hc : c = a ∨ c ∈ s
d : α
hd : d = a ∨ d ∈ s
h : b * d = c * c
hb : b ∈ s
⊢ b = c
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : {a, b}.prod = {c, d}.prod
⊢ ∀ ⦃x : α⦄, x ∈ {a, b} → x ∈ A

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : {a, b}.prod = {c, d}.prod
⊢ ∀ ⦃x : α⦄, x ∈ {c, d} → x ∈ A

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : {a, b}.prod = {c, d}.prod
⊢ ∀ ⦃x : α⦄, x ∈ {a, b} → x ∈ A

case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : {a, b}.prod = {c, d}.prod
⊢ ∀ ⦃x : α⦄, x ∈ {c, d} → x ∈ A
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : {a, b}.prod = {c, d}.prod
⊢ ∀ ⦃x : α⦄, x ∈ {a, b} → x ∈ A

Tactic:
simp [ha, hb, hc, hd]

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

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : {a, b}.prod = {c, d}.prod
⊢ ∀ ⦃x : α⦄, x ∈ {c, d} → x ∈ A

Tactic:
simp [ha, hb, hc, hd]

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ ∀ ⦃x : α⦄, x ∈ {a, b} → x ∈ A

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ ∀ ⦃x : α⦄, x ∈ {c, d} → x ∈ A

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ ∀ ⦃x : α⦄, x ∈ {a, b} → x ∈ A

case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ ∀ ⦃x : α⦄, x ∈ {c, d} → x ∈ A
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ ∀ ⦃x : α⦄, x ∈ {a, b} → x ∈ A

Tactic:
simp [ha, hb, hc, hd]

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

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanIso 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
⊢ ∀ ⦃x : α⦄, x ∈ {c, d} → x ∈ A

Tactic:
simp [ha, hb, hc, hd]

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

Goal state before:
pp: M N : ℕ
⊢ rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N

Tactic:
by
  simp_rw [rothNumberNat_def]
  rw [range_add_eq_union, ← addRothNumber_map_add_left (range N) M]
  exact addRothNumber_union_le _ _

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

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ addRothNumber (Iio k) ≤ rothNumberNat ↑k

Tactic:
open Fin.CommRing in -- TODO: should this be refactored to avoid needing the coercion?
  suffices h : Set.BijOn (Nat.cast : ℕ → Fin n.succ) (range k) (Iio k : Finset (Fin n.succ)) by
    exact (AddHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h
  refine ⟨?_, (CharP.natCast_injOn_Iio _ n.succ).mono (by simp), ?_⟩
  · simpa using! fun x ↦ natCast_strictMono (is_le k)
  simp only [Set.SurjOn, coe_Iio, Set.subset_def, Set.mem_Iio, Set.mem_image, lt_def, coe_range]
  exact fun x hx ↦ ⟨x, hx, by simp⟩

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

Goal state before:
pp: case e'_6
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ Iio ↑(k + 1) = Iic ↑k

pp: case e'_7
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ Iio (k + 1) = Iic k

Tactic:
<;>

Goal state after:
case e'_6
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ Iio ↑(k + 1) = Iic ↑k

case e'_7
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
⊢ Iio (k + 1) = Iic k
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 2 < rexp 1

pp: ⊢ 0 < rexp 1

Tactic:
<;>

Goal state after:
⊢ 2 < rexp 1

⊢ 0 < rexp 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ 3) * (69 / 50) ≤ √(log (2 ^ 12))

Tactic:
simp only [Real.log_pow, Nat.cast_ofNat]

Goal state after:
N : ℕ
hN : 4096 ≤ N
⊢ 3 * log 2 * (69 / 50) ≤ √(12 * log 2)