mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ℳ : ι → Submodule R M
inst✝² : Decomposition ℳ
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
h : ∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype
i : ι
⊢ (f ∘ₗ ↑(decomposeLinearEquiv ℳ).symm) ∘ₗ lof R ι (fun i ↦ ↥(ℳ i)) i =
    (g ∘ₗ ↑(decomposeLinearEquiv ℳ).symm) ∘ₗ lof R ι (fun i ↦ ↥(ℳ i)) i

Tactic:
by
      simp_rw [LinearMap.comp_assoc, decomposeLinearEquiv_symm_comp_lof ℳ i, h]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ↑(0 0) = 0

Tactic:
zero_apply,

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ↑0 = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ Q.toMatrix'.transpose i j = Q.toMatrix' i j

Tactic:
rw [toMatrix', Matrix.transpose_apply, LinearMap.toMatrix₂'_apply, LinearMap.toMatrix₂'_apply,
    ← QuadraticMap.associated_isSymm]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ reverse ∘ₗ involute.toLinearMap = involute.toLinearMap ∘ₗ reverse

Tactic:
ext x
  simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply]
  induction x using CliffordAlgebra.induction with
  | algebraMap => simp
  | ι => simp
  | mul a b ha hb => simp only [ha, hb, reverse.map_mul, map_mul]
  | add a b ha hb => simp only [ha, hb, reverse.map_add, map_add]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
n : ℕ
x : Fin n → ↑M
⊢ (ConcreteCategory.hom (map f n)) (mk x) = mk (⇑(ConcreteCategory.hom f) ∘ x)

Tactic:
by
  apply exteriorPower.map_apply_ιMulti

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ LeftInverse ⇑(map g) ⇑(map f) ↔ LeftInverse ⇑g ⇑f

Tactic:
by
  refine ⟨fun h x => ?_, fun h => CliffordAlgebra.leftInverse_map_of_leftInverse _ _ h⟩
  simpa using h (ι _ x)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
hgm : ∃ c, (c.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
⊢ m ∈ span R (range u)

Tactic:
obtain ⟨cm, hm⟩ := hgm

Goal state after:
ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
⊢ m ∈ span R (range u)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a.refine_1
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ range (⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) ⊆ s

Tactic:
Set.range_comp,

Goal state after:
case a.refine_1
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ ⇑ExteriorAlgebra.ιInv '' range (Subtype.val ∘ f) ⊆ s
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ (Λ.chainComplexMap (f ≫ g)).f n = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f n

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    obtain _ | n := n
    all_goals
      dsimp
      simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]
      congr 1
      cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
⊢ IsConnected (StructuredArrow { as := default } F) ↔ F.Final

Tactic:
refine ⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
x✝ : IsConnected (StructuredArrow { as := default } F)
⊢ ∀ (d : Discrete T), IsConnected (StructuredArrow d F)
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
⊢ IsConnected (CostructuredArrow F { as := default }) ↔ F.Initial

Tactic:
refine ⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
x✝ : IsConnected (CostructuredArrow F { as := default })
⊢ ∀ (d : Discrete T), IsConnected (CostructuredArrow F d)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : CartesianMonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ F).inv.app j = (ρ_ (F.obj j)).inv

Tactic:
by
  rw [← cancel_mono ((ρ_ (F.obj j)).hom), Iso.inv_hom_id, ← rightUnitor_hom_app,
    Iso.inv_hom_id_app]

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ F.partialLeftAdjointMap g ≫ F.partialLeftAdjointHomEquiv.symm f = F.partialLeftAdjointHomEquiv.symm (g.hom ≫ f)

Tactic:
by
  rw [Equiv.eq_symm_apply, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map,
    assoc, ← partialLeftAdjointHomEquiv_comp, id_comp, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ ∀ (j : WalkingParallelPair), (pushforward φ).leftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj j)

Tactic:
rintro (_ | _)

Goal state after:
case zero
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).leftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.zero)

case one
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).leftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.one)
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G G' : Subfunctor F✝
S : Set (Subfunctor F✝)
U✝ V✝ : C
f : U✝ ⟶ V✝
x : F✝.obj U✝
F : Subfunctor F✝
h : F ∈ S
h' : x ∈ (fun T ↦ T.obj U✝) F
⊢ ∃ i ∈ S, (hom (F✝.map f)) x ∈ i.obj V✝

Tactic:
exact ⟨_, h, F.map f h'⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)]
      ((ConcreteCategory.hom ((R ⋙ forget₂ CommRingCat RingCat).map f)) a • (ConcreteCategory.hom (M₂.map f)) m₂) =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂

Tactic:
TensorProduct.tmul_smul (r := R.map f a)

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (R.map f)) a •
      (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
T Y : C
i : ι
v : T ⟶ Z i
hv : Ti (g i) ⋯ v
⊢ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) (fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) (v ≫ g i)

Tactic:
hp

Goal state after:
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
T Y : C
i : ι
v : T ⟶ Z i
hv : ofArrows (W (g i) ⋯) (p (g i) ⋯) v
⊢ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) (fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) (v ≫ g i)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y : C
ij : (i : ι) × κ (g i) ⋯
⊢ Ti (g ij.fst) ⋯ (p (g ij.fst) ⋯ ij.snd) ∧ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst = p (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
hp

Goal state after:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
Y : C
ij : (i : ι) × κ (g i) ⋯
⊢ ofArrows (W (g ij.fst) ⋯) (p (g ij.fst) ⋯) (p (g ij.fst) ⋯ ij.snd) ∧
    p (g ij.fst) ⋯ ij.snd ≫ g ij.fst = p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
i : s.pt
⊢ (hom g) ((hom s.ι) i) = (hom h) ((hom s.ι) i)

Tactic:
by apply congr_hom s.condition i

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst,
      ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd⟩ ∈
    (pullbackArrows b s).uncurry

Tactic:
exact ⟨Y, u, hu⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
⊢ ∀ (h₁ : (generate R).arrows f₁✝) (h₂ : (generate R).arrows f₂✝),
    g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁✝ h₁) =
        (ConcreteCategory.hom (P.map g₂✝.op)) (x.sieveExtend f₂✝ h₂)

Tactic:
h₁

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
hx : x.Compatible
Y₁✝ Y₂✝ Z✝ : C
g₁✝ : Z✝ ⟶ Y₁✝
g₂✝ : Z✝ ⟶ Y₂✝
f₁✝ : Y₁✝ ⟶ X
f₂✝ : Y₂✝ ⟶ X
h₁ : (generate R).arrows f₁✝
⊢ ∀ (h₂ : (generate R).arrows f₂✝),
    g₁✝ ≫ f₁✝ = g₂✝ ≫ f₂✝ →
      (ConcreteCategory.hom (P.map g₁✝.op)) (x.sieveExtend f₁✝ h₁) =
        (ConcreteCategory.hom (P.map g₂✝.op)) (x.sieveExtend f₂✝ h₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
⊢ ∀ (h₁ : S.arrows f₁) (h₂ : S.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ → (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)

Tactic:
h₁

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
⊢ ∀ (h₂ : S.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ → (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
⊢ ∀ (h₁ : Presieve.functorPullback F T f₁) (h₂ : Presieve.functorPullback F T f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.op ⋙ P).map g₁.op)) (FamilyOfElements.functorPullback F x f₁ h₁) =
        (ConcreteCategory.hom ((F.op ⋙ P).map g₂.op)) (FamilyOfElements.functorPullback F x f₂ h₂)

Tactic:
h₁

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
⊢ ∀ (h₂ : Presieve.functorPullback F T f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.op ⋙ P).map g₁.op)) (FamilyOfElements.functorPullback F x f₁ h₁) =
        (ConcreteCategory.hom ((F.op ⋙ P).map g₂.op)) (FamilyOfElements.functorPullback F x f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
⊢ ∀ (h₁ : R f₁) (h₂ : R f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (Q.map g₁.op)) (x.map f f₁ h₁) = (ConcreteCategory.hom (Q.map g₂.op)) (x.map f f₂ h₂)

Tactic:
h₁

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
⊢ ∀ (h₂ : R f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (Q.map g₁.op)) (x.map f f₁ h₁) = (ConcreteCategory.hom (Q.map g₂.op)) (x.map f f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
⊢ (x.map f).IsAmalgamation ((ConcreteCategory.hom (f.app (op X))) t)

Tactic:
by
  intro Y g hg
  dsimp [FamilyOfElements.map]
  change (f.app _ ≫ Q.map _) _ = _
  rw [← f.naturality, comp_apply, h g hg]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
⊢ ∀ (h₁ : R f₁) (h₂ : R f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ → (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)

Tactic:
h₁

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
⊢ ∀ (h₂ : R f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ → (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.Compatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
by
  rw [Arrows.pullbackCompatible_iff]
  constructor
  · intro t
    ext ij
    simpa [firstMap, secondMap] using t ij.1 ij.2
  · intro t i j
    apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t
    simpa [firstMap, secondMap] using t

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
⊢ x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
h₁

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hs : ∀ (c : Cone (S.arrows.diagram.op ⋙ P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
⊢ x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F : Sheaf J A
X : C
H : ⊥ ∈ J X
⊢ IsTerminal (F.obj.obj (op X))

Tactic:
refine @IsTerminal.ofUnique _ _ _ ?_
  intro Y
  choose t h using F.2 Y _ H (by tauto) (by tauto)
  exact ⟨⟨t⟩, fun a => h.2 a (by tauto)⟩

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
· obtain ⟨t, hA, ht⟩ := h (fun i ↦ x (π i) (ofArrows.mk _))
      (fun i j Z gi gj ↦ hx gi gj (ofArrows.mk _) (ofArrows.mk _))
    exact ⟨t, fun Y f ⟨i⟩ ↦ hA i, fun y hy ↦ ht y (fun i ↦ hy (π i) (ofArrows.mk _))⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : Y ⟶ X
inst✝ : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun i ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P fun i ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ = g₂ ≫ g i₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)

Tactic:
replace h := h =≫ inv f
        simp only [Category.assoc] at h
        exact s.property _ _ _ _ _ h

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
⊢ ∀ (h₁ : (G.sieveOfSection s).arrows f₁) (h₂ : (G.sieveOfSection s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (G.toFunctor.map g₁.op)) (G.familyOfElementsOfSection s f₁ h₁) =
        (ConcreteCategory.hom (G.toFunctor.map g₂.op)) (G.familyOfElementsOfSection s f₂ h₂)

Tactic:
h₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
⊢ ∀ (h₂ : (G.sieveOfSection s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (G.toFunctor.map g₁.op)) (G.familyOfElementsOfSection s f₁ h₁) =
        (ConcreteCategory.hom (G.toFunctor.map g₂.op)) (G.familyOfElementsOfSection s f₂ h₂)