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

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
exact hf.neg.sum_le_integral_Ico hab

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
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 : ℕ
hi : i ∈ Ico a b
⊢ ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
x

Goal state after:
case h
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 : ℕ
hi : i ∈ Ico a b
x : ℝ
⊢ x ∈ Ico ↑i ↑(i + 1) → f ↑i * g ↑i ≤ f x * g (x - 1)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Mono
    ((kernelCokernelCompSequence f g).map' 0 1 instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_2
      instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_4)

Tactic:
by
  dsimp; infer_instance

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
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 ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i * g ↑i ≤ f x * g (x - 1)

Tactic:
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

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
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 : ℕ
hi : i ∈ Ico a b
⊢ ∀ x ∈ Ico ↑i ↑(i + 1), f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
x

Goal state after:
case h
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 : ℕ
hi : i ∈ Ico a b
x : ℝ
⊢ x ∈ Ico ↑i ↑(i + 1) → f x * g (x - 1) ≤ f ↑i * g ↑i
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
cNn : c (N - 1) ≤ n
⊢ ε * (1 + l) * ↑(c (N - 1)) ≤ ε * (1 + l) * ↑n

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h
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 ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
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

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

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := ⋯
faithful : φ.Faithful
⊢ Epi (cm.op.mapNatTrans (preadditiveYonedaMap (preadditiveCoyonedaObj G) Y)).τ₂

Tactic:
suffices φ.map.Surjective by simpa [AddCommGrpCat.epi_iff_surjective, Functor.coe_mapAddHom]
    exact fun f => ⟨f (𝟙 G), by cat_disch⟩

Goal state after:
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:
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.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: 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
⊢ c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ / j ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

Tactic:
by gcongr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : HasLimitsOfShape (Discrete J) C
⊢ ObjectProperty.strictLimitsOfShape IsIndObject (Discrete J) ≤ IsIndObject

Tactic:
rintro _ ⟨F, hF⟩
    exact isIndObject_limit_of_discrete_of_hasLimitsOfShape _ hF

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
⊢ ∃ l, d g ≫ l = d f

Tactic:
let l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) (by
    rw [← kernelFactorThruImage_hom_comp_ι, Category.assoc, kernel_ι_d_comp_d hG _ hg, comp_zero])

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
⊢ ∃ l, d g ≫ l = d f
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass (R.extMk f m hm hf) =
    CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)

Tactic:
simp [extMk]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n m : ℕ
hm : n + 1 = m
⊢ R.extMk 0 m hm ⋯ = 0

Tactic:
simp [extMk]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n m : ℕ
hm : n + 1 = m
f : X ⟶ R.cochainComplex.X ↑n
hf : f ≫ R.cochainComplex.d ↑n ↑m = 0
⊢ R.extMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).hom) m hm ⋯ =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk (Cocycle.fromSingleMk f ⋯ ↑m ⋯ hf))

Tactic:
simp [extMk]

Goal state after:
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 : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = 0
⊢ a = 0

Tactic:
rw [← apply_zero f] at ha
  exact h ha

Goal state after:
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
inst✝ : Epi f
qbar : Pseudoelement Q
q : Over Q
⊢ ((fun g ↦ app f g) (Over.mk (pullback.fst f q.hom))).hom = pullback.snd f q.hom ≫ q.hom

Tactic:
← pullback.condition,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Epi f
qbar : Pseudoelement Q
q : Over Q
⊢ ((fun g ↦ app f g) (Over.mk (pullback.fst f q.hom))).hom = pullback.fst f q.hom ≫ f
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
⊢ R.extEquivCohomologyClass (R.extMk f m hm hf) =
    CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)

Tactic:
simp [extMk]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n m : ℕ
hm : n + 1 = m
⊢ R.extMk 0 m hm ⋯ = 0

Tactic:
simp [extMk]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n m : ℕ
hm : n + 1 = m
f : R.cochainComplex.X (-↑n) ⟶ Y
hf : R.cochainComplex.d (-↑m) (-↑n) ≫ f = 0
⊢ R.extMk ((R.cochainComplexXIso (-↑n) n ⋯).inv ≫ f) m hm ?m.169 =
    R.extEquivCohomologyClass.symm (CohomologyClass.mk (Cocycle.toSingleMk f ⋯ (-↑m) ⋯ hf))

Tactic:
simp [extMk]

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
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:
by
    intro Z z hz
    rw [← L.map_comp] at hz
    rw [map_eq_zero_iff L P, ← exists_epiModSerre_comp_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    refine ⟨_, s ≫ f, MorphismProperty.comp_mem _ _ _ hs hf, by simpa⟩

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
J : Type u_3
inst✝¹ : Category.{v_2, u_3} J
K : J ⥤ Action V G
inst✝ : HasColimit (K ⋙ forget V G)
⊢ PreservesColimit K ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
have (k : SingleObj G) :
      HasColimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
    inferInstanceAs (HasColimit (K ⋙ forget V G))

Goal state after:
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)
this : ∀ (k : SingleObj G), HasColimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k)
⊢ PreservesColimit K ((functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: case h
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ (res V f).map { hom := g.hom, comm := ⋯ } = g

pp: case w
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
h : H
⊢ X.ρ h ≫ g.hom = g.hom ≫ Y.ρ h

Tactic:
· ext
      simp

Goal state after:
case w
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
h : H
⊢ X.ρ h ≫ g.hom = g.hom ≫ Y.ρ h
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✝
hf : Mono f
⊢ Nonempty (NormalMono f)

Tactic:
mono_iff L P

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✝ : D
f : X✝ ⟶ Y✝
hf : ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
⊢ Nonempty (NormalMono f)
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:

Tactic:
_ = (unit s ≫ f ◁ i.right) ▷ h := by simp [-LeftExtension.w]
      _ = unit t ▷ h := congrArg (· ▷ h) (LeftExtension.w i)
      _ = _ := by simp

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 : RightLift f g
i : s ⟶ t
x : B
h : x ⟶ c
⊢ (postcomp x f).map (h ◁ i.left) ≫ CostructuredArrow.hom (t.whisker h) = CostructuredArrow.hom (s.whisker h)

Tactic:
rw [← cancel_epi (α_ h _ _).inv]
    calc
      _ = h ◁ (i.left ▷ f ≫ t.counit) := by simp [-RightLift.w]
      _ = h ◁ s.counit := congrArg (h ◁ ·) (RightLift.w i)
      _ = _ := by simp

Goal state after:
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
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
⊢ t ≫ r = φ

Tactic:
rw [hφ]

Goal state after:
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₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq t l r b
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
⊢ F.isoMapOfCommSq sq = (F.mapComp' t r φ ⋯).symm ≪≫ F.mapComp' l b φ ⋯

Tactic:
by
  subst hφ
  simp [isoMapOfCommSq, mapComp'_eq_mapComp]

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: ⊢ PartialFun ⥤ Pointed

Tactic:
by
  classical
  exact
    { obj := fun X => ⟨(Option X), none⟩
      map := fun f => ⟨Option.elim' none fun a => (f a).toOption, rfl⟩
      map_id := fun X => Pointed.Hom.ext <| funext fun o => Option.recOn o rfl fun a => (by
        dsimp [CategoryStruct.id]
        convert! Part.some_toOption a)
      map_comp := fun f g => Pointed.Hom.ext <| funext fun o => Option.recOn o rfl fun a => by
        dsimp [CategoryStruct.comp]
        rw [Part.bind_toOption g (f a), Option.elim'_eq_elim] }

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

Goal state before:
pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (F.map f).toFunctor.obj ((hom (limit.π (F ⋙ objects) X✝)) Y) = (hom (limit.π (F ⋙ objects) Y✝)) Y

Tactic:
exact congr_hom (limit.w (F ⋙ Cat.objects) f) Y

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsCartesianDistributive C
A B Z : C
f g : Z ⟶ (pair A B).obj { as := WalkingPair.left }
he : f ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = g ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl
⊢ f = g

Tactic:
let ι := coprod.inl (X := A) (Y := B)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsCartesianDistributive C
A B Z : C
f g : Z ⟶ (pair A B).obj { as := WalkingPair.left }
he : f ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = g ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl
ι : A ⟶ A ⨿ B := coprod.inl
⊢ f = g
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ F.map (A.str ≫ strInv h) = (A.str ≫ strInv h) ≫ A.str

Tactic:
by rw [Category.assoc, F.map_comp, strInv, ← Hom.h]

Goal state after:
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 : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ = eqToHom ha ≫ f ≫ eqToHom ⋯
⊢ p.IsHomLift f φ

Tactic:
subst ha hb
  obtain rfl : f = p.map φ := by simpa using h.symm
  infer_instance

Goal state after:
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 : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ ≫ eqToHom hb = eqToHom ha ≫ f
⊢ p.IsHomLift f φ

Tactic:
subst ha hb
  obtain rfl : f = p.map φ := by simpa using h.symm
  infer_instance

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

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : HasFibers p
inst✝ : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
| f

Tactic:
rw [← id_comp f]

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : HasFibers p
inst✝ : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
| 𝟙 R ≫ f
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
j : J
⊢ (α_ (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
          (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
          (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))).inv ≫
      enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ▷
          enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) =
    enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ◁
        enrichedComp V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) ≫
      enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)

Tactic:
rw [enriched_assoc]

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 A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (F.map (pullback.snd f g)))
      ((ConcreteCategory.hom
            (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g ≪≫
                Types.pullbackIsoPullback (F.map f).hom (F.map g).hom).inv).toFun
        ⟨(a, b), h⟩) =
    b

Tactic:
change ((Types.pullbackIsoPullback _ _).inv ≫ _ ≫
    (F ⋙ FintypeCat.incl).map (pullback.snd f g)) _ = _

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom
        ((Types.pullbackIsoPullback ((cospan f g ⋙ F ⋙ FintypeCat.incl).map WalkingCospan.Hom.inl)
              ((cospan f g ⋙ F ⋙ FintypeCat.incl).map WalkingCospan.Hom.inr)).inv ≫
          ((Cone.postcomposeEquivalence (diagramIsoCospan (cospan f g ⋙ F ⋙ FintypeCat.incl))).symm.inverse.map
                ((isLimitOfPreserves (F ⋙ FintypeCat.incl) (pullbackIsPullback f g)).liftConeMorphism
                  ((Cone.postcomposeEquivalence (diagramIsoCospan (cospan f g ⋙ F ⋙ FintypeCat.incl))).symm.functor.obj
                    (limit.cone (cospan ((F ⋙ FintypeCat.incl).map f) ((F ⋙ FintypeCat.incl).map g)))))).hom ≫
            (F ⋙ FintypeCat.incl).map (pullback.snd f g)))
      ⟨(a, b), h⟩ =
    b
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
⊢ Nat.card (F.obj Y).obj < Nat.card (F.obj X).obj

Tactic:
exact lt_card_fiber_of_mono_of_notIso F v hvnoiso

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
σ : (F.obj X).obj → (F.obj X).obj := fun t ↦ (ConcreteCategory.hom (F.map (selfProdProj u t))) b
t s : (F.obj X).obj
hs : (ConcreteCategory.hom (F.map (selfProdProj u t))) b = (ConcreteCategory.hom (F.map (selfProdProj u s))) b
h' : selfProdProj u t = selfProdProj u s
⊢ id t = id s

Tactic:
← selfProdProj_fiber h s,

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
σ : (F.obj X).obj → (F.obj X).obj := fun t ↦ (ConcreteCategory.hom (F.map (selfProdProj u t))) b
t s : (F.obj X).obj
hs : (ConcreteCategory.hom (F.map (selfProdProj u t))) b = (ConcreteCategory.hom (F.map (selfProdProj u s))) b
h' : selfProdProj u t = selfProdProj u s
⊢ id t = id ((ConcreteCategory.hom (F.map (selfProdProj u s))) a)