mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ (opShiftFunctorEquivalence C n).unitIso.hom.app X =
    ((shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n m hnm).inv.app X).unop).op

Tactic:
by
  obtain rfl : m = -n := by lia
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ (opShiftFunctorEquivalence C n).unitIso.inv.app X =
    ((shiftFunctor C n).map ((shiftFunctorOpIso C n m hnm).hom.app X).unop).op ≫
      ((shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op

Tactic:
by
  obtain rfl : m = -n := by lia
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ (opShiftFunctorEquivalence C n).counitIso.hom.app X =
    (shiftFunctorOpIso C n m hnm).hom.app (Opposite.op ((shiftFunctor C n).obj (Opposite.unop X))) ≫
      ((shiftFunctorCompIsoId C n m hnm).inv.app (Opposite.unop X)).op

Tactic:
by
  obtain rfl : m = -n := by lia
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ (opShiftFunctorEquivalence C n).counitIso.inv.app X =
    ((shiftFunctorCompIsoId C n m hnm).hom.app (Opposite.unop X)).op ≫
      (shiftFunctorOpIso C n m hnm).inv.app (Opposite.op ((shiftFunctor C n).obj (Opposite.unop X)))

Tactic:
by
  obtain rfl : m = -n := by lia
  rfl

Goal state after:
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
inst✝⁷ : F.CommShift A
inst✝⁶ : G.CommShift A
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝⁴ : HasShift E A
inst✝³ : F'.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : adj.CommShift A
inst✝ : adj'.CommShift A
⊢ NatTrans.CommShift (adj.comp adj').counit A

Tactic:
rw [comp_counit]
    infer_instance

Goal state after:
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
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
X : C
⊢ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫
      G.map ((Functor.commShiftIso F a).hom.app X) ≫ (Functor.commShiftIso G a).hom.app (F.obj X)

Tactic:
by
  simpa [Functor.commShiftIso_comp_hom_app] using NatTrans.shift_app_comm adj.unit a X

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
this : (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient
⊢ Function.Bijective (⇑↑e ∘ ⇑solution.fromQuotient)

Tactic:
LinearEquiv.coe_coe

Goal state after:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
this : (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient
⊢ Function.Bijective (⇑e ∘ ⇑solution.fromQuotient)
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ ∃ d, a = d ^ n

Tactic:
refine exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one ?_) h
  obtain ⟨x, y, hxy⟩ := cp
  rw [← hxy]
  exact dvd_add (dvd_mul_of_dvd_right (gcd_dvd_left _ _) _)
    (dvd_mul_of_dvd_right (gcd_dvd_right _ _) _)

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
⊢ ∑ g, f g = 0

Tactic:
obtain ⟨x, hx⟩ := IsCyclic.exists_monoid_generator (α := MonoidHom.range f.toHomUnits)
    have hx1 : (x.1 : R) - 1 ≠ 0 := by
      rw [sub_ne_zero]
      contrapose hf
      ext g
      obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩
      simpa [hf, Subtype.ext_iff, Units.ext_iff] using hn.symm
    let c := #{g | f.toHomUnits g = 1}
    calc
      ∑ g : G, f g = ∑ u ∈ univ.image f.toHomUnits, #{g | f.toHomUnits g = u} • (u : R) :=
        sum_comp ((↑) : Rˣ → R) f.toHomUnits
      _ = ∑ u ∈ univ.image f.toHomUnits, c • (u : R) :=
        (sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)
      -- remaining goal 1, proven below
      _ = ∑ b : MonoidHom.range f.toHomUnits, c • (b.1 : R) :=
        (Finset.sum_subtype _ (by simp) _)
      _ = c • ∑ b : MonoidHom.range f.toHomUnits, (b.1 : R) := smul_sum.symm
      _ = c • 0 := congr_arg₂ _ rfl ?_
      -- remaining goal 2, proven below
      _ = 0 := smul_zero _
    · -- remaining goal 1
      apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits
      · simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu
      · exact ⟨1, f.toHomUnits.map_one⟩
    -- remaining goal 2
    calc
      (∑ b : MonoidHom.range f.toHomUnits, (b.1 : R))
        = ∑ n ∈ range (orderOf x), (x.1 : R) ^ n :=
        Eq.symm <|
          sum_nbij (x ^ ·) (by simp)
            (by simpa using pow_injOn_Iio_orderOf)
            (fun b _ => let ⟨n, hn⟩ := hx b
              ⟨n % orderOf x, mem_range.2 (Nat.mod_lt _ (orderOf_pos _)), by simp [hn]⟩)
            (by simp)
      _ = 0 := ?_
    rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]
    norm_cast
    simp [pow_orderOf_eq_one]

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

Goal state before:
pp: n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (j : n), 0 < ∑ i, A i j
⊢ A.det ≠ 0

Tactic:
by
  cases isEmpty_or_nonempty n
  · simp
  · contrapose! h2
    obtain ⟨v, ⟨h_vnz, h_vA⟩⟩ := Matrix.exists_vecMul_eq_zero_iff.mpr h2
    wlog h_sup : 0 < Finset.sup' Finset.univ Finset.univ_nonempty v
    · refine this h1 inferInstance h2 (-1 • v) (by simp [*]) ?_ ?_
      · rw [Matrix.smul_vecMul, h_vA, smul_zero]
      · obtain ⟨i, hi⟩ := Function.ne_iff.mp h_vnz
        simp_rw [Finset.lt_sup'_iff, Finset.mem_univ, true_and] at h_sup ⊢
        simp_rw [not_exists, not_lt] at h_sup
        refine ⟨i, ?_⟩
        rw [Pi.smul_apply, neg_smul, one_smul, Left.neg_pos_iff]
        exact Ne.lt_of_le hi (h_sup i)
    · obtain ⟨j₀, -, h_j₀⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty v
      refine ⟨j₀, ?_⟩
      rw [← mul_le_mul_iff_right₀ (h_j₀ ▸ h_sup), Finset.mul_sum, mul_zero]
      rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]
      refine Finset.sum_le_sum (fun i hi => ?_)
      by_cases h : i = j₀
      · rw [h]
      · exact (mul_le_mul_right_of_neg (h1 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)

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

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ A⁻¹ * A = 1

Tactic:
by
      ext1
      simp [adjugate_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : Std.Associative fun x y ↦ x * y
⊢ mulLeft₃ = mulRight₃

Tactic:
by ext x y z; simp [Std.Associative.assoc]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
⊢ ∀ (y : A ai), (mulHom A) ((of A ai) y) = (mulHom A).flip ((of A ai) y)

Tactic:
ax

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ (mulHom A) ((of A ai) ax) = (mulHom A).flip ((of A ai) ax)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 0
⊢ ↑(((decompose 𝒜) (a * b)) i) = ↑(((decompose 𝒜) a) i) * b

Tactic:
lift b to 𝒜 0 using b_mem
  rw [decompose_mul, decompose_coe, coe_mul_of_apply_of_mem_zero]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : ↑(powersetCard α m)
⊢ (↑t)ᶜ ∈ powersetCard α n

Tactic:
simp [Finset.card_compl, mem_iff.mp t.2]

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
t : ↑(powersetCard α m)
⊢ Fintype.card α - m = n
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 (u ∘ Sum.inr))) (Hom.hom S.f).range

Tactic:
hS.moduleCat_range_eq_ker

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))) (Hom.hom S.g).ker
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 : ↑(M F)
⊢ ↑(M F)

Tactic:
by
    refine Quot.lift (colimitSMulAux F r) ?_ x
    intro x y h
    apply colimitSMulAux_eq_of_rel
    apply Types.FilteredColimit.rel_of_colimitTypeRel
    exact h

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

Goal state before:
pp: ι : 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)
⊢ m - m' ∈ (Hom.hom S.f).range

Tactic:
hS.moduleCat_range_eq_ker

Goal state after:
ι : 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)
⊢ m - m' ∈ (Hom.hom S.g).ker
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : 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))
⊢ ⊤ ≤ span R (range u)

Tactic:
by
  intro m _
  have hgm : S.g m ∈ span R (range (S.g ∘ u ∘ Sum.inr)) := hw mem_top
  rw [Finsupp.mem_span_range_iff_exists_finsupp] at hgm
  obtain ⟨cm, hm⟩ := hgm
  let m' : S.X₂ := Finsupp.sum cm fun j a ↦ a • (u (Sum.inr j))
  have hsub : m - m' ∈ LinearMap.range S.f.hom := by
    rw [hS.moduleCat_range_eq_ker]
    simp only [LinearMap.mem_ker, map_sub, sub_eq_zero]
    rw [← hm, map_finsuppSum]
    simp only [Function.comp_apply, map_smul]
  obtain ⟨n, hnm⟩ := hsub
  have hn : n ∈ span R (range v) := hv mem_top
  rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn
  obtain ⟨cn, hn⟩ := hn
  rw [← hn, map_finsuppSum] at hnm
  rw [← sub_add_cancel m m', ← hnm]
  simp only [map_smul]
  have hn' : (Finsupp.sum cn fun a b ↦ b • S.f (v a)) =
      (Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) := by
    congr; ext a b; rw [← Function.comp_apply (f := S.f), ← huv, Function.comp_apply]
  rw [hn']
  apply add_mem
  · rw [Finsupp.mem_span_range_iff_exists_finsupp]
    use cn.mapDomain (Sum.inl)
    rw [Finsupp.sum_mapDomain_index_inj Sum.inl_injective]
  · rw [Finsupp.mem_span_range_iff_exists_finsupp]
    use cm.mapDomain (Sum.inr)
    rw [Finsupp.sum_mapDomain_index_inj Sum.inr_injective]

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'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Module.Injective R ↑I

Tactic:
exact Module.Injective.of_ringEquiv eR.symm eI.symm

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) (mk m s) = 0
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)

Tactic:
by
        rw [map_LocalizedModules, ← zero_mk 1, mk_eq, one_smul, smul_zero] at hy
        obtain ⟨a, aS, ha⟩ := Subtype.exists.1 hy
        rw [smul_zero, mk_smul, ← map_smul, ex (a • m)] at ha
        rcases ha with ⟨x, hx⟩
        use mk x (⟨a, aS⟩ * s)
        rw [map_LocalizedModules, hx, ← mk_cancel_common_left ⟨a, aS⟩ s m, mk_smul]

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

Goal state before:
pp: case refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d x✝ : (j : C) × F.obj j
⊢ Zigzag x✝.fst x✝.fst

Tactic:
| refl _ =>

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
⊢ Types.constPUnitFunctor C ≅ ⊤_ C ⥤ Type u

Tactic:
apply_rules [IsTerminal.uniqueUpToIso _ terminalIsTerminal, evaluationJointlyReflectsLimits]
    intro _
    exact isLimitChangeEmptyCone _ Types.isTerminalPUnit _ <| Iso.refl _

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 D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
obtain ⟨c₀, ⟨f₀⟩⟩ := h (IsFiltered.coeq (F.map f) (F.map g))
    refine ⟨_, F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀), F.map_injective ?_⟩
    simp [reassoc_of% (IsFiltered.coeq_condition (F.map f) (F.map g))]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} J₁
inst✝³ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝² : Category.{v_3, u_3} C₁
inst✝¹ : Category.{v_4, u_4} C₂
inst✝ : Category.{v_5, u_5} C
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cocone K₁
c₂ : Cocone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ ((G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)) ≫
      (G.map (c₁.ι.app k₁)).app (K₂.obj k₂) ≫ (G.obj c₁.pt).map (c₂.ι.app k₂) =
    ((G.map (c₁.ι.app j₁)).app (K₂.obj j₂) ≫ (G.obj c₁.pt).map (c₂.ι.app j₂)) ≫ 𝟙 ((G.obj c₁.pt).obj c₂.pt)

Tactic:
simp only [assoc, comp_id, NatTrans.naturality_assoc,
          ← Functor.map_comp, NatTrans.naturality, const_obj_map, const_obj_obj,
          ← NatTrans.comp_app_assoc, c₁.w]

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

Goal state before:
pp: case a.a
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (F.map fj).app k ≫ (F.obj j').map fk

pp: case a
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| s.π.app j

pp: case a.a
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (D.obj j).π.app k

Tactic:
rw [← NatTrans.naturality]

Goal state after:
case a.a
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (F.obj j).map fk ≫ (F.map fj).app k'

case a
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| s.π.app j

case a.a
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (D.obj j).π.app k
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: case a.a
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 c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (F.obj j').map fk ≫ (D.obj j').ι.app k'

pp: case a.a
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 c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| s.ι.app j'

pp: case a
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 c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (F.map fj).app k

Tactic:
(D.obj j').ι.naturality

Goal state after:
case a.a
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 c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (D.obj j').ι.app k ≫ ((const K).obj (D.obj j').pt).map fk

case a.a
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 c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| s.ι.app j'

case a
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 c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
| (F.map fj).app k
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)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ G.map (f₁, f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    (colimit.ι ((curry.obj G).obj x.1) x.2 ≫ colimit.ι (curry.obj G ⋙ colim) x.1) ≫ 𝟙 (colimit (curry.obj G ⋙ colim))

Tactic:
rw [← colimit.w (F := curry.obj G ⋙ colim) (f := f₁),
          Category.assoc, Category.comp_id, Prod.fac' (f₁, f₂),
          G.map_comp_assoc, ← curry_obj_map_app, ← curry_obj_obj_map]

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)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ ((curry.obj G).map (f₁, f₂).1).app x.2 ≫
      ((curry.obj G).obj y.1).map (f₁, f₂).2 ≫
        colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    colimit.ι ((curry.obj G).obj x.1) x.2 ≫ (curry.obj G ⋙ colim).map f₁ ≫ colimit.ι (curry.obj G ⋙ colim) y.1