mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : 1 ≤ |x|
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
by
  wlog! h : 0 ≤ x
  · simpa [T_eval_neg, abs_mul, abs_unit_intCast] using @this n (-x) (by grind) (by grind)
  · exact one_le_eval_T_real n (abs_of_nonneg h ▸ hx) |>.trans <| le_abs_self _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
⊢ L.weierstrassPExceptSummand l₀ = L.weierstrassPSummand

Tactic:
by
  grind [weierstrassPSummand, weierstrassPExceptSummand]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ x = cos (↑n * arccos x / ↑n)

Tactic:
rw [mul_div_cancel_left₀ _ (by simpa), cos_arccos (by grind) (by grind)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ ↑↑k * π = ↑↑n * (↑k * π / ↑n)

Tactic:
simp [field]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ ↑↑n * (↑k * π / ↑n) = ↑↑k * π

Tactic:
simp [field]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x → ∃ k ≤ n, x = cos (↑k * π / ↑n)

pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ (∃ k ≤ n, x = cos (↑k * π / ↑n)) → IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x

Tactic:
· intro h
    apply (abs_eval_T_real_eq_one_iff hn x).mp
    apply eq_of_le_of_ge (abs_eval_T_real_le_one n (by grind))
    refine h.elim (fun h => ?_) (fun h => ?_)
    · refine le_abs.mpr (.inr (le_neg_of_le_neg ?_))
      have := isMinOn_iff.mp h (cos (1 * π / n)) (by grind [abs_cos_le_one])
      rw [(eval_T_real_eq_neg_one_iff hn (cos (1 * π / n))).mpr ⟨1, Nat.one_le_iff_ne_zero.mpr hn,
        by simp⟩] at this
      assumption
    · refine le_abs.mpr (.inl ?_)
      have := isMaxOn_iff.mp h (cos (0 * π / n)) (by simp)
      rw [(eval_T_real_eq_one_iff hn _).mpr ⟨0, by simp, by simp⟩] at this
      assumption

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ (∃ k ≤ n, x = cos (↑k * π / ↑n)) → IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
n : ℕ
⊢ a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
Finset.sum_range_succ,

Goal state after:
R : Type u_1
a b : R
inst✝ : CommSemiring R
n : ℕ
⊢ a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * (∑ x ∈ Finset.range n, a ^ x + a ^ n)
Module: Mathlib.Tactic.NormNum.NatFib

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ a * (2 * b - a) = a'

Tactic:
← h1

Goal state after:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ a * (2 * b - a) = a * (2 * b - a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
hf : ∀ (y : ℝ), ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))
⊢ |∑ p ∈ f.support, f p • eval x p| ≤ eval 1 ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
← hf 1

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
hf : ∀ (y : ℝ), ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))
⊢ |∑ p ∈ f.support, f p • eval x p| ≤ ∑ p ∈ f.support, f p • eval 1 p
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∑ i ∈ Finset.range n, logDeriv (fun z ↦ 1 + sineTerm z i) x = ∑ j ∈ Finset.range n, cotTerm x j

Tactic:
logDeriv_sineTerm_eq_cotTerm hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + (↑n + 1) ≠ 0

Tactic:
· simpa using (integerComplement_add_ne_zero hz ((n : ℤ) + 1))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
h0 : ∑' (n : ℕ+), ((x - ↑↑n)⁻¹ + (x + ↑↑n)⁻¹) = ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
h1 : ↑π * (↑π * x).cot - x⁻¹ = ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
⊢ ↑π * (↑π * x).cot = x⁻¹ + ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)

Tactic:
← h1

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
h0 : ∑' (n : ℕ+), ((x - ↑↑n)⁻¹ + (x + ↑↑n)⁻¹) = ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
h1 : ↑π * (↑π * x).cot - x⁻¹ = ∑' (n : ℕ), ((x - (↑n + 1))⁻¹ + (x + (↑n + 1))⁻¹)
⊢ ↑π * (↑π * x).cot = x⁻¹ + (↑π * (↑π * x).cot - x⁻¹)
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g

Tactic:
by
  rw [← SetLike.mem_coe, coe_commutant]
  rfl

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ u (c N) - ↑(c N) * l + (↑(c N) - ↑(c (N - 1))) * l ≤ ε * ↑(c N) + ε * ↑(c (N - 1)) * l

Tactic:
gcongr
        · exact (ha N (a.le_succ.trans aN)).2
        · linarith only [IcN]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
this✝² : (preadditiveCoyonedaObj G).PreservesInjectiveObjects
this✝¹ : (tensorObj G).PreservesMonomorphisms
this✝ : PreservesBinaryBiproducts (tensorObj G)
this : (tensorObj G).Additive
⊢ PreservesFiniteLimits (tensorObj G)

Tactic:
have : (tensorObj G).PreservesHomology :=
    (tensorObj G).preservesHomology_of_preservesMonos_and_cokernels

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
this✝³ : (preadditiveCoyonedaObj G).PreservesInjectiveObjects
this✝² : (tensorObj G).PreservesMonomorphisms
this✝¹ : PreservesBinaryBiproducts (tensorObj G)
this✝ : (tensorObj G).Additive
this : (tensorObj G).PreservesHomology
⊢ PreservesFiniteLimits (tensorObj G)
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ (Over.Hom.left (Φ.toColon Ψ).hom).app X ≫ (Φ.colon Ψ).ι.app X = Φ.ι.app X

Tactic:
rw [← NatTrans.comp_app, Over.w]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ I.ι ≫ (I.homotopyEquiv J).hom = J.ι

Tactic:
by simp [homotopyEquiv]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ J.ι ≫ (I.homotopyEquiv J).inv = I.ι

Tactic:
by simp [homotopyEquiv]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Injective ((ofCocomplex Z).X n)

Tactic:
obtain (_ | _ | _ | n) := n

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X 0)

case succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X (0 + 1))

case succ.succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective ((ofCocomplex Z).X (0 + 1 + 1))

case succ.succ.succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Injective ((ofCocomplex Z).X (n + 1 + 1 + 1))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Abelian D
P : ObjectProperty C
inst✝² : P.IsSerreClass
F : C ⥤ D
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel

Tactic:
by
  refine ⟨P.le_kernel_of_isoModSerre_isInvertedBy F, fun hF X Y f ⟨h₁, h₂⟩ ↦ ?_⟩
  have : Mono (F.map f) :=
    (((ShortComplex.mk _ _ (kernel.condition f)).exact_of_f_is_kernel
      (kernelIsKernel f)).map F).mono_g (((hF _ h₁).eq_of_src _ _))
  have : Epi (F.map f) :=
    (((ShortComplex.mk _ _ (cokernel.condition f)).exact_of_g_is_cokernel
      (cokernelIsCokernel f)).map F).epi_f (((hF _ h₂).eq_of_tgt _ _))
  exact isIso_of_mono_of_epi (F.map f)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ P.isoModSerre (Abelian.image.ι f)

Tactic:
by
  rw [isoModSerre_iff_of_mono]
  dsimp [epiModSerre] at hf ⊢
  exact P.prop_of_iso
    (asIso (cokernel.map f _ (Abelian.factorThruImage f) (𝟙 Y) (by simp))) hf

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : HasKernels C
inst✝ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
this : CreatesLimit (parallelPair f 0) P.ι
⊢ PreservesLimit (parallelPair f 0) P.ι

Tactic:
have := P.hasLimit_parallelPair_comp_ι f

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : HasKernels C
inst✝ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
this✝ : CreatesLimit (parallelPair f 0) P.ι
this : HasLimit (parallelPair f 0 ⋙ P.ι)
⊢ PreservesLimit (parallelPair f 0) P.ι
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
X : Action V PUnit.{?u.12 + 1}
x✝ : PUnit.{?u.12 + 1}
⊢ X.ρ PUnit.unit = 𝟙 X.V

Tactic:
exact ρ_one X

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ ((res V f).map g₁).hom = g₂.hom

Tactic:
← res_map_hom _ f g₂,

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ ((res V f).map g₁).hom = ((res V f).map g₂).hom
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ (whiskeringLeft L P E).essImage F

Tactic:
refine ⟨⟨Localization.lift F.obj hF L, ?_⟩,
      ⟨ObjectProperty.isoMk _ (Localization.fac F.obj hF L)⟩⟩

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ exactFunctor D E (Localization.lift F.obj hF L)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a : B
⊢ (α.naturality (𝟙 a)).hom =
    (F.mapId a).hom ▷ α.app a ≫ (λ_ (α.app a)).hom ≫ (ρ_ (α.app a)).inv ≫ α.app a ◁ (G.mapId a).inv

Tactic:
simp [← assoc, ← IsIso.comp_inv_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).hom =
    (F.mapComp f g).hom ▷ α.app c ≫
      (α_ (F.map f) (F.map g) (α.app c)).hom ≫
        F.map f ◁ (α.naturality g).hom ≫
          (α_ (F.map f) (α.app b) (G.map g)).inv ≫
            (α.naturality f).hom ▷ G.map g ≫ (α_ (α.app a) (G.map f) (G.map g)).hom ≫ α.app a ◁ (G.mapComp f g).inv

Tactic:
simp [← assoc, ← IsIso.comp_inv_eq]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x✝ : ∫ F
⊢ (mapCompIso α β).hom.app x✝ = eqToHom ⋯

Tactic:
by simp [mapCompIso]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x✝ : ∫ᶜ F
⊢ (mapCompIso α β).hom.app x✝ = eqToHom ⋯

Tactic:
by simp [mapCompIso]

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} J✝
J : Type ?u.6
inst✝ : Category.{v_1, ?u.6} J
X : Type u_1
f : ConnectedComponents J → X
x : ConnectedComponents J
⊢ liftFunctor J (functorToDiscrete X f) x = f x

Tactic:
obtain ⟨x, h⟩ := Quotient.exists_rep x

Goal state after:
J✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} J✝
J : Type ?u.6
inst✝ : Category.{v_1, ?u.6} J
X : Type u_1
f : ConnectedComponents J → X
x✝ : ConnectedComponents J
x : J
h : ⟦x⟧ = x✝
⊢ liftFunctor J (functorToDiscrete X f) x✝ = f x✝
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X : PartialFun
⊢ partialFunToPointed.map
        ((NatIso.ofComponents
                (fun X ↦
                  PartialFun.Iso.mk
                    { toFun := fun a ↦ ⟨some a, ⋯⟩, invFun := fun a ↦ Option.get ↑a ⋯, left_inv := ⋯, right_inv := ⋯ })
                ⋯).hom.app
          X) ≫
      (NatIso.ofComponents (fun X ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯).hom.app
        (partialFunToPointed.obj X) =
    𝟙 (partialFunToPointed.obj X)

Tactic:
by
    ext (_ | x)
    · rfl
    · simp
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j : J
⊢ ∀ (j' : J) (f_1 : j ⟶ j'),
    (hom
          ((homDiagram
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  X✝)
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  Y✝)).map
            f_1))
        (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) =
      eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
j'

Goal state after:
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
⊢ ∀ (f_1 : j ⟶ j'),
    (hom
          ((homDiagram
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  X✝)
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  Y✝)).map
            f_1))
        (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) =
      eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
⊢ φ₁ = φ₂

Tactic:
have : φ₁' = φ₂' := by
    apply (adj.homEquiv U _).symm.injective
    apply (Over.forget X).map_injective
    simpa using! h₁

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
this : φ₁' = φ₂'
⊢ φ₁ = φ₂
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: J : Type u_1
K : Type u_2
X✝ Y✝ : Discrete J × Discrete K
x✝ : X✝ ⟶ Y✝
f₁ : X✝.1 ⟶ Y✝.1
f₂ : X✝.2 ⟶ Y✝.2
⊢ (match X✝ with
    | (x, y) => { as := (x.as, y.as) }) =
    match Y✝ with
    | (x, y) => { as := (x.as, y.as) }

Tactic:
by discrete_cases; dsimp; rw [f₁, f₂]

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.SumsProducts

Goal state before:
pp: C : Type u_1
C' : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
D : Type u_3
inst✝³ : Category.{v_3, u_3} D
inst✝² : IsDiscrete C
inst✝¹ : IsDiscrete C'
inst✝ : IsDiscrete D
x y : C ⊕ C'
f g : x ⟶ y
⊢ f = g

Tactic:
cases f <;> cases g
        · case inl x y f g => rw [((by assumption : IsDiscrete C).subsingleton x y).allEq f g]
        · case inr x y f g => rw [((by assumption : IsDiscrete C').subsingleton x y).allEq f g]

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply inf_le_inf <;> rw [← Subobject.pullback_comp, ← Subobject.pullback_comp]

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: case h₁
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂R X Y Z).hom = coprod.inl ≫ (coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)).hom

Tactic:
simp [leftDistrib_hom, rightDistrib_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: case h₂
C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : HasBinaryCoproducts C
inst✝¹ : SymmetricCategory C
inst✝ : IsMonoidalDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ≫ (coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ ∂L X Y Z ≪≫ β_ X (Y ⨿ Z)).hom

Tactic:
simp [leftDistrib_hom, rightDistrib_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫ L'.obj X' ◁ ((μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom) =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
← h₂

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫ L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom) =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
⊢ S.ShortExact

Tactic:
· have : Mono S.f := by
      rw [hP.jointlyReflectMonomorphisms.mono_iff]
      exact fun i ↦ (hS i).mono_f
    have : Epi S.g := by
      rw [hP.jointlyReflectEpimorphisms.epi_iff]
      exact fun i ↦ (hS i).epi_g
    exact { exact := (hP.exact_iff S).2 (fun i ↦ (hS i).exact) }

Goal state after: