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

Goal state before:
pp: case pos
α : 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)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : m = 0
⊢ g ^ m = 1 ↔ m = 0

pp: case neg
α : 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)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : ¬m = 0
⊢ g ^ m = 1 ↔ m = 0

Tactic:
· simp only [hm0, pow_zero]

Goal state after:
case neg
α : 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)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : ¬m = 0
⊢ g ^ m = 1 ↔ m = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
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 := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (↑↑v).length g
⊢ g ^ p = 1

pp: case refine_2
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 := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (↑↑v).length g
hg' : g = 1
⊢ v = v₀

Tactic:
· rw [← List.prod_replicate, ← v.1.2, ← hg, show v.val.val.prod = 1 from v.2]

Goal state after:
case refine_2
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 := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (↑↑v).length g
hg' : g = 1
⊢ v = v₀
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr.inr.inr
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
⊢ ↑((i.cycleIcc j) (if x = k then j else x + 1)) = ↑(if x = k then i else x + 1)

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : x = k
⊢ ↑((i.cycleIcc j) j) = ↑i

case neg
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : ¬x = k
⊢ ↑((i.cycleIcc j) (x + 1)) = ↑(x + 1)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
hy : y ∈ Subgroup.zpowers ↑d
m : ℤ
hm : (fun x ↦ ↑c ^ x) m = x
⊢ x.Disjoint y

Tactic:
obtain ⟨n, hn⟩ := hy

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x ↦ ↑c ^ x) m = x
n : ℤ
hn : (fun x ↦ ↑d ^ x) n = y
⊢ x.Disjoint y
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
⊢ ∏ x ∈ D, f (σ x.snd) (σ x.fst) =
    ∏ x ∈ D,
      ↑↑(if
                σ⁻¹ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩.snd <
                  σ⁻¹ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩.fst then
              1
            else -1) *
        f ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩.snd ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩.fst

Tactic:
refine Finset.prod_congr rfl fun ⟨x₁, x₂⟩ hx ↦ ?_

Goal state after:
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : ⟨x₁, x₂⟩ ∈ D
⊢ f (σ ⟨x₁, x₂⟩.snd) (σ ⟨x₁, x₂⟩.fst) =
    ↑↑(if
              σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd <
                σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst then
            1
          else -1) *
      f ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd
        ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
⊢ (∀ a ∈ c.support, c a = g a) → ∀ a ∈ (k * c * k⁻¹).support, (k * c * k⁻¹) a = (k * g * k⁻¹) a

Tactic:
intro hc

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ k✝ c✝ g k c : Perm α
hc : ∀ a ∈ c.support, c a = g a
⊢ ∀ a ∈ (k * c * k⁻¹).support, (k * c * k⁻¹) a = (k * g * k⁻¹) a
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✝⁴ : Semiring 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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
s : (i : ι) → { s // ∀ (i_1 : κ i), i_1 ∈ s ∨ (x i).toFun i_1 = 0 }
p : (i : ι) → κ i
h : ((f p) fun i ↦ (x i) (p i)) ≠ 0
i : ι
⊢ ¬(x i).toFun ((fun i x ↦ p i) i ⋯) = 0

Tactic:
exact mt ((f p).map_coord_zero (m := fun i => x i _) i) h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ g.cycleFactorsFinset →
    (Commute z c ↔
      ∃ (hc : ∀ (x : α), z x ∈ c.support ↔ x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c)

Tactic:
intro hc

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute z c ↔ ∃ (hc : ∀ (x : α), z x ∈ c.support ↔ x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c
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:
ext f p a; simp

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
s : ℤˣ
A : Matrix n n R
c : R
⊢ detp s (c • A) = c ^ Fintype.card n * detp s A

Tactic:
by
  simp [detp, Finset.mul_sum, Finset.prod_mul_distrib]

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
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)

Goal state after:
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 with i i ∈ univ, ∏ k, A k (i k)
⊢ (A * adjp s A) i i = detp s A
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 : ι) → 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
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this✝¹ : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
this✝ : A i₀ = B i₀ ∪ C i₀
j : α i₀
hj : j ∈ C i₀
this : j = j₂
⊢ j₂ ∉ B i₀

Tactic:
simp only [B, Finset.mem_sdiff, not_true, not_false_iff, Finset.mem_singleton,
        update_self, and_false]

Goal state after:
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
A : Matrix n n R
c : R
⊢ (c • A).det = ((diagonal fun x ↦ c) * A).det

Tactic:
smul_eq_diagonal_mul

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
c : R
⊢ ((diagonal fun x ↦ c) * A).det = ((diagonal fun x ↦ c) * A).det
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
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ A.det = 0

Tactic:
rw [← det_transpose]
  exact det_eq_zero_of_row_eq_zero j h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsCofilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ (h.homEquiv (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ f =
    (h.homEquiv (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ g

Tactic:
rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (IsFiltered.coeqHom f.unop g.unop).op ≫ f = (IsFiltered.coeqHom f.unop g.unop).op ≫ g

Tactic:
by
      rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
      congr 1
      exact IsFiltered.coeq_condition f.unop g.unop

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

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
⊢ c.IsColimit → Nonempty (Limits.IsColimit (F.coconeTypesEquiv c))

Tactic:
intro hc

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : c.IsColimit
⊢ Nonempty (Limits.IsColimit (F.coconeTypesEquiv c))
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case inl
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
z : (i : ι) → M₁ i
i : ↑s
⊢ update m (e.symm i) z (e.symm i) ↑i = update (fun j ↦ m (e.symm j) ↑j) (e (e.symm i)) (z ↑(e (e.symm i))) i

Tactic:
rw [Equiv.apply_symm_apply e i, update_self, update_self]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift

Goal state before:
pp: J✝ : Type u_1
inst✝ : Category.{v_1, u_1} J✝
K : J✝ ⥤ Type u
c✝ : Cocone K
hc✝ : IsColimit c✝
lc : Cocone (K ⋙ uliftFunctor.{v, u})
J : Type w
x✝ : Category.{w', w} J
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
⊢ Nonempty (IsColimit (uliftFunctor.{v, u}.mapCocone c))

Tactic:
rw [isColimit_iff_coconeTypesIsColimit]

Goal state after:
J✝ : Type u_1
inst✝ : Category.{v_1, u_1} J✝
K : J✝ ⥤ Type u
c✝ : Cocone K
hc✝ : IsColimit c✝
lc : Cocone (K ⋙ uliftFunctor.{v, u})
J : Type w
x✝ : Category.{w', w} J
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
⊢ ((F ⋙ uliftFunctor.{v, u}).coconeTypesEquiv.symm (uliftFunctor.{v, u}.mapCocone c)).IsColimit
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso ((Cone.functoriality K F).map f)

Tactic:
rw [this]
          infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this✝ : (Cone.functoriality K F).map f = i.inv
this : IsIso ((Cone.functoriality K F).map f)
⊢ IsLimit d

Tactic:
haveI : IsIso f := isIso_of_reflects_iso f (Cone.functoriality K F)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this✝¹ : (Cone.functoriality K F).map f = i.inv
this✝ : IsIso ((Cone.functoriality K F).map f)
this : IsIso f
⊢ IsLimit d
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso ((Cocone.functoriality K F).map f)

Tactic:
rw [this]
          infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesLimitsOfShape J F
K : J' ⥤ C
c : Cone (K ⋙ F)
hc : IsLimit c
⊢ LiftableCone K F c

Tactic:
refine ⟨(Cone.whiskeringEquivalence e).inverse.obj
          (liftLimit (hc.whiskerEquivalence e)), ?_⟩

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ : J ⥤ C
J' : Type w₁
inst✝¹ : Category.{w'₁, w₁} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : CreatesLimitsOfShape J F
K : J' ⥤ C
c : Cone (K ⋙ F)
hc : IsLimit c
⊢ F.mapCone ((Cone.whiskeringEquivalence e).inverse.obj (liftLimit (hc.whiskerEquivalence e))) ≅ c
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
s : P.obj (op X)
Y : C
f : Y ⟶ X
⊢ (ConcreteCategory.hom ((shrinkYonedaEquiv.symm s).app (op Y))) (shrinkYonedaObjObjEquiv.symm f) =
    (ConcreteCategory.hom (P.map f.op)) s

Tactic:
by
  obtain ⟨g, rfl⟩ := shrinkYonedaEquiv.surjective s
  simp [map_shrinkYonedaEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (shrinkCoyonedaObjObjEquiv (shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f))).op = f

Tactic:
by
    simp [shrinkCoyonedaEquiv_shrinkCoyoneda_map f]

Goal state after:
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
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
i : ι
x✝ : ↑(of R (G i))
⊢ (Hom.hom (↟(f i i ⋯))) x✝ = (Hom.hom (𝟙 (of R (G i)))) x✝

Tactic:
apply Module.DirectedSystem.map_self

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ofHom (Hom.hom f).ker.subtype ≫ f = 0

Tactic:
ext x; exact x.2

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 : C
⊢ X ◁ (α_ Y (𝟙_ C) (𝟙_ C)).inv ≫ X ◁ (ρ_ Y).hom ▷ 𝟙_ C ≫ (α_ X Y (𝟙_ C)).inv =
    (α_ X Y (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (X ⊗ Y) ◁ (λ_ (𝟙_ C)).hom

Tactic:
← whiskerLeft_comp_assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ ((α_ Y (𝟙_ C) (𝟙_ C)).inv ≫ (ρ_ Y).hom ▷ 𝟙_ C) ≫ (α_ X Y (𝟙_ C)).inv =
    (α_ X Y (𝟙_ C ⊗ 𝟙_ C)).inv ≫ (X ⊗ Y) ◁ (λ_ (𝟙_ C)).hom
Module: Mathlib.CategoryTheory.Monoidal.Category

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

Tactic:
rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
      cancel_epi (X ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
      associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
      associator_inv_naturality_right]

Goal state after:
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
X : C
f : J → C
j✝ : J
⊢ { pt := X ⊗ (biproduct.bicone f).pt, π := fun j ↦ X ◁ biproduct.π f j, ι := fun j ↦ X ◁ biproduct.ι f j, ι_π := ⋯ }.π
      j✝ =
    (∑ j, X ◁ biproduct.π f j ≫ biproduct.ι (fun j ↦ X ⊗ f j) j) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝

Tactic:
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, ite_true, eqToHom_refl, Category.comp_id]

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

Goal state before:
pp: case intro
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✝ : Finite J
X : C
f : J → C
j : J
val✝ : Fintype J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j ↦ X ⊗ f j) j = X ◁ biproduct.π f j

Tactic:
simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f)

Tactic:
ext : 1
  apply TensorProduct.ext'
  intro x y
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
x✝ : HasLimitsOfShape J Cᵒᵖ
this : HasLimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ
⊢ HasColimitsOfShape Jᵒᵖ C

Tactic:
exact hasColimitsOfShape_of_hasLimitsOfShape_op

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ F.obj X✝ ◁ μ F Y✝ Z✝ ≫
      μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (α_ X✝ Y✝ Z✝).inv ≫ F.map (β (X✝ ⊗ Y✝) Z✝).hom ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ μ F Y✝ Z✝ ≫
      F.obj X✝ ◁ F.map (β Y✝ Z✝).hom ≫ μ F X✝ (Z✝ ⊗ Y✝) ≫ F.map (α_ X✝ Z✝ Y✝).inv ≫ F.map ((β X✝ Z✝).hom ▷ Y✝)

Tactic:
← whiskerLeft_comp_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ F.obj X✝ ◁ μ F Y✝ Z✝ ≫
      μ F X✝ (Y✝ ⊗ Z✝) ≫ F.map (α_ X✝ Y✝ Z✝).inv ≫ F.map (β (X✝ ⊗ Y✝) Z✝).hom ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ (μ F Y✝ Z✝ ≫ F.map (β Y✝ Z✝).hom) ≫
      μ F X✝ (Z✝ ⊗ Y✝) ≫ F.map (α_ X✝ Z✝ Y✝).inv ≫ F.map ((β X✝ Z✝).hom ▷ Y✝)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ (Z₁ ⊗ Z₂) ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ = tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂)

Tactic:
convert! tensorμ_natural (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1 <;> simp

Goal state after: