mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case pos
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
    apply le_antisymm
    · rw [← Int.zpow_le_iff_le_log hb hr, ← rpow_intCast b]
      refine le_of_le_of_eq ?_ (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr)
      exact rpow_le_rpow_of_exponent_le hb1'.le (Int.floor_le _)
    · rw [Int.le_floor, le_logb_iff_rpow_le hb1' hr, rpow_intCast]
      exact Int.zpow_log_le_self hb hr

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ ‖∫ (x : X), f x ∂μ‖ ≤ μ.real Set.univ * ‖f‖

Tactic:
calc  ‖∫ x, f x ∂μ‖
    _ ≤ ∫ x, ‖f x‖ ∂μ := norm_integral_le_integral_norm _
    _ ≤ ∫ _, ‖f‖ ∂μ := ?_
    _ = μ.real Set.univ • ‖f‖ := by rw [integral_const]
  apply integral_mono _ (integrable_const ‖f‖) (fun x ↦ f.norm_coe_le_norm x) -- NOTE: `gcongr`?
  exact (integrable_norm_iff f.continuous.measurable.aestronglyMeasurable).mpr (f.integrable μ)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ r < μ (closure K)

Tactic:
· exact hK3.trans_le (measure_mono subset_closure)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ r < μ (closure K)

Tactic:
· exact hK3.trans_le (measure_mono subset_closure)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
n✝ n : ℕ
x✝ : α × α
⊢ x✝ ∈ Prod.swap ⁻¹' t n ↔ x✝ ∈ t n

Tactic:
exact (t n).comm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h_meas
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (fun ω ↦ (u n).mulExpNegMulSq (g ω)) P

Tactic:
exact Eventually.of_forall (fun n => g.continuous.mulExpNegMulSq.aestronglyMeasurable)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) fun s ↦ MeasurableSet s ∧ P s ≠ ∞
⊢ P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet

Tactic:
convert! this
    simp only [iff_self_and]
    exact fun _ ↦ measure_ne_top P _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case inr
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b

Tactic:
simp only [hlt.not_ge, false_iff, not_le]
    refine (lt_pow_nthRoot_add_one hn b).trans_le ?_
    gcongr
    assumption

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬ContinuousAt ℘[L] x

Tactic:
eta_expand

Goal state after:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬ContinuousAt (fun z ↦ ℘[L] z) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: ⊢ deriv arcsin = fun x ↦ 1 / √(1 - x ^ 2)

Tactic:
funext x
  by_cases h : x ≠ -1 ∧ x ≠ 1
  · exact (hasDerivAt_arcsin h.1 h.2).deriv
  · rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
    simp only [not_and_or, Ne, Classical.not_not] at h
    rcases h with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∉ L.lattice
h₁ : ∀ (l : ↥L.lattice), ↑l ≠ l₀
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - 0)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
simp [h₁, tsum_mul_left, sumInvPow, add_assoc,
        one_add_one_eq_two, ← zpow_natCast, -neg_add_rev]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

Tactic:
by
  have := log_stirlingSeq_bounded_aux n
  rw [stirlingSeq_one, log_div (by positivity), log_exp, log_sqrt] at this <;> grind

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

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, ((fun θ ↦ f (cos θ)) ∘ arccos) x * -(1 / √(1 - x ^ 2))

Tactic:
Function.comp_apply

Goal state after:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, f (cos (arccos x)) * -(1 / √(1 - x ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ ↑n)| = 1 ↔ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
by
  constructor
  · intro hTx
    have hx := (abs_eval_T_real_le_one_iff (Nat.cast_ne_zero.mpr hn) x).mpr (le_of_eq hTx)
    rw [← cos_arccos (neg_le_of_abs_le hx) (le_of_max_le_left hx), T_real_cos,
      Int.cast_natCast, abs_cos_eq_one_iff] at hTx
    obtain ⟨k, hk⟩ := hTx
    have hk' : k = n * (arccos x / π) := by simpa [field]
    lift k to ℕ using (by rw [← Int.cast_nonneg_iff (R := ℝ), hk']; positivity [arccos_nonneg x])
    simp only [Int.cast_natCast] at hk hk'
    have hkn : (k : ℝ) ≤ n := by
      rw [← mul_one (n : ℝ), hk']
      gcongr
      exact div_le_one_of_le₀ (arccos_le_pi x) (by positivity)
    refine ⟨k, by simpa using hkn, ?_⟩
    convert! congr(cos ($hk.symm / n))
    rw [mul_div_cancel_left₀ _ (by simpa), cos_arccos (by grind) (by grind)]
  · rintro ⟨k, hk, rfl⟩
    rw [T_real_cos, abs_cos_eq_one_iff]
    exact ⟨k, by simp [field]⟩

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

Goal state before:
pp: c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z + ↑d + ↑e) =Θ[cofinite] fun n ↦ ↑n

Tactic:
by
  apply IsTheta.add_isLittleO <;>
  [refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real); skip] <;>
  simpa [-Int.cofinite_eq] using
    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real

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

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ 0 ≤ (fun x ↦ ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm

Tactic:
exact fun n ↦ Real.rpow_nonneg (norm_nonneg _) _

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

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
this : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ n / n.gcd (2 * k + 1) = 1

Tactic:
by grind [Rat.den_pos]

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
two_mul,

Goal state after:
n : ℤ
⊢ fib (n + n) = fib n * (2 * fib (n + 1) - fib n)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: α : Type u_1
inst✝ : CommSemiring α
⊢ fibRec.IsSolution fun x ↦ ↑(Nat.fib x)

Tactic:
rw [fibRec]

Goal state after:
α : Type u_1
inst✝ : CommSemiring α
⊢ { order := 2, coeffs := ![1, 1] }.IsSolution fun x ↦ ↑(Nat.fib x)
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
⊢ biprod.inl ≫ π f g = g ≫ cokernel.π (f ≫ g)

Tactic:
by simp [π]

Goal state after:
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
⊢ biprod.inr ≫ π f g = cokernel.π (f ≫ g)

Tactic:
by simp [π]

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

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
hy₂ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')

Tactic:
rw [← hy, hy₁, Types.FilteredColimit.colimit_eq_iff] at hy₂

Goal state after:
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
hy₂ :
  ∃ k_1 f g,
    (hom ((F s).map f)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk) =
      (hom ((F s).map g)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
⊢ QuasiIso R.ι'

Tactic:
dsimp [ι']; infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
⊢ { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ }.Exact

Tactic:
let α : ShortComplex.mk f (cokernel.π f) (by simp) ⟶ ShortComplex.mk f (d f) (by simp) :=
    { τ₁ := 𝟙 _
      τ₂ := 𝟙 _
      τ₃ := Injective.ι _ }

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ } ⟶
  { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ } :=
  { τ₁ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁,
    τ₂ := 𝟙 { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂,
    τ₃ := ι { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: case e_g.e_a
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
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ inv (DerivedCategory.Q.map R.ι') ≫ (singleFunctor C 0 ⋙ DerivedCategory.Q).map g =
    DerivedCategory.Q.map φ.hom' ≫ inv (DerivedCategory.Q.map R'.ι')

Tactic:
simpa only [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq,
    Functor.map_comp] using! DerivedCategory.Q.congr_map φ.ι'_comp_hom'.symm

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ F.map f ≫
      (injectiveResolution Y).toRightDerivedZero' F ≫
        (CochainComplex.isoHomologyπ₀
              ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex)).hom ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex) =
    ((injectiveResolution X).toRightDerivedZero' F ≫
        (CochainComplex.isoHomologyπ₀
              ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)).hom ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)) ≫
      (F.rightDerived 0).map f

Tactic:
by
    dsimp [rightDerived]
    rw [assoc, assoc, InjectiveResolution.toRightDerivedZero'_naturality_assoc f
      (injectiveResolution X) (injectiveResolution Y)
      (InjectiveResolution.desc f _ _) (by simp),
      ← HomologicalComplex.homologyπ_naturality_assoc]
    erw [← NatTrans.naturality]
    rfl

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ f = g

Tactic:
lift_unique f,

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ lift (f.comp inl) (f.comp inr) ⋯ = g
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Group G
A : Action V G
g : G
⊢ A.ρ (g * g⁻¹) = 𝟙 A.V

Tactic:
by rw [mul_inv_cancel, ρ_one]

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
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
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g ↔
    F.map (U.map (adj₁.counit.app X)) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm g =
      adj₁.counit.app ((U ⋙ F).obj X) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm g

Tactic:
← (adj₁.homEquiv _ _).symm.injective.eq_iff,

Goal state after:
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
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ (adj₁.homEquiv (U.obj (F.obj (U.obj X))) ((𝟭 B).obj (R.obj Y))).symm (U.map (F.map g ≫ adj₁.counit.app (R.obj Y))) =
      (adj₁.homEquiv (U.obj (F.obj (U.obj X))) ((𝟭 B).obj (R.obj Y))).symm (U.map (adj₁.counit.app X) ≫ g) ↔
    F.map (U.map (adj₁.counit.app X)) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm g =
      adj₁.counit.app ((U ⋙ F).obj X) ≫ (adj₁.homEquiv (U.obj X) (R.obj Y)).symm g
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
⊢ Quot.map (Hom₂.whisker_right (𝟙 b)) ⋯ (Quot.mk Rel η) =
    { hom := Quot.mk Rel (Hom₂.right_unitor f), inv := Quot.mk Rel (Hom₂.right_unitor_inv f), hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      Quot.mk Rel η ≫
        { hom := Quot.mk Rel (Hom₂.right_unitor g), inv := Quot.mk Rel (Hom₂.right_unitor_inv g), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.inv

Tactic:
exact Quot.sound (Rel.whisker_right_id η)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } })) ≫
      MonoidalCategoryStruct.whiskerLeft (F.map (𝟙 { as := { as := () } })) (F.mapId { as := { as := () } }) =
    (MonoidalCategoryStruct.rightUnitor (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
simp only [tensorUnit_def, tensorObj_def, whiskerLeft_def, rightUnitor_def]

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } })) ≫
      F.map (𝟙 { as := { as := () } }) ◁ F.mapId { as := { as := () } } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
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
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f

Tactic:
rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]

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)
k : b ⟶ x := s.extension
θ : g ≫ h ⟶ f ≫ s.extension := s.unit
sτ : LeftExtension f g := mk (k ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ θ ▷ u ⊗≫ 𝟙 (f ≫ k ≫ u))
τ : t.extension ⟶ k ≫ u := H.desc sτ
sσ : LeftLift u (t.extension ≫ 𝟙 c) := LeftLift.mk k ((ρ_ t.extension).hom ≫ τ)
σ : t.extension ≫ h ⟶ k := H'.desc sσ
⊢ t.extension ◁ η' ⊗≫ σ ▷ u = 𝟙 (t.extension ≫ 𝟙 c) ⊗≫ τ

Tactic:
simpa [bicategoricalComp] using (H' _).fac (.mk _ <| (ρ_ _).hom ≫ τ)

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)
i : I
x✝³ x✝² : C i
x✝¹ x✝ : x✝³ ⟶ x✝²
h : (incl i).map x✝¹ = (incl i).map x✝
⊢ x✝¹ = x✝

Tactic:
injection h

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case inl.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y

pp: case inl.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ 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:
· injection Part.mem_unique ⟨h₁, h₂⟩ h'

Goal state after:
case inl.refine_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ 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.Category.Cat.Limit

Goal state before:
pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ ∀ (j j' : J) (f_1 : j ⟶ j'),
    (hom
          ((homDiagram
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  X✝)
                ((hom
                    (limit.lift (F ⋙ objects)
                      { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
                  Y✝)).map
            f_1))
        (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) =
      eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
intro j j' h
        dsimp [Functor.comp_obj, homDiagram_obj]
        simp only [Functor.map_comp, eqToHom_map, ← Functor.comp_map, Category.assoc, eqToHom_trans,
          eqToHom_trans_assoc]
        have := congr($((s.π.naturality h).symm).toFunctor)
        dsimp at this
        rw [Functor.id_comp] at this
        rw [Functor.congr_hom this f]
        simp

Goal state after: