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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ g = swap a (g a) * swap (g a) (g (g a)) ↔ a ∈ g.support

Tactic:
constructor
  · intro hg
    rw [mem_support]
    intro hx
    apply hg3.isCycle.ne_one
    simpa [hx] using! hg
  intro ha
  have ha' := hg3.support_eq_iff_mem_support.mpr ha
  have ha'' := hg3.nodup_iff_mem_support.mpr ha
  ext x
  simp only [coe_mul, Function.comp_apply]
  by_cases h : x ∈ g.support
  · 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]
  · rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]
    rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]
    simpa [notMem_support] using! h

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ detp 1 (diagonal fun x ↦ 1) = 1

Tactic:
detp_one_diagonal,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ ∏ i, 1 = 1
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
d : n → R
⊢ detp (-1) (diagonal d) = 0

Tactic:
by
  rw [detp, sum_eq_zero]
  intro σ hσ
  have hσ1 : σ ≠ 1 := by
    contrapose hσ
    rw [hσ, mem_ofSign, sign_one]
    decide
  obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)
  exact prod_eq_zero (mem_univ i) (diagonal_apply_ne' _ hi)

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

Goal state before:
pp: case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x.neg = descFunLift F s x'.neg

Tactic:
dsimp

Goal state after:
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ -descFunLift F s x = -descFunLift F s x'
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.add y) = descFunLift F s (x'.add y)

Tactic:
dsimp

Goal state after:
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x' + descFunLift F s y
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.add y) = descFunLift F s (x.add y')

Tactic:
dsimp

Goal state after:
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x + descFunLift F s y'
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)

Tactic:
dsimp

Goal state after:
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x' * descFunLift F s y
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x.mul y')

Tactic:
dsimp

Goal state after:
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x * descFunLift F s y'
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 + descFunLift F s x = descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x + 0 = descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (one.mul x) = descFunLift F s x

Tactic:
dsimp

Goal state after:
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 1 * descFunLift F s x = descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.mul one) = descFunLift F s x

Tactic:
dsimp

Goal state after:
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x * 1 = descFunLift F s x
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

Goal state after:
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 + descFunLift F s x = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s y + descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s ((x.mul y).mul z) = descFunLift F s (x.mul (y.mul z))

Tactic:
dsimp

Goal state after:
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * descFunLift F s y * descFunLift F s z =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * (descFunLift F s y + descFunLift F s z) =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ (descFunLift F s x + descFunLift F s y) * descFunLift F s z =
    descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 * descFunLift F s x = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x * 0 = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x.neg = descFunLift F s x'.neg

Tactic:
dsimp

Goal state after:
case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ -descFunLift F s x = -descFunLift F s x'
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.add y) = descFunLift F s (x'.add y)

Tactic:
dsimp

Goal state after:
case a.add_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x' + descFunLift F s y
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.add y) = descFunLift F s (x.add y')

Tactic:
dsimp

Goal state after:
case a.add_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x + descFunLift F s y'
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)

Tactic:
dsimp

Goal state after:
case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x' * descFunLift F s y
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x.mul y')

Tactic:
dsimp

Goal state after:
case a.mul_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x * descFunLift F s y'
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 + descFunLift F s x = descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x + 0 = descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (one.mul x) = descFunLift F s x

Tactic:
dsimp

Goal state after:
case a.one_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 1 * descFunLift F s x = descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.mul one) = descFunLift F s x

Tactic:
dsimp

Goal state after:
case a.mul_one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x * 1 = descFunLift F s x
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

Goal state after:
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 + descFunLift F s x = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.add_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s y + descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.mul_comm
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y : Prequotient F
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s y * descFunLift F s x
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s ((x.mul y).mul z) = descFunLift F s (x.mul (y.mul z))

Tactic:
dsimp

Goal state after:
case a.mul_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * descFunLift F s y * descFunLift F s z =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * (descFunLift F s y + descFunLift F s z) =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ (descFunLift F s x + descFunLift F s y) * descFunLift F s z =
    descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 * descFunLift F s x = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
dsimp

Goal state after:
case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s x * 0 = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ ColimitType F → ↑s.pt

Tactic:
fapply Quot.lift
  · exact descFunLift F s
  · intro x y r
    induction r with
    | refl => rfl
    | symm x y _ ih => exact ih.symm
    | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
    | map j j' f x => exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x
    | zero j => simp +instances
    | one j => simp +instances
    | neg j x => simp +instances
    | add j x y => simp +instances
    | mul j x y => simp +instances
    | neg_1 x x' r ih => dsimp; rw [ih]
    | add_1 x x' y r ih => dsimp; rw [ih]
    | add_2 x y y' r ih => dsimp; rw [ih]
    | mul_1 x x' y r ih => dsimp; rw [ih]
    | mul_2 x y y' r ih => dsimp; rw [ih]
    | zero_add x => dsimp; rw [zero_add]
    | add_zero x => dsimp; rw [add_zero]
    | one_mul x => dsimp; rw [one_mul]
    | mul_one x => dsimp; rw [mul_one]
    | neg_add_cancel x => dsimp; rw [neg_add_cancel]
    | add_comm x y => dsimp; rw [add_comm]
    | mul_comm x y => dsimp; rw [mul_comm]
    | add_assoc x y z => dsimp; rw [add_assoc]
    | mul_assoc x y z => dsimp; rw [mul_assoc]
    | left_distrib x y z => dsimp; rw [mul_add]
    | right_distrib x y z => dsimp; rw [add_mul]
    | zero_mul x => dsimp; rw [zero_mul]
    | mul_zero x => dsimp; rw [mul_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 : Matrix n n R
⊢ M.det = ∑ σ, ↑↑(sign σ) * ∏ i, M (σ i) i

Tactic:
simp [det_apply, Units.smul_def]

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
⊢ (diagonal d).det = ∏ i, d i

Tactic:
rw [det_apply']
  refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_
  · rintro σ - h2
    obtain ⟨x, h3⟩ := not_forall.1 (mt Equiv.ext h2)
    convert! mul_zero (ε σ)
    apply Finset.prod_eq_zero (mem_univ x)
    exact if_neg h3
  · simp
  · simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ f ⋯ = f ⋯ ≫ ((Functor.const J).obj Z).map g

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ f ⋯ = f ⋯ ≫ 𝟙 Z
Module: Mathlib.CategoryTheory.Filtered.Basic

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

Tactic:
obtain ⟨t, k₁t, k₂t, ht⟩ := span f₁ g₁
  obtain ⟨s, ts, hs⟩ := IsFilteredOrEmpty.cocone_maps (f₂ ≫ k₁t) (g₂ ≫ k₂t)
  simp_rw [Category.assoc] at hs
  exact ⟨s, k₁t ≫ ts, k₂t ≫ ts, by simp only [← Category.assoc, ht], hs⟩

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

Goal state before:
pp: case of_equiv
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
ι : Type u_1
inst✝ : Finite ι
k₁ k₂ : C
ι₁ ι₂ : Type u_1
e : ι₁ ≃ ι₂
IH : ∀ (j : ι₁ → C) (f : (i : ι₁) → j i ⟶ k₁) (g : (i : ι₁) → j i ⟶ k₂), ∃ s α β, ∀ (i : ι₁), f i ≫ α = g i ≫ β
j : ι₂ → C
f : (i : ι₂) → j i ⟶ k₁
g : (i : ι₂) → j i ⟶ k₂
⊢ ∃ s α β, ∀ (i : ι₂), f i ≫ α = g i ≫ β

Tactic:
obtain ⟨s, α, β, H⟩ := IH (j ∘ e) (f <| e ·) (g <| e ·)
    exact ⟨s, α, β, e.forall_congr_right.mp H⟩

Goal state after: