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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)

Tactic:
by
  classical
    cases nonempty_fintype β
    constructor
    · intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      rcases this with h | _
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
    · intro h
      obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
      have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
      refine hf'.of_pow fun x hx => ?_
      rw [hm]
      exact support_pow_le _ n hx

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ sign (prodCongrLeft σ) = ∏ k, sign (σ k)

Tactic:
refine (sign_eq_sign_of_equiv _ _ (prodComm β α) ?_).trans (sign_prodCongrRight σ)

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ∀ (x : β × α), (prodComm β α) ((prodCongrLeft σ) x) = (prodCongrRight σ) ((prodComm β α) x)
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: 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
⊢ (ϕ i) y * 1 = (ϕ i) y

Tactic:
exact mul_one _

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ ∀ (n : ℕ), (f.cycleOf x ^ n) x = (f ^ n) x

Tactic:
intro n
  induction n with
  | zero => rfl
  | succ n hn =>
    rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]
    exact ⟨n, rfl⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Tactic:
by
  rw [sum_smul_sum, ← sum_product']
  simp_rw [product_self_eq_disjiUnion_perm hσ, sum_disjiUnion, sum_map, Embedding.coeFn_mk]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : f.SameCycle x y
⊢ (f.cycleOf x) y = f y

Tactic:
rw [h.cycleOf_apply]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset).val =
    Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val +
      Multiset.map (Finset.card ∘ support) τ.cycleFactorsFinset.val

Tactic:
←
    Multiset.map_add,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset).val =
    Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset.val + τ.cycleFactorsFinset.val)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case intro.mp
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : σ ∈ l
a : α
ha : σ a ≠ a
⊢ σ a = l.prod a

Tactic:
exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
this : fixedPoints f = ↑(support σ)ᶜ
⊢ Fintype.card ↑(fixedPoints f) = #(support σ)ᶜ

Tactic:
simp only [this]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
this : fixedPoints f = ↑(support σ)ᶜ
⊢ Fintype.card ↑↑(support σ)ᶜ = #(support σ)ᶜ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i : Fin n
inst✝ : NeZero n
⊢ i.cycleIcc i = 1

Tactic:
by
  ext k
  simp only [Perm.coe_one, id_eq]
  rcases lt_trichotomy k i with ch | ch | ch
  · simp [-cycleIcc_def_le, cycleIcc_of_lt, ch]
  · simp [-cycleIcc_def_le, ch]
  · simp [-cycleIcc_def_le, cycleIcc_of_gt, ch]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
⊢ p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : l.toFinset = f.cycleFactorsFinset
⊢ p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : f (update v i (g i • v i)) = 0
⊢ f v = 0

Tactic:
rw [f.map_update_smul, Function.update_eq_self, smul_eq_zero] at this

Goal state after:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : g i = 0 ∨ f v = 0
⊢ f v = 0
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case e'_2.h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
⊢ {x ∈ ofSign s | x none = i} = Finset.image (fun σ ↦ decomposeOption.symm (i, σ)) (ofSign (sign (swap none i) * s))

Tactic:
ext σ; simp only [mem_filter, mem_ofSign, mem_image]
    exact ⟨fun _ ↦ ⟨σ.removeNone, by rw [← optionCongr_sign]; aesop⟩, by aesop⟩

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
M N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
this : ∏ j, M (τ j) (σ j) = ∏ j, M ((τ * σ⁻¹) j) j
h : ↑↑(sign σ) * ↑↑(sign (τ * σ⁻¹)) = ↑↑(sign τ)
⊢ (∏ i, N (σ i) i) * ↑↑(sign τ) * ∏ j, M (τ j) (σ j) = (∏ i, N (σ i) i) * ↑↑(sign τ) * ∏ i, M ((τ * σ⁻¹) i) i

Tactic:
simp only [this]

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

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

Tactic:
← prod_mul_distrib,

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β

Tactic:
by
  obtain ⟨s, α, β, H⟩ := crown ![j₁, j₂, j₃] (Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ nofun)))
     (Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ nofun)))
  exact ⟨s, α, β, H 0, H 1, H 2⟩

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
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 ≠ (σ * τ) l
hl2 : l ∈ {τ⁻¹ j}ᶜ
h0 : ∀ (k : n), k ∈ {τ⁻¹ j}ᶜ ↔ τ k ∈ {j}ᶜ
⊢ IsAddUnit ((∏ i ∈ {τ⁻¹ j}ᶜ, A i (τ i)) * ∏ i ∈ {τ⁻¹ j}ᶜ, B (τ i) (σ (τ i)))

Tactic:
← prod_mul_distrib,

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 ≠ (σ * τ) l
hl2 : l ∈ {τ⁻¹ j}ᶜ
h0 : ∀ (k : n), k ∈ {τ⁻¹ j}ᶜ ↔ τ k ∈ {j}ᶜ
⊢ IsAddUnit (∏ x ∈ {τ⁻¹ j}ᶜ, A x (τ x) * B (τ x) (σ (τ x)))
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case e'_2.e'_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : (fun X ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i) = (colimitCocone F).pt
⊢ (hom ((colimitCocone F).ι.app i)) xi =
    (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app i)) xi)

pp: case e'_2.e'_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : (fun X ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i) = (colimitCocone F).pt
⊢ (hom ((colimitCocone F).ι.app j)) xj =
    (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app j)) xj)

Tactic:
· exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm

Goal state after:
case e'_2.e'_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : (fun X ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i) = (colimitCocone F).pt
⊢ (hom ((colimitCocone F).ι.app j)) xj =
    (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app j)) xj)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: ι : 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
a : α
z : (i : ι) → M₁ i
⊢ (fun i ↦ update m a z (e.symm i) ↑i) = fun i ↦ update (fun j ↦ m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Tactic:
ext i
  rcases eq_or_ne a (e.symm i) with rfl | hne
  · rw [Equiv.apply_symm_apply e i, update_self, update_self]
  · rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]

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
⊢ ((F ⋙ uliftFunctor.{v, u}).coconeTypesEquiv.symm (uliftFunctor.{v, u}.mapCocone c)).IsColimit

Tactic:
exact (((isColimit_iff_coconeTypesIsColimit _).1 ⟨hc⟩).precompose
          (G := F ⋙ uliftFunctor.{v}) (fun _ ↦ Equiv.ulift)
          (fun _ ↦ rfl)).of_equiv Equiv.ulift.symm (fun _ _ ↦ rfl)

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)
⊢ IsLimit d

Tactic:
by
        let d' : Cone K := (h (F.mapCone d) hd).toLiftableCone.liftedCone
        let i : F.mapCone d' ≅ F.mapCone d :=
          (h (F.mapCone d) hd).toLiftableCone.validLift
        let hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
        let f : d ⟶ d' := hd'.liftConeMorphism d
        have : (Cone.functoriality K F).map f = i.inv :=
          (hd.ofIsoLimit i.symm).uniq_cone_morphism
        haveI : IsIso ((Cone.functoriality K F).map f) := by
          rw [this]
          infer_instance
        haveI : IsIso f := isIso_of_reflects_iso f (Cone.functoriality K F)
        exact IsLimit.ofIsoLimit hd' (asIso f).symm

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 s
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)
inst✝ : IsFilteredOrEmpty J
D : Cocone F
hD : IsColimit D
k j : J
y : ToType (F.obj j)
⊢ (ConcreteCategory.hom (D.ι.app (IsFiltered.max k j))) ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax k j))) y) =
    (ConcreteCategory.hom (D.ι.app j)) y

Tactic:
rw [← ConcreteCategory.comp_apply]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
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)
inst✝ : IsFilteredOrEmpty J
D : Cocone F
hD : IsColimit D
k j : J
y : ToType (F.obj j)
⊢ (ConcreteCategory.hom (F.map (IsFiltered.rightToMax k j) ≫ D.ι.app (IsFiltered.max k j))) y =
    (ConcreteCategory.hom (D.ι.app j)) y
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
P : Cᵒᵖ ⥤ Type w
f : shrinkYoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.op)) (shrinkYonedaEquiv f) =
    (ConcreteCategory.hom (f.app (op Y))) (shrinkYonedaObjObjEquiv.symm g)

Tactic:
simp [shrinkYonedaObjObjEquiv, shrinkYonedaEquiv, shrinkYoneda,
    ← comp_apply, ← NatTrans.naturality]

Goal state after:
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
X : D
⊢ h.counit.app X ≫ R.preimage (h.unit.app (R.obj X)) = 𝟙 ((R ⋙ L).obj X)

Tactic:
simp [← h.counit_naturality (R.preimage (h.unit.app (R.obj X)))]

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ (λ_ (F.obj X)).hom = εIso.hom ▷ F.obj X ≫ (μIso (𝟙_ C) X).hom ≫ F.map (λ_ X).hom

Tactic:
rw [← cancel_mono (λ_ (F.obj X)).inv, Iso.hom_inv_id, oplax_left_unitality]
    simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η : h ⟶ i
η₁ : g ⊗ h ⟶ g ⊗ i
η₂ : f ⊗ g ⊗ h ⟶ f ⊗ g ⊗ i
η₃ : f ⊗ g ⊗ h ⟶ (f ⊗ g) ⊗ i
η₄ : (f ⊗ g) ⊗ h ⟶ (f ⊗ g) ⊗ i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ (α_ f g i).inv = η₃
e_η₄ : (α_ f g h).hom ≫ η₃ = η₄
⊢ (f ⊗ g) ◁ η = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g h : C
η : f ⟶ f'
η₁ : f ⊗ g ⟶ f' ⊗ g
η₂ : (f ⊗ g) ⊗ h ⟶ (f' ⊗ g) ⊗ h
η₃ : (f ⊗ g) ⊗ h ⟶ f' ⊗ g ⊗ h
η₄ : f ⊗ g ⊗ h ⟶ f' ⊗ g ⊗ h
e_η₁ : η ▷ g = η₁
e_η₂ : η₁ ▷ h = η₂
e_η₃ : η₂ ≫ (α_ f' g h).hom = η₃
e_η₄ : (α_ f g h).inv ≫ η₃ = η₄
⊢ η ▷ (g ⊗ h) = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]

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

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

Tactic:
braiding_naturality_left_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.obj Y✝) (F.obj Z✝)).inv ≫
      (β_ (F.obj X✝ ⊗ F.obj Y✝) (F.obj Z✝)).hom ≫ F.obj Z✝ ◁ μ F X✝ Y✝ ≫ μ F Z✝ (X✝ ⊗ Y✝) ≫ F.map (α_ Z✝ X✝ Y✝).inv =
    F.obj X✝ ◁ (β_ (F.obj Y✝) (F.obj Z✝)).hom ≫
      (α_ (F.obj X✝) (F.obj Z✝) (F.obj Y✝)).inv ≫
        (β_ (F.obj X✝) (F.obj Z✝)).hom ▷ F.obj Y✝ ≫ μ F Z✝ X✝ ▷ F.obj Y✝ ≫ μ F (Z✝ ⊗ X✝) Y✝
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),
    (α_ X Y Z).inv ≫ (β (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (β Y Z).hom ≫ (α_ X Z Y).inv ≫ (β X Z).hom ▷ Y

Tactic:
by
    intros
    apply F.map_injective
    refine (cancel_epi (μ F _ _)).1 ?_
    refine (cancel_epi (_ ◁ μ F _ _)).1 ?_
    rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp, ←
      μ_natural_right_assoc, ← whiskerLeft_comp_assoc, w,
      whiskerLeft_comp_assoc, Functor.LaxMonoidal.associativity_inv_assoc,
      Functor.LaxMonoidal.associativity_inv_assoc, ← μ_natural_left,
      ← comp_whiskerRight_assoc, w, comp_whiskerRight_assoc, reassoc_of% w,
      braiding_naturality_left_assoc, Functor.LaxMonoidal.associativity_inv, hexagon_reverse_assoc]

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
j : J
x : ↑((F ⋙ uliftFunctor).obj j)
⊢ (QuotientAddGroup.lift (Relations (F ⋙ uliftFunctor))
        (DFinsupp.sumAddHom fun j ↦
          ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)).comp
            ↑AddEquiv.ulift)
        ⋯)
      (((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
          (DFinsupp.singleAddHom (fun j ↦ ↑(uliftFunctor.obj (F.obj j))) j))
        x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x.down

Tactic:
conv_lhs => erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
    (DFinsupp.singleAddHom _ j), QuotientAddGroup.lift_mk']

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑((F ⋙ uliftFunctor).obj j)
⊢ (DFinsupp.sumAddHom fun j ↦
        ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)).comp ↑AddEquiv.ulift)
      ((DFinsupp.singleAddHom (fun j ↦ ↑((F ⋙ uliftFunctor).obj j)) j) x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x.down
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
f : M →ₗ[R] A
⊢ ((lift R) f).range = Algebra.adjoin R (Set.range ⇑f)

Tactic:
simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → (ι R) x = (algebraMap R (TensorAlgebra R M)) r

Tactic:
rintro ⟨rfl, rfl⟩
    rw [map_zero, map_zero]

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

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹.snd = (inl r⁻¹).snd

Tactic:
rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_zero]

Goal state after: