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

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

Tactic:
rw [← hf.right _ (mem_support.mpr hfx)] at hx

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : f x = x
hfx : ¬f x = x
⊢ σ (f⁻¹ x) = x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
rw [← hf.right _ (mem_support.mpr hfx)] at hx

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : f x = x
hfx : ¬f x = x
⊢ τ (f⁻¹ x) = 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 : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : 0 • 0 = 0
⊢ f m = 0

Tactic:
← update_eq_self i m,

Goal state after:
R : Type uR
ι : Type uι
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₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : 0 • 0 = 0
⊢ f (update m i (m i)) = 0
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
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι]→ₗ[R] N
g✝ g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
f g : M [⋀^ι]→ₗ[R] N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨⟨_, _, _⟩, _⟩

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
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f f' : M [⋀^ι]→ₗ[R] N
g✝ g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
g : M [⋀^ι]→ₗ[R] N
toFun✝ : (ι → M) → N
map_update_add'✝ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
    toFun✝ (update m i (x + y)) = toFun✝ (update m i x) + toFun✝ (update m i y)
map_update_smul'✝ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), toFun✝ (update m i (c • x)) = c • toFun✝ (update m i x)
map_eq_zero_of_eq'✝ :
  ∀ (v : ι → M) (i j : ι),
    v i = v j →
      i ≠ j →
        { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝ }.toFun v = 0
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝,
        map_eq_zero_of_eq' := map_eq_zero_of_eq'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_update_add' := map_update_add'✝, map_update_smul' := map_update_smul'✝,
      map_eq_zero_of_eq' := map_eq_zero_of_eq'✝ } =
    g
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case e'_3.a
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
x✝ : Perm n
a✝ : x✝ ∈ ofSign (sign (swap none i) * s)
⊢ ∏ k, A.submatrix some (⇑(swap none i) ∘ some) k (x✝ k) = ∏ k ∈ {none}ᶜ, A k ((decomposeOption.symm (i, x✝)) k)

Tactic:
convert (prod_image (Option.some_injective n).injOn).symm

Goal state after:
case e'_2.a
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
x✝¹ : Perm n
a✝¹ : x✝¹ ∈ ofSign (sign (swap none i) * s)
x✝ : n
a✝ : x✝ ∈ univ
⊢ A.submatrix some (⇑(swap none i) ∘ some) x✝ (x✝¹ x✝) = A (some x✝) ((decomposeOption.symm (i, x✝¹)) (some x✝))

case e'_3.h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
x✝ : Perm n
a✝ : x✝ ∈ ofSign (sign (swap none i) * s)
⊢ {none}ᶜ = Finset.image some univ
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case e'_3.h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
x✝ : Perm n
a✝ : x✝ ∈ ofSign (sign (swap none i) * s)
⊢ {none}ᶜ = Finset.image some univ

Tactic:
· apply SetLike.coe_injective; simp [← Set.compl_range_some]

Goal state after:
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 + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)

Tactic:
add_assoc

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: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x * y) = descFun F s x * descFun F s y

Tactic:
by exact Quot.induction_on₂ x y fun a b => rfl

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

Goal state before:
pp: case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x✝ : ↑(colimitCocone F).pt
x : Prequotient F
ih : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x.neg) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x.neg)

Tactic:
| neg x ih =>

Goal state after:
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 + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)

Tactic:
add_assoc

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.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
add_assoc

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
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
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
| ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) +
    (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
add_assoc

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
| ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) +
    (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x * y) = descFun F s x * descFun F s y

Tactic:
by exact Quot.induction_on₂ x y fun a b => rfl

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

Goal state before:
pp: case neg
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x✝ : ↑(colimitCocone F).pt
x : Prequotient F
ih : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x.neg) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x.neg)

Tactic:
| neg x ih =>

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

Goal state before:
pp: case h.inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty (X ⟶ S')
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ Nonempty (Y ⟶ max X S')

Tactic:
· exact ⟨(w' (Finset.mem_of_mem_insert_of_ne mY h)).some ≫ rightToMax _ _⟩

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 := ⋯
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) := ⋯
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.obj j, ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩⟩ ∈ H

Tactic:
simp only [O, H, Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq,
    true_and, exists_and_left]

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'
⊢ ∃ a, F.obj a = F.obj j ∧ ∃ x x_1, ⟨F.obj x, ⟨⋯, ⟨⋯, F.map x_1⟩⟩⟩ ≍ ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩
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
α : Type u_3
inst✝³ : Monoid α
inst✝² : MulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ (c • A).det = c ^ Fintype.card n • A.det

Tactic:
← smul_one_smul R c A,

Goal state after:
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
R : Type v
inst✝⁴ : CommRing R
α : Type u_3
inst✝³ : Monoid α
inst✝² : MulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ ((c • 1) • A).det = c ^ Fintype.card n • A.det
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σ : σ ∈ preserving_snd
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ

Tactic:
rw [mem_preserving_snd] at hσ

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
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ
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
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
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : σ ∉ preserving_snd
⊢ ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i = 0

Tactic:
rw [mem_preserving_snd] at hσ

Goal state after:
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
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (σ x).2 = x.2
⊢ ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i = 0
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x x' y : (j : J) × ↑(F.obj j)
h : (F ⋙ forget MonCat).ColimitTypeRel x x'
⊢ colimitMulAux F x y = colimitMulAux F x' y

Tactic:
apply colimitMulAux_eq_of_rel_left

Goal state after:
case refine_2
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x✝ y✝ : M F
x x' y : (j : J) × ↑(F.obj j)
h : (F ⋙ forget MonCat).ColimitTypeRel x x'
⊢ Types.FilteredColimit.Rel (F ⋙ forget MonCat) x x'
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z : M₂
⊢ MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

Tactic:
rw [← mkPiRing_zero, mkPiRing_eq_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ F.map (𝟙 X ×ₘ f ≫ g) = F.map (𝟙 X ×ₘ f) ≫ F.map (𝟙 X ×ₘ g)

Tactic:
by simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C × D ⥤ E
X✝ Y✝ : C
f : X✝ ⟶ Y✝
Y Y' : D
g : Y ⟶ Y'
⊢ { obj := fun Y ↦ F.obj (X✝, Y), map := fun {X Y} g ↦ F.map (𝟙 X✝ ×ₘ g), map_id := ⋯, map_comp := ⋯ }.map g ≫
      F.map (f ×ₘ 𝟙 Y') =
    F.map (f ×ₘ 𝟙 Y) ≫
      { obj := fun Y ↦ F.obj (Y✝, Y), map := fun {X Y} g ↦ F.map (𝟙 Y✝ ×ₘ g), map_id := ⋯, map_comp := ⋯ }.map g

Tactic:
by simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
j : J
⊢ { app := fun k ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π ((evaluation K C).obj k) }, naturality := ⋯ } ≫
      c.π.app j =
    s.π.app j

Tactic:
ext k

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
j : J
k : K
⊢ ({ app := fun k ↦ (t k).lift { pt := s.pt.obj k, π := whiskerRight s.π ((evaluation K C).obj k) }, naturality := ⋯ } ≫
          c.π.app j).app
      k =
    (s.π.app j).app k
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → LimitCone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
⊢ ((const J).obj
            { obj := fun k ↦ (c k).cone.pt,
              map := fun {k₁ k₂} f ↦ (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f },
              map_id := ⋯, map_comp := ⋯ }).map
        g ≫
      { app := fun k ↦ (c k).cone.π.app j₂, naturality := ⋯ } =
    { app := fun k ↦ (c k).cone.π.app j₁, naturality := ⋯ } ≫ F.map g

Tactic:
ext k

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → LimitCone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
k : K
⊢ (((const J).obj
                { obj := fun k ↦ (c k).cone.pt,
                  map := fun {k₁ k₂} f ↦
                    (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f },
                  map_id := ⋯, map_comp := ⋯ }).map
            g ≫
          { app := fun k ↦ (c k).cone.π.app j₂, naturality := ⋯ }).app
      k =
    ({ app := fun k ↦ (c k).cone.π.app j₁, naturality := ⋯ } ≫ F.map g).app k
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫
      { app := fun k ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι ((evaluation K C).obj k) },
        naturality := ⋯ } =
    s.ι.app j

Tactic:
ext k

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cocone F
t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)
s : Cocone F
j : J
k : K
⊢ (c.ι.app j ≫
          { app := fun k ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι ((evaluation K C).obj k) },
            naturality := ⋯ }).app
      k =
    (s.ι.app j).app k
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → ColimitCocone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
⊢ F.map g ≫ { app := fun k ↦ (c k).cocone.ι.app j₂, naturality := ⋯ } =
    { app := fun k ↦ (c k).cocone.ι.app j₁, naturality := ⋯ } ≫
      ((const J).obj
            { obj := fun k ↦ (c k).cocone.pt,
              map := fun {k₁ k₂} f ↦
                (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι },
              map_id := ⋯, map_comp := ⋯ }).map
        g

Tactic:
ext k

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : (k : K) → ColimitCocone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
k : K
⊢ (F.map g ≫ { app := fun k ↦ (c k).cocone.ι.app j₂, naturality := ⋯ }).app k =
    ({ app := fun k ↦ (c k).cocone.ι.app j₁, naturality := ⋯ } ≫
          ((const J).obj
                { obj := fun k ↦ (c k).cocone.pt,
                  map := fun {k₁ k₂} f ↦
                    (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι },
                  map_id := ⋯, map_comp := ⋯ }).map
            g).app
      k