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

Goal state before:
pp: case refine_1
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
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
⊢ ∀ᶠ (b : ℕ) in atTop, d < u b / ↑b

Tactic:
obtain ⟨ε, hε, εpos⟩ : ∃ ε : ℝ, d + ε * (1 + l) < l ∧ 0 < ε := by
      have L : Tendsto (fun ε => d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
      simp only [zero_mul, add_zero] at L
      exact (((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists
    filter_upwards [B ε εpos, Ioi_mem_atTop 0] with n hn npos
    simp_rw [div_eq_inv_mul]
    calc
      d < (n : ℝ)⁻¹ * n * (l - ε * (1 + l)) := by
        rw [inv_mul_cancel₀, one_mul]
        · linarith only [hε]
        · exact Nat.cast_ne_zero.2 (ne_of_gt npos)
      _ = (n : ℝ)⁻¹ * (n * l - ε * (1 + l) * n) := by ring
      _ ≤ (n : ℝ)⁻¹ * u n := by gcongr; linarith only [hn]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case min.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure f (max n m).succ).fst

pp: case min.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨(max n m).succ, ?min.refine_1⟩ =
    {
        obj :=
          min (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
            (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj

Tactic:
· simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]

Goal state after:
case min.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f
      ⟨(max n m).succ, ⋯.mpr (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)⟩ =
    {
        obj :=
          min (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
            (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case min.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f
      ⟨(max n m).succ, ⋯.mpr (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)⟩ =
    {
        obj :=
          min (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
            (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj

Tactic:
· simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case eq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f
      ⟨(max n m).succ, ⋯.mpr (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')⟩ =
    { obj := eq g g', property := ⋯ }.obj

Tactic:
· simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl

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

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                  (limit.π K j) ≫
                (functorToInterchangeIso A K).inv.app j).app
            i ≫
          ((flipFunctorToInterchange A K).hom.app i ≫
                  colimit.ι ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ (whiskeringLeft J Cᵒᵖ (Type u)).obj K) i ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom).app
              j ≫
            (K.isoWhiskerLeft
                    ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                      (Presheaf.isColimitTautologicalCocone A))).hom.app
              j

Tactic:
ι_colimitCompWhiskeringLeftIsoCompColimit_hom,

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                  (limit.π K j) ≫
                (functorToInterchangeIso A K).inv.app j).app
            i ≫
          ((flipFunctorToInterchange A K).hom.app i ≫
                  K.whiskerLeft (colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda) i)).app
              j ≫
            (K.isoWhiskerLeft
                    ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                      (Presheaf.isColimitTautologicalCocone A))).hom.app
              j
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ C
F : C ⥤ Type u₂
inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((colimitHomIsoLimitYoneda (D.rightOp ⋙ coyoneda) F).hom ≫
          limit.π ((D.rightOp ⋙ coyoneda).op ⋙ yoneda.obj F) (op i) ≫
            ((D ⋙ Prod.sectL C F).isoWhiskerLeft (coyonedaLemma C)).hom.app (op i)))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj (op i))))
          ((ConcreteCategory.hom ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)))) (𝟙 (D.obj (op i)))) }

Tactic:
rw [← Category.assoc, colimitHomIsoLimitYoneda_hom_comp_π]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ C
F : C ⥤ Type u₂
inst✝¹ : HasColimit (D.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ (ConcreteCategory.hom
        ((yoneda.obj F).map (colimit.ι (D.rightOp ⋙ coyoneda) i).op ≫
          ((D ⋙ Prod.sectL C F).isoWhiskerLeft (coyonedaLemma C)).hom.app (op i)))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj (op i))))
          ((ConcreteCategory.hom ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)))) (𝟙 (D.obj (op i)))) }
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ (ConcreteCategory.hom
        ((colimitHomIsoLimitYoneda (D.unop ⋙ yoneda) F).hom ≫
          limit.π ((D.unop ⋙ yoneda).op ⋙ yoneda.obj F) i ≫
            ((D ⋙ Prod.sectL Cᵒᵖ F).isoWhiskerLeft (yonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }

Tactic:
rw [← Category.assoc, colimitHomIsoLimitYoneda_hom_comp_π]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ (ConcreteCategory.hom
        ((yoneda.obj F).map (colimit.ι (D.unop ⋙ yoneda) (unop i)).op ≫
          ((D ⋙ Prod.sectL Cᵒᵖ F).isoWhiskerLeft (yonedaLemma C)).hom.app i))
      f =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ a ∈ (ModuleCat.Hom.hom y.hom).range

Tactic:
refine ⟨q a'', ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom y.hom) ((ConcreteCategory.hom q) a'') = a
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
hz : L.map z ≫ L.map f = 0
⊢ L.map z = 0

Tactic:
rw [← L.map_comp] at 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 ≫ 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
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

Tactic:
rw [← L.map_comp] at 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 ≫ z) = 0
⊢ L.map z = 0
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
J : Type u_3
inst✝¹ : Category.{v_2, u_3} J
K : J ⥤ Action V G
inst✝ : HasColimit (K ⋙ forget V G)
⊢ PreservesColimit K (forget V G)

Tactic:
change PreservesColimit K ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
  have (k : SingleObj G) :
      HasColimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
    inferInstanceAs (HasColimit (K ⋙ forget V G))
  infer_instance

Goal state after:
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✝ : Preadditive V
X Y : Action V G
f : X ⟶ Y
⊢ ∀ (g : G), X.ρ g ≫ (-f.hom) = (-f.hom) ≫ Y.ρ g

Tactic:
by simp [f.comm]

Goal state after:
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✝ : Preadditive V
X Y : Action V G
n : ℕ
f : X ⟶ Y
⊢ ∀ (g : G), X.ρ g ≫ (n • f.hom) = (n • f.hom) ≫ Y.ρ g

Tactic:
by simp [f.comm]

Goal state after:
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✝ : Preadditive V
X Y : Action V G
n : ℤ
f : X ⟶ Y
⊢ ∀ (g : G), X.ρ g ≫ (n • f.hom) = (n • f.hom) ≫ Y.ρ g

Tactic:
by simp [f.comm]

Goal state after:
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✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r : R
f : X ⟶ Y
⊢ ∀ (g : G), X.ρ g ≫ (r • f.hom) = (r • f.hom) ≫ Y.ρ g

Tactic:
by simp [f.comm]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ T.map (T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ (beckAlgebraCofork X).π ≫ { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ?refine_1 } = s.π

pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt},
    (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ?refine_1 }

Tactic:
· dsimp
      rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ (beckAlgebraCofork X).π ≫ { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ } = s.π

case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt},
    (beckAlgebraCofork X).π ≫ m = s.π → m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a' ⟶ F.obj a
g : a ⟶ b
⊢ f ◁ Γ.app a ▷ G.map g ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ F.map g ◁ Γ.app b

Tactic:
simp_rw [← whiskerLeft_comp, naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : Modification η θ
b c : B
a' : C
f : a' ⟶ F.obj b
g : b ⟶ c
⊢ f ◁ F.map g ◁ Γ.app c ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ Γ.app b ▷ G.map g

Tactic:
simp_rw [← Bicategory.whiskerLeft_comp, naturality]

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
⊢ ∀ {X Y Z : (i : I) × C i} (f : X ⟶ Y) (g : Y ⟶ Z), descMap F X Z (f ≫ g) = descMap F X Y f ≫ descMap F Y Z g

Tactic:
rintro ⟨i, X⟩ ⟨_, Y⟩ ⟨_, Z⟩ ⟨f⟩ ⟨g⟩

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
i : I
X Y✝¹ : C i
f : X ⟶ Y✝¹
Y✝ : C i
g : Y✝¹ ⟶ Y✝
⊢ descMap F ⟨i, X⟩ ⟨i, Y✝⟩ (SigmaHom.mk f ≫ SigmaHom.mk g) =
    descMap F ⟨i, X⟩ ⟨i, Y✝¹⟩ (SigmaHom.mk f) ≫ descMap F ⟨i, Y✝¹⟩ ⟨i, Y✝⟩ (SigmaHom.mk g)
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) 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₃
⊢ 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 ⋯

Tactic:
obtain ⟨h₁, h₂⟩ := h

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) 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₃
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inr a'
⊢ 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 ⋯
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMultiplicative
h : ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (f ⊗ₘ g)
X x✝¹ x✝ : C
g : x✝¹ ⟶ x✝
hg : W g
⊢ W (X ◁ g)

Tactic:
by simpa using h (𝟙 X) g (W.id_mem _) hg

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₃ Y₁ : LocalizedMonoidal L W ε
i : X₁ ≅ Y₁
⊢ i.hom ▷ X₂ ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom ≫ i.inv ▷ (X₂ ⊗ X₃) = (α_ X₁ X₂ X₃).hom

Tactic:
by
  simp only [associator_naturality₁_assoc, ← whiskerRight_comp,
    Iso.hom_inv_id, whiskerRight_id, comp_id]

Goal state after:
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✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ X ◁ coprod.inl ≫ (∂L X Y Z).inv = coprod.inl

Tactic:
apply (cancel_iso_hom_right _ _ (∂L X Y Z)).mp

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ (X ◁ coprod.inl ≫ (∂L X Y Z).inv) ≫ (∂L X Y Z).hom = coprod.inl ≫ (∂L X Y Z).hom
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✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ X ◁ coprod.inr ≫ (∂L X Y Z).inv = coprod.inr

Tactic:
apply (cancel_iso_hom_right _ _ (∂L X Y Z)).mp

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ (X ◁ coprod.inr ≫ (∂L X Y Z).inv) ≫ (∂L X Y Z).hom = coprod.inr ≫ (∂L X Y Z).hom
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ p.obj b = T

Tactic:
domain_eq p (𝟙 T) ψ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₂} 𝒳
inst✝² : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst✝ : p.IsHomLift (𝟙 T) ψ
⊢ T = T
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: 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✝⁵ : HasZeroMorphisms C
inst✝⁴ : (i : I) → HasZeroMorphisms (D i)
inst✝³ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), (F i).PreservesHomology
inst✝ : HasZeroObject C
S : ShortComplex C
⊢ S.Exact ↔ ∀ (i : I), (S.map (F i)).Exact

Tactic:
refine ⟨fun hS i ↦ hS.map _, fun hS ↦ ?_⟩
  simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢
  rw [hP.isZero_iff]
  exact fun i ↦ (hS i).of_iso (S.mapHomologyIso (F i)).symm

Goal state after: