mathlib-initiative/mathlib-tactics huggingface dataset:
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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
⊢ 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
εpos

Goal state after:
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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case b0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ 0 ≤ f x

Tactic:
fpos

Goal state after:
case b0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ f ↑a ≤ f x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
⊢ ∑ i ∈ Finset.Ico a b, f ↑i * g ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, f x * g (x - 1)

Tactic:
apply sum_Ico_le_integral_of_le (f := fun x ↦ f x * g x) hab
  · intro i hi x hx
    simp only [Nat.cast_add, Nat.cast_one, mem_Ico, ← Nat.add_one_le_iff] at hx hi
    rify at hi
    gcongr
    · grw [gpos]; apply hg <;> grind
    · grw [fpos]; apply hf <;> grind
    · apply hf <;> grind
    · apply hg <;> grind
  · apply Integrable.mono_measure _ (volume.restrict_mono_set Ico_subset_Icc_self)
    apply (hf.integrableOn_isCompact isCompact_Icc).mul_of_top_left
    apply AntitoneOn.memLp_isCompact isCompact_Icc
    intro _ _ _ _ _
    apply hg <;> grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case b0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ 0 ≤ f ↑i

Tactic:
fpos

Goal state after:
case b0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ f ↑b ≤ f ↑i
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
G : (s : α) → I s ⥤ C := fun s ↦ (F.obj { as := s }).presentation.F
s : Discrete α
⊢ colimit (G s.as ⋙ Ind.yoneda) ≅ F.obj s

Tactic:
exact Ind.colimitPresentationCompYoneda _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : PreservesFiniteLimits (F C)
⊢ PreservesFiniteLimits (F C ⋙ G C ⋙ H C)

Tactic:
have : PreservesFiniteLimits (G C) := by rw [G]; apply preservesFiniteLimits_rightOp

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

Goal state before:
pp: case refine_1
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
y y' : (fun X ↦ X) (colimit (pointwiseProduct F))
hy : (hom (colimitPointwiseProductToProductColimit F)) y = (hom (colimitPointwiseProductToProductColimit F)) y'
⊢ y = y'

pp: case refine_2
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : (fun X ↦ X) (∏ᶜ fun s ↦ colimit (F s))
⊢ ∃ a, (hom (colimitPointwiseProductToProductColimit F)) a = x

Tactic:
· obtain ⟨ky, yk₀, hyk₀⟩ := Types.jointly_surjective' y
    obtain ⟨ky', yk₀', hyk₀'⟩ := Types.jointly_surjective' y'
    let k := IsFiltered.max ky ky'
    let yk : (pointwiseProduct F).obj k :=
      (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
    let yk' : (pointwiseProduct F).obj k :=
      (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
    obtain rfl : y = colimit.ι (pointwiseProduct F) k yk := by
      simp only [k, yk, colimit.w_apply, hyk₀]
    obtain rfl : y' = colimit.ι (pointwiseProduct F) k yk' := by
      simp only [k, yk', colimit.w_apply, hyk₀']
    dsimp at yk yk'
    have hch : ∀ (s : α), ∃ (i' : I s) (hi' : k s ⟶ i'),
        (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk) =
          (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk') := by
      intro s
      have hy₁ := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s) yk
      have hy₂ := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s) yk'
      dsimp at hy₁ hy₂ hy
      rw [← hy, hy₁, Types.FilteredColimit.colimit_eq_iff] at hy₂
      obtain ⟨i₀, f₀, g₀, h₀⟩ := hy₂
      refine ⟨IsFiltered.coeq f₀ g₀, f₀ ≫ IsFiltered.coeqHom f₀ g₀, ?_⟩
      conv_rhs => rw [IsFiltered.coeq_condition]
      dsimp [Functor.pi] at h₀
      simp [h₀]
    choose k' f hk' using hch
    apply Types.colimit_sound' f f
    exact Types.limit_ext' _ _ _ (fun ⟨s⟩ => by simpa [Functor.pi, Pi.map_π_apply] using hk' s)

Goal state after:
case refine_2
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : (fun X ↦ X) (∏ᶜ fun s ↦ colimit (F s))
⊢ ∃ a, (hom (colimitPointwiseProductToProductColimit F)) a = x
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms

Tactic:
rw [injective_iff_preservesEpimorphisms_yoneda_obj]
  refine
    ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrpCat)).PreservesEpimorphisms => ?_, ?_⟩
  · exact
      Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)
  · intro
    exact (inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)

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

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : (fun X ↦ X) (∏ᶜ fun s ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk : ∀ (s : α), (hom (colimit.ι (F s) (k s))) (p s) = (hom (Pi.π (fun s ↦ colimit (F s)) s)) x
x✝ : Discrete α
s : α
this :
  (hom (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (productIso fun j ↦ (F j).obj (k j)).inv) p) =
    (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) ((hom (productIso fun j ↦ (F j).obj (k j)).inv) p)
⊢ (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) ((hom (productIso fun j ↦ (F j).obj (k j)).inv) p) =
    (hom (limit.π (Discrete.functor fun s ↦ colimit (F s)) { as := s })) x

Tactic:
simpa [Functor.pi] using hk _

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
inst✝³ : HasProductsOfShape ι C
inst✝² : IsIPCOfShape.{w, u_1, v, u} ι C
inst✝¹ : HasFilteredColimitsOfSize.{w, w, v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ D ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
by
    refine ⟨evaluationJointlyReflectsColimits _ fun X ↦ ?_⟩
    exact IsColimit.equivOfNatIsoOfIso (pointwiseProductCompEvaluation F X).symm _ _
      (evaluationCoconePointwiseProductIso F X c).symm
      (IsIPCOfShape.nonempty_isColimit fun i ↦ isColimitOfPreserves _ (hc i)).some

Goal state after:
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
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
⊢ (Φ.colon Ψ).ι.app X ≫ Φ.π.app X = 0

Tactic:
colon_ι_app_π_app,

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
⊢ (Φ.colonπ Ψ).app X ≫ Ψ.ι.app (Φ.quotient.obj X) = 0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0

Tactic:
exact (pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))

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.fst (Abelian.factorThruImage S.f) c ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f) =
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f)

Tactic:
by
          rw [← Category.assoc, pullback.condition]

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

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
inst✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization G.kernel.isoModSerre

Tactic:
by
  rw [isoModSerre_kernel_eq_inverseImage_isomorphisms G]
  exact adj.isLocalization

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 : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Mono (L.map f)
⊢ L.map 0 = 0

Tactic:
L.map_zero

Goal state after:
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 : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Mono (L.map f)
⊢ 0 = 0
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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
⊢ ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0

Tactic:
intro Z z hz

Goal state after:
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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : L.map z ≫ L.map f = 0
⊢ L.map z = 0
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 : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ L.map 0 = 0

Tactic:
L.map_zero

Goal state after:
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 : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ 0 = 0
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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
hf : P.epiModSerre f
⊢ ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0

Tactic:
intro Z z hz

Goal state after:
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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
hz : L.map f ≫ L.map z = 0
⊢ L.map z = 0
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
F : N ⋊[φ] G →* H
⊢ F = lift (F.comp inl) (F.comp inr) ⋯

Tactic:
DFunLike.ext_iff

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G), F x = (lift (F.comp inl) (F.comp inr) ⋯) x
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteLimits V
⊢ PreservesFiniteLimits ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
have : PreservesFiniteLimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) := by
    constructor
    intro _ _ _
    infer_instance

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteLimits V
this : PreservesFiniteLimits ((evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ PreservesFiniteLimits ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.obj X)ᘁ ◁ F.map f ≫ (F.obj X)ᘁ ◁ inv (F.map f) ≫ ε_ (F.obj X) (F.obj X)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ

Tactic:
← MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.obj X)ᘁ ◁ (F.map f ≫ inv (F.map f)) ≫ ε_ (F.obj X) (F.obj X)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: case refine_1
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ F.map (U.map (h X).right ≫ U.map (adj₁.counit.app X)) ≫ s.π = adj₁.counit.app (h X).W ≫ (h X).right ≫ s.π

Tactic:
F.map_comp_assoc,

Goal state after:
case refine_1
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ F.map (U.map (h X).right) ≫ F.map (U.map (adj₁.counit.app X)) ≫ s.π = adj₁.counit.app (h X).W ≫ (h X).right ≫ s.π
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ

Tactic:
intro a b f g h η θ

Goal state after:
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ Quot.lift (liftHom₂ F) ⋯ (η ≫ θ) = Quot.lift (liftHom₂ F) ⋯ η ≫ Quot.lift (liftHom₂ F) ⋯ θ
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) = F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm

Tactic:
by
  ext
  simp [naturality_id_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u

Tactic:
rw [← rightZigzag, Hε]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ ((ρ_ u).hom ≫ (λ_ u).inv) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq t l r b
⊢ l ≫ b = t ≫ r

Tactic:
by rw [sq.w]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ f.fix a'
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Tactic:
simp only [fix, Part.mem_assert_iff] at h₃

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ :
  ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a' h
⊢ ∃ h,
    b ∈
      WellFounded.fixF
        (fun a IH ↦
          Part.assert (f a).Dom fun hf ↦
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.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✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
hsT : ∀ (X : AsSmall T), sT.counitInv.app X = 𝟙 ((𝟭 (AsSmall T)).obj X)
X : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x
⊢ (𝟭 (AsSmall T)).map (Iso.refl (F''.obj X).left).hom ≫
      ((pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)).obj X).hom =
    (F''.obj X).hom

Tactic:
simp [F'', hsT]

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₁ X₂ X₃ : C
⊢ (((Localization.associator L' L' L' L' L' L' W W W W W (curriedAssociatorNatIso C) (tensorBifunctor L W ε)
                    (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)).hom.app
              (L'.obj X₁)).app
          (L'.obj X₂)).app
      (L'.obj X₃) =
    ((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv

Tactic:
Localization.associator_hom_app_app_app

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₁ X₂ X₃ : C
⊢ ((tensorBifunctor L W ε).map
            (((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                        (tensorBifunctor L W ε)).hom.app
                  X₁).app
              X₂)).app
        (L'.obj X₃) ≫
      ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                    (tensorBifunctor L W ε)).hom.app
              (((curriedTensor C).obj X₁).obj X₂)).app
          X₃ ≫
        L'.map ((((curriedAssociatorNatIso C).hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                        (tensorBifunctor L W ε)).inv.app
                  X₁).app
              (((curriedTensor C).obj X₂).obj X₃) ≫
            ((tensorBifunctor L W ε).obj (L'.obj X₁)).map
              (((Lifting₂.iso L' L' W W
                          (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                          (tensorBifunctor L W ε)).inv.app
                    X₂).app
                X₃) =
    ((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ▷ X

Tactic:
by
  rw [rightDistrib_hom, coprod.inr_desc]

Goal state after: