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

Goal state before:
pp: case neg
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : y = y
h✝¹ : ¬a = x
h✝ : ¬a = y
ha : a ≠ a
⊢ x = a

Tactic:
tauto

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

Goal state before:
pp: case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : ¬y = x
h✝¹ : ¬y = y
h✝ : a = x
ha : y ≠ a
⊢ y = a

Tactic:
tauto

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

Goal state before:
pp: case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : ¬y = y
h✝¹ : ¬a = x
h✝ : a = y
ha : x ≠ a
⊢ y = a

Tactic:
tauto

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

Goal state before:
pp: case neg
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : ¬y = y
h✝¹ : ¬a = x
h✝ : ¬a = y
ha : a ≠ a
⊢ y = a

Tactic:
tauto

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝ : b = f (f x)
⊢ ¬x = b

Tactic:
tauto

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝¹ : ¬b = f (f x)
h✝ : b = f x
⊢ ¬f x = b

Tactic:
tauto

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

Goal state before:
pp: case neg
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝¹ : ¬b = f (f x)
h✝ : ¬b = f x
⊢ ¬b = f b

Tactic:
tauto

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

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

pp: case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
· intro a b ha hb hc hd
    refine (Finset.coe_subset.mpr (support_mul_le a b)).trans ?_
    rw [Finset.sup_eq_union, Finset.coe_union, Set.union_subset_iff]
    exact ⟨hc, hd⟩

Goal state after:
case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
⊢ ↑g.support ⊆ Set.ofPred p → g ∈ ofSubtype.range

Tactic:
· intro hg
    refine ⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩
    by_cases hx : g x = x
    · rw [hx]
    · refine iff_of_true (hg ?_) (hg ?_) <;> simpa

Goal state after:
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: k : ℕ
l : List ℕ
⊢ l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k

Tactic:
coprime_list_prod_left_iff

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

Goal state before:
pp: case inl
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hfyx : ¬y = f x
hy : ¬f y = y
j : ℤ
hyx : ¬x = x
hj : (f ^ (j - i)) x = y
hji : (f ^ (j - i)) x = x
⊢ False

Tactic:
tauto

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

Goal state before:
pp: case inr
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hy : ¬f y = y
j : ℤ
hfyx : ¬f x = f x
hj : (f ^ (j - i)) x = y
hji : (f ^ (j - i)) x = f x
⊢ False

Tactic:
tauto

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ #f.support = orderOf f

Tactic:
hf.orderOf

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ #f.support = #f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : ¬f y = y
⊢ ¬(f x = x ↔ f y = y)

Tactic:
tauto

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x x✝ : α
h : f x✝ ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle x x✝ ∧ x ∈ f.support

Tactic:
exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff_aux.1 h).1,
      (mem_support_cycleOf_iff_aux.1 h).2⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : Option α × Perm α
x : Option α
σ : Perm α
this : removeNone (swap none x * optionCongr σ) = σ
⊢ (fun σ ↦ (σ none, removeNone σ)) ((fun i ↦ swap none i.1 * optionCongr i.2) (x, σ)) = (x, σ)

Tactic:
simp [this]

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

Goal state before:
pp: case pos
ι : 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 : α
h : g y = y
h✝ : g.SameCycle x y
hy : ¬y = g y
⊢ False

Tactic:
tauto

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

Goal state before:
pp: case neg
ι : 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 : α
h : g y = y
h✝ : ¬g.SameCycle x y
hy : ¬y = y
⊢ False

Tactic:
tauto

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
this : a ∈ ⊥
⊢ False

Tactic:
tauto

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

Goal state before:
pp: case mpr.h.ha
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ g a ∈ g.support

Tactic:
Perm.apply_mem_support

Goal state after:
case mpr.h.ha
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ a ∈ g.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y * swap z t).cycleType = {2, 2}

Tactic:
rw [(disjoint_swap_swap h).cycleType_mul]
  rw [isSwap_iff_cycleType.mp ?_, isSwap_iff_cycleType.mp ?_]
  · simp
  · rw [swap_isSwap_iff]; grind
  · rw [swap_isSwap_iff]; grind

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
hv : ¬Injective v
⊢ f v = 0

Tactic:
rw [Function.Injective] at hv

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
hv : ¬∀ ⦃a₁ a₂ : ι⦄, v a₁ = v a₂ → a₁ = a₂
⊢ f v = 0
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✝¹⁵ : Semiring R
inst✝¹⁴ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : (i : Fin n.succ) → Module R (M i)
inst✝⁸ : (i : ι) → Module R (M₁ i)
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝⁴ : (i : ι) → AddCommMonoid (M₁' i)
inst✝³ : (i : ι) → Module R (M₁' i)
inst✝² : (i : ι) → AddCommMonoid (M₁'' i)
inst✝¹ : (i : ι) → Module R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i →ₗ[R] M₁' i
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
this : ∀ (j : ι) (z : M₁ i), (f j) (update m i z j) = update (fun k ↦ (f k) (m k)) i ((f i) z) j
⊢ (g fun i_1 ↦ (f i_1) (update m i (x + y) i_1)) =
    (g fun i_1 ↦ (f i_1) (update m i x i_1)) + g fun i_1 ↦ (f i_1) (update m i y i_1)

Tactic:
simp [this]

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✝¹⁵ : Semiring R
inst✝¹⁴ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : (i : Fin n.succ) → Module R (M i)
inst✝⁸ : (i : ι) → Module R (M₁ i)
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝⁴ : (i : ι) → AddCommMonoid (M₁' i)
inst✝³ : (i : ι) → Module R (M₁' i)
inst✝² : (i : ι) → AddCommMonoid (M₁'' i)
inst✝¹ : (i : ι) → Module R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i →ₗ[R] M₁' i
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
this : ∀ (j : ι) (z : M₁ i), (f j) (update m i z j) = update (fun k ↦ (f k) (m k)) i ((f i) z) j
⊢ (g fun i_1 ↦ (f i_1) (update m i (c • x) i_1)) = c • g fun i_1 ↦ (f i_1) (update m i x i_1)

Tactic:
simp [this]

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

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
⊢ (-A).det = (-(1 • A)).det

Tactic:
one_smul

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
⊢ (-A).det = (-A).det
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
⊢ ∃ S, ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)

Tactic:
induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use min X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨minToLeft _ _⟩
    · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : IsCofilteredOrEmpty C
inst✝ : IsCofilteredOrEmpty D
k l : C × D
f g : k ⟶ l
⊢ (eqHom f.1 g.1, eqHom f.2 g.2) ≫ f = (eqHom f.1 g.1, eqHom f.2 g.2) ≫ g

Tactic:
by simp [eq_condition]

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✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update v i (a + b) (σ i_1)) = (m fun i_1 ↦ update v i a (σ i_1)) + m fun i_1 ↦ update v i b (σ i_1)

Tactic:
simp_rw [Function.update_apply_equiv_apply v]

Goal state after:
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✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) (a + b) i_1) =
    (m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) a i_1) + m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) b i_1
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✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a : R
b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update v i (a • b) (σ i_1)) = a • m fun i_1 ↦ update v i b (σ i_1)

Tactic:
simp_rw [Function.update_apply_equiv_apply v]

Goal state after:
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✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a : R
b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) (a • b) i_1) = a • m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) b i_1
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : Fintype ι
c : ι → R
m : (i : ι) → M₁ i
⊢ (f fun i ↦ c i • m i) = (∏ i, c i) • f m

Tactic:
simpa using map_piecewise_smul f c m Finset.univ

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
t : Cocone F
x y : ↑(R F)
⊢ (descAddMonoidHom t) (x * y) = (descAddMonoidHom t) x * (descAddMonoidHom t) y

Tactic:
simp [← descMonoidHom_apply_eq]

Goal state after:
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ s, f (s.piecewise h x) = f x + (f.linearDeriv x) h + ∑ s with 2 ≤ #s, f (s.piecewise h x)

Tactic:
← Finset.powerset_univ,

Goal state after:
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ s ∈ Finset.univ.powerset, f (s.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ s ∈ Finset.univ.powerset with 2 ≤ #s, f (s.piecewise h x)
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ f (x + h) = f x + (f.linearDeriv x) h + ∑ s with 2 ≤ #s, f (s.piecewise h x)

Tactic:
rw [add_comm, map_add_univ, ← Finset.powerset_univ,
      ← sum_filter_add_sum_filter_not _ (2 ≤ #·)]

Goal state after:
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) +
      ∑ x_1 ∈ Finset.univ.powerset with ¬2 ≤ #x_1, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ s ∈ Finset.univ.powerset with 2 ≤ #s, f (s.piecewise h x)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
X : C
c : Cone F
hc : IsLimit c
⊢ Nonempty (IsLimit ((yoneda.obj X).mapCone c))

Tactic:
by
    rw [Types.isLimit_iff]
    intro s hs
    exact ⟨(hc.lift (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩)).unop,
      fun j => Quiver.Hom.op_inj (hc.fac (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩) j),
      fun m hm => Quiver.Hom.op_inj
        (hc.uniq (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩) _
          (fun j => Quiver.Hom.unop_inj (hm j)))⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ G.mapCocone (liftColimit ((IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) c).symm t)) ≅ c

Tactic:
by
        refine (IsColimit.mapCoconeEquiv h ?_).uniqueUpToIso t
        apply IsColimit.ofIsoColimit _ (liftedColimitMapsToOriginal _).symm
        apply (IsColimit.precomposeHomEquiv _ _).symm t

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (uliftYoneda.{w', v, u}.obj X).map f ≫ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso.hom =
    (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso.hom ≫ (shrinkYoneda.{max w' v, v, u}.obj X).map f

Tactic:
by
      ext
      exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm _ _).symm

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
this : s.ι.app = fun i ↦ ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m
x✝ : ↑(directLimitCocone G f).pt
⊢ (Hom.hom m) x✝ = (Hom.hom (↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯))) x✝

Tactic:
simp [this]

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✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
this : L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
⊢ L.map ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y)) = f

Tactic:
simp [this]

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✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
this : R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
⊢ R.map (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f) = f

Tactic:
simp [this]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h
⊢ g = h

Tactic:
by
  cases nonempty_fintype J
  apply (cancel_epi (leftDistributor X f).inv).mp
  ext
  simp [w]

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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f ⋙ G)).hom).obj (G.mapCone c))

Tactic:
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _).symm

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯)
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ Injective ⇑(ConcreteCategory.hom (f ≫ g))

Tactic:
rw [hom_comp]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.injective C f
hg : MorphismProperty.injective C g
⊢ Injective (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f))