mathlib-initiative/mathlib-tactics huggingface dataset:
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
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap p ^ n) =
    Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map reverseOp.toLinearMap p) ^ n

Tactic:
Submodule.map_unop_pow

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ powersetCard α n = ∅ ↔ Nat.card α < n

Tactic:
by
  rw [← Set.ncard_eq_zero, ← _root_.Nat.card_coe_set_eq, powersetCard.card, Nat.choose_eq_zero_iff]

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 : ℕ
v : Fin n → M
⊢ (ιMulti R n) v ∈ ↑(⋀[R]^n M)

Tactic:
rw [ιMulti_apply]

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (List.ofFn fun i ↦ (ι R) (v i)).prod ∈ ↑(⋀[R]^n M)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) ((ιMulti R n) v) = (f n) v

Tactic:
rw [ιMulti_apply]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f n) v
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 : ℕ
f : Fin n → ↑↑(ι R).range
hu : (List.ofFn fun i ↦ ↑(f i)).prod ∈ ↑(ι R).range ^ n
⊢ ((ιMulti R n) fun i ↦ ιInv ↑(f i)) = (List.ofFn fun i ↦ ↑(f i)).prod

Tactic:
rw [ιMulti_apply]

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → ↑↑(ι R).range
hu : (List.ofFn fun i ↦ ↑(f i)).prod ∈ ↑(ι R).range ^ n
⊢ (List.ofFn fun i ↦ (ι R) (ιInv ↑(f i))).prod = (List.ofFn fun i ↦ ↑(f i)).prod
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 : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
⊢ colimitSMulAux F r x = colimitSMulAux F r y

Tactic:
by
  apply M.mk_eq
  obtain ⟨k, f, g, hfg⟩ := h
  use k, f, g
  simp only [Functor.comp_obj, Functor.comp_map, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk] at hfg
  simp [hfg]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasInjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this : HasExt C := HasExt.standard C
⊢ Subsingleton (Ext Y X i)

Tactic:
have := hX.subsingleton' i hi

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasInjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this✝ : HasExt C := HasExt.standard C
this : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X i)
⊢ Subsingleton (Ext Y X i)
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext Y S.X₁ i
⊢ x₃.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
rw [x₃.eq_zero_of_hasInjectiveDimensionLT n hi, Ext.zero_comp]

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

Goal state before:
pp: case a.refine_2
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.ιMulti R n) (⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) = (List.ofFn fun i ↦ ↑(f i)).prod

Tactic:
rw [ExteriorAlgebra.ιMulti_apply]
      apply congrArg (List.prod ∘ List.ofFn)
      ext i
      obtain ⟨m, -, hm⟩ := (Set.mem_image _ _ _).mp (f i).2
      rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₂) = Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₁) + Module.rank R ↑S.X₃

Tactic:
Module.Free.rank_eq_card_chooseBasisIndex R S.X₃,

Goal state after:
R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₂) =
    Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₁) + Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₃)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : I → ↥(span R (range v))
hf : ⇑(span R (range v)).subtype ∘ f = v
⊢ (map n (span R (range v)).subtype).range = span R (range (ιMulti_family R n v))

Tactic:
have htop : Submodule.span R (Set.range f) = ⊤ := by
    apply SetLike.coe_injective
    apply Set.image_injective.mpr (Submodule.span R (Set.range v)).injective_subtype
    rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]

Goal state after:
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : I → ↥(span R (range v))
hf : ⇑(span R (range v)).subtype ∘ f = v
htop : span R (range f) = ⊤
⊢ (map n (span R (range v)).subtype).range = span R (range (ιMulti_family R n v))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝² : Closed A
inst✝¹ : BraidedCategory C
I : C
t : IsInitial I
inst✝ : MonoidalClosed C
⊢ default ≫ curry ((mulZero t).hom ≫ t.to B) = 𝟙 (I ⟹ B)

Tactic:
by
    rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mulZero t).inv]
    apply t.hom_ext

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
inst✝ : IsCofiltered (CostructuredArrow F d)
c₁ c₂ : C
s₁ : F.obj c₁ ⟶ d
s₂ : F.obj c₂ ⟶ d
⊢ ∃ c t₁ t₂, F.map t₁ ≫ s₁ = F.map t₂ ≫ s₂

Tactic:
obtain ⟨W, p₁, p₂, -⟩ := IsCofilteredOrEmpty.cone_objs
    (CostructuredArrow.mk s₁) (CostructuredArrow.mk s₂)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
inst✝ : IsCofiltered (CostructuredArrow F d)
c₁ c₂ : C
s₁ : F.obj c₁ ⟶ d
s₂ : F.obj c₂ ⟶ d
W : CostructuredArrow F d
p₁ : W ⟶ CostructuredArrow.mk s₁
p₂ : W ⟶ CostructuredArrow.mk s₂
⊢ ∃ c t₁ t₂, F.map t₁ ≫ s₁ = F.map t₂ ≫ s₂
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ ((const K).obj c.pt).map f ≫ c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f

Tactic:
by
                  simpa using @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j, k') (𝟙 j, f)

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 : F.PartialLeftAdjointSource
⊢ F.partialLeftAdjointMap (𝟙 X) = 𝟙 (F.partialLeftAdjointObj X)

Tactic:
by
    apply F.partialLeftAdjointHomEquiv.injective
    simp [partialLeftAdjointHomEquiv_map]

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
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R = ⊤

Tactic:
← top_le_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ⊤ ≤ Sieve.pullback f R
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ sInf ((fun J ↦ J.coverings) '' T) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ sInf ((fun J ↦ J.coverings) '' T) Y
⊢ S.bind Ti ∈ sInf ((fun J ↦ J.coverings) '' T) X

Tactic:
by
      simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists, Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter] at hS hTi ⊢
      intro t ht
      exact t.transitive S Ti (hS t ht) (fun Y f H ↦ hTi f H t ht)

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
Y : C
hk : ι
⊢ pullbackArrows f (ofArrows Z g) (pullback.snd (g hk) f)

Tactic:
exact pullbackArrows.mk _ _ (ofArrows.mk hk)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
⊢ ∃ ι Y f, R = ofArrows Y f

Tactic:
let ι := { x : Σ Z, (Z ⟶ X) // R x.2 }

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
ι : Type (max 0 u₁ v₁) := { x // R x.snd }
⊢ ∃ ι Y f, R = ofArrows Y f
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)
Y : C
⊢ ∀ (f : Y ⟶ X) (h : R f), (ConcreteCategory.hom (P.map f.op)) t = x f h

Tactic:
u

Goal state after:
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)
Y : C
u : Y ⟶ X
⊢ ∀ (h : R u), (ConcreteCategory.hom (P.map u.op)) t = x u h
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂

Tactic:
by
  have q₁ := h₁ (𝟙 X) (by tauto)
  have q₂ := h₂ (𝟙 X) (by tauto)
  simp only [op_id, Functor.map_id, id_apply] at q₁ q₂
  rw [q₁, q₂]

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

Goal state before:
pp: case mpr
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
t : (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
i : I
⊢ ∀ (j : I),
    (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op))
        ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x i) =
      (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op))
        ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x j)

Tactic:
j

Goal state after:
case mpr
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
t : (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
i j : I
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op))
      ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op))
      ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x j)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (equivShrink ((j : I) → P.obj (op (X j)))).symm
        ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
      x →
    ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
· intro q i
    rw [← q]
    simp [Iso.toEquiv, forkMap]

Goal state after:
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)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((J.diagramPullback P f).app (op S) ≫ colimit.ι (J.diagram P Y) ((J.pullback f).op.obj (op S))))
      ((Meq.equiv P S).symm x) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P Y) (op (S.pullback f))))
      ((Meq.equiv P (S.pullback f)).symm (x.pullback f))

Tactic:
CategoryTheory.comp_apply (x := (Meq.equiv P S).symm x)

Goal state after:
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)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P Y) ((J.pullback f).op.obj (op S))))
      ((ConcreteCategory.hom ((J.diagramPullback P f).app (op S))) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P Y) (op (S.pullback f))))
      ((Meq.equiv P (S.pullback f)).symm (x.pullback f))
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
⊢ ∀ (f : W ⟶ X) (h_1 : R f),
    (ConcreteCategory.hom (P.map f.op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯) = x f h_1

Tactic:
j

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
⊢ ∀ (h_1 : R j), (ConcreteCategory.hom (P.map j.op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯) = x j h_1
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
trans : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows

Tactic:
by simpa using trans (𝟙 _)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
⊢ (G.preimage p).image p ≤ G

Tactic:
image_le_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
⊢ G.preimage p ≤ G.preimage p
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ ⊤.image p ≤ G

Tactic:
image_le_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ ⊤ ≤ G.preimage p
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p ≤ G

Tactic:
image_le_iff

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ G.preimage p ≤ G.preimage p
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J P
⊢ IsSheaf J (P ⋙ s)

Tactic:
rw [isSheaf_iff_isLimit] at h ⊢
  apply fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfPreserves s t

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

Goal state before:
pp: case e'_2
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✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h1.op)) ((Meq.equiv P S✝).symm x)) =
    ↑(x.refine h1) i

pp: case e'_3
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✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op S)).index P) i))
      ((ConcreteCategory.hom ((J.diagram P X).map h2.op)) ((Meq.equiv P T).symm y)) =
    ↑(y.refine h2) i

Tactic:
all_goals
      dsimp [diagram]
      rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
      erw [Meq.equiv_symm_eq_apply]
      cases i; rfl

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
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
⊢ ∀ ⦃f₂ : V₂ ⟶ U⦄ (h₁ : S'.arrows g₃) (h₂ : S'.arrows f₂),
    g₁ ≫ g₃ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' g₃ h₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' f₂ h₂)

Tactic:
g₄

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
⊢ ∀ (h₁ : S'.arrows g₃) (h₂ : S'.arrows g₄),
    g₁ ≫ g₃ = g₂ ≫ g₄ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' g₃ h₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' g₄ h₂)
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 : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
⊢ ∀ ⦃f_1 : W ⟶ unop V⦄,
    (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows f_1 →
      (ConcreteCategory.hom (F'.map f_1.op))
          ((ConcreteCategory.hom
                ((sheafify J G).toFunctor.map i ≫
                  ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯)).toFun
            s) =
        (ConcreteCategory.hom (F'.map f_1.op))
          ((ConcreteCategory.hom ((↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map i)).toFun
            s)

Tactic:
j

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
⊢ (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows j →
    (ConcreteCategory.hom (F'.map j.op))
        ((ConcreteCategory.hom
              ((sheafify J G).toFunctor.map i ≫ ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯)).toFun
          s) =
      (ConcreteCategory.hom (F'.map j.op))
        ((ConcreteCategory.hom ((↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map i)).toFun s)