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

Goal state before:
pp: case inr
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
have := hs.to_subtype
    have := hs'.to_subtype
    obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance
    refine ⟨(Equiv.addRight 1).extendDomain f, ?_, fun x hx =>
      of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
    convert! Int.addRight_one_isCycle.isCycleOn.extendDomain f
    rw [Set.image_comp, Equiv.image_eq_preimage_symm]
    ext
    simp

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

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : #s ≤ 1
⊢ #(range #s) ≤ 1

Tactic:
card_range

Goal state after:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : #s ≤ 1
⊢ #s ≤ 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ✝ σ τ : Perm α
hστ : σ.Disjoint τ
x✝ : σ.IsCycle
hσ : σ⁻¹.cycleType = σ.cycleType
hτ : τ⁻¹.cycleType = τ.cycleType
⊢ (σ * τ)⁻¹.cycleType = (σ * τ).cycleType

Tactic:
by
      simp only [mul_inv_rev, hστ.cycleType_mul, hστ.symm.inv_left.inv_right.cycleType_mul, hσ, hτ,
        add_comm]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Tactic:
· rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos.succ
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1)) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
· exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : (n + 1) • orderOf σ < 2 * orderOf σ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle

Tactic:
nsmul_eq_mul,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : ↑(n + 1) * orderOf σ < 2 * orderOf σ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝
l : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, g x = x
x✝ : α
⊢ 1 x✝ = g x✝

Tactic:
simp [*]

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

Goal state before:
pp: case h
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ Commute g⁻¹ (g.cycleOf x)

pp: case hx
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ (g.cycleOf x) y = y

Tactic:
· rw [Commute.inv_left_iff, commute_iff_eq]
              ext z; by_cases hz : SameCycle g x z
              · simp [cycleOf_apply, hz]
              · simp [cycleOf_apply_of_not_sameCycle, hz]

Goal state after:
case hx
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ (g.cycleOf x) y = y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
obtain _ := not_forall.mp (mt ext hσ.ne_one)
    rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]

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

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

Tactic:
by
  rw [one_eq]
  exact Set.uniqueSingleton (Vector.nil.cons 1)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
⊢ H = ⊤

Tactic:
have : Fact (Fintype.card α).Prime := ⟨h0⟩
  obtain ⟨σ, hσ⟩ := exists_prime_orderOf_dvd_card (Fintype.card α) h1
  have hσ1 : orderOf (σ : Perm α) = Fintype.card α := (Subgroup.orderOf_coe σ).trans hσ
  have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1
  have hσ3 : (σ : Perm α).support = ⊤ :=
    Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1)
  have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3
  rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset_iff, Set.singleton_subset_iff]
  exact ⟨Subtype.mem σ, h2⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support + (Fintype.card α - #σ.support) • 1 = Fintype.card α

Tactic:
nsmul_eq_mul,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support + ↑(Fintype.card α - #σ.support) * 1 = Fintype.card α
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case inr
ι : Type uι
κ : ι → Type uκ
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)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : q ≠ p
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = (DFinsupp.single p ((f p) m)) q

Tactic:
DFinsupp.single_eq_of_ne hpq

Goal state after:
case inr
ι : Type uι
κ : ι → Type uκ
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)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : q ≠ p
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = 0
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i ≃ₗ[R] M₁' i
f' : (i : ι) → M₁ i →ₗ[R] M₁' i := fun i ↦ ↑(f i)
⊢ g.compLinearMap f' = compLinearMap 0 f' ↔ g = 0

Tactic:
compLinearMap_inj f' fun i => (f i).surjective

Goal state after:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i ≃ₗ[R] M₁' i
f' : (i : ι) → M₁ i →ₗ[R] M₁' i := fun i ↦ ↑(f i)
⊢ g = 0 ↔ g = 0
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
p : n
hcol : A.col p = 0
⊢ detp s A = 0

Tactic:
by
  simpa using detp_eq_of_row_eq_zero (A := Aᵀ) s hcol

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

Goal state before:
pp: case a.neg_add_cancel
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.neg.add x) = descFunLift F s zero

Tactic:
dsimp; rw [neg_add_cancel]

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

Goal state before:
pp: case a.neg_add_cancel
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.neg.add x) = descFunLift F s zero

Tactic:
dsimp; rw [neg_add_cancel]

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
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ ∏ i, diagonal d (σ i) i = 0

Tactic:
apply Finset.prod_eq_zero (mem_univ x)

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ diagonal d (σ x) x = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N P : Matrix m m R
⊢ (M * N * P).det = (M * P * N).det

Tactic:
by
  rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ

Tactic:
have hσ' x : (σ.symm x).snd = x.snd := by simpa [eq_comm] using hσ (σ.symm x)

Goal state after:
case refine_3
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ | ∀ (x : n × o), (σ x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ j f, (hom (F.map f)) x = (hom (F.map f)) y) → ∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y

Tactic:
rintro ⟨j, f, h⟩

Goal state after:
case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
j : J
f : i ⟶ j
h : (hom (F.map f)) x = (hom (F.map f)) y
⊢ ∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
z : (i : { a // a ∉ s }) → M₁ ↑i
⊢ ∀ [inst : DecidableEq α] (m : α → (i : ι) → M₁ i) (i : α) (x y : (i : ι) → M₁ i),
    (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i (x + y) (e.symm i_1) ↑i_1) =
      (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i x (e.symm i_1) ↑i_1) +
        ((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i y (e.symm i_1) ↑i_1

Tactic:
classical simp [iteratedFDeriv_aux]

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

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
z : (i : { a // a ∉ s }) → M₁ ↑i
⊢ ∀ [inst : DecidableEq α] (m : α → (i : ι) → M₁ i) (i : α) (c : R) (x : (i : ι) → M₁ i),
    (((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i (c • x) (e.symm i_1) ↑i_1) =
      c • ((f.domDomRestrictₗ fun i ↦ i ∈ s) z) fun i_1 ↦ update m i x (e.symm i_1) ↑i_1

Tactic:
classical simp [iteratedFDeriv_aux]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
⊢ (-1) ^ ↑i = ↑↑(sign i.cycleRange)

Tactic:
simp [Fin.sign_cycleRange]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
i : J
x : ↑((F ⋙ forget₂ CommMonCat MonCat).obj i)
j : J
y : ↑((F ⋙ forget₂ CommMonCat MonCat).obj j)
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩

Tactic:
rw [colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ ⟨j, y⟩ k f g,
        colimit_mul_mk_eq.{v, u} (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ ⟨i, x⟩ k g f]

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
i : J
x : ↑((F ⋙ forget₂ CommMonCat MonCat).obj i)
j : J
y : ↑((F ⋙ forget₂ CommMonCat MonCat).obj j)
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      ⟨k,
        (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map f)) ⟨i, x⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map g)) ⟨j, y⟩.snd⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      ⟨k,
        (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map g)) ⟨j, y⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map f)) ⟨i, x⟩.snd⟩
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c✝ : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = s j
this : ∀ (c : Cone F) (y : c.pt), ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j
x : (c : Cone F) → c.pt → c✝.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) (x c y) ∧
      ∀ (y_1 : c✝.pt), (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) y_1 → y_1 = x c y
c : Cone F
f : c.pt ⟶ c✝.pt
hf : ∀ (j : J), f ≫ c✝.π.app j = c.π.app j
⊢ f = ↾x c

Tactic:
by ext y; exact (hx c y).2 (f y) (fun j ↦ congr_hom (hf j) y)

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

Goal state before:
pp: case neg
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 ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∉ s
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) = v j

Tactic:
if_pos fun h ↦ (hjs h).elim,

Goal state after:
case neg
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 ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∉ s
⊢ s.piecewise a v j = v j
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
r : R
k : J
hjk : j ⟶ k
y : ToType ((F ⋙ forget₂ (AlgCat R) RingCat).obj k)
⊢ ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) r * (ConcreteCategory.hom (c.ι.app k)) y =
    (ConcreteCategory.hom (c.ι.app k)) y * ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) r

Tactic:
simp [← dsimp% c.w hjk, ← dsimp% (c.ι.app k).hom.map_mul, Algebra.commutes']

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : f.toRatLinearMap = g.toRatLinearMap
x : M
⊢ f x = g x

Tactic:
exact LinearMap.congr_fun h x

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
x✝ : ↑M
⊢ (((mk R ↑(of R R) ↑M).compr₂ₛₗ (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom))) 1) x✝ =
    (((mk R ↑(of R R) ↑M).compr₂ₛₗ (Hom.hom ((leftUnitor M).hom ≫ f))) 1) x✝

Tactic:
simp [tensorHom, tensorObj, leftUnitor]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) ?m.112))

pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ (span g f).map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right =
    (span g f).map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left

Tactic:
· -- Need to unfold these to allow the `PreservesColimit` instance to be found.
      dsimp only [span_map_fst, span_map_snd]
      exact isColimitOfPreserves _ (PushoutCocone.flipIsColimit hc)

Goal state after:
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
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).ContainsIdentities
⊢ (⨅ i, W i).ContainsIdentities

Tactic:
← sInf_range

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).ContainsIdentities
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).ContainsIdentities
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
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsStableUnderComposition
⊢ (⨅ i, W i).IsStableUnderComposition

Tactic:
← sInf_range

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsStableUnderComposition
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).IsStableUnderComposition
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
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsMultiplicative
⊢ (⨅ i, W i).IsMultiplicative

Tactic:
← sInf_range

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).IsMultiplicative
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).IsMultiplicative
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 Y Z : C
⊢ (β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X =
    𝟙 ((X ⊗ Y) ⊗ Z) ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 ((Z ⊗ Y) ⊗ X)

Tactic:
rw [← cancel_epi (α_ X Y Z).inv, ← cancel_mono (α_ Z Y X).hom]
  convert! yang_baxter X Y Z using 1
  all_goals monoidal

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ ((pushoutIsoOpPullback f g).inv.unop ≫ pullback.fst f.unop g.unop).op = (pushout.inl f g).unop.op

Tactic:
simp [← pushoutIsoOpPullback_inl_hom]

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).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv

Tactic:
apply (cancel_mono (λ_ X).hom).1
  simp only [assoc, braiding_leftUnitor, Iso.inv_hom_id]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
l : List (tsze R M)
⊢ l.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst l)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst l)).prod)
        l.zipIdx).sum

Tactic:
induction l with
  | nil => simp
  | cons x xs ih =>
    rw [List.zipIdx_cons']
    simp_rw [List.map_cons, List.map_map, Function.comp_def, Prod.map_snd, Prod.map_fst, id,
      List.take_zero, List.take_succ_cons, List.prod_nil, List.prod_cons, snd_mul, one_smul,
      List.drop, mul_smul, List.sum_cons, fst_list_prod, ih, List.smul_sum, List.map_map,
      ← smul_comm (_ : R) (_ : Rᵐᵒᵖ)]
    exact add_comm _ _

Goal state after: