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

Goal state before:
pp: n : ℕ
⊢ (swap 0 1).signAux = ∏ x ∈ {⟨1, 0⟩}, if (swap 0 1) x.fst ≤ (swap 0 1) x.snd then -1 else 1

Tactic:
refine Eq.symm (prod_subset (fun ⟨x₁, x₂⟩ => by
      simp +contextual [mem_finPairsLT]) fun a ha₁ ha₂ => ?_)
    rcases a with ⟨a₁, a₂⟩
    replace ha₁ : a₂ < a₁ := mem_finPairsLT.1 ha₁
    dsimp only
    rcases a₁.zero_le.eq_or_lt with (rfl | H)
    · exact absurd a₂.zero_le ha₁.not_ge
    rcases a₂.zero_le.eq_or_lt with (rfl | H')
    · simp only [and_true, heq_iff_eq, mem_singleton, Sigma.mk.inj_iff] at ha₂
      have : 1 < a₁ := lt_of_le_of_ne' (Nat.succ_le_of_lt ha₁) ha₂
      have h01 : Equiv.swap (0 : Fin (n + 2)) 1 0 = 1 := by simp
      rw [swap_apply_of_ne_of_ne (ne_of_gt H) ha₂, h01, if_neg this.not_ge]
    · have le : 1 ≤ a₂ := Nat.succ_le_of_lt H'
      have lt : 1 < a₁ := le.trans_lt ha₁
      have h01 : Equiv.swap (0 : Fin (n + 2)) 1 1 = 0 := by simp only [swap_apply_right]
      rcases le.eq_or_lt with (rfl | lt')
      · rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_ge]
      · rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
          swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_ge]

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
⊢ orderOf f = #f.support

Tactic:
by
  rw [← Fintype.card_zpowers, ← Fintype.card_coe]
  convert! Fintype.card_congr (IsCycle.zpowersEquivSupport hf)

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

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : ¬f z = z
⊢ (f ^ n) z = 1 z

Tactic:
obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)

Goal state after:
case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ n) z = 1 z
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝ : DecidableEq ι
i : ι
y : N i
j : ι
hj : j ≠ i ∧ j ∈ Finset.univ
⊢ (ϕ j) (Pi.mulSingle i y j) = 1

Tactic:
simp [hj]

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

Goal state before:
pp: α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
x : α
hx : x ∈ {x | hs'.toFinset.toList.formPerm x ≠ x}
⊢ x ∈ s

Tactic:
simpa using List.mem_of_formPerm_apply_ne hx

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℕ
⊢ (f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x

Tactic:
convert! cycleOf_apply_apply_zpow_self f x k using 1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
n : ℕ
hn : n ∈ σ.cycleType
⊢ 2 ∣ n

Tactic:
_root_.le_antisymm
          (Nat.le_of_dvd zero_lt_two <|
            (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
          (two_le_of_mem_cycleType hn)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
n : ℕ
hn : n ∈ σ.cycleType
⊢ 2 ∣ 2
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ ↑(j + 1).castSucc < ↑i.succ

Tactic:
simpa [this] using hlt

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

Goal state before:
pp: case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ.succAbove j = (swap 0 i.succ) j.succ

Tactic:
Fin.succAbove_of_le_castSucc,

Goal state after:
case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ = (swap 0 i.succ) j.succ

case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, σ a = a

Tactic:
contrapose! hα
    simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
    exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
      (card_compl_support_modEq hσ).symm)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑(vectorsProdEqOne G 0)

Tactic:
zero_eq

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑{Vector.nil}
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
⊢ ↑((i.cycleIcc i) k) = ↑k

Tactic:
rcases lt_trichotomy k i with ch | ch | ch

Goal state after:
case inl
n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
ch : k < i
⊢ ↑((i.cycleIcc i) k) = ↑k

case inr.inl
n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
ch : k = i
⊢ ↑((i.cycleIcc i) k) = ↑k

case inr.inr
n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
ch : i < k
⊢ ↑((i.cycleIcc i) k) = ↑k
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
⊢ ∃ x, orderOf x = p

Tactic:
have := Fintype.ofFinite G
  rw [Nat.card_eq_fintype_card] at hdvd
  exact exists_prime_orderOf_dvd_card p hdvd

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ ∀ x ∈ g.cycleFactorsFinset, Commute k (id x)

Tactic:
simpa only [id_eq] using hk

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N✝ : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N✝ p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N✝ p)
N : Type u_1
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
⊢ (LinearMap.pi fun p ↦ compLinearMapₗ fun i ↦ DFinsupp.lsingle (p i)) ∘ₗ
      LinearMap.compMultilinearMapₗ R ((DFinsupp.lsum ℕ) fun x ↦ LinearMap.id) ∘ₗ dfinsuppFamilyₗ =
    LinearMap.id

Tactic:
by ext f p a; simp

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

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
e₁ e₂ : m ≃ n
h : A.IsDetpBalanced a b
⊢ a * detp (1 * sign (e₁.symm.trans e₂)) A + b * detp (-1 * sign (e₁.symm.trans e₂)) A =
    b * detp (1 * sign (e₁.symm.trans e₂)) A + a * detp (-1 * sign (e₁.symm.trans e₂)) A

Tactic:
apply h.mul_add_mul_eq

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
⊢ detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
let bij : Finset (n → n) := (disjUnion (ofSign 1) (ofSign (-1)) ofSign_disjoint).map ι

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
h : ∀ {s t : ℤˣ}, detp s A * detp t B = ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
⊢ detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
⊢ X.as = { as := PUnit.unit }.as

Tactic:
by trivial

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ Y.as = { as := PUnit.unit }.as

Tactic:
by trivial

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
σ : n → n
hσ✝ : ¬Function.Injective σ
i j : n
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j) k) = σ k
⊢ ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) = ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i)

Tactic:
← mul_neg_one,

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
σ : n → n
hσ✝ : ¬Function.Injective σ
i j : n
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j) k) = σ k
⊢ ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) = ∑ τ ∈ ofSign (1 * -1), ∏ i, A i (σ i) * B (σ i) (τ i)
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
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
x : n
hx : x ∈ univ
σ : Perm n
hσ : σ ∈ {i_1 ∈ ofSign s | i_1 i = x}
⊢ A i x * ∏ k ∈ {i}ᶜ, A k (σ k) = ∏ k, A k (σ k)

Tactic:
rw [← prod_mul_prod_compl ({i} : Finset n), prod_singleton, (mem_filter.mp hσ).2]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ Y : Discrete PUnit.{u_1 + 1}
⊢ { as := PUnit.unit }.as = x✝.as

Tactic:
by trivial

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ { as := PUnit.unit }.as = X.as

Tactic:
by trivial

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 : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι'
m : (i : ι') → M₁ (σ.symm i)
i : ι'
⊢ ∀ (x y : M₁ (σ.symm i)),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i x) + (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m i y)

Tactic:
by
        let := σ.decidableEq
        rw [← σ.apply_symm_apply i]
        intro x y
        simp only [comp_apply, piCongrLeft'_symm_update, f.map_update_add]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
h : ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel x y
⊢ colimitInvAux F x = colimitInvAux F y

Tactic:
apply colimitInvAux_eq_of_rel

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x✝ : ↑(G F)
x y : (j : J) × ↑(F.obj j)
h : ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel x y
⊢ Types.FilteredColimit.Rel (F ⋙ forget GrpCat) x y
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
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * ↑(sign σ)) • ∏ i', A ((decomposeFin.symm (i.succ, σ)) i') i' =
    (-1 * ↑(sign σ)) • (A i.succ 0 * ∏ i', A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ)

Tactic:
simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
        Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ ((colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f) ≫ (colimitObjIsoColimitCompEvaluation F j).hom =
    colimMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
← Iso.eq_comp_inv,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv
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:
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)

Goal state after:
case refine_1
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
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) 1, ⋯⟩ =
    1

case refine_2
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
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩

case refine_3
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
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) 0, ⋯⟩ =
    0

case refine_4
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
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩

case refine_5
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
s : Cone F
⊢ ∀ (r : R),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) ((algebraMap R ↑s.1) r), ⋯⟩ =
      (algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) r
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).hom = ∑ j, biproduct.π f j ▷ X ≫ biproduct.ι (fun j ↦ f j ⊗ X) j

Tactic:
ext
  dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
  erw [biproduct.lift_π]
  simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]

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.LaxMonoidal
X Y Z : C
⊢ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom

Tactic:
by
  rw [associativity, Iso.inv_hom_id_assoc]

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.OplaxMonoidal
X : C
⊢ (δ F (𝟙_ C) X ≫ η F ▷ F.obj X) ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom

Tactic:
← Iso.eq_comp_inv,

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X = F.map (λ_ X).hom ≫ (λ_ (F.obj X)).inv
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.OplaxMonoidal
X : C
⊢ (δ F X (𝟙_ C) ≫ F.obj X ◁ η F) ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom

Tactic:
← Iso.eq_comp_inv,

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F = F.map (ρ_ X).hom ≫ (ρ_ (F.obj X)).inv
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
x : ↑Y✝
y : ↑X✝
⊢ (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom (0 ▷ X✝))) x) y =
    (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom 0)) x) y

Tactic:
simp [ModuleCat.hom_whiskerRight]

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

Goal state before:
pp: case refine_4
R : Type u
inst✝ : CommRing R
X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : Y✝ ⟶ Z✝
x : ↑Y✝
y : ↑X✝
⊢ (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom ((f✝ + g✝) ▷ X✝))) x) y =
    (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom (f✝ ▷ X✝ + g✝ ▷ X✝))) x) y

Tactic:
simp [ModuleCat.hom_whiskerRight]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
r✝ : R
Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
X✝ : ModuleCat R
x : ↑Y✝
y : ↑X✝
⊢ (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom ((r✝ • f✝) ▷ X✝))) x) y =
    (((TensorProduct.mk R ↑Y✝ ↑X✝).compr₂ₛₗ (Hom.hom (r✝ • f✝ ▷ X✝))) x) y

Tactic:
simp [ModuleCat.hom_whiskerRight]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
f₁ f₂ f₃ f₄ : C
α α' : f₁ ⟶ f₂
η η' : f₂ ⟶ f₃
ηs ηs' : f₃ ⟶ f₄
e_α : α = α'
e_η : η = η'
e_ηs : ηs = ηs'
⊢ α ≫ η ≫ ηs = α' ≫ η' ≫ ηs'

Tactic:
by
  simp [e_α, e_η, e_ηs]

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) = (μIso F X Y).inv

Tactic:
← CategoryTheory.IsIso.inv_eq_inv

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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
⊢ CategoryTheory.inv (CategoryTheory.inv (μ F X Y)) = CategoryTheory.inv (μIso F X Y).inv
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
⊢ Function.Injective (@toOplaxMonoidal C inst✝³ inst✝² D inst✝¹ inst✝ F)

Tactic:
intro a b eq
  ext1
  · rw [← cancel_mono (εIso _).inv]
    rw [εIso_inv, ε_η, ← @ε_η _ _ _ _ _ _ _ a, ← εIso_inv]
    exact congr(_ ≫ ($eq.symm).η)
  · ext
    rw [← cancel_mono (μIso F _ _).inv]
    rw [μIso_inv, μ_δ, ← @μ_δ _ _ _ _ _ _ _ a, ← μIso_inv]
    exact congr(_ ≫ ($eq.symm).δ _ _)
  · exact congr(($eq).η)
  · exact congr(($eq).δ)

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)) ((ι (F ⋙ uliftFunctor) j) { down := a }) =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)

Tactic:
erw [Quot.ι_desc]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((uliftFunctor.mapCocone c).ι.app j)) { down := a } =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)
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₂
c : C
⊢ G.map (adj₁.unit.app c) ≫ α.app (L₁.obj c) =
    adj₂.unit.app (G.obj ((𝟭 C).obj c)) ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app ((𝟭 C).obj c))

Tactic:
by
  conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]
  exact (unit_mateEquiv adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) c)

Goal state after: