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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
⊢ Bijective fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩

Tactic:
by
      constructor
      · rintro ⟨a, m, rfl⟩ ⟨b, n, rfl⟩ h
        ext y
        by_cases hy : σ y = y
        · simp_rw [zpow_apply_eq_self_of_apply_eq_self hy]
        · obtain ⟨i, rfl⟩ := (Classical.choose_spec hσ).2 hy
          rw [Subtype.coe_mk, Subtype.coe_mk, zpow_apply_comm σ m i, zpow_apply_comm σ n i]
          exact congr_arg _ (Subtype.ext_iff.mp h)
      · rintro ⟨y, hy⟩
        rw [mem_support] at hy
        obtain ⟨n, rfl⟩ := (Classical.choose_spec hσ).2 hy
        exact ⟨⟨σ ^ n, n, rfl⟩, rfl⟩

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

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∈ fixedPoints ⇑g
⊢ g x = x

Tactic:
exact hx

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
n : ℕ
H : ¬f ^ n = 1
x : α
hx : x ∈ f.support
⊢ x ∈ (f ^ n).support

Tactic:
contrapose H

Goal state after:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
⊢ f ^ n = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ f.support

Tactic:
exact support_pow_le _ n hx

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

Goal state before:
pp: α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
⊢ (↑(range #s)).PairwiseDisjoint fun k ↦ map { toFun := fun i ↦ (i, (f ^ k) i), inj' := ⋯ } s

Tactic:
obtain hs | _ := (s : Set α).subsingleton_or_nontrivial
  · refine Set.Subsingleton.pairwise ?_ _
    simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs ⊢
    rwa [card_range]
  classical
    rintro m hm n hn hmn
    simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk,
      not_exists, not_and, forall_exists_index, and_imp, Prod.forall, Prod.mk_inj]
    rintro _ _ _ - rfl rfl a ha rfl h
    rw [hf.pow_apply_eq_pow_apply ha] at h
    rw [mem_coe, mem_range] at hm hn
    exact hmn.symm (h.eq_of_lt_of_lt hn hm)

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : ¬f.SameCycle x y
hy : y ≠ y
⊢ y ∈ f.support

Tactic:
· exact absurd rfl hy

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

Goal state before:
pp: case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ g x ≠ x

Tactic:
exact hx

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

Goal state before:
pp: n : ℕ
x : Fin (n + 2)
hx' : (finRotate (n + 2)) x ≠ x
⊢ (finRotate (n + 2) ^ ↑↑x) 0 = x

Tactic:
clear hx'

Goal state after:
n : ℕ
x : Fin (n + 2)
⊢ (finRotate (n + 2) ^ ↑↑x) 0 = x
Module: Mathlib.GroupTheory.Perm.Fin

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

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:
· exact (Fin.succ_injective _).ne hlt.ne

Goal state after:
case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc < i.succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k < j
inst✝ : NeZero n
⊢ (i.cycleIcc j) k = k + 1

Tactic:
simp [cycleIcc_of_le_of_le hik (le_of_lt hkj), Fin.ne_of_lt hkj]

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

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
⊢ f' ≫ (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY' =
    (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'

Tactic:
rw [← Category.assoc]

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
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 : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
obtain ⟨l, hl1, hl2⟩ := exists_mem_ne (one_lt_card_support_of_ne_one h) (τ⁻¹ j)

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 : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ∈ (σ * τ).support
hl2 : l ≠ τ⁻¹ j
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))
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
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
⊢ vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)

Tactic:
updateRow_ne hij,

Goal state after:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
⊢ vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • (vecMulVec u v).updateRow i v 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
A B : Matrix n n R
hAB : A * B = 1
h0 :
  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)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B

Tactic:
rw [hAB, detp_one_one, detp_neg_one_one, zero_add] at h0

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
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
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
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 :
  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)
⊢ B * A = 1

Tactic:
rw [hAB, detp_one_one, detp_neg_one_one, zero_add] at h0

Goal state after:
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
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
⊢ B * A = 1
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
c' : F.CoconeTypes
e : c.pt ≃ c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = e (c.ι j x)
y : F.ColimitType
⊢ F.descColimitType c' y = (⇑e ∘ F.descColimitType c) y

Tactic:
obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
c' : F.CoconeTypes
e : c.pt ≃ c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = e (c.ι j x)
j : J
x : F.obj j
⊢ F.descColimitType c' (F.ιColimitType j x) = (⇑e ∘ F.descColimitType c) (F.ιColimitType j x)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
y : F.ColimitType
⊢ hc.down.desc F.coconeTypes (F.descColimitType c y) = y

Tactic:
obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
j : J
x : F.obj j
⊢ hc.down.desc F.coconeTypes (F.descColimitType c (F.ιColimitType j x)) = F.ιColimitType j x
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
y : F.ColimitType
⊢ F.descColimitType F.coconeTypes y = id y

Tactic:
obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
j : J
x : F.obj j
⊢ F.descColimitType F.coconeTypes (F.ιColimitType j x) = id (F.ιColimitType j x)
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
⊢ FilteredColimit.Rel F = Relation.EqvGen F.ColimitTypeRel

Tactic:
by
  ext ⟨j, x⟩ ⟨j', y⟩
  constructor
  · apply eqvGen_colimitTypeRel_of_rel
  · rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
    exact Relation.EqvGen.mono (rel_of_colimitTypeRel F) _ _

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y z : M F
⊢ x * y * z = x * (y * z)

Tactic:
by
      obtain ⟨j₁, x₁, rfl⟩ := x.mk_surjective
      obtain ⟨j₂, y₂, rfl⟩ := y.mk_surjective
      obtain ⟨j₃, z₃, rfl⟩ := z.mk_surjective
      obtain ⟨j, f₁, f₂, f₃, x, y, z, h₁, h₂, h₃⟩ :
          ∃ (j : J) (f₁ : j₁ ⟶ j) (f₂ : j₂ ⟶ j) (f₃ : j₃ ⟶ j) (x y z : F.obj j),
          F.map f₁ x₁ = x ∧ F.map f₂ y₂ = y ∧ F.map f₃ z₃ = z :=
        ⟨IsFiltered.max₃ j₁ j₂ j₃, IsFiltered.firstToMax₃ _ _ _,
          IsFiltered.secondToMax₃ _ _ _, IsFiltered.thirdToMax₃ _ _ _,
          _, _, _, rfl, rfl, rfl⟩
      simp only [← M.map_mk F f₁, ← M.map_mk F f₂, ← M.map_mk F f₃, h₁, h₂, h₃,
        colimit_mul_mk_eq', mul_assoc]

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

Goal state before:
pp: case hg
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 := ⋯
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((limitCone F).π.app (Opposite.op 0)))

pp: case hf
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 := ⋯
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective ⇑(ConcreteCategory.hom i.hom)

Tactic:
· exact surjective_π_app_zero_of_surjective_map_aux hF

Goal state after:
case hf
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 := ⋯
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Function.Surjective ⇑(ConcreteCategory.hom i.hom)
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ RingCat
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      ofHom
        (SemiRingCat.Hom.hom
          ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRingCat)).ι.app x✝)) =
    ofHom
        (SemiRingCat.Hom.hom
          ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRingCat)).ι.app x✝¹)) ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
by
        ext
        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget RingCat)).ι.naturality_apply f _

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

Goal state before:
pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.map f.1).app X.2 ≫ (T.app Y.1).app X.2

pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.1).map f.2

Tactic:
← NatTrans.comp_app,

Goal state after:
case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.map f.1 ≫ T.app Y.1).app X.2

case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.1).map f.2
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 : ι) → 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 ι
⊢ f (s.piecewise a v) - f (s.piecewise b v) =
    ∑ i ∈ s, f fun j ↦ if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j

Tactic:
by
  rw [← s.piecewise_idem_right b a, map_sub_map_piecewise]
  refine Finset.sum_congr rfl fun i hi ↦ congr_arg f <| funext fun j ↦ ?_
  by_cases hjs : j ∈ s
  · rw [if_pos hjs]; by_cases hji : j < i
    · rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]
    rw [if_neg (Classical.not_imp.mpr ⟨hjs, hji⟩), if_neg hji]
    obtain rfl | hij := eq_or_ne i j
    · rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]
    · rw [if_neg hij, if_neg hij.symm]
  · rw [if_neg hjs, if_pos fun h ↦ (hjs h).elim, s.piecewise_eq_of_notMem _ _ hjs]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
X Y : J
f : X ⟶ Y
x : K
⊢ (F.flip.obj x).map f ≫ colimit.ι (F.flip.obj x) Y = colimit.ι (F.flip.obj x) X

Tactic:
colimit.w

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
X Y : J
f : X ⟶ Y
x : K
⊢ colimit.ι (F.flip.obj x) X = colimit.ι (F.flip.obj x) X
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this : R.whiskerLeft h.unit ≫ (R.associator L R).inv ≫ whiskerRight h.counit R = R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (R.whiskerLeft h.unit)

Tactic:
← IsIso.eq_comp_inv

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this :
  R.whiskerLeft h.unit = (R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R)
⊢ IsIso (R.whiskerLeft h.unit)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this : whiskerRight h.unit L ≫ (L.associator R L).hom ≫ L.whiskerLeft h.counit = L.leftUnitor.hom ≫ L.rightUnitor.inv
⊢ IsIso (whiskerRight h.unit L)

Tactic:
← IsIso.eq_comp_inv

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this :
  whiskerRight h.unit L = (L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit)
⊢ IsIso (whiskerRight h.unit L)
Module: Mathlib.CategoryTheory.Monoidal.Category

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

Tactic:
by
  rw [← assoc, ← rightUnitor_naturality]; simp

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 X' Y' : C
f : X ≅ Y
g : X' ≅ Y'
⊢ (f.inv ⊗ₘ g.inv) ≫ (f.hom ⊗ₘ g.hom) = 𝟙 (Y ⊗ Y')

Tactic:
simp [Iso.inv_hom_id, Iso.inv_hom_id]

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

Tactic:
by
  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.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

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

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

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:
· exact congr(($eq).ε)

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
⊢ μ 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.toLaxMonoidal = b.toLaxMonoidal
⊢ η 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.toLaxMonoidal = b.toLaxMonoidal
⊢ δ F = δ 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.toLaxMonoidal = b.toLaxMonoidal
x✝¹ x✝ : C
⊢ (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝ = (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝

Tactic:
rw [μIso_hom, μ_δ, ← @μ_δ _ _ _ _ _ _ _ a, ← μIso_hom]

Goal state after:
case δ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
x✝¹ x✝ : C
⊢ (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝ = μ F x✝¹ x✝ ≫ δ F x✝¹ x✝
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
⊢ identities C ≤ identities C

Tactic:
by rfl

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

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

Tactic:
rw [← Category.assoc]

Goal state after:
case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
g✝ : Y✝ ⟶ Z✝
x✝ y✝ z✝ : C
f' : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf' : W.multiplicativeClosure f'
hg : W g
h_rec : ∀ (f : X✝ ⟶ x✝), W.multiplicativeClosure f → W.multiplicativeClosure (f ≫ f')
f : X✝ ⟶ x✝
hf : W.multiplicativeClosure f
⊢ W.multiplicativeClosure ((f ≫ f') ≫ g)
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✝ : Y✝ ⟶ Z✝
⊢ μ F X✝ Y✝ ≫ F.map (X✝ ◁ f✝) ≫ F.map (β X✝ Z✝).hom = μ F X✝ Y✝ ≫ F.map ((β X✝ Y✝).hom ≫ f✝ ▷ X✝)

Tactic:
← μ_natural_right_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✝ : Y✝ ⟶ Z✝
⊢ F.obj X✝ ◁ F.map f✝ ≫ μ F X✝ Z✝ ≫ F.map (β X✝ Z✝).hom = μ F X✝ Y✝ ≫ F.map ((β X✝ Y✝).hom ≫ f✝ ▷ X✝)