mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ e.hom = ((singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α) ≫ e.hom

Tactic:
dsimp [α, e]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    ((singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
        (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫
          homologyMap ι i ≫ homologyι L i ≫ (pOpcyclesIso L (i - 1) i ⋯ ⋯).inv) ≫
      pOpcycles L i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
f : M ⟶ N
hf : Mono f
⊢ ((mk₀ f).postcomp L ⋯).ker = ⊥

Tactic:
AddSubgroup.eq_bot_iff_forall

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
f : M ⟶ N
hf : Mono f
⊢ ∀ x ∈ ((mk₀ f).postcomp L ⋯).ker, x = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
⊢ ((mk₀ g).precomp L ⋯).ker = ⊥

Tactic:
AddSubgroup.eq_bot_iff_forall

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
⊢ ∀ x ∈ ((mk₀ g).precomp L ⋯).ker, x = 0
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k l : ℕ
h : k ∣ l
⊢ rootsOfUnity k M ≤ rootsOfUnity l M

Tactic:
obtain ⟨d, rfl⟩ := h
  intro ζ h
  simp_all only [mem_rootsOfUnity, pow_mul, one_pow]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_2
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
hb : b = 0
⊢ transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F)

Tactic:
simp only [hb, mem_center_iff, scalar_apply, transvection_coe, single_zero,
      add_zero, diagonal_eq_one]

Goal state after:
case refine_2
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
hb : b = 0
⊢ ∃ r, r ^ Fintype.card ι = 1 ∧ (fun x ↦ r) = 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

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
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ x * ((algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * y) - x * ((ι Q) b * (ι Q) a * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)

Tactic:
Algebra.left_comm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * ((ι Q) b * (ι Q) a * y) =
    (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

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
a b : M
⊢ QuadraticMap.polar (⇑Q) a b • (ι Q) a - (algebraMap R (CliffordAlgebra Q)) (Q a) * (ι Q) b =
    (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
←
    Algebra.smul_def,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ QuadraticMap.polar (⇑Q) a b • (ι Q) a - Q a • (ι Q) b = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
⊢ { toFun := ⇑((of A 0).comp GAlgebra.toFun), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
    x * { toFun := ⇑((of A 0).comp GAlgebra.toFun), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
change AddMonoidHom.mul (DirectSum.of _ _ _) x = AddMonoidHom.mul.flip (DirectSum.of _ _ _) x

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
⊢ (AddMonoidHom.mul ((of A 0) (GAlgebra.toFun r))) x = (AddMonoidHom.mul.flip ((of A 0) (GAlgebra.toFun r))) x
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
⊢ ↑0 = 0

Tactic:
by simp only [NatCast.natCast, GSemiring.natCast_zero, map_zero]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i : ι
⊢ A i →+ R

Tactic:
exact (F : (⨁ i, A i) →+ R).comp (of _ i)

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

Goal state before:
pp: case refine_2.refine_3
ι : 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
⊢ ∀ (m m' : A),
    ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m) 0) →
      ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m')) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m') 0) →
        ↑(((decompose 𝒜) (↑⟨c, hc⟩ * (m + m'))) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) (m + m')) 0)

Tactic:
intro _

Goal state after:
case refine_2.refine_3
ι : 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 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
m✝ : A
⊢ ∀ (m' : A),
    ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m✝)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m✝) 0) →
      ↑(((decompose 𝒜) (↑⟨c, hc⟩ * m')) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) m') 0) →
        ↑(((decompose 𝒜) (↑⟨c, hc⟩ * (m✝ + m'))) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) (m✝ + m')) 0)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
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 𝒜
a : ↥(𝒜 0)
⊢ (projZeroRingHom' 𝒜) ↑a = a

Tactic:
ext; simp only [coe_projZeroRingHom'_apply, projZeroRingHom_apply, decompose_coe, of_eq_same]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
⊢ ((toLinearMap₂' R) M).SeparatingRight ↔ M.SeparatingRight

Tactic:
refine ⟨fun h ↦ separatingRight_def.mpr ?_, SeparatingRight.toLinearMap₂'⟩
  exact fun v hv => h v fun w => (M.toLinearMap₂'_apply' _ _).trans <| hv w

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

Goal state before:
pp: case e_fst.ι_mul
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
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m✝ : M
m : CliffordAlgebra Q
x : M
hx : (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m).1 = m
⊢ (((foldr'Aux Q f) x) (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m)).1 = (ι Q) x * m

Tactic:
foldr'Aux_apply_apply,

Goal state after:
case e_fst.ι_mul
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
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m✝ : M
m : CliffordAlgebra Q
x : M
hx : (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m).1 = m
⊢ ((ι Q) x * (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m).1, (f x) (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m)).1 = (ι Q) x * m
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inr.refine_2.refine_2
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'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j✝ i✝ : Fin (d + 1)
i j : Fin d
hij : j.succ ≠ i.succ
⊢ (B ↑(v' j)) ↑(v' i) = 0

Tactic:
· exact hv₁ (ne_of_apply_ne _ hij)

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
r : R
⊢ (liftAlternating f) ((algebraMap R (ExteriorAlgebra R M)) r) = r • (f 0) 0

Tactic:
by
  rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]

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
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m = { app := fun X ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ }

Tactic:
by
    ext1 X
    apply (hc X).uniq ((evaluation R X).mapCone s)
    intro j
    dsimp
    rw [← hm, comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape (Discrete PEmpty.{1}) colim
⊢ (k : C) → IsLimit (((evaluation C (Type u)).obj k).mapCone (asEmptyCone (Types.constPUnitFunctor C)))

Tactic:
intro _

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape (Discrete PEmpty.{1}) colim
k✝ : C
⊢ IsLimit (((evaluation C (Type u)).obj k✝).mapCone (asEmptyCone (Types.constPUnitFunctor C)))
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
X : C₀
⊢ ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)

Tactic:
let f : StructuredArrow X (fromFinalModel.{w} C₀) := Classical.arbitrary _

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
X : C₀
f : StructuredArrow X (fromFinalModel C₀) := Classical.arbitrary (StructuredArrow X (fromFinalModel C₀))
⊢ ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ {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 _

Goal state after:
case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
d✝ : J₂
⊢ ∀ {c : J₁} (s s' : d✝ ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
Module: Mathlib.CategoryTheory.Filtered.Final

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

Tactic:
intro _

Goal state after:
case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
d✝ : J₂
⊢ ∀ {c : J₁} (s s' : hf.functor.obj c ⟶ d✝), ∃ c' t, hf.functor.map t ≫ s = hf.functor.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
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
Q' : (j : J) → IsColimit (Q.obj j) := fun j ↦ colimit.isColimit ((curry.obj G).obj j)
c' : Cocone G
f : (coconeOfHasColimitCurryCompColim G).pt ⟶ c'.pt
h : ∀ (j : J × K), (coconeOfHasColimitCurryCompColim G).ι.app j ≫ f = c'.ι.app j
⊢ f = colimit.desc (curry.obj G ⋙ colim) (coconeOfCoconeCurry G Q' c')

Tactic:
by
      dsimp [coconeOfHasColimitCurryCompColim] at f h ⊢
      refine colimit.hom_ext (F := curry.obj G ⋙ colim) (fun j ↦ colimit.hom_ext (fun k ↦ ?_))
      simp [← h ⟨j, k⟩, Q']

Goal state after:
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
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
by
  rw [← cancel_mono (colimitIsoColimitCurryCompColim G).inv]
  simp

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

Goal state before:
pp: C₀ : Type u_1
inst✝ : Category.{v_1, u_1} C₀
F G : C₀ ⥤ C₀
adj : F ⊣ G
e : G ≅ 𝟭 C₀
⊢ (conjugateEquiv id adj) (adj.leftAdjointIdIso e).hom = e.inv

Tactic:
by
  simp [leftAdjointIdIso]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ : R.category
⊢ ∀ ⦃Y : R.category⦄ (f : g₁ ⟶ Y),
    R.diagram.map f ≫ x Y.obj.hom ⋯ = x g₁.obj.hom ⋯ ≫ ((Functor.const R.category).obj W).map f

Tactic:
g₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ g₂ : R.category
⊢ ∀ (f : g₁ ⟶ g₂), R.diagram.map f ≫ x g₂.obj.hom ⋯ = x g₁.obj.hom ⋯ ≫ ((Functor.const R.category).obj W).map f
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
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 ((yoneda.obj s.pt).map g₁.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ h₁) =
        (ConcreteCategory.hom ((yoneda.obj s.pt).map g₂.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₂ h₂)

Tactic:
g₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
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 ((yoneda.obj s.pt).map g₁.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s f₁ h₁) =
        (ConcreteCategory.hom ((yoneda.obj s.pt).map g₂.op)) (S.arrows.yonedaFamilyOfElements_fromCocone s 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
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
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:
g₂

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
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.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
⊢ x.sieveExtend.Compatible

Tactic:
intro _

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₁✝ : C
⊢ ∀ ⦃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: 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
hx : (x.map f).Compatible
Y Z W : C
g₁ : W ⟶ Y
⊢ ∀ (g₂ : W ⟶ Z) ⦃f₁ : Y ⟶ X⦄ ⦃f₂ : Z ⟶ 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:
g₂

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
hx : (x.map f).Compatible
Y Z W : C
g₁ : W ⟶ Y
g₂ : W ⟶ Z
⊢ ∀ ⦃f₁ : Y ⟶ X⦄ ⦃f₂ : Z ⟶ 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.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:
g₂

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:
g₂

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 : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = (ConcreteCategory.hom (P.map f₂.op)) (x (f₁ ≫ f) hf)

Tactic:
rw [← h (f₁ ≫ f) f₂ hf]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = x (f₂ ≫ f₁ ≫ 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
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:
g₂

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₂)