mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType.sum + (Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α

Tactic:
sum_cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support + (Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType = {2} → σ.IsSwap

Tactic:
intro h
    simp [← card_support_eq_two, ← sum_cycleType, h]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : σ.cycleType = 0
⊢ σ.IsThreeCycle

Tactic:
rw [← sum_cycleType, h0, sum_zero] at h

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : 0 = 3
h0 : σ.cycleType = 0
⊢ σ.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case intro.cons
β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ✝ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val✝ : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
⊢ (∀ τ ∈ σ :: l, τ.IsCycle) → List.Pairwise Disjoint (σ :: l) → P (σ :: l).prod

Tactic:
| cons σ l ih =>

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ σ.Disjoint (τ * f⁻¹)

Tactic:
rw [mem_cycleFactorsFinset_iff] at hf
        intro x
        rcases hd x with hx | hx
        · exact Or.inl hx
        · refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support
⊢ ∀ (a : ℤ), c.subtypePermOfSupport ^ a = k.subtypePerm hc' ↔ g.subtypePerm ⋯ ^ a = k.subtypePerm hc'

Tactic:
intro n

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support
n : ℤ
⊢ c.subtypePermOfSupport ^ n = k.subtypePerm hc' ↔ g.subtypePerm ⋯ ^ n = k.subtypePerm hc'
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹⁶ : Semiring R
inst✝¹⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid M₃
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : (i : Fin n.succ) → Module R (M i)
inst✝⁹ : (i : ι) → Module R (M₁ i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝⁴ : (i : ι) → Module R (M₁' i)
inst✝³ : (i : ι) → AddCommMonoid (M₁'' i)
inst✝² : (i : ι) → Module R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → β i → Type u_2
inst✝¹ : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst✝ : (i : ι) → (b : β i) → Module R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N i.fst i.snd) (i : (i : ι) × β i) (x y : N i.fst i.snd),
    (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i (x + y)) i_1)) =
      (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i x) i_1)) + g fun i_1 ↦ (f i_1) (Sigma.curry (update m i y) i_1)

Tactic:
classical
    simp +instances [Subsingleton.elim hDecEqSigma Sigma.instDecidableEqSigma,
      Sigma.curry_update, Function.apply_update (fun i ↦ f i)]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹⁶ : Semiring R
inst✝¹⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : AddCommMonoid M₃
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : (i : Fin n.succ) → Module R (M i)
inst✝⁹ : (i : ι) → Module R (M₁ i)
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M₃
inst✝⁶ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝⁴ : (i : ι) → Module R (M₁' i)
inst✝³ : (i : ι) → AddCommMonoid (M₁'' i)
inst✝² : (i : ι) → Module R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → β i → Type u_2
inst✝¹ : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst✝ : (i : ι) → (b : β i) → Module R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N i.fst i.snd) (i : (i : ι) × β i) (c : R) (x : N i.fst i.snd),
    (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i (c • x)) i_1)) =
      c • g fun i_1 ↦ (f i_1) (Sigma.curry (update m i x) i_1)

Tactic:
classical
    simp +instances [Subsingleton.elim hDecEqSigma Sigma.instDecidableEqSigma,
      Sigma.curry_update, Function.apply_update (fun i ↦ f i)]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: case mpr.refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x : c.pt
f₁ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := true }
⊢ ∃ a, F.descColimitType c a = x

Tactic:
let f₂ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun x => ULift.up (∃ a, F.descColimitType c a = x)

Goal state after:
case mpr.refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x : c.pt
f₁ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := true }
f₂ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := decide (∃ a, F.descColimitType c a = x) }
⊢ ∃ a, F.descColimitType c a = x
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ 1 * M.mk F ⟨j, x⟩ = M.mk F ⟨j, x⟩

Tactic:
colimit_one_eq F j,

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, 1⟩ * M.mk F ⟨j, x⟩ = M.mk F ⟨j, x⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ * 1 = M.mk F ⟨j, x⟩

Tactic:
colimit_one_eq F j,

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
x : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ * M.mk F ⟨j, 1⟩ = M.mk F ⟨j, x⟩
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
⊢ ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j

pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j
⊢ IsLimit c

Tactic:
· let cs := coneOfSection hs
    exact ⟨t.lift cs ⟨⟩, fun j ↦ congr_hom (t.fac cs j) ⟨⟩,
      fun x hx ↦ congr_hom (CC := fun X ↦ X)
        (t.uniq cs (↾fun _ ↦ x) fun j ↦ by ext; exact hx j) ⟨⟩⟩

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j
⊢ IsLimit c
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.unop = (Quiver.Hom.op ((hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s))) (𝟙 (unop s.pt)))).unop

Tactic:
apply (Types.isLimitEquivSections (hc s.pt.unop)).injective

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ (Types.isLimitEquivSections (hc (unop s.pt))) m.unop =
    (Types.isLimitEquivSections (hc (unop s.pt)))
      (Quiver.Hom.op ((hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s))) (𝟙 (unop s.pt)))).unop
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ X
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj X).map g)) (shrinkYonedaObjObjEquiv.symm f) =
    shrinkYonedaObjObjEquiv.symm (g.unop ≫ f)

Tactic:
simp [shrinkYoneda_obj_map]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ ∀ (x y : ↑s✝.1),
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
        (x * y) =
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
        (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y

Tactic:
intro x y
      simp only [Types.Small.limitCone_pt, Functor.comp_obj, Functor.mapCone_pt,
        Types.Small.limitConeIsLimit_lift, Functor.const_obj_obj, Functor.mapCone_π_app,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, map_mul]
      rw [← equivShrink_mul]
      rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
P : ObjectProperty C
tensorUnit : P (𝟙_ C)
tensorObj : ∀ (X Y : C), P X → P Y → P (X ⊗ Y)
X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ (homMk (x✝¹.hom ⊗ₘ x✝.hom)).hom = (homMk (x✝¹.hom ▷ X₂✝.obj) ≫ homMk (Y₁✝.obj ◁ x✝.hom)).hom

Tactic:
apply tensorHom_def

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X₁ Y₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ F.map (f ⊗ₘ g) = F.map (f ▷ X₂ ≫ Y₁ ◁ g)

Tactic:
fData.tensorHom_eq,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X₁ Y₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (fData.μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (fData.μIso Y₁ Y₂).hom = F.map (f ▷ X₂ ≫ Y₁ ◁ g)
Module: Mathlib.CategoryTheory.Monoidal.Discrete

Goal state before:
pp: M : Type u
inst✝² : Monoid M
N : Type u'
inst✝¹ : Monoid N
K : Type u
inst✝ : Monoid K
F : M →* N
G : N →* K
⊢ ε (monoidalFunctor F ⋙ monoidalFunctor G) ≫ (monoidalFunctorComp F G).hom.app (𝟙_ (Discrete M)) =
    ε (monoidalFunctor (G.comp F))

Tactic:
dsimp only [comp_ε, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_ε]
    simp [eqToHom_map]

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

Goal state before:
pp: case η
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ (εIso F).hom ≫ η F = (εIso F).hom ≫ η F

Tactic:
rw [εIso_hom, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_hom]

Goal state after:
case η
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ (εIso F).hom ≫ η F = ε F ≫ η F
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasPushouts C
⊢ HasPullbacks Cᵒᵖ

Tactic:
have : HasColimitsOfShape WalkingCospanᵒᵖ C :=
    hasColimitsOfShape_of_equivalence walkingCospanOpEquiv.symm
  apply hasLimitsOfShape_op_of_hasColimitsOfShape

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (𝟙_ C) (G.obj X) ≫ η F ▷ F.obj (G.obj X) ≫ (λ_ (F.obj (G.obj X))).hom ≫ adj.counit.app X

Tactic:
left_unitality_hom_assoc

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X = F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : naturalityProperty app f
hg : naturalityProperty app g
⊢ naturalityProperty app (f ≫ g)

Tactic:
by
    simp only [naturalityProperty] at hf hg ⊢
    simp only [Functor.map_comp, Category.assoc, hg]
    slice_lhs 1 2 => rw [hf]
    rw [Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
h : W f✝
g : y✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (f✝ ≫ g)

Tactic:
exact .of_comp _ g h hg

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ μ G X Y ≫ G.map (β_ X Y).hom = (β_ (G.obj X) (G.obj Y)).hom ≫ μ G Y X

Tactic:
this X Y,

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (β_ (G.obj X) (G.obj Y)).hom ≫ μ G Y X
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R✝ : Type w
inst✝⁴ : Ring R✝
J : Type u
inst✝³ : Category.{v, u} J
F : J ⥤ ModuleCat R✝
R : Type w
inst✝² : CommRing R
M ι : Type u
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Cocone (Discrete.functor fun x ↦ of R M)
f : (finsuppCocone R M ι).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (finsuppCocone R M ι).ι.app j ≫ f = s.ι.app j
i : ι
x : M
⊢ (Hom.hom f ∘ₗ Finsupp.lsingle i) x =
    (Hom.hom (↟((Finsupp.lsum R) fun i ↦ Hom.hom (s.ι.app { as := i }))) ∘ₗ Finsupp.lsingle i) x

Tactic:
simpa using! congr($(h ⟨i⟩) (x : M))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ ((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫
        (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫
          (X₁ ⊗ X₂) ◁ (β_ X₃ (Y₁ ⊗ Y₂)).hom ▷ Y₃ ≫
            (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫
      ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫
            X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷
          (X₃ ⊗ Y₃) ≫
        (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
    𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃)

Tactic:
by
          rw [braiding_tensor_right_hom]; monoidal

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : TensorAlgebra R M
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι R))

Tactic:
induction x using induction with

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (TensorAlgebra R M)) r
⊢ x = 0 ∧ r = 0

Tactic:
let : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (TensorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ x = 0 ∧ r = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ ∀ (n : ℕ), x.snd <• x.fst ^ n = x.fst ^ n •> x.snd

Tactic:
intro n

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
⊢ (conjugateEquiv adj₁ adj₁).symm (𝟙 R₁) = 𝟙 L₁

Tactic:
by
  rw [Equiv.symm_apply_eq]
  simp only [conjugateEquiv_id]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ lTensor (A × B) counit ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1

Tactic:
ext : 1
    · rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
    · rw [comp_assoc, comul_comp_inr, ← comp_assoc, lTensor_comp_map, counit_comp_inr,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : ↑Y
s : S
⊢ s • (ConcreteCategory.hom g) y = (ConcreteCategory.hom g) (s • y)

Tactic:
map_smul

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : ↑Y
s : S
⊢ s • (ConcreteCategory.hom g) y = s • (ConcreteCategory.hom g) y
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s'✝ : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
s' : S := s'✝
⊢ s' • (ConcreteCategory.hom g) y = (ConcreteCategory.hom g) (s' • y)

Tactic:
map_smul

Goal state after:
case tmul
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s'✝ : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
s' : S := s'✝
⊢ s' • (ConcreteCategory.hom g) y = s' • (ConcreteCategory.hom g) y