mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
this✝ : Epi S.g
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ HomologicalComplex.homologyMap S.g i ≫ 𝟙 (S.X₃.homology i) = HomologicalComplex.homologyMap S.g i ≫ 0

Tactic:
← cancel_epi (HomologicalComplex.homologyMap S.f i)

Goal state after:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
this✝ : Epi S.g
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i ≫ 𝟙 (S.X₃.homology i) =
    HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i ≫ 0
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
⊢ CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)

Tactic:
by
  intro
  simp only [Functor.id_obj, Functor.comp_obj, Functor.CommShift.isoZero_hom_app,
    Functor.map_comp, assoc, unit_naturality_assoc,
    ← cancel_mono ((shiftFunctorZero C A).hom.app _), ← G.map_comp_assoc, Iso.inv_hom_id_app,
    Functor.id_obj, Functor.map_id, id_comp, NatTrans.naturality, Functor.id_map, assoc, comp_id]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
⊢ M.SeparatingLeft ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0

Tactic:
by
  refine forall_congr' fun v ↦ ⟨fun hM hv ↦ hM ?_, fun hM hv ↦ hM ?_⟩ <;>
  convert! hv

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

Goal state before:
pp: ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
⊢ e.toMatrix v = (LinearMap.toMatrix e e) ((e.constr ℕ) v)

Tactic:
ext
  rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S✝ : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (L →* ↥S)
f : L →* Rˣ
⊢ ∃ a, (fun f ↦ S.subtype.comp f) a = f

Tactic:
have H a : f a ∈ S := by
    rw [mem_rootsOfUnity, ← map_pow, Monoid.pow_exponent_eq_one, map_one]

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S✝ : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
L : Type u_7
inst✝¹ : LeftCancelMonoid L
inst✝ : Finite L
S : Subgroup Rˣ := rootsOfUnity (Monoid.exponent L) R
this : Finite (L →* ↥S)
f : L →* Rˣ
H : ∀ (a : L), f a ∈ S
⊢ ∃ a, (fun f ↦ S.subtype.comp f) a = f
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring S₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module S₁ N₂
inst✝³ : Module S₂ N₂
inst✝² : SMulCommClass S₂ S₁ N₂
inst✝¹ : Fintype n
inst✝ : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
c : R₁
v : n → R₁
w : m → R₂
⊢ ∑ i, ∑ j, σ₂ (w j) •> σ₁ ((c •> v) i) •> f i j = σ₁ c •> ∑ i, ∑ j, σ₂ (w j) •> σ₁ (v i) •> f i j

Tactic:
simp only [Pi.smul_apply, smul_sum, smul_eq_mul, σ₁.map_mul, ← smul_comm _ (σ₁ c), mul_smul]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p
⊢ x ∈ p

Tactic:
← DirectSum.sum_support_decompose ℳ x

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) x), ↑(((decompose ℳ) x) i) ∈ p
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ f (a • x) * g (a • x) = (a * a) • (f x * g x)

Tactic:
map_smulₛₗ,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ (RingHom.id R) a • f x * g (a • x) = (a * a) • (f x * g x)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ a • f x * g (a • x) = (a * a) • (f x * g x)

Tactic:
map_smulₛₗ,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ a • f x * (RingHom.id R) a • g x = (a * a) • (f x * g x)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case refine_2.refine_2
ι : 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
⊢ ∀ {i_1 : ι} (m : ↥(𝒜 i_1)),
    ↑(((decompose 𝒜) (↑⟨c, hc⟩ * ↑m)) 0) = ↑(((decompose 𝒜) ↑⟨c, hc⟩) 0) * ↑(((decompose 𝒜) ↑m) 0)

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:
· rintro j ⟨c', hc'⟩
        simp only
        by_cases h : i + j = 0
        · rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]
        · rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]
          rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'
          · simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]
          · simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]

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 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.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
k : ι
hk : k < m + n
⊢ (r * r') k = 0

Tactic:
rw [Subtype.ext_iff, ZeroMemClass.coe_zero, coe_mul_apply]

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
k : ι
hk : k < m + n
⊢ ∑ ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = k, ↑(r ij.1) * ↑(r' ij.2) = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ (map f) ((ιMulti R n) m) = (ιMulti R n) (⇑f ∘ m)

Tactic:
rw [ιMulti_apply, ιMulti_apply, map_list_prod]
  simp only [List.map_ofFn, Function.comp_def, map_apply_ι]

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

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
Y : C
hi : 1 ≤ 0
e : Ext Y X 0
⊢ e = 0

Tactic:
simp at hi

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

Goal state before:
pp: case zero
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 + 1)
this : HasExt C := HasExt.standard C
hi : n + 1 ≤ 0
Y : C
x₃ : Ext Y S.X₁ 0
⊢ x₃ = 0

Tactic:
simp at hi

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

Goal state before:
pp: case h
ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := ⋯
n : ↑S.X₁
cn : ι →₀ R
hnm : (cn.sum fun a b ↦ (Hom.hom S.f) (b • v a)) = m - m'
hn : (cn.sum fun i a ↦ a • v i) = n
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ ((Finsupp.mapDomain Sum.inr cm).sum fun i a ↦ a • u i) = m'

Tactic:
Finsupp.sum_mapDomain_index_inj Sum.inr_injective

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
r : R
i : ℕ
hi : i < 0
⊢ M

Tactic:
simp at hi

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
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right ≫ t) =
    (StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))).hom

Tactic:
simpa using ht.symm

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ (Cocone.precompose
          (NatIso.ofComponents (fun x ↦ Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj x)) ⋯).inv).obj
      (Cocone.whisker (Functor.diag J) (c₁.tensor₂ c₂)) ≅
    c₁.tensor c₂

Tactic:
exact Cocone.ext (Iso.refl _)

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
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cone (uncurry.obj F) → Cone D.conePoints :=
  fun s ↦
    { pt := s.pt,
      π :=
        { app := fun j ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (uncurry.obj F)
p : J × K
h1 :
  (Q p.1).lift
        ((Cone.postcompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).hom).obj
          (Cone.whisker (Prod.sectR p.1 K) s)) ≫
      (D.obj p.1).π.app p.2 =
    s.π.app (p.1, p.2)
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p

Tactic:
have h2 := (P.fac (S s) p.1)

Goal state after:
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)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cone (uncurry.obj F) → Cone D.conePoints :=
  fun s ↦
    { pt := s.pt,
      π :=
        { app := fun j ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (uncurry.obj F)
p : J × K
h1 :
  (Q p.1).lift
        ((Cone.postcompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).hom).obj
          (Cone.whisker (Prod.sectR p.1 K) s)) ≫
      (D.obj p.1).π.app p.2 =
    s.π.app (p.1, p.2)
h2 : P.lift (S s) ≫ (coneOfConeUncurry Q c).π.app p.1 = (S s).π.app p.1
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p
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 : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cocone (uncurry.obj F) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
p : J × K
h1 :
  (D.obj p.1).ι.app p.2 ≫
      (Q p.1).desc
        ((Cocone.precompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).inv).obj
          (Cocone.whisker (Prod.sectR p.1 K) s)) =
    s.ι.app (p.1, p.2)
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p

Tactic:
have h2 := (P.fac (S s) p.1)

Goal state after:
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 : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cocone (uncurry.obj F) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
p : J × K
h1 :
  (D.obj p.1).ι.app p.2 ≫
      (Q p.1).desc
        ((Cocone.precompose (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj p.1).obj x)) ⋯).inv).obj
          (Cocone.whisker (Prod.sectR p.1 K) s)) =
    s.ι.app (p.1, p.2)
h2 : (coconeOfCoconeUncurry Q c).ι.app p.1 ≫ P.desc (S s) = (S s).ι.app p.1
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p
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)
i : G ≅ uncurry.obj (curry.obj G)
this : HasColimit (uncurry.obj (curry.obj G))
⊢ colimit G ≅ colimit (curry.obj G ⋙ colim)

Tactic:
trans colimit (uncurry.obj ((@curry J _ K _ C _).obj G))

Goal state after:
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)
i : G ≅ uncurry.obj (curry.obj G)
this : HasColimit (uncurry.obj (curry.obj G))
⊢ colimit G ≅ colimit (uncurry.obj (curry.obj G))

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)
i : G ≅ uncurry.obj (curry.obj G)
this : HasColimit (uncurry.obj (curry.obj G))
⊢ colimit (uncurry.obj (curry.obj G)) ≅ colimit (curry.obj G ⋙ colim)
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✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (G.map (Prod.mkHom (𝟙 j) (𝟙 k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
CategoryTheory.Bifunctor.map_id

Goal state after:
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✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
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
F : PresheafOfModules R
G : ModuleCat ↑cR.pt
⊢ (colimitAdjunction hcR).homEquiv F G = ↑(ModuleColimit.homEquiv hcR (colimit.isColimit F.presheaf))

Tactic:
simp [colimitAdjunction]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
⊢ IsIso ⊤.ι

Tactic:
refine @NatIso.isIso_of_isIso_app _ _ _ _ _ _ _ ?_
  intro X
  rw [isIso_iff_bijective]
  exact ⟨Subtype.coe_injective, fun x => ⟨⟨x, _root_.trivial⟩, rfl⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ Sieve.pullback f S ∈ ⊥ Y ↔ S.arrows f

Tactic:
bot_covering,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ Sieve.pullback f S = ⊤ ↔ S.arrows f
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
hF : (X : C) → IsInitial (F.obj X)
X : C
⊢ (Cocone.precompose ((empty D).emptyExt (empty (C ⥤ D) ⋙ (evaluation C D).obj X)).inv).obj (asEmptyCocone (F.obj X)) ≅
    ((evaluation C D).obj X).mapCocone (asEmptyCocone F)

Tactic:
exact Cocone.ext (Iso.refl _)

Goal state after:
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✝ R : Sieve X
h : Y ⟶ X
S : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ Y
g : S.arrows (f✝ ≫ h)
⊢ ∀ (g : Z✝ ⟶ Y✝), S.arrows ((g ≫ f✝) ≫ h)

Tactic:
simp [g]

Goal state after:
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

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
hu : R u
⊢ (ConcreteCategory.hom (P.map u.op)) t = x u hu