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

Goal state before:
pp: z : ℍ
c d : ℝ
hc : 1 ≤ c ^ 2
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
rcases z with ⟨z, hz⟩
  have H1 : z.im ≤ √((c * z.re + d) ^ 2 + (c * z).im ^ 2) := by
    rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]
    exact (le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)
  simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ← pow_two, add_im, mul_im,
    coe_im, ofReal_im, zero_mul, add_zero, min_le_iff] using! Or.inl H1

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

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ k ≤ n ∧ Even k ∧ x = cos (↑k * π / ↑n)

Tactic:
refine ⟨hk₁, ?_, hk₂⟩

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Even k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos (↑k * π / ↑n)
⊢ eval x (T ℝ ↑n) = 1

Tactic:
hx,

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos (↑k * π / ↑n)
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = -1
⊢ ∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans ((abs_neg 1).trans abs_one))

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ ∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ k ≤ n ∧ Odd k ∧ x = cos (↑k * π / ↑n)

Tactic:
refine ⟨hk₁, ?_, hk₂⟩

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Odd k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos (↑k * π / ↑n)
⊢ eval x (T ℝ ↑n) = -1

Tactic:
hx,

Goal state after:
case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos (↑k * π / ↑n)
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = -1
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ (fun n ↦ ↑(Nat.fib n)) = fun n ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
by
  rw [fibRec.eq_iff_eqOn_range_order]
  · intro i hi
    norm_cast at hi
    fin_cases hi <;> simp
  · exact fib_isSol_fibRec
  · suffices LinearRecurrence.IsSolution fibRec
        ((fun n ↦ (√5)⁻¹ * φ ^ n) - (fun n ↦ (√5)⁻¹ * ψ ^ n)) by
      convert! this
      rw [Pi.sub_apply]
      ring
    apply (@fibRec ℝ _).solSpace.sub_mem
    · exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenRatio_isSol_fibRec
    · exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldenConj_isSol_fibRec

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
⊢ ∫ (a : ℝ) in Ioi 0, a ^ (↑k + 1 - 1) * rexp (-(c * a)) ≠ 0

Tactic:
key

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
⊢ (1 / c) ^ (↑k + 1) * Gamma (↑k + 1) ≠ 0
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
convert! (sum_integral_adjacent_intervals hf.intervalIntegrable_subset).symm
    simp

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 : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ f = 0

Tactic:
by
  rw [← Category.id_comp f]
  exact (pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))

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
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
R : C
p : R ⟶ ((fun g ↦ app f g) a).left
q : R ⟶ ((fun g ↦ app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g ↦ app f g) a).hom = q ≫ ((fun g ↦ app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g ⟦a'⟧ = 0
X : C
p' : X ⟶ ((fun g_1 ↦ app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 ↦ app g g_1) a').hom = q' ≫ (Over.mk 0).hom
this : a'.hom ≫ g = 0
⊢ 𝟙 R ≫ (app g (Over.mk a'')).hom = p ≫ (app g a).hom

Tactic:
by simp [a'', sub_eq_add_neg, this]

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
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.rightDerivedToHomotopyCategory.map f =
    F.rightDerivedToHomotopyCategory.map f ≫
      (J.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (J.isoRightDerivedToHomotopyCategoryObj F).inv

Tactic:
Iso.hom_inv_id,

Goal state after:
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
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.rightDerivedToHomotopyCategory.map f =
    F.rightDerivedToHomotopyCategory.map f ≫ 𝟙 (F.rightDerivedToHomotopyCategory.obj Y)
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderQuotients
i✝ X₁✝ X₂✝ : C
f✝ : X₁✝ ⟶ X₂✝
k : CokernelCofork f✝
hk : IsColimit k
hf : MorphismProperty.ofObjectProperty P P f✝
this : Epi (Cofork.π k) := Cofork.IsColimit.epi hk
⊢ P k.pt

Tactic:
exact P.prop_of_epi k.π hf.2

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.PreservesMonomorphisms
this : L.EssSurj
Z : C
z : Z ⟶ X
hw : ∃ X' s, ∃ (_ : P.isoModSerre s), s ≫ z ≫ f = 0
⊢ ∃ l, l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z

Tactic:
obtain ⟨Z', t, ht, fac⟩ := hw

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 : C
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.EssSurj
Z : C
z : Z ⟶ X
Z' : C
t : Z' ⟶ Z
ht : P.isoModSerre t
fac : t ≫ z ≫ f = 0
⊢ ∃ l, l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z
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✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ (f.hom ≫ f.inv).hom = 𝟙 M.V

Tactic:
Iso.hom_inv_id,

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ (𝟙 M).hom = 𝟙 M.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
this✝ : L.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
hw : ∃ Y' s, ∃ (_ : P.isoModSerre s), (f ≫ z) ≫ s = 0
⊢ ∃ l, L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯

Tactic:
obtain ⟨Z', t, ht, fac⟩ := hw

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 : C
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : (f ≫ z) ≫ t = 0
⊢ ∃ l, L.map (cokernel.π f) ≫ l = L.map z ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
have : Continuous v := by fun_prop

Goal state after:
V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
this : Continuous v
⊢ Continuous fun p ↦ p.1 • p.2
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C), Mono (t.leftToRight.app X)) ↔ ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)

Tactic:
refine ⟨fun h X ↦ by rw [← leftToRight_app_obj]; exact h _, fun h X ↦ ?_⟩

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (t.leftToRight.app X)
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:
by
      rw [whisker_exchange]
      bicategory

Goal state after:
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:
by
      rw [whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₁₂ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
D₁₂ : Type u_9
D₂₃ : Type u_10
C : Type u_11
D : Type u_12
inst✝²¹ : Category.{v_1, u_1} C₁
inst✝²⁰ : Category.{v_2, u_2} C₂
inst✝¹⁹ : Category.{v_3, u_3} C₃
inst✝¹⁸ : Category.{v_4, u_6} D₁
inst✝¹⁷ : Category.{v_5, u_7} D₂
inst✝¹⁶ : Category.{v_6, u_8} D₃
inst✝¹⁵ : Category.{v_7, u_4} C₁₂
inst✝¹⁴ : Category.{v_8, u_5} C₂₃
inst✝¹³ : Category.{v_9, u_9} D₁₂
inst✝¹² : Category.{v_10, u_10} D₂₃
inst✝¹¹ : Category.{v_11, u_11} C
inst✝¹⁰ : Category.{v_12, u_12} D
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
L₁₂ : C₁₂ ⥤ D₁₂
L₂₃ : C₂₃ ⥤ D₂₃
L : C ⥤ D
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
W₁₂ : MorphismProperty C₁₂
W₂₃ : MorphismProperty C₂₃
inst✝⁹ : W₁.ContainsIdentities
inst✝⁸ : W₂.ContainsIdentities
inst✝⁷ : W₃.ContainsIdentities
inst✝⁶ : L₁.IsLocalization W₁
inst✝⁵ : L₂.IsLocalization W₂
inst✝⁴ : L₃.IsLocalization W₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C
F : C₁ ⥤ C₂₃ ⥤ C
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
iso : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
F₁₂' : D₁ ⥤ D₂ ⥤ D₁₂
G' : D₁₂ ⥤ D₃ ⥤ D
F' : D₁ ⥤ D₂₃ ⥤ D
G₂₃' : D₂ ⥤ D₃ ⥤ D₂₃
inst✝³ : Lifting₂ L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂'
inst✝² : Lifting₂ L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G'
inst✝¹ : Lifting₂ L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F'
inst✝ : Lifting₂ L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃'
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((associator L₁ L₂ L₃ L₁₂ L₂₃ L W₁ W₂ W₃ W₁₂ W₂₃ iso F₁₂' G' F' G₂₃').hom.app (L₁.obj X₁)).app (L₂.obj X₂)).app
      (L₃.obj X₃) =
    (G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂').hom.app X₁).app X₂)).app
        (L₃.obj X₃) ≫
      ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G').hom.app ((F₁₂.obj X₁).obj X₂)).app X₃ ≫
        L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight C₂₃ C D).obj L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
            (F'.obj (L₁.obj X₁)).map
              (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight C₃ C₂₃ D₂₃).obj L₂₃) G₂₃').inv.app X₂).app X₃)

Tactic:
dsimp [associator]
  rw [lift₃NatTrans_app_app_app]
  dsimp [Lifting₃.iso, Lifting₃.bifunctorComp₁₂, Lifting₃.bifunctorComp₂₃]
  simp only [Category.assoc]

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

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u₁
inst✝¹ : EnrichedCategory V D
E : Type u₂
inst✝ : EnrichedCategory V E
F G H : EnrichedFunctor V C D
α : F ⟶ G
β : G ⟶ H
I : EnrichedFunctor V D E
X : C
⊢ (whiskerRight { out := α.out ≫ β.out } I).out.app X = (whiskerRight α I ≫ whiskerRight β I).out.app X

Tactic:
simp only [whiskerRight_out_app, NatTrans.comp_app, EnrichedFunctor.category_comp_out,
    EnrichedFunctor.forget, EnrichedFunctor.comp_obj, EnrichedFunctor.comp_map]

Goal state after:
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u₁
inst✝¹ : EnrichedCategory V D
E : Type u₂
inst✝ : EnrichedCategory V E
F G H : EnrichedFunctor V C D
α : F ⟶ G
β : G ⟶ H
I : EnrichedFunctor V D E
X : C
⊢ homOf V (homTo V (α.out.app X ≫ β.out.app X) ≫ I.map (F.obj («to» V X)) (H.obj («to» V X))) =
    homOf V (homTo V (α.out.app X) ≫ I.map (F.obj («to» V X)) (G.obj («to» V X))) ≫
      homOf V (homTo V (β.out.app X) ≫ I.map (G.obj («to» V X)) (H.obj («to» V X)))
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ≫ e₁.inv = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ e₁.hom ≫ e₁.inv

Tactic:
Iso.hom_inv_id,

Goal state after:
case e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ (ρ_ X).hom ≫ e₁.inv = (e₁.inv ⊗ₘ ε.inv) ≫ (μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom ≫ 𝟙 (L'.obj X')
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ L'.obj X' ◁ L'.map (λ_ Y').hom ≫ (μ L W ε X' Y').hom ≫ (μ L W ε X' Y').inv =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : L'.obj X' ≅ X
Y' : C
e₂ : L'.obj Y' ≅ Y
h₁ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ (μ L W ε X' (𝟙_ C ⊗ Y')).hom =
    ((μ L W ε X' (𝟙_ C)).hom ⊗ₘ 𝟙 (L'.obj Y')) ≫ (μ L W ε (X' ⊗ 𝟙_ C) Y').hom ≫ L'.map (α_ X' (𝟙_ C) Y').hom
h₂ : (ε' L W ε).hom ▷ L'.obj Y' ≫ (λ_ (L'.obj Y')).hom = (μ L W ε (𝟙_ C) Y').hom ≫ L'.map (λ_ Y').hom
h₃ :
  (α_ (L'.obj X') (L'.obj (𝟙_ C)) (L'.obj Y')).hom ≫
      L'.obj X' ◁ (μ L W ε (𝟙_ C) Y').hom ≫ L'.obj X' ◁ L'.map (λ_ Y').hom ≫ 𝟙 (L'.obj X' ⊗ L'.obj Y') =
    ((μ L W ε X' (𝟙_ C)).hom ≫ L'.map (ρ_ X').hom) ▷ L'.obj Y'
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
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
inst✝ : p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Tactic:
by
  subst_hom_lift p f φ; simp

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
inst✝ : p.IsHomLift f φ
⊢ p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯

Tactic:
by
  subst_hom_lift p f φ; simp

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

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
inst✝ : p.IsCocartesian f φ
⊢ IsCocartesian.map p f φ φ = 𝟙 b

Tactic:
by
  subst_hom_lift p f φ; symm
  apply map_uniq
  simp only [comp_id]

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

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
inst✝ : p.IsStronglyCocartesian f φ
⊢ map p f φ ⋯ φ = 𝟙 b

Tactic:
by
  subst_hom_lift p f φ; symm
  apply map_uniq
  simp only [comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
X Y : C
w : X ⟶ Y
hw : W w
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ F.HasPointwiseLeftDerivedFunctorAt W Y

Tactic:
by
  simp only [F.hasPointwiseLeftDerivedFunctorAt_iff W.Q W]
  exact hasPointwiseRightKanExtensionAt_iff_of_iso W.Q F (Localization.isoOfHom W.Q W w hw)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_5, u_2} H
F F' : C ⥤ H
e : F ≅ F'
W : MorphismProperty C
⊢ F.HasLeftDerivedFunctor W ↔ F'.HasLeftDerivedFunctor W

Tactic:
rw [hasLeftDerivedFunctor_iff F W.Q W, hasLeftDerivedFunctor_iff F' W.Q W,
    hasRightExtension_iff_of_iso₂ W.Q e]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
i : WalkingPair
⊢ s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt

Tactic:
by
      cases i
      · exact Fan.IsLimit.lift h₁ (fun a ↦ s.proj (.inl a))
      · exact Fan.IsLimit.lift h₂ (fun a ↦ s.proj (.inr a))

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f✝ : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
equiv : ContAction FintypeCat (Aut F') ≌ ContAction FintypeCat (Aut F) :=
  (Equivalence.mapContAction (Aut F') FintypeCat.uSwitchEquivalence ⋯ ⋯).trans (ContAction.resEquiv FintypeCat f✝)
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (functorToContAction F).map f ≫
      (ObjectProperty.isoMk Action.IsContinuous
          (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj Y✝)) ⋯)).hom =
    (ObjectProperty.isoMk Action.IsContinuous
          (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X✝)) ⋯)).hom ≫
      (functorToContAction F' ⋙ equiv.functor).map f

Tactic:
by
        ext : 2
        exact FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (F.map f)

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul (Aut F) X.V.obj
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun i ↦ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i)))) ≅ X
g : ι → C
gu :
  ∀ (i : ι),
    Nonempty ((functorToAction F).obj (g i) ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i))))
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Tactic:
exact ⟨∐ g, ⟨PreservesCoproduct.iso (functorToAction F) g ≪≫
    Sigma.mapIso (fun i ↦ (gu i).some) ≪≫ u⟩⟩

Goal state after: