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
ε : ℝ
ε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, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(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
aN' : a ≤ N - 1
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
have cNn : c (N - 1) ≤ n := by
      have : N - 1 < N := Nat.pred_lt Npos.ne'
      simpa only [not_lt] using Nat.find_min exN this

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 < ε
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, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n
Module: Mathlib.CategoryTheory.Generator.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasColimits C
inst✝ : EnoughProjectives C
G : C
hG : IsCoseparator G
T : Cᵒᵖ
hT₁ : Injective T
hT₂ : IsCoseparator T
⊢ ∃ G, Projective G ∧ IsSeparator G

Tactic:
exact ⟨unop T, inferInstance, (isSeparator_unop_iff _).2 hT₂⟩

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
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
⊢ Tendsto (fun ε ↦ l + ε * (1 + ε + l)) (𝓝 0) (𝓝 (l + 0 * (1 + 0 + l)))

Tactic:
exact
          tendsto_const_nhds.add
            (tendsto_id.mul ((tendsto_const_nhds.add tendsto_id).add tendsto_const_nhds))

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case refine_2
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∀ᶠ (i : ℕ) in atTop, ∫ (x : ℝ) in ↑N..↑i + ↑N, ‖f x‖ ≤ ∑' (n : ℕ), f ↑(n + N)

Tactic:
filter_upwards [eventually_gt_atTop 0] with M hM
    calc
      _ = ∫ x in N..M+N, f x := by
        refine intervalIntegral.integral_congr_uIoo fun x ↦ ?_
        grind [Real.norm_of_nonneg, uIoo_of_le]
      _ ≤ ∑ n ∈ Finset.range M, f (n + N : ℕ) := by
        convert! AntitoneOn.integral_le_sum (anti.mono _) using 2 <;> grind
      _ ≤ _ := by grind [summable.sum_le_tsum, Nat.cast_pos]

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

Goal state before:
pp: case max.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ (FilteredClosureSmall.bundledAbstractFilteredClosure f (Max.max n m).succ).fst

pp: case max.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f ⟨(Max.max n m).succ, ?max.refine_1⟩ =
    {
        obj :=
          max (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
            (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj

Tactic:
· simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
      refine FilteredClosureSmall.InductiveStep.max ?_ ?_ x y
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]

Goal state after:
case max.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f
      ⟨(Max.max n m).succ, ⋯.mpr (FilteredClosureSmall.InductiveStep.max ⋯ ⋯ x y)⟩ =
    {
        obj :=
          max (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
            (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ Real.log j / Real.log c * Real.log (c⁻¹ ^ 2) = Real.log (1 / j ^ 2)

Tactic:
simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]

Goal state after:
case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ Real.log j / Real.log c * (↑2 * Real.log c) = ↑2 * Real.log j
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1).inv.f 0 ≫
      (HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat).f 0 =
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv

Tactic:
rw [HomologicalComplex.extendMap_f _ _ (i := 0) (by simp),
    HomologicalComplex.extendSingleIso_inv_f]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ ((HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
        (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X).inv ≫
          (((HomologicalComplex.single C (ComplexShape.up ℕ) 0).obj X).extendXIso ComplexShape.embeddingUpNat
              ι'._proof_1).inv) ≫
      (((HomologicalComplex.single C (ComplexShape.up ℕ) 0).obj X).extendXIso ComplexShape.embeddingUpNat ⋯).hom ≫
        R.ι.f 0 ≫ (HomologicalComplex.extendXIso R.cocomplex ComplexShape.embeddingUpNat ⋯).inv =
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ Mono (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ })

Tactic:
rw [ModuleCat.mono_iff_injective]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ Function.Injective
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ sq₁.IsPullback ↔ sq₂.IsPullback

Tactic:
by
  rw [← IsPullback.map_iff sq₁ uliftFunctor.{max u v},
      ← IsPullback.map_iff sq₂ uliftFunctor.{max u v}]
  refine iff_of_iso (Square.isoMk
    (((Equiv.trans Equiv.ulift e₁).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₂).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₃).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₄).trans Equiv.ulift.symm).toIso)
    ?_ ?_ ?_ ?_)
  all_goals ext; apply ULift.down_injective
  · simpa [types_comp, uliftFunctor_map] using congrFun comm₁₂ _
  · simpa [types_comp, uliftFunctor_map] using congrFun comm₁₃ _
  · simpa [types_comp, uliftFunctor_map] using congrFun comm₂₄ _
  · simpa [types_comp, uliftFunctor_map] using congrFun comm₃₄ _

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

Goal state before:
pp: case inr
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.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.f
l : L.obj φ.X' ⟶ L.obj (kernel f)
hl : l ≫ L.map (kernel.ι f) = L.map φ.f
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w

Tactic:
exact ⟨(L.objObjPreimageIso W).inv ≫ inv (L.map φ.s) ≫ l, by simp [hl, ← hφ]⟩

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

Goal state before:
pp: 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
⊢ { l //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }

Tactic:
have h₂ : (T : C ⥤ C).map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f := s.π.h

Goal state after:
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
⊢ { l //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: 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
⊢ { l //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }

Tactic:
refine ⟨⟨T.η.app _ ≫ s.π.f, ?_⟩, ?_, ?_⟩

Goal state after:
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

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.π

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 }
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ F.map (U.map (R.map f)) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f

Tactic:
simp [dsimp% adj₂.homEquiv_unit _ _ f ]

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

Goal state before:
pp: case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g✝) =
    (normalizeAux nil f).comp (normalizeAux nil (g.comp g✝))

Tactic:
ihg g,

Goal state after:
case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (f.comp g✝) = (normalizeAux nil f).comp (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ ((normalizeAux nil f).comp (normalizeAux nil g)).comp (normalizeAux nil g✝) =
    (normalizeAux nil f).comp ((normalizeAux nil g).comp (normalizeAux nil g✝))
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a : ∫ F
⊢ eqToHom ⋯ ≫
      { base := (𝟙 a).base,
          fiber :=
            (α.naturality (𝟙 a).base.toLoc).inv.toNatTrans.app a.fiber ≫
              (α.app { as := a.base }).toFunctor.map (𝟙 a).fiber }.fiber =
    (𝟙 { base := a.base, fiber := (α.app { as := a.base }).toFunctor.obj a.fiber }).fiber

Tactic:
· simp [StrongTrans.naturality_id_inv_app, ← map_comp, ← Cat.Hom₂.comp_app]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
⊢ t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit

Tactic:
simpa [bicategoricalComp] using τ₀'.w

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
⊢ b ∈ f.fix a

Tactic:
simp only [fix, Part.mem_assert_iff]
    rcases h with (⟨h₁, h₂⟩ | ⟨a', h, h₃⟩)
    · refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
      · injection Part.mem_unique ⟨h₁, h₂⟩ h'
      · rw [WellFounded.fixF_eq]
        -- Porting note: used to be simp [h₁, h₂]
        apply Part.mem_assert h₁
        split
        next e =>
          injection h₂.symm.trans e with h; simp [h]
        next e =>
          injection h₂.symm.trans e
    · simp only [fix, Part.mem_assert_iff] at h₃
      obtain ⟨h₃, h₄⟩ := h₃
      refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
      · injection Part.mem_unique h h' with e
        exact e ▸ h₃
      · obtain ⟨h₁, h₂⟩ := h
        grind [WellFounded.fixF_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ (eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom) ≫ eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv =
    𝟙 (X ⟶[V] Y)

Tactic:
rw [← eHom_whisker_exchange]

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ (eHomWhiskerLeft V X β.hom ≫ eHomWhiskerRight V α.inv Y₁) ≫ eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv =
    𝟙 (X ⟶[V] Y)
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ (eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv) ≫ eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom =
    𝟙 (X₁ ⟶[V] Y₁)

Tactic:
rw [← eHom_whisker_exchange]

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ (eHomWhiskerLeft V X₁ β.inv ≫ eHomWhiskerRight V α.hom Y) ≫ eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom =
    𝟙 (X₁ ⟶[V] Y₁)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
⊢ φ ≫ φ' = 𝟙 a

Tactic:
apply IsStronglyCartesian.ext p (p.map φ) φ (𝟙 (p.obj a))

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := ⋯
inv_hom : φ' ≫ φ = 𝟙 b
h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
⊢ (φ ≫ φ') ≫ φ = 𝟙 a ≫ φ
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
| (F.map (coeqHom u v)).toFunctor.obj ((F.map u).toFunctor.obj { base := c, fiber := f }.fiber)

Tactic:
rw [← Cat.Hom.comp_obj, ← F.map_comp, coeq_condition, F.map_comp,
        Cat.Hom.comp_obj]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
| (F.map (coeqHom u v)).toFunctor.obj ((F.map v).toFunctor.obj { base := c, fiber := f }.fiber)
Module: Mathlib.CategoryTheory.Limits.FintypeCat

Goal state before:
pp: J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Type u_1
inst✝ : ∀ (j : J), Finite (K.obj j)
⊢ Fintype (limit K)

Tactic:
by
  have : Fintype (sections K) := Fintype.ofFinite (sections K)
  exact Fintype.ofEquiv (sections K) (Types.limitEquivSections K).symm

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
x : (F.obj X).obj
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
⊢ (ConcreteCategory.hom
        ((Types.equalizerIso ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).map WalkingParallelPairHom.left)
              ((parallelPair f g ⋙ F ⋙ FintypeCat.incl).map WalkingParallelPairHom.right)).inv ≫
          ((Cone.postcomposeEquivalence
                        (diagramIsoParallelPair (parallelPair f g ⋙ F ⋙ FintypeCat.incl))).symm.inverse.map
                ((isLimitOfPreserves (F ⋙ FintypeCat.incl) (equalizerIsEqualizer f g)).liftConeMorphism
                  ((Cone.postcomposeEquivalence
                            (diagramIsoParallelPair (parallelPair f g ⋙ F ⋙ FintypeCat.incl))).symm.functor.obj
                    (limit.cone (parallelPair ((F ⋙ FintypeCat.incl).map f) ((F ⋙ FintypeCat.incl).map g)))))).hom ≫
            (F ⋙ FintypeCat.incl).map (equalizer.ι f g)))
      ⟨x, h⟩ =
    x

Tactic:
erw [PreservesEqualizer.iso_inv_ι, Types.equalizerIso_inv_comp_ι]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
x : (F.obj X).obj
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
⊢ (ConcreteCategory.hom (↾Subtype.val)) ⟨x, h⟩ = x
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯).π.app
        { as := WalkingPair.left } ≫
      c₁.proj val✝ =
    s.proj (Sum.inl val✝)

Tactic:
simp only [pair_obj_left, mk_π_app, IsLimit.fac]

Goal state after: