mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ (fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) = fun x ↦ y

Tactic:
ext
    rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem]
    exact Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n
k : ℕ
xv x : CliffordAlgebra Q
y : x ∈ ((ι Q).range ^ 2) ^ k * (ι Q).range ^ n.val
hx : CliffordAlgebra Q
hy : hx ∈ ((ι Q).range ^ 2) ^ k * (ι Q).range ^ n.val
ihx : motive x ⋯
ihy : motive hx ⋯
⊢ motive (x + hx) ⋯

Tactic:
| add x y hx hy ihx ihy =>

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (CliffordAlgebra Q)) r) ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
rx : CliffordAlgebra Q
h : rx ∈ (ι Q).range ^ ZMod.val 0
⊢ motive rx ⋯

Tactic:
obtain ⟨r, rfl⟩ := Submodule.mem_one.mp h

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 0 → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (CliffordAlgebra Q)) r) ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) (hy : y ∈ evenOdd Q 0),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
r : R
h : (Algebra.algebraMap R (CliffordAlgebra Q)) r ∈ (ι Q).range ^ ZMod.val 0
⊢ motive ((Algebra.algebraMap R (CliffordAlgebra Q)) r) ⋯
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
r✝ : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ r✝ • (g.compAlternatingMap (f 0)) 0 = r✝ • g ((f 0) 0)

Tactic:
LinearMap.compAlternatingMap_apply

Goal state after:
case algebraMap
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
r✝ : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ r✝ • g ((f 0) 0) = r✝ • g ((f 0) 0)
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ LinearIndependent R (u ∘ Sum.inl) ∧
    LinearIndependent R (u ∘ Sum.inr) ∧ Disjoint (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))

Tactic:
refine ⟨?_, LinearIndependent.of_comp S.g.hom hw, disjoint_span_sum hS hw huv⟩

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ LinearIndependent R (u ∘ Sum.inl)
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : ↑(M F)
⊢ r • (x + y) = r • x + r • y

Tactic:
obtain ⟨i, x, rfl⟩ := M.mk_surjective F x
    obtain ⟨j, y, rfl⟩ := M.mk_surjective F y
    rw [colimit_smul_mk_eq, colimit_smul_mk_eq,
      colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
      (IsFiltered.rightToMax i j), colimit_smul_mk_eq, smul_add,
      colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
      (IsFiltered.rightToMax i j), map_smul, map_smul]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ (F.obj j).map (f ≫ g) ≫
      colimit.ι (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).inv =
    (F.whiskerLeft (restriction R f)).app j ≫
      colimit.ι (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) j ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
              (colimMap (F.whiskerLeft (restriction R g)) ≫
                (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g)))
                    (F ⋙ evaluation R Z)).inv) ≫
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv

Tactic:
erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (f ≫ g)).hom),
      ι_preservesColimitIso_inv_assoc (G := ModuleCat.restrictScalars (R.map f).hom)]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ (F.obj j).map (f ≫ g) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (colimMap (F.whiskerLeft (restriction R g)) ≫
              (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ IsConnected C ↔ IsConnected D

Tactic:
isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} C,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔ IsConnected D
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ (∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁) →
    (∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
· intro h
    constructor
    · intro j₂
      obtain ⟨j₁, h₁⟩ := h j₂
      exact ⟨j₁, ⟨homOfLE h₁⟩⟩
    · intro _ c _ _
      exact ⟨c, 𝟙 _, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : C
x : ↑(M.obj (Opposite.op X))
⊢ (ConcreteCategory.hom ((freeYonedaEquiv.symm x).app (Opposite.op X)))
      (ModuleCat.freeMk (𝟙 (Opposite.unop (Opposite.op X)))) =
    x

Tactic:
simp [freeYonedaEquiv, freeHomEquiv, yonedaEquiv]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : ↑(M.obj (F.op.obj X✝))
⊢ (ModuleCat.Hom.hom (M.map (F.op.map (f ≫ g)))) x =
    (ModuleCat.Hom.hom
        (M.map (F.op.map f) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((F.op ⋙ R).map f))).map (M.map (F.op.map g)) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((F.op ⋙ R).map f)) (RingCat.Hom.hom ((F.op ⋙ R).map g))
                    (RingCat.Hom.hom ((F.op ⋙ R).map (f ≫ g))) ⋯).inv.app
              (ModuleCat.of ↑((F.op ⋙ R).obj Z✝) ↑(M.obj (F.op.obj Z✝)))))
      x

Tactic:
exact (M.congr_map_apply (F.op.map_comp f g) x).trans (by simp)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ J Y

Tactic:
Sieve.pullback_inter,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f R ⊓ Sieve.pullback f S ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Presieve Y
Z : C
h : Z ⟶ X
Y : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S f
hg : R hf g
fac : g ≫ f = h
⊢ Nonempty (S.BindStruct R h)

