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

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x a : α
ha : a ∈ ↑(f.cycleOf x).support
b : α
hb : b ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle a b

Tactic:
mem_coe,

Goal state after:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x a : α
ha : a ∈ (f.cycleOf x).support
b : α
hb : b ∈ (f.cycleOf x).support
⊢ f.SameCycle a b
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
· rw [← cycleOf_eq_one_iff] at hx
    simp [hx]

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ (f ^ 1) x = y

Tactic:
obtain ⟨k, rfl⟩ := h

Goal state after:
case neg
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : x ∉ f.support
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
⊢ r + ↑(#g.support) * q = n ∧ 0 ≤ r ∧ r < ↑(#g.support)

Tactic:
rw [← Int.ediv_emod_unique _]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
⊢ n / ↑(#g.support) = q ∧ n % ↑(#g.support) = r

α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
⊢ 0 < ↑(#g.support)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case neg
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑i + 1 + 1 = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Tactic:
Function.Injective.map_swap Fin.val_injective,

Goal state after:
case neg
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑i + 1 + 1 = (swap ↑0 ↑1) ↑((finRotate (n✝ + 1)) i).succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case zero
i j : Fin 0
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

pp: case succ
n✝ : ℕ
i j : Fin (n✝ + 1)
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
· rcases j with ⟨_, ⟨⟩⟩

Goal state after:
case succ
n✝ : ℕ
i j : Fin (n✝ + 1)
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inr.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ 0 < i.succ

Tactic:
apply Fin.succ_pos

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

Goal state before:
pp: n : ℕ
i : Fin n
inst✝ : NeZero n
h0 : i ≠ 0
⊢ i.cycleRange.IsCycle

Tactic:
obtain ⟨i, hi⟩ := i
  cases i
  · exact (h0 rfl).elim
  exact isCycle_finRotate.extendDomain _

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

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
⊢ (i.cycleIcc j) k = k

Tactic:
have kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i)) := by
      simp [range_natAdd_castLEEmb]; lia
    have : (((addNatEmb (n - (n - i.1))).trans (finCongr _).toEmbedding).toEquivRange.symm ⟨k, kin⟩)
      = subNat i.1 (k.cast (by lia)) (by simp; lia) := by
      simpa [symm_apply_eq] using eq_of_val_eq (by simp; lia)
    simp only [cycleIcc_to_cycleRange hij kin, natAdd_castLEEmb, this,
      Function.Embedding.trans_apply, addNatEmb_apply, coe_toEmbedding, finCongr_apply]
    rw [cycleRange_of_gt]
    · exact eq_of_val_eq (by simp; lia)
    · exact lt_def.mpr (by simp [sub_val_of_le hij]; lia)

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

Goal state before:
pp: case neg
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
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) ⋯
ch : ¬k = j
this : subNat (↑i) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯ + 1).addNat (n - (n - ↑i)))) = ↑(k + 1)

Tactic:
subNat

Goal state after:
case neg
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
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) ⋯
ch : ¬k = j
this : subNat (↑i) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ ↑(Fin.cast ⋯ ((⟨↑(Fin.cast ⋯ k) - ↑i, ⋯⟩ + 1).addNat (n - (n - ↑i)))) = ↑(k + 1)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
⊢ ⇑(i.cycleIcc j) ∘ j.succAbove = i.succAbove

Tactic:
by
  grind [cycleIcc_of_lt, succAbove_of_castSucc_lt, cycleIcc_of_ge_of_lt,
    succAbove_of_le_castSucc, coeSucc_eq_succ, cycleIcc_of_gt]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.partition = τ.partition

Tactic:
rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]

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 : Matrix n n R
inst✝ : IsEmpty n
⊢ detp (-1) A = 0

Tactic:
rw [detp, ofSign, univ_unique]
  convert sum_empty
  simp +decide

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x ↦ M) N'
v : ι → M
⊢ (alternatization m) v = ∑ σ, Perm.sign σ • (domDomCongr σ m) v

Tactic:
simp only [alternatization_def, smul_apply, sum_apply]

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 : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
s t : ℤˣ
this : detp 1 A = detp (-1) A
⊢ detp s A = detp t A

Tactic:
obtain rfl | rfl := Int.units_eq_one_or s <;>
  obtain rfl | rfl := Int.units_eq_one_or t <;>
  first | rfl | rw [this]

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
A : (i : ι) → Finset (α i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
n : ℕ
h : ∑ i, #(A i) = n
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
let := fun i => Classical.decEq (α i)

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
A : (i : ι) → Finset (α i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
n : ℕ
h : ∑ i, #(A i) = n
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
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
σ : Perm n
M : Matrix n n R
⊢ (M.submatrix id ⇑σ)ᵀ.det = ↑↑(sign σ) * M.det

Tactic:
transpose_submatrix,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
σ : Perm n
M : Matrix n n R
⊢ (Mᵀ.submatrix (⇑σ) id).det = ↑↑(sign σ) * M.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
⊢ |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|

Tactic:
have hee : e₂ = e₁.trans (e₁.symm.trans e₂) := by ext; simp

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Surjective (F.descColimitType c) → ∀ (z : c.pt), ∃ i x, c.ι i x = z

pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (z : c.pt), ∃ i x, c.ι i x = z) → Function.Surjective (F.descColimitType c)

Tactic:
· intro h z
    obtain ⟨⟨i, x⟩, rfl⟩ := h z
    exact ⟨i, x, rfl⟩

Goal state after:
case mpr
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (z : c.pt), ∃ i x, c.ι i x = z) → Function.Surjective (F.descColimitType c)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσ : σ ∈ ↑(↑(sumCongrHom m n).range).toFinset
⊢ σ ∈ (fun σ ↦ σ.1.sumCongr σ.2) '' ↑univ

Tactic:
mem_coe,

Goal state after:
case e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσ : σ ∈ (↑(sumCongrHom m n).range).toFinset
⊢ σ ∈ (fun σ ↦ σ.1.sumCongr σ.2) '' ↑univ
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ (↑i + ↑j) * A i j * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
    (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
transpose_submatrix,

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ (↑i + ↑j) * A i j * (Aᵀᵀ.submatrix i.succAbove j.succAbove).det =
    (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (c.π.app (Opposite.op 0)))

Tactic:
rw [this, types_comp]

Goal state after:
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective (⇑(ConcreteCategory.hom ((limitCone F).π.app (Opposite.op 0))) ∘ ⇑(ConcreteCategory.hom i.hom))
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : j < i
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j

pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j

Tactic:
· rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]

Goal state after:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
x✝ : ↑(R F)
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ (descMonoidHom t) (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩) =
    (descAddMonoidHom t) (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j, x⟩)

Tactic:
rw [descMonoidHom_quotMk t x, descAddMonoidHom_quotMk t x]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
⊢ let ff := fun a ↦ (ConcreteCategory.hom (D.ι.app a.fst)) a.snd;
  Function.Surjective ff

Tactic:
intro ff x
  let E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
  let hE : IsColimit E := isColimitOfPreserves (forget C) hD
  obtain ⟨j, y, hy⟩ := Types.jointly_surjective_of_isColimit hE x
  exact ⟨⟨j, y⟩, hy⟩

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ MonCat
a b : (j : J) → ↑(F.obj j)
ah : a ∈ (F ⋙ forget MonCat).sections
bh : b ∈ (F ⋙ forget MonCat).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget MonCat).map f)) ((a * b) j) = (a * b) j'

Tactic:
by simp [← ah f, ← bh f]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone F
hc : IsLimit c
⊢ IsLimit ((forget₂ CommGrpCat GrpCat).mapCone c)

Tactic:
by
    have : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat) := by
      rw [GrpCat.hasLimit_iff_small_sections]
      change Small.{u} (F ⋙ forget CommGrpCat).sections
      rw [← CommGrpCat.hasLimit_iff_small_sections]
      exact ⟨_, hc⟩
    exact isLimitOfPreserves _ hc

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M₁ M₂ M₃ M₄ : SemimoduleCat R
f g : M₁ ⊗ M₂ ⊗ M₃ ⟶ M₄
h :
  ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
    (ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) = (ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))
⊢ (α_ M₁ M₂ M₃).hom ≫ f = (α_ M₁ M₂ M₃).hom ≫ g

Tactic:
exact tensor_ext₃' h

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : M₁ ⊗ M₂ ⊗ M₃ ⟶ M₄
h :
  ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
    (ConcreteCategory.hom f) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) = (ConcreteCategory.hom g) (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃))
⊢ (α_ M₁ M₂ M₃).hom ≫ f = (α_ M₁ M₂ M₃).hom ≫ g

Tactic:
exact tensor_ext₃' h

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
⊢ CategoryTheory.inv (δ F X Y) = μ F X Y

Tactic:
by simp [← inv_μ]

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
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝

Tactic:
rw [← cancel_epi (μIso F _ _).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
x✝¹ x✝ : C
⊢ (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝ = (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝
Module: Mathlib.Algebra.Category.ModuleCat.EpiMono

Goal state before:
pp: R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi ((forget (ModuleCat R)).map f)

Tactic:
CategoryTheory.ofHom_epi_iff_surjective,

Goal state after:
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)
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₂ Y₁ Y₂ : C
⊢ tensorμ X₁ X₂ Y₁ Y₂ ≫ tensorδ X₁ X₂ Y₁ Y₂ = 𝟙 ((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂)

Tactic:
by
  simp only [tensorμ, ← whiskerLeft_comp_assoc, tensorδ, assoc, Iso.inv_hom_id_assoc,
    Iso.hom_inv_id_assoc, hom_inv_whiskerRight_assoc, Iso.inv_hom_id, whiskerLeft_id, id_comp,
    Iso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ (α.natTrans.app X✝ ≫ (L₁ ⋙ H).map (adj₁.unit.app X✝)) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) = α.natTrans.app X✝

Tactic:
Functor.comp_map,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ (α.natTrans.app X✝ ≫ H.map (L₁.map (adj₁.unit.app X✝))) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) = α.natTrans.app X✝
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X✝ : D
⊢ (G.map (adj₁.unit.app (R₁.obj X✝)) ≫ (R₁ ⋙ G).map (adj₁.counit.app X✝)) ≫ β.natTrans.app X✝ = β.natTrans.app X✝

Tactic:
Functor.comp_map,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X✝ : D
⊢ (G.map (adj₁.unit.app (R₁.obj X✝)) ≫ G.map (R₁.map (adj₁.counit.app X✝))) ≫ β.natTrans.app X✝ = β.natTrans.app X✝
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
          R₃.map (H₂.map (L₂.map (R₂.map (α.natTrans.app (R₁.obj b))))) ≫
            R₃.map (H₂.map (adj₂.counit.app (H₁.obj (L₁.obj (R₁.obj b))))) ≫
              R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))

Tactic:
slice_rhs 4 5 =>
    rw [← R₃.map_comp, ← H₂.map_comp, ← Functor.comp_map _ L₂, adj₂.counit.naturality]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (L₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))))) ≫
          R₃.map (H₂.map (adj₂.counit.app (L₂.obj (G₁.obj (R₁.obj b))) ≫ (𝟭 D).map (α.natTrans.app (R₁.obj b)))) ≫
            R₃.map (H₂.map (H₁.map (adj₁.counit.app b)))
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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ (lift R) (g.toLinearMap ∘ₗ ι R) = g

Tactic:
rw [← lift_symm_apply]
  exact (lift R).apply_symm_apply g

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 : M
r : R
⊢ (ι R) x = (algebraMap R (TensorAlgebra R M)) r ↔ x = 0 ∧ r = 0

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · let : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
    have : IsCentralScalar R M := ⟨fun r m => rfl⟩
    have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := lift_ι_apply _ _
    rw [h, AlgHom.commutes] at hf0
    have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
    exact this.symm.imp_left Eq.symm
  · rintro ⟨rfl, rfl⟩
    rw [map_zero, map_zero]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : DivisionSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝ : Invertible x
⊢ ⅟x = x⁻¹

Tactic:
by
  let := invertibleFstOfInvertible x
  ext <;> simp [fst_invOf, snd_invOf]

Goal state after: