mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map f g = f ≫ inl

Tactic:
rw [biprod.map_eq_map']

Goal state after:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map' f g = f ≫ inl
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map f g = g ≫ inr

Tactic:
rw [biprod.map_eq_map']

Goal state after:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map' f g = g ≫ inr
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: case _private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk._private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
hom'✝¹ hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝¹ }.hom = { hom' := hom'✝ }.hom
⊢ { hom' := hom'✝¹ } = { hom' := hom'✝ }

Tactic:
simpa using! h

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟↑e ≫ ↟↑e.symm = 𝟙 (of R X₁)

Tactic:
ext; apply e.left_inv

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

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
⊢ c.length = n → c = ones n

Tactic:
contrapose

Goal state after:
case mpr
n : ℕ
c : Composition n
⊢ ¬c = ones n → ¬c.length = n
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
⊢ PreservesBinaryBiproduct X Y F

Tactic:
have : Epi (splitEpiBiprodComparison F X Y).section_ := by simpa

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
this : Epi (F.splitEpiBiprodComparison X Y).section_
⊢ PreservesBinaryBiproduct X Y F
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ (e.viaFintypeEmbedding f) (f a) = f (e a)

Tactic:
by
  rw [Equiv.Perm.viaFintypeEmbedding]
  convert! Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hd : l.Nodup
h : l ~r l'
⊢ l.formPerm = l'.formPerm

Tactic:
by
  obtain ⟨n, rfl⟩ := h
  exact (formPerm_rotate l hd n).symm

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
⊢ swap x y ∈ H

Tactic:
have hx : x ∈ univ := Finset.mem_univ x

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : x ∈ univ
⊢ swap x y ∈ H
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
⊢ closure {σ, τ} = ⊤

Tactic:
obtain ⟨i, hi⟩ :=
    h1.exists_pow_eq (mem_support.mp ((Finset.ext_iff.mp h2 x).mpr (Finset.mem_univ x)))
      (mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
⊢ closure {σ, τ} = ⊤
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n i : ℕ
h : i + 1 < n + 1
⊢ (iterate f a (n + 1))[i + 1]? = some (f^[i + 1] a)

Tactic:
simp [getElem?_iterate f (f a) n i (by simpa using h)]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y ↦ (swap x y).signAux3 hs = -1

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin α

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
n : ℕ
e : α ≃ Fin n
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y ↦ (swap x y).signAux3 hs = -1
Module: Mathlib.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
n : ℤ
⊢ a * (b ^ n * b) = a * b ^ (n + 1)

Tactic:
mul_zpow_self

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
n : ℤ
⊢ a * b ^ (n + 1) = a * b ^ (n + 1)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case neg
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : ¬a = a'
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Tactic:
refine Or.inr ⟨fun h => not_or_intro ha' notMem_l ((List.mem_cons).mp h), ?_⟩
      rw [prodExtendRight_apply_ne _ ha']

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

Goal state before:
pp: case succ.succ
n : ℕ
ih : sign (finRotate (n + 1)) = (-1) ^ (n + 1 - 1)
⊢ sign (finRotate (n + 1 + 1)) = (-1) ^ (n + 1 + 1 - 1)

Tactic:
rw [finRotate_succ_eq_decomposeFin]
      simp [ih, pow_succ]

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

Goal state before:
pp: n x : ℕ
hx : x < n + 2
⊢ (finRotate (n + 2) ^ ↑↑⟨x, hx⟩) 0 = ⟨x, hx⟩

Tactic:
zpow_natCast,

Goal state after:
n x : ℕ
hx : x < n + 2
⊢ (finRotate (n + 2) ^ ↑⟨x, hx⟩) 0 = ⟨x, hx⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
⊢ IsConj (σ * π) τ

Tactic:
obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'

Goal state after:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
⊢ IsConj (σ * π) τ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case zero
n : ℕ
inst✝ : NeZero n
hi : 0 < n
h0 : ⟨0, hi⟩ ≠ 0
⊢ ⟨0, hi⟩.cycleRange.IsCycle

pp: case succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.IsCycle

Tactic:
· exact (h0 rfl).elim

Goal state after:
case succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.IsCycle
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case zero
n : ℕ
inst✝ : NeZero n
hi : 0 < n
h0 : ⟨0, hi⟩ ≠ 0
⊢ ⟨0, hi⟩.cycleRange.cycleType = {↑⟨0, hi⟩ + 1}

pp: case succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.cycleType = {↑⟨n✝ + 1, hi⟩ + 1}

Tactic:
· exact (h0 rfl).elim

Goal state after:
case succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.cycleType = {↑⟨n✝ + 1, hi⟩ + 1}
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
⊢ σ ∈ l ↔ ∀ (a : α), σ a ≠ a → σ a = l.prod a

Tactic:
classical
    cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert! hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)

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

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

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

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ f.cycleOf a = c.cycleOf a

Tactic:
← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ f.cycleOf a = (c * (f * c⁻¹)).cycleOf a

case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ (f * c⁻¹) a = a
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ Nat.Coprime 2 (_root_.orderOf g)

Tactic:
rw [ht.orderOf]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ Nat.Coprime 2 3
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case ha
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Fintype (κ i)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι'
f : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
⊢ ∀ (i : ((i : ι) → κ i) × ι') (b : R) (f : Π₀ (i : ((i : ι) → κ i) × ι'), R),
    f i = 0 →
      b ≠ 0 →
        (freeDFinsuppEquiv f) x = ∑ p, f p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i)) →
          (freeDFinsuppEquiv (DFinsupp.single i b + f)) x =
            ∑ p, (DFinsupp.single i b + f) p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
rintro p r f - - hfx

Goal state after:
case ha
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Fintype (κ i)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι'
f✝ : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
p : ((i : ι) → κ i) × ι'
r : R
f : Π₀ (i : ((i : ι) → κ i) × ι'), R
hfx : (freeDFinsuppEquiv f) x = ∑ p, f p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))
⊢ (freeDFinsuppEquiv (DFinsupp.single p r + f)) x =
    ∑ p_1, (DFinsupp.single p r + f) p_1 • DFinsupp.single p_1.2 (∏ i, (x i) (p_1.1 i))
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
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
⊢ f.compLinearMap 0 = 0

Tactic:
by
  ext
  simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]

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

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

Tactic:
mf'

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

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

Tactic:
mf'

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
⊢ (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mX' ≫ f' = (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
⊢ M.det = N.det

Tactic:
congr
    ext i j
    refine Fin.cases (h0 j) (fun i => ?_) i
    rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬(hom (t.ι.app x_1)) x_2 = x
⊢ (↾fun x ↦ { down := True }) = ↾fun y ↦ { down := y ≠ x }

Tactic:
refine h.hom_ext fun j ↦ ?_

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬(hom (t.ι.app x_1)) x_2 = x
j : J
⊢ (t.ι.app j ≫ ↾fun x ↦ { down := True }) = t.ι.app j ≫ ↾fun y ↦ { down := y ≠ x }
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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
x y : M₁ ↑i
⊢ f.domDomRestrict P (update m i (x + y)) = f.domDomRestrict P (update m i x) + f.domDomRestrict P (update m i y)

Tactic:
ext v
    simp [domDomRestrict_aux_right]

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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
c : R
x : M₁ ↑i
⊢ f.domDomRestrict P (update m i (c • x)) = c • f.domDomRestrict P (update m i x)

Tactic:
ext v
    simp [domDomRestrict_aux_right]

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

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂ ≫ α))) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂ ≫ α))) y =
    (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₃ j₂ ≫ γ))) x' *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₃ j₂ ≫ γ))) y

Tactic:
h₁,

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map (f ≫ β))) x * (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂ ≫ α))) y =
    (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₃ j₂ ≫ γ))) x' *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₃ j₂ ≫ γ))) y
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₂ j₁ ≫ α))) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₂ j₁ ≫ α))) y =
    (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₂ j₃ ≫ γ))) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₂ j₃ ≫ γ))) y'

Tactic:
h₁,

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₂ j₁ ≫ α))) x * (ConcreteCategory.hom (F.map (f ≫ β))) y =
    (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₂ j₃ ≫ γ))) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₂ j₃ ≫ γ))) y'
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂ ≫ α))) x *
      (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂ ≫ α))) y =
    (ConcreteCategory.hom (F.map (f ≫ β))) x * (ConcreteCategory.hom (F.map (g ≫ β))) y

Tactic:
h₁,

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ (ConcreteCategory.hom (F.map (f ≫ β))) x * (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂ ≫ α))) y =
    (ConcreteCategory.hom (F.map (f ≫ β))) x * (ConcreteCategory.hom (F.map (g ≫ β))) y