Tactic:
exact ⟨{ hf := hf, hg := hg, fac := fac, .. }⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) = R

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ≤ R

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ R ≤ ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
⊢ pushforward f (ofArrows U g) = ofArrows U fun x ↦ g x ≫ f

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
⊢ pushforward f (ofArrows U g) ≤ ofArrows U fun x ↦ g x ≫ f

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
⊢ (ofArrows U fun x ↦ g x ≫ f) ≤ pushforward f (ofArrows U g)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Ss : Set (Sieve X)
Y : C
f : Y ⟶ X
⊢ (sSup Ss).arrows f ↔ ∃ S, ∃ (_ : S ∈ Ss), S.arrows f

Tactic:
simp [sSup, Sieve.sup]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) = generate R

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ≤ generate R

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ generate R ≤ ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom
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
inst✝ : Mono f
x : FamilyOfElements P R
t : P.obj (op X)
ht : (x.map f).IsAmalgamation ((ConcreteCategory.hom (f.app (op X))) t)
⊢ x.IsAmalgamation t

Tactic:
intro Y u hu
  refine injective_of_mono (f.app _) ?_
  simpa using ht _ hu

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ofArrows P p₁ = pullback g (ofArrows X f)

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ofArrows P p₁ ≤ pullback g (ofArrows X f)

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ pullback g (ofArrows X f) ≤ ofArrows P p₁
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
⊢ (∃! a_1, (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ a_1 = S.shrinkFunctorIsoFunctor.homFromEquiv.symm a) ↔
    ∃! g, S.functorInclusion ≫ g = a

Tactic:
Equiv.existsUnique_congr_left (shrinkYonedaIsoYoneda.app X).homFromEquiv

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
⊢ (∃! b,
      (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (shrinkYonedaIsoYoneda.app X).homFromEquiv.symm b =
        S.shrinkFunctorIsoFunctor.homFromEquiv.symm a) ↔
    ∃! g, S.functorInclusion ≫ g = a
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (v ≫ Sieve.ofArrows.h hv' ≫ f (Sieve.ofArrows.i hv'))

Tactic:
← reassoc_of% hu

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (u ≫ u' ≫ f (Sieve.ofArrows.i hv'))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f g : Y ⟶ X
h : f = g
hf : (↑S).arrows f
⊢ (↑S).arrows g

Tactic:
simpa only [← h] using hf

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

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
j : W ⟶ X
hj : R j
⊢ (ConcreteCategory.hom (P.map j.op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯) = x j hj

Tactic:
apply (trans hj).ext

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
j : W ⟶ X
hj : R j
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ W⦄,
    (Sieve.pullback j S).arrows f →
      (ConcreteCategory.hom (P.map f.op))
          ((ConcreteCategory.hom (P.map j.op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯)) =
        (ConcreteCategory.hom (P.map f.op)) (x j hj)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) =
    generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i))

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case e'_2.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) ≤
    generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i))

case e'_2.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i)) ≤
    Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)
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
V W : C
i : V ⟶ unop U
hi : (ConcreteCategory.hom (F.map i.op)) s ∈ G.obj (op V)
j : W ⟶ V
⊢ (ConcreteCategory.hom (F.map (j ≫ i).op)) s ∈ G.obj (op W)

Tactic:
simpa using G.map _ hi

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
⊢ G ≤ sheafify J G

Tactic:
intro U s hs

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ s ∈ (sheafify J G).obj U
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
⊢ sheafify J G ≤ G

Tactic:
intro U s hs

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ s ∈ G.obj U
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 : X ⟶ Y
⊢ IsSeparatedFor P (singleton f) ↔ Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))

Tactic:
rw [IsSeparatedFor, Equiv.forall_congr_left (Presieve.FamilyOfElements.singletonEquiv P f)]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)) (t₁ t₂ : P.obj (op Y)),
      ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₁ →
        ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₂ → t₁ = t₂) ↔
    Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
B : J.Cover X := S.bind W
ex : B ⟶ Sx := homOfLE ⋯
⊢ B ≤ Sy

Tactic:
by
        rintro Y f ⟨Z, e1, e2, he2, he1, hee⟩
        rw [← hee]
        apply leOfHom (h2 ⟨_, _, he2⟩)
        exact he1

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ (imageMonoFactorization f).I ⟶ I.I

Tactic:
haveI M := (Sheaf.Hom.mono_iff_presheaf_mono J (Type (max v u)) _).mp I.m_mono
        refine ⟨Subfunctor.homOfLe ?_ ≫ inv (Subfunctor.toRange I.m.1)⟩
        apply Subfunctor.sheafify_le
        · conv_lhs => rw [← I.fac]
          apply Subfunctor.range_comp_le
        · rw [← isSheaf_iff_isSheaf_of_type]
          exact F'.2
        · apply Presieve.isSheaf_iso J (asIso <| Subfunctor.toRange I.m.1)
          rw [← isSheaf_iff_isSheaf_of_type]
          exact I.I.2

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : ↑S.pt
⊢ ((ConcreteCategory.hom m) x).1 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).1

Tactic:
specialize h ⟨WalkingPair.left⟩
      apply_fun fun e => e x at h
      exact h

Goal state after: