mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in ↑i..↑(i + 1), f ↑i ≤ ∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in ↑i..↑(i + 1), g x

Tactic:
gcongr with i hi
    apply integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)
    exact h _ (by simpa using hi) _ (Ioo_subset_Ico_self hx)

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.range (b - a), f ↑(a + (x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Tactic:
suffices ∑ x ∈ .range (b - a), f (a + ↑(x + 1)) ≤ ∫ x in a..a + ↑(b - a), f x by simp_all

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.range (b - a), f (↑a + ↑(x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ Summable fun n ↦ f ↑n

Tactic:
by
  rw [← summable_nat_add_iff (N + 1)]
  refine summable_of_sum_range_le (c := ∫ t in Ioi (N : ℝ), f t) (by grind) fun M ↦ ?_
  calc
    _ = ∑ n ∈ Finset.Ico N (N + M), f (n + 1 : ℕ) := by rw [Finset.sum_Ico_eq_sum_range]; grind
    _ ≤ _ := (anti.mono Icc_subset_Ici_self).sum_Ico_le_integral integrable nonneg

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ ((yonedaYonedaColimit F).app (op X)).inv =
    (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (yoneda.op.obj (op X))).hom ≫
      colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Tactic:
dsimp [yonedaYonedaColimit]
  simp only [Iso.cancel_iso_hom_left]
  apply colimit.hom_ext
  intro j
  rw [colimit.ι_post, ι_colimMap_assoc]
  simp only [← CategoryTheory.Functor.assoc, comp_evaluation]
  rw [ι_preservesColimitIso_inv_assoc]
  simp only [← comp_evaluation, comp_obj, evaluation_obj_obj, yoneda_obj_obj, uliftFunctor_obj,
    whiskerLeft_app, uliftFunctor_map, Functor.comp_map, evaluation_obj_map, yoneda_map_app]
  ext η Y f
  dsimp [largeCurriedYonedaLemma, yonedaOpCompYonedaObj, yonedaEquiv]
  simp only [← comp_apply, Category.assoc, colimitObjIsoColimitCompEvaluation_ι_inv,
    ← NatTrans.naturality, ← NatTrans.naturality_assoc, yoneda_obj_obj, yoneda_obj_map,
    Quiver.Hom.unop_op]
  simp

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

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * c * (c ^ 2)⁻¹ ≤ c ^ 2

Tactic:
mul_assoc,

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * (c * (c ^ 2)⁻¹) ≤ c ^ 2
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2) ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2

Tactic:
rw [← mul_sum, ← mul_div_assoc']

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹ / j ^ 2)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : ∀ (b : B), IsConnected (CostructuredArrow L (R.obj b))
b : B
⊢ IsConnected (CostructuredArrow (snd L R) b)

Tactic:
have := final_of_adjunction (costructuredArrowSndAdjunction L R b)

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : ∀ (b : B), IsConnected (CostructuredArrow L (R.obj b))
b : B
this : (costructuredArrowSndInclusion L R b).Final
⊢ IsConnected (CostructuredArrow (snd L R) b)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this✝¹ : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
this✝ : (fst R.op L.op).Initial
this : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Initial
⊢ (snd L R).Final

Tactic:
have : (snd L R).op.Initial := initial_of_natIso <| opFunctorCompFst _ _

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this✝² : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
this✝¹ : (fst R.op L.op).Initial
this✝ : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Initial
this : (snd L R).op.Initial
⊢ (snd L R).Final
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ (J : ι → Type w) [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [inst_2 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct F)), IsIso (colimitPointwiseProductToProductColimit F)
J : ι → Type w
x✝² : (i : ι) → SmallCategory (J i)
x✝¹ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
x✝ : ∀ (i : ι), HasColimit (F i)
w✝ : HasColimit (pointwiseProduct F)
h : IsIso (colimitPointwiseProductToProductColimit F)
⊢ Nonempty (IsColimit (coconePointwiseProduct fun i ↦ colimit.cocone (F i)))

Tactic:
IsColimit.nonempty_isColimit_iff_isIso_desc (colimit.isColimit _)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ (J : ι → Type w) [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [inst_2 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct F)), IsIso (colimitPointwiseProductToProductColimit F)
J : ι → Type w
x✝² : (i : ι) → SmallCategory (J i)
x✝¹ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
x✝ : ∀ (i : ι), HasColimit (F i)
w✝ : HasColimit (pointwiseProduct F)
h : IsIso (colimitPointwiseProductToProductColimit F)
⊢ IsIso ((colimit.isColimit (pointwiseProduct F)).desc (coconePointwiseProduct fun i ↦ colimit.cocone (F i)))
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (functor C).Faithful

Tactic:
functor

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (F C ⋙ G C ⋙ H C).Faithful
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (functor C).Full

Tactic:
functor

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (F C ⋙ G C ⋙ H C).Full
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteLimits (functor C)

Tactic:
functor

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteLimits (F C ⋙ G C ⋙ H C)
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteColimits (functor C)

Tactic:
functor

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteColimits (F C ⋙ G C ⋙ H C)
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
⊢ Over.Hom.left (Φ.toColon Ψ).hom ≫ Φ.colonπ Ψ = 0

Tactic:
simp [toColon]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Tactic:
rw [Category.assoc]
          congr

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
φ : P.cocomplex ⟶ Q.cocomplex
comm : P.ι.f 0 ≫ φ.f 0 = f ≫ Q.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map f ≫ Q.toRightDerivedZero' F =
    P.toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0

Tactic:
simp only [← cancel_mono (HomologicalComplex.iCycles _ _), assoc,
    toRightDerivedZero'_comp_iCycles,
    CochainComplex.single₀_obj_zero, HomologicalComplex.cyclesMap_i,
    Functor.mapHomologicalComplex_map_f, toRightDerivedZero'_comp_iCycles_assoc,
    ← F.map_comp, comm]

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

Goal state before:
pp: 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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this : PreservesLimit (parallelPair NormalMono.g 0) L
⊢ NormalMono (L.map f')

Tactic:
exact {
      Z := L.obj hf'.Z
      g := L.map hf'.g
      w := by rw [← L.map_comp]; simp [hf'.w]
      isLimit :=
        (KernelFork.isLimitMapConeEquiv _ L).1
          (isLimitOfPreserves L hf'.isLimit) }

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
⊢ { l //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }

Tactic:
by
    have := fun Y ↦ h Y |>.mono
    refine ⟨((h X).lift' s.ι ?_).1, ?_, ?_⟩
    · rw [← cancel_mono (adj₁.unit.app ((h X).Z)), assoc, ← adj₁.unit_naturality (h _).left]
      dsimp only [Functor.comp_obj]
      have := s.condition
      dsimp only [Functor.comp_obj] at this
      rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]
    · apply ((h X).lift' s.ι _).2
    · intro m hm
      rw [← cancel_mono (adj₁.unit.app X)]
      apply hm.trans ((h X).lift' s.ι _).2.symm

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
this : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := inferInstance
⊢ R' ⋙ (Monad.comparison (monadicAdjunction U)).inv ≅ R

Tactic:
exact Functor.isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm ≪≫ R.rightUnitor

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

Goal state before:
pp: case mk.id
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p f✝

Tactic:
| _ =>

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

Goal state before:
pp: case mk.associator
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (fun p ↦ normalizeAux p ((f✝ ≫ g✝) ≫ h✝)) = fun p ↦ normalizeAux p (f✝ ≫ g✝ ≫ h✝)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.associator_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (fun p ↦ normalizeAux p (f✝ ≫ g✝ ≫ h✝)) = fun p ↦ normalizeAux p ((f✝ ≫ g✝) ≫ h✝)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.right_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p ↦ normalizeAux p (f✝ ≫ 𝟙 b✝)) = fun p ↦ normalizeAux p f✝

Tactic:
| _ =>

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

Goal state before:
pp: case mk.right_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p (f✝ ≫ 𝟙 b✝)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.left_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p ↦ normalizeAux p (𝟙 a✝ ≫ f✝)) = fun p ↦ normalizeAux p f✝

Tactic:
| _ =>

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

Goal state before:
pp: case mk.left_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
⊢ (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p (𝟙 a✝ ≫ f✝)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.associator
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.associator f✝ g✝ h✝) ≫ (normalizeIso p (f✝ ≫ g✝ ≫ h✝)).hom =
    (normalizeIso p ((f✝ ≫ g✝) ≫ h✝)).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.associator_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.associator_inv f✝ g✝ h✝) ≫
      (normalizeIso p ((f✝ ≫ g✝) ≫ h✝)).hom =
    (normalizeIso p (f✝ ≫ g✝ ≫ h✝)).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.right_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.right_unitor f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p (f✝ ≫ 𝟙 b✝)).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.right_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.right_unitor_inv f✝) ≫ (normalizeIso p (f✝ ≫ 𝟙 b✝)).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.left_unitor
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.left_unitor f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p (𝟙 a✝ ≫ f✝)).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| _ =>

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

Goal state before:
pp: case mk.left_unitor_inv
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.left_unitor_inv f✝) ≫ (normalizeIso p (𝟙 a✝ ≫ f✝)).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
| _ =>

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i) =
    StructuredArrow.hom (t.whisker h)

Tactic:
← cancel_mono (α_ h _ _).hom

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (StructuredArrow.hom (s.whisker h) ≫ (postcomp x f).map (h ◁ StructuredArrow.Hom.right i)) ≫ (α_ h t.lift f).hom =
    StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ (𝟙 a ≫ f).fiber = f.fiber ≫ eqToHom ⋯

Tactic:
· simp [F.mapComp_id_right_inv_app, Strict.rightUnitor_eqToIso, ← NatTrans.naturality_assoc,
        ← Cat.Hom₂.comp_app]

Goal state after:
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
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst✝¹ : ChosenPullbacksAlong g'
inst✝ : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_3
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_5
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_7
⊢ δ₁ ≫ f' ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f

Tactic:
comm₁,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝² : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst✝¹ : ChosenPullbacksAlong g'
inst✝ : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_3
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_5
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_7
⊢ δ₁ ≫ γ₁ ≫ f = (δ₁ ≫ γ₁) ≫ f
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

Goal state after:
case inl.inl
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
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inl_ C C').map f✝¹ = (Sum.inl_ C C').map f✝

case inr.inr
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'
f✝¹ f✝ : x✝ ⟶ y✝
⊢ (Sum.inr_ C C').map f✝¹ = (Sum.inr_ C C').map f✝
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
x y z : A ⊕ B
f : x ⟶ y
g : y ⟶ z
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (f ≫ g) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) f ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) g

Tactic:
cases f <;> cases g

Goal state after:
case inl.inl
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
x✝ y✝¹ : A
f✝¹ : x✝ ⟶ y✝¹
y✝ : A
f✝ : y✝¹ ⟶ y✝
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝¹ ≫ (Sum.inl_ A B).map f✝) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝¹) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inl_ A B).map f✝)

case inr.inr
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ C
G : B ⥤ C
x✝ y✝¹ : B
f✝¹ : x✝ ⟶ y✝¹
y✝ : B
f✝ : y✝¹ ⟶ y✝
⊢ Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝¹ ≫ (Sum.inr_ A B).map f✝) =
    Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝¹) ≫
      Sum.homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) ((Sum.inr_ A B).map f✝)
Module: Mathlib.CategoryTheory.Sums.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ B
G : C ⥤ D
a a' : A
f : a ⟶ a'
⊢ (F.sum G).map ((Sum.inl_ A C).map f) = (Sum.inl_ B D).map (F.map f)

Tactic:
by
  simp [sum]

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

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ B
G : C ⥤ D
c c' : C
f : c ⟶ c'
⊢ (F.sum G).map ((Sum.inr_ A C).map f) = (Sum.inr_ B D).map (G.map f)

Tactic:
by
  simp [sum]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
x✝ : IsIso ((forgetful 𝒳 𝒴).map α)
⊢ IsIso α

Tactic:
constructor
    use {
      toNatTrans := inv ((forgetful 𝒳 𝒴).map α)
      isHomLift' := fun a ↦ by simp [lift_id_inv_isIso] }
    aesop

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseLeftDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ L.HasPointwiseRightKanExtensionAt F Y

Tactic:
rw [← hasPointwiseRightKanExtensionAt_iff_of_iso _ F (L.objObjPreimageIso Y),
    ← F.hasPointwiseLeftDerivedFunctorAt_iff L W]

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseLeftDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ F.HasPointwiseLeftDerivedFunctorAt W (L.objPreimage Y)