awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℂ
h : (deriv cosh / cosh) x = tanh x
h₁ : (sinh / cosh) x = tanh x
h₂ : sinh x / cosh x = tanh x
h₃ h₄ : sinh x / cosh x = sinh x / cosh x
⊢ logDeriv cosh x = tanh x

Tactic:
rw [logDeriv, Complex.deriv_cosh, Pi.div_apply, Complex.tanh]

Premises used: logDeriv, Complex.tanh, Pi.div_apply, Complex.deriv_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
h : ∀ (x : ℝ), logDeriv cosh x = tanh x
⊢ logDeriv cosh = tanh

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
h : (deriv cosh / cosh) x = tanh x
h₁ : (sinh / cosh) x = tanh x
h₂ : sinh x / cosh x = tanh x
h₃ h₄ : sinh x / cosh x = sinh x / cosh x
⊢ logDeriv cosh x = tanh x

Tactic:
rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]

Premises used: logDeriv, Real.tanh_eq_sinh_div_cosh, Pi.div_apply, Real.deriv_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < Real.sinh x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ Real.sinh x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : x ≠ 0
⊢ Real.sinh x ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
⊢ sinc x = if x = 0 then 1 else sin x / x

Tactic:
rfl

Premises used: Real.sinc, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
⊢ sinc 0 = 1

Tactic:
simp [sinc]

Premises used: Real.sinc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x ≠ 0
⊢ sinc x = sin x / x

Tactic:
simp [sinc, hx]

Premises used: Real.sinc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
h : ∀ (x : ℝ), sinc x = dslope sin 0 x
⊢ sinc = dslope sin 0

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
⊢ sinc x = dslope sin 0 x

Tactic:
simp [dslope, Function.update_apply, sinc, slope, div_eq_inv_mul]

Premises used: Real.sinc, Function.update_apply, slope, dslope, div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
pos : ∀ (hx : x = 0), sinc (-x) = sinc x
neg : ∀ (hx : ¬x = 0), sinc (-x) = sinc x
⊢ sinc (-x) = sinc x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x = 0
⊢ sinc (-x) = sinc x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
⊢ sinc (-x) = sinc x

Tactic:
simp [sinc_of_ne_zero hx, sinc_of_ne_zero (neg_ne_zero.mpr hx)]

Premises used: Iff.mpr, neg_ne_zero, Real.sinc_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
pos : ∀ (hx : x = 0), |sinc x| ≤ 1
neg : ∀ (hx : ¬x = 0), |sinc x| ≤ 1
⊢ |sinc x| ≤ 1

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x = 0
⊢ |sinc x| ≤ 1

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
neg : |sin x| / |x| ≤ 1
⊢ |sinc x| ≤ 1

Tactic:
rw [sinc_of_ne_zero hx, abs_div]

Premises used: abs_div, Real.sinc_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
⊢ |sin x| / |x| ≤ 1

Tactic:
div_le_of_le_mul₀ (abs_nonneg _) zero_le_one ?_

Premises used: div_le_of_le_mul₀, zero_le_one, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
neg : |sin x| ≤ 1 * |x|
⊢ |sin x| / |x| ≤ 1

Tactic:
refine div_le_of_le_mul₀ (abs_nonneg _) zero_le_one ?_

Premises used: div_le_of_le_mul₀, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
neg : |sin x| ≤ |x|
⊢ |sin x| ≤ 1 * |x|

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
⊢ |sin x| ≤ |x|

Tactic:
abs_sin_le_abs

Premises used: Real.abs_sin_le_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
⊢ |sin x| ≤ |x|

Tactic:
exact abs_sin_le_abs

Premises used: Real.abs_sin_le_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
⊢ sinc x ≤ 1

Tactic:
(abs_le.mp (abs_sinc_le_one x)).2

Premises used: Real.abs_sinc_le_one, abs_le, And.right, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
⊢ -1 ≤ sinc x

Tactic:
(abs_le.mp (abs_sinc_le_one x)).1

Premises used: Real.abs_sinc_le_one, abs_le, And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
inl : ∀ (hx : x < 0), sin x / x ≤ |x|⁻¹
inr : sin 0 / 0 ≤ |0|⁻¹
inr₁ : ∀ (hx : 0 < x), sin x / x ≤ |x|⁻¹
⊢ sin x / x ≤ |x|⁻¹

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x < 0
inl : sin x * x⁻¹ * -x ≤ 1
inl₁ : 0 < -x
⊢ sin x / x ≤ |x|⁻¹

Tactic:
rw [abs_of_nonpos hx.le, ← one_div, le_div_iff₀, div_eq_mul_inv]

Premises used: LT.lt.le, div_eq_mul_inv, abs_of_nonpos, one_div, le_div_iff₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x < 0
inl : -(sin x * x * x⁻¹) ≤ 1
⊢ sin x * x⁻¹ * -x ≤ 1

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x < 0
inl : -1 ≤ sin x
⊢ -(sin x * x * x⁻¹) ≤ 1

Tactic:
rw [mul_assoc, mul_inv_cancel₀ hx.ne, mul_one, neg_le]

Premises used: neg_le, mul_inv_cancel₀, mul_assoc, mul_one, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x < 0
⊢ -1 ≤ sin x

Tactic:
neg_one_le_sin x

Premises used: Real.neg_one_le_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x < 0
⊢ -1 ≤ sin x

Tactic:
exact neg_one_le_sin x

Premises used: Real.neg_one_le_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x < 0
⊢ 0 < -x

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
⊢ sin 0 / 0 ≤ |0|⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : 0 < x
inr : sin x ≤ 1
⊢ sin x / x ≤ |x|⁻¹

Tactic:
rw [abs_of_nonneg hx.le, div_eq_mul_inv, mul_inv_le_iff₀ hx, inv_mul_cancel₀ hx.ne']

Premises used: mul_inv_le_iff₀, LT.lt.le, div_eq_mul_inv, LT.lt.ne', abs_of_nonneg, inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : 0 < x
⊢ sin x ≤ 1

Tactic:
sin_le_one x

Premises used: Real.sin_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : 0 < x
⊢ sin x ≤ 1

Tactic:
exact sin_le_one x

Premises used: Real.sin_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x ≠ 0
rw : sin x / x ≤ |x|⁻¹
⊢ sinc x ≤ |x|⁻¹

Tactic:
rw [sinc_of_ne_zero hx]

Premises used: Real.sinc_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x ≠ 0
⊢ sin x / x ≤ |x|⁻¹

Tactic:
sin_div_le_inv_abs x

Premises used: Real.sin_div_le_inv_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x ≠ 0
⊢ sin x / x ≤ |x|⁻¹

Tactic:
exact sin_div_le_inv_abs x

Premises used: Real.sin_div_le_inv_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
⊢ Continuous sinc

Tactic:
continuous_iff_continuousAt.mpr fun x ↦ ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
refine : ∀ (x : ℝ), ContinuousAt sinc x
⊢ Continuous sinc

Tactic:
refine continuous_iff_continuousAt.mpr fun x ↦ ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
rw : ContinuousAt (dslope sin 0) x
⊢ ContinuousAt sinc x

Tactic:
rw [sinc_eq_dslope]

Premises used: Real.sinc_eq_dslope
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
pos : ∀ (hx : x = 0), ContinuousAt (dslope sin 0) x
neg : ∀ (hx : ¬x = 0), ContinuousAt (dslope sin 0) x
⊢ ContinuousAt (dslope sin 0) x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : x = 0
⊢ ContinuousAt (dslope sin 0) x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
neg : ContinuousAt sin x
⊢ ContinuousAt (dslope sin 0) x

Tactic:
rw [continuousAt_dslope_of_ne hx]

Premises used: continuousAt_dslope_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Goal:
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt sin x

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
⊢ F.IsLeftAdjoint

Tactic:
have := adj.isLeftAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
this : F.IsLeftAdjoint
⊢ PreservesColimitsOfShape.{v, u, v₂, v₃, u₂, u₃} J H ↔ PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun {K} ↦ ?_⟩⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Limits.PreservesColimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
this : F.IsLeftAdjoint
refine :
  PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H) → ∀ {K : Functor.{v, v₂, u, u₂} J D}, PreservesColimit K H
⊢ PreservesColimitsOfShape.{v, u, v₂, v₃, u₂, u₃} J H ↔ PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)

Tactic:
refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun {K} ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
this : F.IsLeftAdjoint
h : PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)
K : Functor.{v, v₂, u, u₂} J D
iso : (K ⋙ G) ⋙ F ≅ K := K.associator G F ≪≫ K.isoWhiskerLeft (asIso adj.counit) ≪≫ K.rightUnitor
⊢ PreservesColimit K H

Tactic:
preservesColimit_of_preserves_colimit_cocone
    ((IsColimit.precomposeInvEquiv iso _).symm
      (isColimitOfPreserves F (colimit.isColimit (K ⋙ G)))) ?_

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeInvEquiv, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
this : F.IsLeftAdjoint
h : PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)
K : Functor.{v, v₂, u, u₂} J D
iso : (K ⋙ G) ⋙ F ≅ K := K.associator G F ≪≫ K.isoWhiskerLeft (asIso adj.counit) ≪≫ K.rightUnitor
refine : IsColimit (H.mapCocone ((Cocone.precompose iso.inv).obj (F.mapCocone (colimit.cocone (K ⋙ G)))))
⊢ PreservesColimit K H

Tactic:
refine preservesColimit_of_preserves_colimit_cocone
    ((IsColimit.precomposeInvEquiv iso _).symm
      (isColimitOfPreserves F (colimit.isColimit (K ⋙ G)))) ?_

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeInvEquiv, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
J : Type u
inst_3 : Category.{v, u} J
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
inst_5 : G.Full
inst_6 : G.Faithful
this : F.IsLeftAdjoint
h : PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)
K : Functor.{v, v₂, u, u₂} J D
iso : (K ⋙ G) ⋙ F ≅ K := K.associator G F ≪≫ K.isoWhiskerLeft (asIso adj.counit) ≪≫ K.rightUnitor
⊢ IsColimit (H.mapCocone ((Cocone.precompose iso.inv).obj (F.mapCocone (colimit.cocone (K ⋙ G)))))

Tactic:
exact IsColimit.ofIsoColimit
    ((IsColimit.precomposeInvEquiv
      ((Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight iso H) _).symm
        (isColimitOfPreserves (F ⋙ H) (colimit.isColimit (K ⋙ G))))
          (Cocone.ext (Iso.refl _))

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Functor.associator, CategoryTheory.Iso.refl, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, Equiv.symm, CategoryTheory.Functor.isoWhiskerRight, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeInvEquiv, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_4 : G.Full
inst_5 : G.Faithful
⊢ F.IsLeftAdjoint

Tactic:
have := adj.isLeftAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_4 : G.Full
inst_5 : G.Faithful
this : F.IsLeftAdjoint
⊢ PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔ PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun {J _} ↦ ?_⟩⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesColimitsOfSize.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_4 : G.Full
inst_5 : G.Faithful
this : F.IsLeftAdjoint
refine :
  PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H) →
    ∀ {J : Type u} {x : Category.{v, u} J}, PreservesColimitsOfShape.{v, u, v₂, v₃, u₂, u₃} J H
⊢ PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔ PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)

Tactic:
refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun {J _} ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_4 : G.Full
inst_5 : G.Faithful
this : F.IsLeftAdjoint
h : PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)
J : Type u
x : Category.{v, u} J
rw : PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)
⊢ PreservesColimitsOfShape.{v, u, v₂, v₃, u₂, u₃} J H

Tactic:
rw [adj.preservesColimitsOfShape_iff]

Premises used: CategoryTheory.Adjunction.preservesColimitsOfShape_iff
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
E : Type u₃
inst_2 : Category.{v₃, u₃} E
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
inst_4 : G.Full
inst_5 : G.Faithful
this : F.IsLeftAdjoint
h : PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)
J : Type u
x : Category.{v, u} J
⊢ PreservesColimitsOfShape.{v, u, v₁, v₃, u₁, u₃} J (F ⋙ H)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Balanced
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Balanced.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : Mono f
inst_3 : Epi f
⊢ IsIso f

Tactic:
Balanced.isIso_of_mono_of_epi _

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Balanced
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Balanced.{v, u} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ Mono f ∧ Epi f

Tactic:
⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => isIso_of_mono_of_epi _⟩

Premises used: CategoryTheory.IsIso, inferInstance, And.intro, Iff.intro, CategoryTheory.isIso_of_mono_of_epi, _private.0.CategoryTheory.isIso_iff_mono_and_epi.match_1
-- Module: Mathlib.CategoryTheory.Balanced
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Balanced.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
fmono : Mono f
fepi : Epi f
rw : IsIso.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f.unop.op
⊢ IsIso f

Tactic:
rw [← Quiver.Hom.op_unop f]

Premises used: Quiver.Hom.op_unop
-- Module: Mathlib.CategoryTheory.Balanced
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Balanced.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
fmono : Mono f
fepi : Epi f
⊢ IsIso.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f.unop.op

Tactic:
isIso_of_op _

Premises used: CategoryTheory.isIso_of_op
-- Module: Mathlib.CategoryTheory.Balanced
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Balanced.{v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
fmono : Mono f
fepi : Epi f
⊢ IsIso.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) f.unop.op

Tactic:
exact isIso_of_op _

Premises used: CategoryTheory.isIso_of_op
-- Module: Mathlib.CategoryTheory.Category.GaloisConnection
Goal:
X : Type u
Y : Type v
inst : Preorder X
inst_1 : Preorder Y
L : X ⥤ Y
R : Y ⥤ X
adj : L ⊣ R
⊢ GaloisConnection L.obj R.obj

Tactic:
fun x y =>
  ⟨fun h => ((adj.homEquiv x y).toFun h.hom).le, fun h => ((adj.homEquiv x y).invFun h.hom).le⟩

Premises used: Quiver.Hom.le, Equiv.toFun, LE.le.hom, Iff.intro, CategoryTheory.Adjunction.homEquiv, Equiv.invFun, GaloisConnection
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
⊢ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
⊢ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
⊢ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
⊢ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 3 = f₄

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₂₃ : i₁ ⟶ i₃
f₃₄ : i₂ ⟶ i₄
h₂₃ : f₂ ≫ f₃ = f₂₃
h₃₄ : f₃ ≫ f₄ = f₃₄
⊢ (fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 0 = 𝟙 ((mk₃ f₁ f₂ f₃₄).obj 0)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₂₃ : i₁ ⟶ i₃
f₃₄ : i₂ ⟶ i₄
h₂₃ : f₂ ≫ f₃ = f₂₃
h₃₄ : f₃ ≫ f₄ = f₃₄
⊢ (fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 1 = 𝟙 ((mk₃ f₁ f₂ f₃₄).obj 1)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₂₃ : i₁ ⟶ i₃
f₃₄ : i₂ ⟶ i₄
h₂₃ : f₂ ≫ f₃ = f₂₃
h₃₄ : f₃ ≫ f₄ = f₃₄
⊢ (fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 2 = f₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₂₃ : i₁ ⟶ i₃
f₃₄ : i₂ ⟶ i₄
h₂₃ : f₂ ≫ f₃ = f₂₃
h₃₄ : f₃ ≫ f₄ = f₃₄
⊢ (fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 3 = 𝟙 ((mk₃ f₁ f₂ f₃₄).obj 3)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 0 = 𝟙 ((mk₃ f₁ f₂₃ f₄).obj 0)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 1 = f₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 2 = 𝟙 ((mk₃ f₁ f₂₃ f₄).obj 2)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₁₂ : i₀ ⟶ i₂
f₂₃ : i₁ ⟶ i₃
h₁₂ : f₁ ≫ f₂ = f₁₂
h₂₃ : f₂ ≫ f₃ = f₂₃
⊢ (fourδ₂Toδ₁ f₁ f₂ f₃ f₄ f₁₂ f₂₃ h₁₂ h₂₃).app 3 = 𝟙 ((mk₃ f₁ f₂₃ f₄).obj 3)

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
⊢ (fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 0 = f₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Four
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i₀ i₁ i₂ i₃ i₄ : C
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
⊢ (fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂).app 1 = 𝟙 ((mk₃ f₁₂ f₃ f₄).obj 1)

Tactic:
rfl

Premises used: Fin.ofNat, rfl