mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
hx : ↑(x 1).natAbs ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0

Tactic:
Nat.cast_ne_zero,

Goal state after:
x : Fin 2 → ℤ
hx : (x 1).natAbs ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ Summable fun x ↦ ‖x‖ ^ (-k)

Tactic:
rw [← (finTwoArrowEquiv _).symm.summable_iff, summable_partition _ Int.existsUnique_mem_box]
  · simp only [finTwoArrowEquiv_symm_apply, Function.comp_def]
    refine ⟨fun n ↦ (hasSum_fintype (β := box (α := ℤ × ℤ) n) _).summable, ?_⟩
    suffices Summable fun n : ℕ ↦ ∑' (_ : box (α := ℤ × ℤ) n), (n : ℝ) ^ (-k) by
      refine this.congr fun n ↦ tsum_congr fun p ↦ ?_
      simp only [← Int.mem_box.mp p.2, Nat.cast_max, norm_eq_max_natAbs, Matrix.cons_val_zero,
        Matrix.cons_val_one]
    simp only [tsum_fintype, univ_eq_attach, sum_const, card_attach, nsmul_eq_mul]
    apply ((Real.summable_nat_rpow.mpr (by linarith : 1 - k < -1)).mul_left
      8).of_norm_bounded_eventually_nat
    filter_upwards [Filter.eventually_gt_atTop 0] with n hn
    rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]
  · exact fun n ↦ Real.rpow_nonneg (norm_nonneg _) _

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

Goal state before:
pp: n : ℕ
⊢ (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val

Tactic:
wlog! hn : n ≠ 0
  · simp [hn]
  refine roots_eq_of_degree_eq_card (fun x hx ↦ ?_) ?_
  · obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx
    suffices (U ℝ n).eval x * sin ((k + 1) * π / (n + 1)) = 0 by
      refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this
      field_simp
      norm_cast
      grind
    rw [← hx, U_real_cos, sin_eq_zero_iff]
    use k + 1
    field_simp
    norm_cast
    ring
  · rw [Finset.card_image_of_injOn, Finset.card_range, degree_U_natCast]
    exact (Finset.range n).nodup_map_iff_injOn.mp (roots_U_real_nodup n)

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
⊢ IsLocalMax (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
have zero_lt : 0 < k * π / n := by positivity

Goal state after:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
⊢ IsLocalMax (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
a b : ℤ
⊢ ∃ c, ∀ᶠ (x : Fin 2 → ℤ) in cofinite, ‖((↑(x 0) + ↑a) * ↑z + ↑(x 1) + ↑b)⁻¹‖ ≤ c * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖

Tactic:
have h0 : z ∈ verticalStrip |z.re| (z.im) := by simp [mem_verticalStrip_iff]

Goal state after:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
⊢ ∃ c, ∀ᶠ (x : Fin 2 → ℤ) in cofinite, ‖((↑(x 0) + ↑a) * ↑z + ↑(x 1) + ↑b)⁻¹‖ ≤ c * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
⊢ IsLocalMin (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
have zero_lt : 0 < k * π / n := by positivity

Goal state after:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
⊢ IsLocalMin (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ b * (1 - a ^ (n + 1)) / (1 - a) = -(-(b * (1 - a ^ (n + 1))) / (1 - a))

Tactic:
neg_div,

Goal state after:
R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ b * (1 - a ^ (n + 1)) / (1 - a) = - -(b * (1 - a ^ (n + 1)) / (1 - a))
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ b * (1 - a ^ n) / (1 - a) = -(-(b * (1 - a ^ n)) / (1 - a))

Tactic:
neg_div,

Goal state after:
R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ b * (1 - a ^ n) / (1 - a) = - -(b * (1 - a ^ n) / (1 - a))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_1
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ Summable fun n ↦ ‖↑s / (↑n + 1) ^ 2‖

pp: case refine_2
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun n ↦ ‖↑s / (↑n + 1) ^ 2‖) j

Tactic:
· simpa using summable_pow_div_add (s : ℂ) 2 1 (Nat.one_lt_two)

Goal state after:
case refine_2
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun n ↦ ‖↑s / (↑n + 1) ^ 2‖) j
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: x✝ : ℤ
⊢ fib (x✝ + ↑1) = fib (x✝ - 1) * fib ↑1 + fib x✝ * fib (↑1 + 1)

Tactic:
by grind [fib_add_two, fib_two, fib_one]

Goal state after:
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ (∀ y ∈ S.commutant, (↑e).range ∈ Module.End.invtSubmodule ↑y ∧ (↑e).ker ∈ Module.End.invtSubmodule ↑y) ↔
    ∀ y ∈ S.commutant, (↑e).range ∈ Module.End.invtSubmodule ↑y

Tactic:
he.isIdempotentElem.range_mem_invtSubmodule_iff,

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ (∀ y ∈ S.commutant, e ∘SL y ∘SL e = y ∘SL e ∧ (↑e).ker ∈ Module.End.invtSubmodule ↑y) ↔
    ∀ y ∈ S.commutant, e ∘SL y ∘SL e = y ∘SL e
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i ∈ Finset.range a, f (x₀ + ↑i) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
  exact hf.neg.integral_le_sum

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
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < (↑n)⁻¹ * ↑n * (l - ε * (1 + l))

Tactic:
rw [inv_mul_cancel₀, one_mul]

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
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < l - ε * (1 + l)

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
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ ↑n ≠ 0
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : I ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).inv ≫ coyoneda.map (colimit.ι F i).op = limit.π (F.op ⋙ coyoneda) (op i)

Tactic:
rw [← coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
have (i : ι) : HasColimit (F i) := ⟨_, hc i⟩
    obtain ⟨c', hc', _⟩ := H F
    let e : coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
      coconePointwiseProductIso _ fun i ↦ (hc i).uniqueUpToIso (hc' i)
    rwa [(IsColimit.equivIsoColimit e).nonempty_congr]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ ((singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).symm ≪≫
          isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm).hom ≫
      Fork.ι (KernelFork.ofι (iCycles I.cocomplex 0) ⋯) =
    Fork.ι I.kernelFork

Tactic:
rw [← cancel_epi (singleObjHomologySelfIso (ComplexShape.up ℕ) _ _).hom,
    ← cancel_epi (isoHomologyπ₀ _).hom,
    ← cancel_epi (singleObjCyclesSelfIso (ComplexShape.up ℕ) _ _).inv]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ (singleObjCyclesSelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).inv ≫
      (isoHomologyπ₀ ((single C (ComplexShape.up ℕ) 0).obj I.kernelFork.pt)).hom ≫
        (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).hom ≫
          ((singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).symm ≪≫
                isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm).hom ≫
            Fork.ι (KernelFork.ofι (iCycles I.cocomplex 0) ⋯) =
    (singleObjCyclesSelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).inv ≫
      (isoHomologyπ₀ ((single C (ComplexShape.up ℕ) 0).obj I.kernelFork.pt)).hom ≫
        (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt).hom ≫ Fork.ι I.kernelFork
Module: Mathlib.CategoryTheory.Abelian.Monomorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
x✝³ x✝² x✝¹ : C
f : x✝³ ⟶ x✝¹
g : x✝³ ⟶ x✝²
x✝ : Limits.HasPushout f g
hf : monomorphisms C f
⊢ monomorphisms C (Limits.pushout.inr f g)

Tactic:
simp only [monomorphisms.iff] at hf ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
x✝³ x✝² x✝¹ : C
f : x✝³ ⟶ x✝¹
g : x✝³ ⟶ x✝²
x✝ : Limits.HasPushout f g
hf : Mono f
⊢ Mono (Limits.pushout.inr f g)
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
B : C
hB : Injective B
⊢ Injective ((preadditiveCoyonedaObj G).obj B)

Tactic:
by
    rw [← Module.injective_iff_injective_object]
    simp only [preadditiveCoyonedaObj_obj_carrier]
    refine Module.Baer.injective (fun M g => ?_)
    have h := exists_d_comp_eq_d hG B (ModuleCat.ofHom
      ⟨⟨fun i => i.1.unop, by cat_disch⟩, by cat_disch⟩) ?_ (ModuleCat.ofHom g)
    · obtain ⟨l, hl⟩ := h
      refine ⟨((preadditiveCoyonedaObj G).map l).hom ∘ₗ
        (Preadditive.homSelfLinearEquivEndMulOpposite G).symm.toLinearMap, ?_⟩
      intro f hf
      simpa [d] using! Sigma.ι _ ⟨f, hf⟩ ≫= hl
    · rw [ModuleCat.mono_iff_injective]
      cat_disch

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 : ℕ
α : Ext X Y n
m : ℕ
hm : n + 1 = m
⊢ ∃ f, ∃ (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = α

Tactic:
obtain ⟨x, rfl⟩ := R.extEquivCohomologyClass.symm.surjective α

Goal state after:
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
x : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ ∃ f, ∃ (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = R.extEquivCohomologyClass.symm x
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 : ℕ
α : Ext X Y n
m : ℕ
hm : n + 1 = m
⊢ ∃ f, ∃ (hf : R.complex.d m n ≫ f = 0), R.extMk f m hm hf = α

Tactic:
obtain ⟨x, rfl⟩ := R.extEquivCohomologyClass.symm.surjective α

Goal state after:
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
x : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ ∃ f, ∃ (hf : R.complex.d m n ≫ f = 0), R.extMk f m hm hf = R.extEquivCohomologyClass.symm x
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v g x : G
⊢ Quotient.lift (fun σ ↦ ↑σ * (↑v)⁻¹) ⋯ (↑g * ↑x) = g • (↑x * (↑v)⁻¹)

Tactic:
apply (Quotient.lift_mk _ _ _).trans

Goal state after:
case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v g x : G
⊢ ↑((fun x1 x2 ↦ x1 * x2) g x) * (↑v)⁻¹ = g • (↑x * (↑v)⁻¹)
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✝
x✝ : Epi f
⊢ Epi (L.map f)

Tactic:
simpa only [epi_map_iff _ P] using P.epiModSerre_of_epi f

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

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
⊢ ∀ (X Y Z : Action V G) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g

Tactic:
intros; ext; exact Linear.smul_comp _ _ _ _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    ((α_ (η.app a) (θ.app a) (H.map f)).hom ≫
        η.app a ◁ θ.naturality f ≫
          (α_ (η.app a) (G.map f) (θ.app b)).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ (F.map f) (η.app b) (θ.app b)).hom) ≫
      F.map f ◁ η.app b ◁ Γ.as.app b

Tactic:
rw [whisker_exchange]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        (η.naturality f ▷ θ.app b ≫ (F.map f ≫ η.app b) ◁ Γ.as.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    ((α_ (η.app a) (θ.app a) (H.map f)).hom ≫
        η.app a ◁ θ.naturality f ≫
          (α_ (η.app a) (G.map f) (θ.app b)).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ (F.map f) (η.app b) (θ.app b)).hom) ≫
      F.map f ◁ η.app b ◁ Γ.as.app b
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 ◁ θ.naturality f ▷ H.map g ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
      η.vCompNaturality θ f ▷ H.map g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
          F.map f ◁ η.vCompNaturality θ g ≫
            (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv ≫ F.mapComp f g ▷ η.vCompApp θ c

Tactic:
rw [whisker_exchange]

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 ◁ θ.naturality f ▷ H.map g ⊗≫
        (η.naturality f ▷ (θ.app b ≫ H.map g) ≫ (F.map f ≫ η.app b) ◁ θ.naturality g) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
      η.vCompNaturality θ f ▷ H.map g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
          F.map f ◁ η.vCompNaturality θ g ≫
            (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv ≫ F.mapComp f g ▷ η.vCompApp θ c
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

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
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv

Tactic:
rw [whisker_exchange]

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
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
        (η.naturality f ▷ (θ.app b ≫ H.map g) ≫ (F.map f ≫ η.app b) ◁ θ.naturality g) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    ((α_ (η.app a) (θ.app a) (H.map f)).hom ≫
        η.app a ◁ θ.naturality f ≫
          (α_ (η.app a) (G.map f) (θ.app b)).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ (F.map f) (η.app b) (θ.app b)).hom) ≫
      F.map f ◁ η.app b ◁ Γ.as.app b

Tactic:
rw [whisker_exchange]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        (η.naturality f ▷ θ.app b ≫ (F.map f ≫ η.app b) ◁ Γ.as.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    ((α_ (η.app a) (θ.app a) (H.map f)).hom ≫
        η.app a ◁ θ.naturality f ≫
          (α_ (η.app a) (G.map f) (θ.app b)).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ (F.map f) (η.app b) (θ.app b)).hom) ≫
      F.map f ◁ η.app b ◁ Γ.as.app b
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

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

Tactic:
rw [whisker_exchange]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
      (η.naturality f ▷ θ.app b ≫ (η.app a ≫ G.map f) ◁ Γ.as.app b) ⊗≫
        η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
    𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫ ι.naturality f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)
Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t✝ : LeftExtension f g
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
⊢ ∀ (s : LeftExtension f g) (τ : t.ofCompId ⟶ s), τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))

Tactic:
by
    intro s τ
    ext
    apply P.hom_ext
    simp [← LeftExtension.w τ]

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
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift

Tactic:
rw [whisker_exchange]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ (τ ▷ (u ≫ f) ≫ s.lift ◁ adj.counit) ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ (h ◁ adj.unit ⊗≫ τ ▷ u) ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
rw [whisker_exchange]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ (t.unit ▷ 𝟙 a ≫ (t.lift ≫ u) ◁ t.unit) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)