mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ sumNodes n c P ≤ sumNodes n c (T ℝ ↑n)

Tactic:
rw [sumNodes, sumNodes]
  refine Finset.sum_le_sum (fun i hi => ?_)
  calc
    P.eval (node n i) * (c i) =
      ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * (c i)) :=
      negOnePow_mul_negOnePow_mul_cancel.symm
    _ ≤ 1 * ((-1) ^ i * (c i)) := by
      gcongr
      · exact (hcnonneg i (Finset.mem_Iic.mp hi))
      · exact (negOnePow_mul_le (hPbnd _ node_mem_Icc))
    _ = (T ℝ n).eval (node n i) * (c i) := by
      rw [eval_T_real_node hi, one_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : P = T ℝ ↑n
⊢ sumNodes n c P = sumNodes n c (T ℝ ↑n)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos ((↑r - ↑⌊r⌋) * π) = (-1) ^ ⌊r⌋ * ↑q

Tactic:
rw [sub_mul, cos_sub_int_mul_pi, hq]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
norm_ne_zero_iff

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
simp only [hx, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, norm_zero]

Goal state after:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹

Tactic:
by
  apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
  simp only [Real.rpow_two, abs_mul_abs_self, pow_two]
  simpa using (linear_inv_isBigO_left c₂ hz).mul (linear_inv_isBigO_left c₁ hz)

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable fun n ↦ f n t
m : ℕ
hm :
  ∀ {x : 𝕜},
    x ∈ s →
      (∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s) →
        (∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r) →
          iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x
x : 𝕜
hx : x ∈ s
h : ∀ (k : ℕ), 1 ≤ k → k ≤ m + 1 → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m + 1 → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ SummableLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ iteratedDerivWithin m (fun z ↦ f n z) s z) s) s

Tactic:
· exact SummableLocallyUniformlyOn_congr
        (fun _ _ ht ↦ by rw [iteratedDerivWithin_succ]) (h (m + 1) (by lia) (by lia))

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

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]

Goal state after:
case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + (a * (b * ∑ k ∈ Finset.range n, a ^ k) + b) = a * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable fun n ↦ cotTerm x n

Tactic:
rw [funext fun n ↦ cotTerm_identity hz n]
  apply Summable.mul_left
  suffices Summable fun i : ℕ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by
    rw [← summable_nat_add_iff 1] at this
    simpa using this
  suffices Summable fun i : ℤ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by
    apply this.comp_injective CharZero.cast_injective
  apply (EisensteinSeries.summable_linear_sub_mul_linear_add x 1 1).congr
  simp [mul_comm]

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

Tactic:
intro ε ε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
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
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:
intro ε ε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.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)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
obtain ⟨a, ha⟩ :
      ∃ a : ℕ,
        ∀ b : ℕ, a ≤ b → (c (b + 1) : ℝ) ≤ (1 + ε) * c b ∧ (c b : ℝ) * l - u (c b) ≤ ε * c b :=
      eventually_atTop.1 (cgrowth.and L)

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)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ 1 ≤ ↑⌊c k ^ n⌋₊

Tactic:
simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ (cone k).le]

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 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2)

Tactic:
gcongr with i

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : R.Final
⊢ (snd L R).Final

Tactic:
by
  have := R.final_iff_isFiltered_structuredArrow.mp inferInstance
  exact final_snd_of_isFiltered_structuredArrow L R

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
α : Type u_3
I : α → Type u_4
inst✝¹ : (i : α) → Category.{?u.15, u_4} (I i)
inst✝ : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
X : D
c : (i : α) → Cocone (F i)
j : (i : α) → I i
⊢ (((evaluation D C).obj X).mapCocone (coconePointwiseProduct c)).ι.app j ≫ (piObjIso (fun i ↦ (c i).pt) X).hom =
    ((Cocone.precompose (pointwiseProductCompEvaluation F X).hom).obj
            (coconePointwiseProduct fun i ↦ ((evaluation D C).obj X).mapCocone (c i))).ι.app
      j

Tactic:
dsimp
    ext
    simp [Functor.pi, NatTrans.pi, ← NatTrans.comp_app]

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

Goal state before:
pp: case refine_2
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
l : G ⟶ B
hl :
  d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
    d (ModuleCat.ofHom g)
⊢ ∃ g', ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M), g' x = g ⟨x, mem⟩

Tactic:
refine ⟨((preadditiveCoyonedaObj G).map l).hom ∘ₗ
        (Preadditive.homSelfLinearEquivEndMulOpposite G).symm.toLinearMap, ?_⟩

Goal state after:
case refine_2
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
l : G ⟶ B
hl :
  d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
    d (ModuleCat.ofHom g)
⊢ ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
    (ModuleCat.Hom.hom ((preadditiveCoyonedaObj G).map l) ∘ₗ ↑(Preadditive.homSelfLinearEquivEndMulOpposite G).symm) x =
      g ⟨x, mem⟩
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : P.epiModSerre f
⊢ P.isoModSerre f

Tactic:
isoModSerre_iff_of_mono

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : P.epiModSerre f
⊢ P.epiModSerre f
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
⊢ G.kernel.isoModSerre = (isomorphisms C).inverseImage G

Tactic:
ext X Y f
  refine ⟨(G.kernel.isoModSerre_isInvertedBy_iff G).2 (by rfl) _, fun hf ↦ ?_⟩
  simp only [inverseImage_iff, isomorphisms.iff] at hf
  constructor
  · exact KernelFork.IsLimit.isZero_of_mono
      (KernelFork.mapIsLimit _ (kernelIsKernel f) G)
  · exact CokernelCofork.IsColimit.isZero_of_epi
      (CokernelCofork.mapIsColimit _ (cokernelIsCokernel f) G)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ P.isoModSerre (Abelian.image.ι f)

Tactic:
isoModSerre_iff_of_mono

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ P.epiModSerre (Abelian.image.ι f)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
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
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ P.isoModSerre (kernel.ι (f₁ - f₂))

Tactic:
isoModSerre_iff_of_mono

Goal state after:
case refine_1
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
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ P.epiModSerre (kernel.ι (f₁ - f₂))
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
X✝ Y✝ Z✝ : SingleObj M
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (↾fun x ↦ f ≫ g • x) = (↾fun x ↦ f • x) ≫ ↾fun x ↦ g • x

Tactic:
ext x; exact (smul_smul g f x).symm

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this : L.PreservesMonomorphisms
⊢ Mono f ↔ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
have := Localization.essSurj_mapArrow L P.isoModSerre

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
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
⊢ Mono f ↔ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
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
this : L.PreservesEpimorphisms
⊢ Epi f ↔ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
have := Localization.essSurj_mapArrow L P.isoModSerre

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
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
⊢ Epi f ↔ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
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✝
g : Arrow C
e : L.mapArrow.obj g ≅ Arrow.mk f
this✝ : PreservesLimit (parallelPair g.hom 0) L
this : HasLimit (parallelPair (L.map g.hom) 0)
⊢ HasKernel f

Tactic:
exact hasLimit_of_iso (show parallelPair (L.map g.hom) 0 ≅ _ from
      parallelPair.ext (Arrow.leftFunc.mapIso e) (Arrow.rightFunc.mapIso e))

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (R.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction U)).symm))
⊢ (X : (monadicAdjunction U).toMonad.Algebra) → RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X)

Tactic:
intro X
    simp only [Monad.adj_counit]
    exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f ≫ g = f' ≫ g

Tactic:
rw [h]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f f' : x ⟶ y
h : f = f'
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f' ≫ g' = f ≫ g'

Tactic:
rw [h]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f ≫ g = f ≫ g'

Tactic:
rw [h]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g g' : y ⟶ z
h : g = g'
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ f' ≫ g' = f' ≫ g

Tactic:
rw [h]

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

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

Tactic:
by
    rw [← cancel_mono (α_ h _ _).hom]
    calc
      _ = h ◁ (unit s ≫ i.right ▷ f) := by simp [-LeftLift.w]
      _ = h ◁ unit t := congrArg (h ◁ ·) (LeftLift.w i)
      _ = _ := by simp

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

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ≫ θ.naturality (f ≫ g)) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
naturality_comp θ

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁
          ((α_ (θ.app a) (H.map f) (H.map g)).inv ≫
            θ.naturality f ▷ H.map g ≫
              (α_ (G.map f) (θ.app b) (H.map g)).hom ≫
                G.map f ◁ θ.naturality g ≫ (α_ (G.map f) (G.map g) (θ.app c)).inv ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ F.map₂ β ▷ η.vCompApp θ b ≫ η.vCompNaturality θ g = η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β

Tactic:
by
  calc
    _ = 𝟙 _ ⊗≫ (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫
          η.app a ◁ θ.naturality g ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫
          η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 _ := by
      rw [η.naturality_naturality]
      bicategory
    _ = _ := by
      rw [θ.naturality_naturality]
      bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanLift u (𝟙 a) → ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE

Tactic:
tfae_have 3 → 1
  | ⟨h, h'⟩ => .mk <| (lanLiftIsKan u (𝟙 a)).adjunction <| LanLift.CommuteWith.isKan u (𝟙 a) u

Goal state after:
B : Type u
inst✝ : Bicategory B
a b : B
u : b ⟶ a
tfae_1_to_2 : IsRightAdjoint u → HasAbsLeftKanLift u (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanLift u (𝟙 a) → ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u
tfae_3_to_1 : (∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u) → IsRightAdjoint u
⊢ [IsRightAdjoint u, HasAbsLeftKanLift u (𝟙 a), ∃ (x : HasLeftKanLift u (𝟙 a)), LanLift.CommuteWith u (𝟙 a) u].TFAE