mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y : V
c : K
hz : c • x ∈ K ∙ x
⊢ (c • B x) (y + (-(B x) y / (B x) x) • x) = 0

Tactic:
smul_apply,

Goal state after:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y : V
c : K
hz : c • x ∈ K ∙ x
⊢ c • (B x) (y + (-(B x) y / (B x) x) • x) = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
| succ d ih =>

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 : ℕ
f : Fin n → M
i : Fin n
⊢ (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
by
  induction n with
  | zero => exact i.elim0
  | succ n hn =>
    rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]
    by_cases h : i = 0
    · rw [h, ι_sq_zero, zero_mul]
    · replace hn :=
        congr_arg (ι R (f 0) * ·) <| hn (fun i => f <| Fin.succ i) (i.pred h)
      rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn
      refine (eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn
      rw [← add_mul, ι_add_mul_swap, zero_mul]

Goal state after:
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (((LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) f 0) 0 = (f 1) ![m]

Tactic:
LinearMap.mk₂_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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ ((f (0 + 1)).curryLeft m) 0 = (f 1) ![m]
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₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (⇑(ConcreteCategory.hom S.f) ∘ v))) (span R (range (u ∘ Sum.inr)))

Tactic:
disjoint_comm

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₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range (⇑(ConcreteCategory.hom S.f) ∘ v)))
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
⊢ r • M.mk F ⟨⋯.some, 0⟩ = M.mk F ⟨⋯.some, 0⟩

Tactic:
colimit_smul_mk_eq,

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
⊢ M.mk F ⟨⟨⋯.some, 0⟩.fst, r • ⟨⋯.some, 0⟩.snd⟩ = M.mk F ⟨⋯.some, 0⟩
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
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ r • (M.mk F ⟨i, x⟩ + M.mk F ⟨j, y⟩) = r • M.mk F ⟨i, x⟩ + r • M.mk F ⟨j, y⟩

Tactic:
colimit_smul_mk_eq,

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ r • (M.mk F ⟨i, x⟩ + M.mk F ⟨j, y⟩) = M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + r • M.mk F ⟨j, y⟩
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
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ r • (M.mk F ⟨i, x⟩ + M.mk F ⟨j, y⟩) = M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + r • M.mk F ⟨j, y⟩

Tactic:
colimit_smul_mk_eq,

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ r • (M.mk F ⟨i, x⟩ + M.mk F ⟨j, y⟩) = M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + M.mk F ⟨⟨j, y⟩.fst, r • ⟨j, y⟩.snd⟩
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
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ r •
      M.mk F
        ⟨IsFiltered.max i j,
          (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd + (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩ =
    M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + M.mk F ⟨⟨j, y⟩.fst, r • ⟨j, y⟩.snd⟩

Tactic:
colimit_smul_mk_eq,

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ M.mk F
      ⟨⟨IsFiltered.max i j,
            (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
              (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.fst,
        r •
          ⟨IsFiltered.max i j,
              (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
                (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.snd⟩ =
    M.mk F ⟨⟨i, x⟩.fst, r • ⟨i, x⟩.snd⟩ + M.mk F ⟨⟨j, y⟩.fst, r • ⟨j, y⟩.snd⟩
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ (map n f).compAlternatingMap (ιMulti R n) = (ιMulti R n).compLinearMap f

Tactic:
by
  simp only [map, alternatingMapLinearEquiv_comp_ιMulti]

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
induction n generalizing M N with
  | zero =>
    simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one,
      ← Module.injective_iff_injective_object R M, ← Module.injective_iff_injective_object R' N]
    exact ⟨fun _ ↦ Module.Injective.of_ringEquiv eR e,
      fun _ ↦ Module.Injective.of_ringEquiv eR.symm e.symm⟩
  | succ n ih =>
    let ⟨I', _, f', _⟩ := EnoughInjectives.presentation N
    have : Module.Injective R' I' := Module.injective_module_of_injective_object R' I'
    have injf' : Function.Injective f'.hom := (mono_iff_injective f').mp ‹_›
    let S' : ShortComplex (ModuleCat.{v} R') :=
      ModuleCat.shortComplexOfCompEqZero _ _ f'.hom.exact_map_mkQ_range.linearMap_comp_eq_zero
    have exactS' := ModuleCat.shortComplex_shortExact S'
      f'.hom.exact_map_mkQ_range injf' (Submodule.mkQ_surjective _)
    let I : ModuleCat.{v} R :=
      let := Module.compHom I' eR.toRingHom
      ModuleCat.of R I'
    let eI : I ≃ₛₗ[RingHomClass.toRingHom eR] I' := {
      __ := AddEquiv.refl I
      map_smul' r i := rfl }
    have : Injective (ModuleCat.of R I) := by
      rw [← Module.injective_iff_injective_object]
      exact Module.Injective.of_ringEquiv eR.symm eI.symm
    let f : M →ₗ[R] I := eI.symm.toLinearMap.comp (f'.hom.comp e.toLinearMap)
    have injf : Function.Injective f := by simpa [f]
    let S : ShortComplex (ModuleCat.{v} R) :=
      ModuleCat.shortComplexOfCompEqZero _ _ f.exact_map_mkQ_range.linearMap_comp_eq_zero
    have exactS := ModuleCat.shortComplex_shortExact S
      f.exact_map_mkQ_range injf (Submodule.mkQ_surjective _)
    let eCoker : ModuleCat.of R (I ⧸ f.range) ≃ₛₗ[RingHomClass.toRingHom eR]
      ModuleCat.of R' (I' ⧸ f'.hom.range) :=
      Submodule.Quotient.equiv _ _ eI
        (by simp [f, ← Submodule.map_symm_eq_iff eI, LinearMap.range_comp])
    exact (exactS.hasInjectiveDimensionLT_X₃_iff n inferInstance).symm.trans
      ((ih eCoker).trans (exactS'.hasInjectiveDimensionLT_X₃_iff n inferInstance))

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

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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (((Functor.const J).obj (limitPresheafOfModules F)).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (limit.π (F ⋙ evaluation R Y) j) =
    limit.π (F ⋙ evaluation R X) j ≫ (F.obj j).map f

Tactic:
by
            dsimp
            simp only [assoc, preservesLimitIso_inv_π]
            apply limMap_π

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
⊢ ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
⊢ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'

Tactic:
· intro d
    obtain ⟨c, ⟨t⟩⟩ := h₁ (op d)
    exact ⟨c.unop, ⟨t.unop⟩⟩

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
⊢ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
N : ModuleCat ↑cR.pt
f : M ⟶ M'
g : M' ⟶ (constFunctor cR).obj N
⊢ (homEquiv hcR hcM) ((homEquiv hcR hcM).symm (f ≫ g)) =
    (homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ (homEquiv hcR hcM').symm g)

Tactic:
by
    obtain ⟨g, rfl⟩ := (homEquiv hcR hcM').surjective g
    simp [homEquiv_naturality_left]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
H : Sieve.pullback i S ∈ J X
⊢ S ∈ J Y

Tactic:
convert! J.pullback_stable (inv i) H

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
H : Sieve.pullback i S ∈ J X
⊢ S = Sieve.pullback (inv i) (Sieve.pullback i S)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : K.toGrothendieck ≤ J
X : C
⊢ K.coverings X ⊆ J.toPretopology.coverings X

Tactic:
R

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
h : K.toGrothendieck ≤ J
X : C
R : Presieve X
⊢ R ∈ K.coverings X → R ∈ J.toPretopology.coverings X
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
⊢ ∀ (R : Sieve X),
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
        S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}) →
      R ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}

Tactic:
R

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
⊢ (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}) →
    R ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PJ : IsSheaf K.toGrothendieck P
X : C
⊢ ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
R

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PJ : IsSheaf K.toGrothendieck P
X : C
R : Presieve X
⊢ R ∈ K.coverings X → IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
⊢ (∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j) → Fs = Exists.choose ⋯

Tactic:
HFs

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
⊢ Fs = Exists.choose ⋯
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
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ (FamilyOfElements.restrict ⋯ x).IsAmalgamation t₂

Tactic:
exact isAmalgamation_restrict _ x t₂ ht₂

Goal state after:
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
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ (forkMap R P ≫ firstMap R P) ≫
      limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
        { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } =
    (forkMap R P ≫ secondMap R P) ≫
      limit.π (Discrete.functor fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
        { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }

Tactic:
simp only [firstMap, secondMap, forkMap, limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app,
    Subtype.coe_mk]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map f.op ≫ P.map (pullback.fst f g).op = P.map g.op ≫ P.map (pullback.snd f g).op
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
⊢ ∀ (R : Presieve U), generate R ∈ J U → Nonempty (IsLimit (Fork.ofι (forkMap R P') ⋯))

Tactic:
R

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
⊢ generate R ∈ J U → Nonempty (IsLimit (Fork.ofι (forkMap R P') ⋯))
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
j : W ⟶ unop V
hj : (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows j
⊢ (ConcreteCategory.hom (f.app (op W)))
      (G.familyOfElementsOfSection (↑({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩ } s)) j hj) =
    (ConcreteCategory.hom (F'.map (i ≫ j.op))) (⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯)

Tactic:
change _ = F'.map (j ≫ i.unop).op _

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
hj : (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows j
⊢ (ConcreteCategory.hom (f.app (op W)))
      (G.familyOfElementsOfSection (↑({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩ } s)) j hj) =
    (ConcreteCategory.hom (F'.map (j ≫ i.unop).op)) (⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom = (J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)

Tactic:
ext X
  apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext
  intro W
  dsimp [plusObj, plusMap]
  simp only [ι_colimMap, whiskerRight_app, ι_plusCompIso_hom_assoc,
    GrothendieckTopology.diagramNatTrans_app]
  simp only [← Category.assoc, ← F.map_comp]
  dsimp [colimMap, IsColimit.map]
  simp only [colimit.ι_desc]
  dsimp [Cocone.precompose]
  simp only [Functor.map_comp, Category.assoc, ι_plusCompIso_hom]
  simp only [← Category.assoc]
  congr 1
  dsimp only [diagram] -- Need to unfold `diagram` before `ext` applies.
  ext a
  dsimp
  simp only [diagramCompIso_hom_ι_assoc, Multiequalizer.lift_ι, diagramCompIso_hom_ι,
    Category.assoc]
  simp only [← F.map_comp, Multiequalizer.lift_ι]

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✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ D
⊢ ∀ {Y : Sheaf J D} (f : P ⟶ Q) (g : Q ⟶ (sheafToPresheaf J D).obj Y),
    { toFun := fun e ↦ J.toSheafify P ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        (f ≫ g) =
      (plusPlusSheaf J D).map f ≫
        { toFun := fun e ↦ J.toSheafify Q ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }.symm
          g

Tactic:
R

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✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
⊢ ∀ (f : P ⟶ Q) (g : Q ⟶ (sheafToPresheaf J D).obj R),
    { toFun := fun e ↦ J.toSheafify P ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        (f ≫ g) =
      (plusPlusSheaf J D).map f ≫
        { toFun := fun e ↦ J.toSheafify Q ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }.symm
          g
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
trans (⨆ (j : J), (F.obj j).str.coinduced (c.ι.app j)).IsOpen X

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsOpen X ↔ TopologicalSpace.IsOpen X

J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
s : Cocone (Discrete.functor β)
j : Discrete ι
⊢ (sigmaCofan β).ι.app j ≫
      ofHom { toFun := fun s_1 ↦ (ConcreteCategory.hom (s.ι.app { as := s_1.fst })) s_1.snd, continuous_toFun := ⋯ } =
    s.ι.app j

Tactic:
cases j

Goal state after:
case mk
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
s : Cocone (Discrete.functor β)
as✝ : ι
⊢ (sigmaCofan β).ι.app { as := as✝ } ≫
      ofHom { toFun := fun s_1 ↦ (ConcreteCategory.hom (s.ι.app { as := s_1.fst })) s_1.snd, continuous_toFun := ⋯ } =
    s.ι.app { as := as✝ }