mathlib-initiative/mathlib-tactics huggingface dataset:
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)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x ^ (↑k + 1 - 1) * rexp (-(c * x)) = ↑k ! / c ^ (k + 1)

Tactic:
by
        simp_rw [key, Gamma_nat_eq_factorial, div_eq_mul_inv,
          one_mul, mul_comm, inv_rpow hc.le, ← rpow_natCast]
        norm_cast

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in 0..↑M, x ^ k * rexp (-(c * x)) * rexp c ≤ ↑k ! / c ^ (k + 1) * rexp c

Tactic:
intervalIntegral.integral_mul_const

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ (∫ (x : ℝ) in 0..↑M, x ^ k * rexp (-(c * x))) * rexp c ≤ ↑k ! / c ^ (k + 1) * rexp c
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsSeparator G ↔ (preadditiveCoyoneda.obj (op G)).Faithful

Tactic:
isSeparator_iff_faithful_coyoneda_obj,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (coyoneda.obj (op G)).Faithful ↔ (preadditiveCoyoneda.obj (op G)).Faithful
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
by
  suffices ∑ i ∈ .Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ x in a..a + ↑(b - a), f x by simp_all
  simp_rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range, add_assoc]
  suffices ∑ x ∈ .range (b - a), f (a + ↑(x + 1)) ≤ ∫ x in a..a + ↑(b - a), f x by simp_all
  exact AntitoneOn.sum_le_integral (by simp [hf, hab])

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

Goal state before:
pp: case refine_1
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
⊢ ∀ᶠ (b : ℕ) in atTop, d < u b / ↑b

Tactic:
obtain ⟨ε, hε, εpos⟩ : ∃ ε : ℝ, d + ε * (1 + l) < l ∧ 0 < ε := by
      have L : Tendsto (fun ε => d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
      simp only [zero_mul, add_zero] at L
      exact (((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists

Goal state after:
case refine_1
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 < ε
⊢ ∀ᶠ (b : ℕ) in atTop, d < u b / ↑b
Module: Mathlib.Analysis.SpecificLimits.FloorPow

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

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

Tactic:
· refine tendsto_nat_floor_div_atTop.comp ?_
      exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)

Goal state after:
case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ ↑⌊c k ^ n⌋₊ / c k ^ n) atTop (𝓝 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
hM : 0 < M
⊢ ∫ (x : ℝ) in ↑N..↑M + ↑N, ‖f x‖ = ∫ (x : ℝ) in ↑N..↑M + ↑N, f x

Tactic:
refine intervalIntegral.integral_congr_uIoo fun x ↦ ?_

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
M : ℕ
hM : 0 < M
x : ℝ
⊢ x ∈ uIoo (↑N) (↑M + ↑N) → ‖f x‖ = f x
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: c : ℝ
hc : 1 < c
i : ℕ
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc
  rcases eq_or_ne i 0 with (rfl | hi)
  · simp only [pow_zero, Nat.floor_one, Nat.cast_one, mul_one, sub_le_self_iff, inv_nonneg, cpos.le]
  calc
    (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹ := by ring
    _ ≤ c ^ i - 1 := by
      gcongr
      simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi
    _ ≤ ⌊c ^ i⌋₊ := (Nat.sub_one_lt_floor _).le

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case base
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := f x, property := ⋯ }.obj

Tactic:
refine ⟨⟨0, ?_⟩,?_⟩

Goal state after:
case base.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure f 0).fst

case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨0, ?base.refine_1⟩ = { obj := f x, property := ⋯ }.obj
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
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ (ConcreteCategory.hom (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i))
      ((ConcreteCategory.hom (colimitYonedaHomIsoLimit D F).hom) f) =
    {
      down :=
        (ConcreteCategory.hom (f.app (D.obj i)))
          ((ConcreteCategory.hom ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i))) (𝟙 (unop (D.obj i)))) }

Tactic:
by
  change ((colimitYonedaHomIsoLimit D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i)) f = _
  simp only [colimitYonedaHomIsoLimit, Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]
  rw [← Category.assoc, colimitHomIsoLimitYoneda_hom_comp_π]
  dsimp [yonedaLemma]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h
j : J
⊢ { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ g =
    { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ h

Tactic:
← cancel_epi (pullbackObjIso _ _ _).inv

Goal state after:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g h : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ h
j : J
⊢ (pullbackObjIso c.ι ((Functor.const J).map f) j).inv ≫
      { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ g =
    (pullbackObjIso c.ι ((Functor.const J).map f) j).inv ≫
      { pt := X, ι := pullback.snd c.ι ((Functor.const J).map f) }.ι.app j ≫ f ≫ h
Module: Mathlib.CategoryTheory.Abelian.Injective.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hJ : Injective J
⊢ (preadditiveYonedaObj J).PreservesHomology

Tactic:
let := (injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' J).mp hJ

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hJ : Injective J
this : (preadditiveYonedaObj J).PreservesEpimorphisms :=
  (injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' J).mp hJ
⊢ (preadditiveYonedaObj J).PreservesHomology
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
inst✝ : Injective Z
n : ℕ
⊢ Injective (((single₀ C).obj Z).X n)

Tactic:
cases n
    · simpa
    · apply IsZero.injective
      apply HomologicalComplex.isZero_single_obj_X
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: case refine_4
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
x✝ : (sq₁.map uliftFunctor.{max u v, v}).X₃
⊢ ((ConcreteCategory.hom
            ((sq₁.map uliftFunctor.{max u v, v}).f₃₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom)).toFun
        x✝).down =
    ((ConcreteCategory.hom
            (((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₃₄)).toFun
        x✝).down

Tactic:
simpa [types_comp, uliftFunctor_map] using congrFun comm₃₄ _

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
X' : C
R' : ProjectiveResolution X'
f : X ⟶ X'
φ : R.Hom R' f
n : ℤ
m : ℕ
h : -↑m = n
⊢ φ.hom'.f n = (R.cochainComplexXIso n m h).hom ≫ φ.hom.f m ≫ (R'.cochainComplexXIso n m h).inv

Tactic:
simp [hom', HomologicalComplex.extendMap_f _
    ComplexShape.embeddingDownNat (i := m) (i' := n) (by dsimp; lia),
    cochainComplexXIso]

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 G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((NatTrans.rightDerivedToHomotopyCategory α).app X) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) ≫
      HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv

Tactic:
rw [InjectiveResolution.rightDerivedToHomotopyCategory_app_eq α P,
    Functor.map_comp, Functor.map_comp, assoc]

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 G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
        HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
              (P.isoRightDerivedToHomotopyCategoryObj G).inv
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

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

Tactic:
exact P.prop_of_iso
    (asIso (cokernel.map f _ (Abelian.factorThruImage f) (𝟙 Y) (by simp))) hf

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

Goal state before:
pp: V : Type (u + 1)
inst✝³ : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst✝² : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝¹ : ConcreteCategory V FV
G : Type u_3
inst✝ : Monoid G
X : Action V G
x : ToType X
⊢ 1 • x = x

Tactic:
change ConcreteCategory.hom (X.ρ 1) x = x

Goal state after:
V : Type (u + 1)
inst✝³ : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst✝² : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝¹ : ConcreteCategory V FV
G : Type u_3
inst✝ : Monoid G
X : Action V G
x : ToType X
⊢ (ConcreteCategory.hom (X.ρ 1)) x = x
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
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
⊢ (lift fn fg h).comp inl = fn

Tactic:
by ext; simp

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
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
⊢ (lift fn fg h).comp inr = fg

Tactic:
by ext; simp

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
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
F : N ⋊[φ] G →* H
x✝ : G
⊢ (F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝)) =
    (MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝))).comp (F.comp inl)

Tactic:
by ext; simp [inl_aut]

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
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))
x✝ : G₁
⊢ MulEquiv.trans (φ₁ x✝) fn = fn.trans (((↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)) (fg x✝))

Tactic:
by ext; simp

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
J : Type u_3
inst✝ : Category.{v_2, u_3} J
F : J ⥤ Action V G
c✝ : Cone F
h : IsLimit ((forget V G).mapCone c✝)
⊢ IsLimit c✝

Tactic:
by
    apply isLimitOfReflects ((Action.functorCategoryEquivalence V G).functor)
    exact evaluationJointlyReflectsLimits _ (fun _ => h)

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✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
⊢ MonoidHom.id H = (↑f).comp ↑f.symm

Tactic:
by ext; simp

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✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
⊢ (↑f.symm).comp ↑f = MonoidHom.id G

Tactic:
by ext; simp

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

Goal state before:
pp: V✝ : Type u_1
inst✝³ : Category.{v_1, u_1} V✝
V : Type u_2
W : Type u_3
inst✝² : Category.{v_2, u_2} V
inst✝¹ : Category.{v_3, u_3} W
G : Type u_4
inst✝ : Monoid G
E : V ≌ W
X : Action V G
⊢ (E.functor.mapAction G).map
        ((Functor.mapActionCongr G E.unitIso ≪≫ Functor.mapActionComp G E.functor E.inverse).hom.app X) ≫
      ((Functor.mapActionComp G E.inverse E.functor).symm ≪≫ Functor.mapActionCongr G E.counitIso).hom.app
        ((E.functor.mapAction G).obj X) =
    𝟙 ((E.functor.mapAction G).obj X)

Tactic:
by ext; simp

Goal state after:
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
⊢ ContinuousMonoidHom.id H = (↑f).comp ↑f.symm

Tactic:
by ext; simp

Goal state after:
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
⊢ (↑f.symm).comp ↑f = ContinuousMonoidHom.id G

Tactic:
by ext; simp

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

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)

Tactic:
induction n with
  | zero => exact Prod.ext rfl (funext fun x => Fin.elim0 x)
  | succ n hn =>
    refine Prod.ext rfl (funext fun x => ?_)
    induction x using Fin.cases
    <;> simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]
    <;> rfl

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X✝ Y✝ : Action V G
x✝¹ : X✝ ⟶ Y✝
x✝ : Action V G
⊢ (F.mapAction G).map x✝¹ ▷ (F.mapAction G).obj x✝ ≫ { hom := μ F Y✝.V x✝.V, comm := ⋯ } =
    { hom := μ F X✝.V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map (x✝¹ ▷ x✝)

Tactic:
by ext; simp

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X✝ Y✝ x✝¹ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ (F.mapAction G).obj x✝¹ ◁ (F.mapAction G).map x✝ ≫ { hom := μ F x✝¹.V Y✝.V, comm := ⋯ } =
    { hom := μ F x✝¹.V X✝.V, comm := ⋯ } ≫ (F.mapAction G).map (x✝¹ ◁ x✝)

Tactic:
by ext; simp

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
x✝² x✝¹ x✝ : Action V G
⊢ { hom := μ F x✝².V x✝¹.V, comm := ⋯ } ▷ (F.mapAction G).obj x✝ ≫
      { hom := μ F (x✝² ⊗ x✝¹).V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((F.mapAction G).obj x✝²) ((F.mapAction G).obj x✝¹) ((F.mapAction G).obj x✝)).hom ≫
      (F.mapAction G).obj x✝² ◁ { hom := μ F x✝¹.V x✝.V, comm := ⋯ } ≫ { hom := μ F x✝².V (x✝¹ ⊗ x✝).V, comm := ⋯ }

Tactic:
by ext; simp

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
x✝ : Action V G
⊢ (λ_ ((F.mapAction G).obj x✝)).hom =
    { hom := ε F, comm := ⋯ } ▷ (F.mapAction G).obj x✝ ≫
      { hom := μ F (𝟙_ (Action V G)).V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map (λ_ x✝).hom

Tactic:
by ext; simp

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
x✝ : Action V G
⊢ (ρ_ ((F.mapAction G).obj x✝)).hom =
    (F.mapAction G).obj x✝ ◁ { hom := ε F, comm := ⋯ } ≫
      { hom := μ F x✝.V (𝟙_ (Action V G)).V, comm := ⋯ } ≫ (F.mapAction G).map (ρ_ x✝).hom

Tactic:
by ext; simp

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
X✝ Y✝ : Action V G
x✝¹ : X✝ ⟶ Y✝
x✝ : Action V G
⊢ { hom := δ F X✝.V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map x✝¹ ▷ (F.mapAction G).obj x✝ =
    (F.mapAction G).map (x✝¹ ▷ x✝) ≫ { hom := δ F Y✝.V x✝.V, comm := ⋯ }

Tactic:
by ext; simp

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
X✝ Y✝ x✝¹ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ { hom := δ F x✝¹.V X✝.V, comm := ⋯ } ≫ (F.mapAction G).obj x✝¹ ◁ (F.mapAction G).map x✝ =
    (F.mapAction G).map (x✝¹ ◁ x✝) ≫ { hom := δ F x✝¹.V Y✝.V, comm := ⋯ }

Tactic:
by ext; simp

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.OplaxMonoidal
x✝² x✝¹ x✝ : Action V G
⊢ { hom := δ F (x✝² ⊗ x✝¹).V x✝.V, comm := ⋯ } ≫
      { hom := δ F x✝².V x✝¹.V, comm := ⋯ } ▷ (F.mapAction G).obj x✝ ≫
        (α_ ((F.mapAction G).obj x✝²) ((F.mapAction G).obj x✝¹) ((F.mapAction G).obj x✝)).hom =
    (F.mapAction G).map (α_ x✝² x✝¹ x✝).hom ≫
      { hom := δ F x✝².V (x✝¹ ⊗ x✝).V, comm := ⋯ } ≫ (F.mapAction G).obj x✝² ◁ { hom := δ F x✝¹.V x✝.V, comm := ⋯ }

Tactic:
by ext; simp

Goal state after: