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

Goal state before:
pp: z : ℂ
c k : ℤ
hk : 2 ≤ k
⊢ Summable fun d ↦ ((↑c * z + ↑d) ^ k)⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)

Goal state after:
z : ℂ
c k : ℤ
hk : 2 ≤ k
⊢ (fun n ↦ ((↑c * z + ↑n) ^ k)⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ ↑k)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ Summable fun c ↦ ((↑c * z + ↑d) ^ k)⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)

Goal state after:
z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ (fun n ↦ ((↑n * z + ↑d) ^ k)⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ ↑k)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: a b : ℤ
this : ∀ (x : Fin 2 → ℤ), ![x 0 + a, x 1 + b] = x + ![a, b]
⊢ (fun x ↦ x) =Θ[cofinite] fun x ↦ ‖x‖

Tactic:
rw [← isTheta_norm_left]

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

Goal state before:
pp: L : PeriodPair
x : ℂ
⊢ AnalyticAt ℂ L.relation x

Tactic:
by
  by_cases hx : x ∈ L.lattice
  · lift x to L.lattice using hx
    have := L.analyticAt_relation_zero
    rw [← sub_self x.1] at this
    convert! this.comp (f := (· - x.1)) (by fun_prop)
    ext a
    simp
  · have : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x := by
      have := L.analyticOnNhd_derivWeierstrassP _ hx
      have := L.analyticOnNhd_weierstrassP _ hx
      fun_prop
    apply this.congr
    filter_upwards [L.isClosed_lattice.isOpen_compl.mem_nhds hx] with x hx
    simp_all [relation]

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

Goal state before:
pp: case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ eval x (T ℝ ↑n)

Tactic:
have := isMaxOn_iff.mp h (cos (0 * π / n)) (by simp)

Goal state after:
case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
this : eval (cos (0 * π / ↑n)) (T ℝ ↑n) ≤ eval x (T ℝ ↑n)
⊢ 1 ≤ eval x (T ℝ ↑n)
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn =>
    rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]
    congr
    rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one,
      Finset.mul_sum, Finset.mul_sum]
    congr with k
    ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 = -(-x ^ 2 / (↑n + 1) ^ 2)

Tactic:
neg_div',

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 = - -x ^ 2 / (↑n + 1) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ (↑π * x).cot * ↑π - 1 / x = ↑π * (↑π * x).cot - 1 / x

pp: case ha
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π ≠ 0

pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0

Tactic:
· ring

Goal state after:
case ha
x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π ≠ 0

x : ℂ
hz : x ∈ ℂ_ℤ
this : (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) = fun z ↦ (Complex.sin ∘ fun t ↦ ↑π * t) z / (↑π * z)
⊢ ↑π * x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ (x - (↑n + 1) + (x + (↑n + 1))) / ((x - (↑n + 1)) * (x + (↑n + 1))) = 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))

pp: case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - (↑n + 1) ≠ 0

pp: case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + (↑n + 1) ≠ 0

Tactic:
· ring

Goal state after:
case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - (↑n + 1) ≠ 0

case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + (↑n + 1) ≠ 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ (Iso.refl
          {
              X₁ :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                    ((CochainComplex.single₀ C).obj Z)).X₂,
              X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
              X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
              f :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                    (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
              g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
              zero := ⋯ }.X₂).hom ≫
      { X₁ := Z, X₂ := under Z, X₃ := syzygies (Injective.ι Z), f := Injective.ι Z, g := d (Injective.ι Z),
          zero := ⋯ }.g =
    {
          X₁ :=
            ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                ((CochainComplex.single₀ C).obj Z)).X₂,
          X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
          X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
          f :=
            ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
          g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
          zero := ⋯ }.g ≫
      (Iso.refl
          {
              X₁ :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                    ((CochainComplex.single₀ C).obj Z)).X₂,
              X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
              X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
              f :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                    (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
              g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
              zero := ⋯ }.X₃).hom

Tactic:
by simp [ofCocomplex]

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 : C
inst✝ : Injective X
⊢ IsIso ((self X).toRightDerivedZero' F)

Tactic:
dsimp [InjectiveResolution.toRightDerivedZero']

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
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ IsIso
    (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj ((CochainComplex.single₀ C).obj X)).liftCycles (F.map (𝟙 X)) 1
      toRightDerivedZero'._proof_1 ⋯)
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
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ IsIso (P.toRightDerivedZero' F)

Tactic:
dsimp [InjectiveResolution.toRightDerivedZero']

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
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ IsIso
    (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).liftCycles (F.map (P.ι.f 0)) 1
      InjectiveResolution.toRightDerivedZero'._proof_1 ⋯)
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
⊢ rightHom.comp inl = 1

Tactic:
by ext; simp [rightHom]

Goal state after:
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
g : G
⊢ N.ρ g = ((forget V G).mapIso f).conj (M.ρ g)

Tactic:
rw [Iso.conj_apply, Iso.eq_inv_comp]; simp [f.hom.comm]

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

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
X Y : InducedBicategory C F
f : X ⟶ Y
⊢ (eqToHom ⋯).hom = eqToHom ⋯

Tactic:
simp only [eqToHom_refl, Hom.category_id_hom]

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

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝ : Bicategory C
F : B → C
X Y : InducedBicategory C F
f : F X ⟶ F Y
⊢ (mkHom₂ (eqToHom ⋯)).hom = (eqToHom ⋯).hom

Tactic:
simp only [eqToHom_refl, Hom.category_id_hom]

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
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        θ.naturality f ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
calc
        _ = 𝟙 _ ⊗≫ (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
              θ.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ ι.app b ⊗≫ (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫
              θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [← whisker_exchange]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv

Tactic:
F.mapComp_id_right_hom f,

Goal state after:
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.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).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₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫
        F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f ⋯).inv

Tactic:
rw [← cancel_epi (F.mapComp' f₀₂ f₂₃ f).hom, Iso.hom_inv_id]
  simp [mapComp'₀₂₃_hom _ _ _ _ _ _ f h₀₂ h₁₃ hf]

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)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
⊢ ∀ (X : (i : I) × C i), descMap F X X (𝟙 X) = 𝟙 ((F X.fst).obj X.snd)

Tactic:
by
    rintro ⟨i, X⟩
    apply (F i).map_id

Goal state after:
Module: Mathlib.CategoryTheory.DinatTrans

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ C ⥤ D
δ : F ⤞ G
α : G ⟶ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (α.app (op X✝)).app X✝ ≫ (H.obj (op X✝)).map f =
    (F.obj (op Y✝)).map f ≫ δ.app Y✝ ≫ (G.map f.op).app Y✝ ≫ (α.app (op X✝)).app Y✝

Tactic:
← δ.dinaturality_assoc f,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ C ⥤ D
δ : F ⤞ G
α : G ⟶ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (α.app (op X✝)).app X✝ ≫ (H.obj (op X✝)).map f =
    (F.map f.op).app X✝ ≫ δ.app X✝ ≫ (G.obj (op X✝)).map f ≫ (α.app (op X✝)).app Y✝
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ (μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ▷ L'.obj X₄ ≫
        L'.map (α_ X₁ X₂ X₃).hom ▷ L'.obj X₄ ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ▷ L'.obj X₄ ≫
            (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
              (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
                L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ ≫
                  L'.obj X₁ ◁
                    ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
                      L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom

Tactic:
reassoc_of% this,

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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ (μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ▷ L'.obj X₄ ≫
        L'.map (α_ X₁ X₂ X₃).hom ▷ L'.obj X₄ ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ▷ L'.obj X₄ ≫
            (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom ≫
              L'.obj X₁ ◁
                ((μ L W ε (X₂ ⊗ X₃) X₄).hom ≫
                  L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ (𝟙 (L'.obj X₂) ⊗ₘ (μ L W ε X₃ X₄).inv)) =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f = 𝟙 A.V

Tactic:
exact right_inv h

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

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : ForgetEnrichment V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
⊢ ((λ_ (𝟙_ V)).inv ≫ (homTo V f ⊗ₘ homTo V g) ≫ eComp V («to» V x) («to» V y) («to» V z)).op = f.op ≫ g.op

Tactic:
tensorHom_eComp_op_eq,

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : ForgetEnrichment V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
⊢ ((λ_ (𝟙_ V)).inv ≫
        (β_ (𝟙_ V) (𝟙_ V)).hom ≫
          (homTo V g ⊗ₘ homTo V f) ≫
            eComp V (Opposite.unop («to» V z)) (Opposite.unop («to» V y)) (Opposite.unop («to» V x))).op =
    f.op ≫ g.op
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
S : 𝒮
ha : 𝒳.p.obj a = S
⊢ 𝒴.p.IsHomLift (𝟙 S) (α.app a)

Tactic:
subst ha

Goal state after:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a)
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

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

Tactic:
subst ha

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : p.IsPreFibered
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
⊢ ∃ b φ, p.IsCartesian f φ
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := ⋯
this✝¹ : Fintype ↑T
this✝ : MulAction G (FintypeCat.of ↑T).obj := ⋯
T' : Action FintypeCat G := ⋯
i : T' ⟶ X := ⋯
this : Mono i
⊢ Nonempty ((Action.forget FintypeCat G).obj T').obj

Tactic:
exact Set.Nonempty.coe_sort (MulAction.nonempty_orbit x)

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
⊢ Nat.card (Aut A) ≤ Nat.card (F.obj A).obj

Tactic:
have h : Nonempty (F.obj A) := inferInstance

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsConnected A
h : Nonempty (F.obj A).obj
⊢ Nat.card (Aut A) ≤ Nat.card (F.obj A).obj
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y := ⋯
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) := ⋯
this✝¹ : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := ⋯
hgvi : (functorToAction F).map g = v.inv ≫ i
this✝ : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
⊢ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = f

Tactic:
← cancel_epi ((functorToAction F).map ψ)

Goal state after:
case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this✝¹ : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this✝ : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
⊢ (functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = (functorToAction F).map ψ ≫ f
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
f : Aut F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom
        (F.map
          ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop ((autMulEquivAutGalois F) f))).hom))
      a =
    (ConcreteCategory.hom (f.hom.app A)) a

Tactic:
by
  dsimp [autMulEquivAutGalois, endMulEquivAutGalois]
  rw [endEquivAutGalois_π]
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
H : Set (Aut F)
h1 : 1 ∈ H
h : IsOpen H
⊢ ∃ I x, (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ H

Tactic:
by
  obtain ⟨U, hUopen, rfl⟩ := isOpen_induced_iff.mp h
  obtain ⟨I, u, ho, ha⟩ := isOpen_pi_iff.mp hUopen 1 h1
  choose fι ff fc h4 h5 h6 using (fun X : I => has_decomp_connected_components X.val)
  refine ⟨⋃ X, Set.range (ff X), Fintype.ofFinite _, ?_, ?_⟩
  · rintro X ⟨A, ⟨Y, rfl⟩, hA2⟩
    obtain ⟨i, rfl⟩ := hA2
    exact h5 Y i
  · refine fun σ h ↦ ha (fun X XinI ↦ ?_)
    suffices h : autEmbedding F σ X = 1 by
      rw [h]
      exact (ho X XinI).right
    have h : σ.hom.app X = 𝟙 (F.obj X) := by
      have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _
      ext x
      obtain ⟨⟨j⟩, a, ha : F.map _ a = x⟩ := Limits.FintypeCat.jointly_surjective
        (Discrete.functor (ff ⟨X, XinI⟩) ⋙ F) _ (Limits.isColimitOfPreserves F (h4 ⟨X, XinI⟩)) x
      rw [FintypeCat.id_apply, ← ha, NatTrans.naturality_apply]
      simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]
    exact Iso.ext h

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
b : (F.obj A).obj
hb : (ConcreteCategory.hom (F.map f)) b = y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
σ : Aut F
hσ : (ConcreteCategory.hom (σ.hom.app A)) a = b
⊢ ∃ g, g • x = y

Tactic:
use σ

Goal state after:
case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
b : (F.obj A).obj
hb : (ConcreteCategory.hom (F.map f)) b = y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
σ : Aut F
hσ : (ConcreteCategory.hom (σ.hom.app A)) a = b
⊢ σ • x = y