mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
hₗ : m ≫ b.fst = s.π.app { as := WalkingPair.left }
hᵣ : m ≫ b.snd = s.π.app { as := WalkingPair.right }
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr

Tactic:
simpa [← hₗ, ← hᵣ] using m ≫= total.symm

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case cons
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i, x i = n
n : ℕ
⊢ (∃ a, a.1 + a.2 = n ∧ (a.1, a.2) = (x₀, ∑ i, x i)) ↔ x₀ + ∑ i, x i = n

Tactic:
exists_eq_right

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x : Fin (k + 1) → ℕ
hx₁ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id a)
hx₂ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id b)
⊢ False

Tactic:
· rw [List.mem_map] at hx₁ hx₂
      obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
      dsimp at h₁₂
      rw [Fin.cons_inj, Nat.succ_inj] at h₁₂
      obtain ⟨h₁₂, rfl⟩ := h₁₂
      rw [Function.onFun, h₁₂] at h
      exact h (List.mem_map_of_mem hx₁) (List.mem_map_of_mem hx₂)

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (fun a_2 b ↦ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a.1 a_2) (Fin.cons a.1 b))
        (antidiagonalTuple k a.2)) ∧
    Pairwise
      (fun a₁ a₂ ↦
        ∀ (x : Fin (k + 1) → ℕ) (x_1 : Fin k → ℕ),
          x_1 ∈ antidiagonalTuple k a₁.2 ∧ Fin.cons a₁.1 x_1 = x →
            ∀ (y : Fin (k + 1) → ℕ) (x_2 : Fin k → ℕ),
              x_2 ∈ antidiagonalTuple k a₂.2 ∧ Fin.cons a₂.1 x_2 = y →
                Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) x y)
      (antidiagonal n)

Tactic:
and_imp,

Goal state after:
k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (fun a_2 b ↦ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a.1 a_2) (Fin.cons a.1 b))
        (antidiagonalTuple k a.2)) ∧
    Pairwise
      (fun a₁ a₂ ↦
        ∀ (x : Fin (k + 1) → ℕ),
          ∀ x_1 ∈ antidiagonalTuple k a₁.2,
            Fin.cons a₁.1 x_1 = x →
              ∀ (y : Fin (k + 1) → ℕ),
                ∀ x_2 ∈ antidiagonalTuple k a₂.2,
                  Fin.cons a₂.1 x_2 = y → Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) x y)
      (antidiagonal n)
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
⊢ m ∈ p.parts.toFinset ↔ count m p.parts * m ≠ 0

Tactic:
by
    suffices m ∈ p.parts → m ≠ 0 by simpa
    grind

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case refl
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ c.blocks = c'.blocks

Tactic:
exact H

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

Goal state before:
pp: α : Type u_1
f : Perm α
n : ℤ
x : α
⊢ f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Tactic:
by
  rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
⊢ spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ

Tactic:
by ext; simp; tauto

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
⊢ sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ

Tactic:
by ext; simp; tauto

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ 1 < #f.support

Tactic:
simp_rw [one_lt_card_iff, mem_support, ← not_or]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ ∃ a b, ¬(f a = a ∨ f b = b ∨ a = b)
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
rcases this.eq_or_lt with (rfl | hn')

Goal state after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
w : (x :: xs).Nodup
h : xs.length < (x :: xs).length
this : xs.length ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = (x :: xs)[(xs.length + 1) % (x :: xs).length]

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.toFinset ⊆ {x | l.formPerm x ≠ x}

Tactic:
· intro x hx
    simp only [Finset.mem_coe, mem_toFinset] at hx
    obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
    rw [Set.mem_ofPred_eq, formPerm_apply_getElem _ h]
    intro H
    rw [nodup_iff_injective_get, Function.Injective] at h
    specialize h H
    rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'
    · simp only [← hn', Nat.mod_self] at h
      refine not_exists.mpr h' ?_
      rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]
    · simp [Nat.mod_eq_of_lt hn'] at h

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: a : ℤ
ha : IsUnit a
⊢ a ^ 2 = 1

Tactic:
by rw [sq, isUnit_mul_self ha]

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ ↑u ^ 2 = ↑1

Tactic:
Units.val_one,

Goal state after:
u : ℤˣ
⊢ ↑u ^ 2 = 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case h.h
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
hk : k < ((x :: y :: l).rotate n).length
⊢ ∀ (h₂ : k < (x' :: y' :: l').length), ((x :: y :: l).rotate n)[k] = (x' :: y' :: l')[k]

Tactic:
hk'

Goal state after:
case h.h
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
hk : k < ((x :: y :: l).rotate n).length
hk' : k < (x' :: y' :: l').length
⊢ ((x :: y :: l).rotate n)[k] = (x' :: y' :: l')[k]
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
x✝ : (_ : Fin (n + 2)) × Fin (n + 2)
x₁ x₂ : Fin (n + 2)
⊢ ⟨x₁, x₂⟩ ∈ {⟨1, 0⟩} → ⟨x₁, x₂⟩ ∈ finPairsLT (n + 2)

Tactic:
simp +contextual [mem_finPairsLT]

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

Goal state before:
pp: α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
⊢ f = g

Tactic:
have : f.support = g.support := by
    refine le_antisymm h ?_
    intro z hz
    obtain ⟨x, hx, _⟩ := id hf
    have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
    obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
    have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
      intro x hx
      exact h' x (mem_of_mem_inter_left hx)
    rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]
  refine Equiv.Perm.support_congr h ?_
  simpa [← this] using h'

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

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

Tactic:
by
  simp_rw [hc.commute_iff', Subgroup.mem_zpowers_iff]
  refine exists_congr fun hc' => exists_congr fun k => ?_
  rw [subtypePermOfSupport, subtypePerm_zpow c k]
  simp only [Perm.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
  apply forall_congr'
  intro a
  by_cases ha : a ∈ c.support
  · rw [imp_iff_right ha, ofSubtype_subtypePerm_of_mem hc' ha]
  · rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← notMem_support]
    · exact Finset.notMem_mono (support_zpow_le c k) ha
    · exact ha

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.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ∃ n, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)

Tactic:
refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩
  · rw [tsub_add_cancel_of_le]
    rw [Nat.succ_le_iff, card_cycleType_pos, Ne, ← orderOf_eq_one_iff]
    exact hσ.ne_one
  · exact (hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycleType hn)).resolve_left
      (one_lt_of_mem_cycleType hn).ne'

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

Goal state before:
pp: case refine_3.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}

Tactic:
rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
        erase_eq_of_notMem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]

Goal state after:
case refine_3.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ τ.Disjoint (σ * f⁻¹)

case refine_3.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ f ∉ τ.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
x : α
h : x ∈ g.support
⊢ g x = (swap a (g a)) ((swap (g a) (g (g a))) x)

Tactic:
simp only [ha', Finset.mem_insert, Finset.mem_singleton] at h
    rcases h with rfl | (rfl | rfl)
    · rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]
      simp
    · rw [swap_apply_left, swap_apply_of_ne_of_ne (by grind) (by grind)]
    · simp only [swap_apply_right]
      suffices (g ^ 3) a = a by simpa
      simp [← hg3.orderOf]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
m : M
⊢ update (update v i m) j m i = m

Tactic:
Function.update_of_ne hij,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
m : M
⊢ update v i m i = m
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case inl.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp 1 A

Tactic:
first | rfl | rw [this]

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

Goal state before:
pp: case inl.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp (-1) A

Tactic:
first | rfl | rw [this]

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

Goal state before:
pp: case inr.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp (-1) A = detp 1 A

Tactic:
first | rfl | rw [this]

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

Goal state before:
pp: case inr.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp (-1) A = detp (-1) A

Tactic:
first | rfl | rw [this]

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ (colimitSetoid F) (Prequotient.of j 0) zero

Tactic:
apply Relation.zero

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ (colimitSetoid F) (Prequotient.of j 0) zero

Tactic:
apply Relation.zero

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
p : n → n
H : ∃ a₁ a₂, p a₁ = p a₂ ∧ a₁ ≠ a₂
⊢ ∃ i j, p i = p j ∧ i ≠ j

Tactic:
exact H

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ (ts ≫ k₁t) ≫ f₂ = (ts ≫ k₂t) ≫ g₂

Tactic:
by simp only [Category.assoc, hs]

Goal state after:
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:
ext ⟨j, x⟩ ⟨j', y⟩

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩ ↔ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', 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
⊢ A.det = ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Tactic:
rw [Matrix.det_apply, Finset.univ_perm_fin_succ, ← Finset.univ_product_univ]

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ σ ∈ Finset.map decomposeFin.symm.toEmbedding (univ ×ˢ univ), sign σ • ∏ i, A (σ i) i =
    ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)

Tactic:
have := α.2

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
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
this : NatTrans.IsMonoidal α.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ.hom

Tactic:
by
      simp [← reassoc_of% (congrArg Iso.hom h_θ)]

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
F : Jᵒᵖ ⥤ C
inst✝ : HasLimit F
j : J
⊢ colimit.ι F.rightOp j ≫ (colimitRightOpIsoUnopLimit F).hom = (limit.π F (op j)).op

Tactic:
simp [colimitRightOpIsoUnopLimit]

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

Goal state before:
pp: case map.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f✝¹ : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x✝ y✝ : C
f : x✝ ⟶ y✝
hf : W f
⊢ (W.strictMap F).multiplicativeClosure (F.map f)

Tactic:
exact le_multiplicativeClosure _ _ ⟨hf⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom = (ρ_ X).hom ≫ (λ_ X).inv

Tactic:
simp [← rightUnitor_inv_braiding]

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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ G.obj x✝¹ ◁ G.map x✝ ≫ ((i.symm.app x✝¹ ⊗ᵢ i.symm.app Y✝) ≪≫ μIso F x✝¹ Y✝ ≪≫ i.app (x✝¹ ⊗ Y✝)).hom =
    ((i.symm.app x✝¹ ⊗ᵢ i.symm.app X✝) ≪≫ μIso F x✝¹ X✝ ≪≫ i.app (x✝¹ ⊗ X✝)).hom ≫ G.map (x✝¹ ◁ x✝)

Tactic:
by simp [NatTrans.whiskerLeft_app_tensor_app_assoc]

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

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

Tactic:
map_id

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ α.natTrans.app X✝ ≫ 𝟙 (H.obj (L₁.obj X✝)) = α.natTrans.app X✝
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 g : TensorAlgebra R M →ₐ[R] A
w : f.toLinearMap ∘ₗ ι R = g.toLinearMap ∘ₗ ι R
⊢ f = g

Tactic:
rw [← lift_symm_apply, ← lift_symm_apply] at w

Goal state after:
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 g : TensorAlgebra R M →ₐ[R] A
w : (lift R).symm f = (lift R).symm g
⊢ f = g
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
⊢ inl 1⁻¹ = inl 1

Tactic:
inv_one

Goal state after:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
⊢ inl 1 = inl 1
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
⊢ map ((↑f).copy f' h) ((↑f).copy f' h) ∘ₗ comul = comul ∘ₗ (↑f).copy f' h

Tactic:
by simp only [(f : A →ₗ[R] B).copy_eq f' h,
      CoalgHomClass.map_comp_comul]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ comul = (comul ∘ₗ ↑↑e) ∘ₗ ↑e.toLinearEquiv.symm

Tactic:
← toLinearEquiv_toLinearMap,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ comul = (comul ∘ₗ ↑e.toLinearEquiv) ∘ₗ ↑e.toLinearEquiv.symm
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
r : R
t : S
⊢ g (r • t * s) = (RingHom.id R) r • g (t * s)

Tactic:
simp [← map_smul, ModuleCat.restrictScalars.smul_def (M := ModuleCat.of _ S), mul_assoc]

Goal state after: