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

Goal state before:
pp: case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ (finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)

Tactic:
rw [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]

Goal state after:
case succ
n x : ℕ
ih : ∀ (hx : x < n + 2), ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
hx : x + 1 < n + 2
⊢ ¬↑⟨x, ⋯⟩ = n + 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ (finRotate n).IsCycle

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Goal state after:
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).IsCycle
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ (finRotate n).cycleType = {n}

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Goal state after:
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).cycleType = {2 + m}
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : ¬i = j
hj1 : ↑(i + 1) = ↑i + 1
⊢ ↑(i.castLT ⋯) + 1 < ↑j + 1

Tactic:
simp; lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑i ≤ ↑(Fin.cast ⋯ k)

Tactic:
simp; lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑k = ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i))))

Tactic:
simp; lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i)))) = ↑k

Tactic:
simp; lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑i ≤ ↑(Fin.cast ⋯ k)

Tactic:
simp; lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑k = ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i))))

Tactic:
simp; lia

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

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
k✝ k : ℕ
hk : ∀ (v : ↑(vectorsProdEqOne G p)), (σ ^ k) v = f k v
v : ↑(vectorsProdEqOne G p)
⊢ f k (σ v) = f k (f 1 v)

Tactic:
simp only [σ, coe_fn_mk]

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

Goal state before:
pp: case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ f.cycleFactorsFinset.noncommProd id ⋯ * g.cycleFactorsFinset.noncommProd id ⋯ = f * g

Tactic:
rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
⊢ ↑↑(sign σ) * ∏ i, diagonal d (σ i) i = 0

Tactic:
obtain ⟨x, h3⟩ := not_forall.1 (mt Equiv.ext h2)

Goal state after:
case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ ↑↑(sign σ) * ∏ i, diagonal d (σ i) i = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
this : ∏ j, M (τ j) (σ j) = ∏ j, M ((τ * σ⁻¹) j) j
⊢ ↑↑(sign (τ * σ⁻¹)) * ↑↑(sign σ) = ↑↑(sign (τ * σ⁻¹ * σ))

Tactic:
sign_mul (τ * σ⁻¹)

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
this : ∏ j, M (τ j) (σ j) = ∏ j, M ((τ * σ⁻¹) j) j
⊢ ↑↑(sign (τ * σ⁻¹)) * ↑↑(sign σ) = ↑↑(sign (τ * σ⁻¹) * sign σ)
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
⊢ (A * adjp s A) i i = detp s A

Tactic:
have key := sum_fiberwise_eq_sum_filter (ofSign s) univ (· i) fun σ ↦ ∏ k, A k (σ k)
  simp_rw [mem_univ, filter_true] at key
  simp_rw [mul_apply, adjp_apply, mul_sum, detp, ← key]
  refine sum_congr rfl fun x hx ↦ sum_congr rfl fun σ hσ ↦ ?_
  rw [← prod_mul_prod_compl ({i} : Finset n), prod_singleton, (mem_filter.mp hσ).2]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
k : n
hk : ¬k = τ (σ k)
⊢ IsAddUnit ((∏ k, B k (τ k)) * ∏ k, A k (σ k))

Tactic:
← Equiv.prod_comp σ,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
σ : Perm n
hσ : sign σ = s
τ : Perm n
hτ : sign τ = t
k : n
hk : ¬k = τ (σ k)
⊢ IsAddUnit ((∏ i, B (σ i) (τ (σ i))) * ∏ k, A k (σ k))
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 }
f₂ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := decide (∃ a, F.descColimitType c a = x) }
⊢ f₁ = f₂

Tactic:
refine hc.hom_ext fun j => ?_

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) }
j : J
⊢ (F.coconeTypesEquiv c).ι.app j ≫ f₁ = (F.coconeTypesEquiv c).ι.app j ≫ f₂
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∃ j y, (hom (t.ι.app j)) y = x

Tactic:
by_contra hx

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ¬∃ j y, (hom (t.ι.app j)) y = x
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
⊢ ∀ (k : o) (x : n), ((σ (x, k)).1, k) = σ (x, k)

Tactic:
intro k x

Goal state after:
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
k : o
x : n
⊢ ((σ (x, k)).1, k) = σ (x, k)
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map α)) ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₂ j₁))) x) *
      (ConcreteCategory.hom (F.map α)) ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₂ j₁))) y) =
    (ConcreteCategory.hom (F.map γ)) ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₂ j₃))) x) *
      (ConcreteCategory.hom (F.map γ)) ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₂ j₃))) y')

Tactic:
← comp_apply,

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₂ j₁) ≫ F.map α)) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₂ j₁) ≫ F.map α)) y =
    (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₂ j₃) ≫ F.map γ)) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₂ j₃) ≫ F.map γ)) y'
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
c : Cone F
hc : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone c)
this : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
⊢ IsLimit c

Tactic:
have : Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R))) := by
      simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using! this

Goal state after:
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
c : Cone F
hc : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone c)
this✝ : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
this : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
⊢ IsLimit c
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
⊢ IsLimit (limitCone F)

Tactic:
by
  refine
    IsLimit.ofFaithful (forget (AlgCat R)) (Types.Small.limitConeIsLimit.{v, w} _)
      (fun s => ofHom
        { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_,
          commutes' := ?_ })
      (fun s => rfl)
  · congr
    ext j
    simp
  · intro x y
    ext j
    simp
    rfl
  · ext j
    simp
    rfl
  · intro x y
    ext j
    simp
    rfl
  · intro r
    simp only [Equiv.algebraMap_def, Equiv.symm_symm]
    apply congrArg
    apply Subtype.ext
    ext j
    exact (s.π.app j).hom.commutes r

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : Y ≅ Z
⊢ X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (X ⊗ Z)

Tactic:
by
  rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

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

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
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ ε (𝟭 C) ≫ adj.unit.app (𝟙_ C) = ε (F ⋙ G)

Tactic:
by
    dsimp
    rw [id_comp, ← unit_app_unit_comp_map_η adj, assoc, Monoidal.map_η_ε]
    dsimp
    rw [comp_id]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ (((α_ (unop W) (unop X) (unop Y)).symm.op.hom.unop ▷ unop Z).op ≫
        (α_ (unop W) (unop (op (unop X ⊗ unop Y))) (unop Z)).symm.op.hom ≫
          (unop W ◁ (α_ (unop X) (unop Y) (unop Z)).symm.op.hom.unop).op).unop =
    ((α_ (unop (op (unop W ⊗ unop X))) (unop Y) (unop Z)).symm.op.hom ≫
        (α_ (unop W) (unop X) (unop (op (unop Y ⊗ unop Z)))).symm.op.hom).unop

Tactic:
dsimp; monoidal_coherence

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ ((α_ (unop X) (unop (op (𝟙_ C))) (unop Y)).symm.op.hom ≫ (unop X ◁ (λ_ (unop Y)).symm.op.hom.unop).op).unop =
    ((ρ_ (unop X)).symm.op.hom.unop ▷ unop Y).op.unop

Tactic:
dsimp; monoidal_coherence

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ ((Z.unmop ◁ (α_ Y.unmop X.unmop W.unmop).symm.mop.hom.unmop).mop ≫
        (α_ Z.unmop { unmop := Y.unmop ⊗ X.unmop }.unmop W.unmop).symm.mop.hom ≫
          ((α_ Z.unmop Y.unmop X.unmop).symm.mop.hom.unmop ▷ W.unmop).mop).unmop =
    ((α_ Z.unmop Y.unmop { unmop := X.unmop ⊗ W.unmop }.unmop).symm.mop.hom ≫
        (α_ { unmop := Z.unmop ⊗ Y.unmop }.unmop X.unmop W.unmop).symm.mop.hom).unmop

Tactic:
dsimp; monoidal_coherence

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᴹᵒᵖ
⊢ ((α_ Y.unmop { unmop := 𝟙_ C }.unmop X.unmop).symm.mop.hom ≫ ((ρ_ Y.unmop).mop.hom.unmop ▷ X.unmop).mop).unmop =
    (Y.unmop ◁ (λ_ X.unmop).mop.hom.unmop).mop.unmop

Tactic:
dsimp; monoidal_coherence

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ ε (mopMopEquivalence C).inverse =
    (mopMopEquivalence C).toAdjunction.unit.app (𝟙_ Cᴹᵒᵖᴹᵒᵖ) ≫
      (mopMopEquivalence C).inverse.map (η (mopMopEquivalence C).functor)

Tactic:
simp [ε, η, mopMopEquivalence, Equivalence.trans, unmopEquiv, ε]

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
⊢ η F = η F

Tactic:
rw [← cancel_epi (ε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 = (εIso F).hom ≫ η F
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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ ε F = ε F

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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ μ F = μ F

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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ η F = η F

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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ δ F = δ F

Tactic:
· rw [← cancel_mono (εIso _).inv]
    rw [εIso_inv, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_inv]
    exact congr(_ ≫ ($eq.symm).η)

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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ μ F = μ F

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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ η F = η F

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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ δ F = δ F
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case leftAdjoint_μ
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
this : G.LaxMonoidal := ⋯
⊢ autoParam
    (∀ (X Y : D),
      μ G X Y =
        adj.unit.app (G.obj X ⊗ G.obj Y) ≫ G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)))
    IsMonoidal.leftAdjoint_μ._autoParam

Tactic:
· intro _ _
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsLimit c.unop → IsColimit c

Tactic:
· intro h
    exact (IsColimit.equivIsoColimit c.unopOpIso).toFun
      ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv walkingCospanOpEquiv.symm).toFun h.op))

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
F : C ⥤ D
⊢ Function.Injective (@toMonoidal C inst✝⁵ inst✝⁴ inst✝³ D inst✝² inst✝¹ inst✝ F)

Tactic:
by rintro ⟨⟩ ⟨⟩ rfl; rfl

Goal state after:
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)) (j : Discrete ι),
    (finsuppCocone R M ι).ι.app j ≫ ↟((Finsupp.lsum R) fun i ↦ Hom.hom (s.ι.app { as := i })) = s.ι.app j

Tactic:
aesop (add simp finsuppCocone)

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ (Hom.hom f).range ≤ (Hom.hom (cokernel.π f)).ker

Tactic:
by
      rintro _ ⟨x, rfl⟩
      exact cokernel.condition_apply f x

Goal state after:
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
x y : M
⊢ (mapGen ⇑f) (f x) (f y) ↔ c x y

Tactic:
rw [mapGen_eq_map_of_surjective f h hf, Relation.map_apply]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
x y : M
⊢ (∃ a b, c a b ∧ f a = f x ∧ f b = f y) ↔ c x y
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N →+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ (c.comapQuotientEquivRangeS f hcd).symm ⟨↑(f x), ⋯⟩ = ↑x

Tactic:
by
  simp [RingEquiv.symm_apply_eq]

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

Goal state before:
pp: case hl
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
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul x))

Tactic:
← comp_apply,

Goal state after:
case hl
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
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
            ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
          TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
        x) =
    (lTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
        TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
      x