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 d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
⊢ d (c x) = d x ↔ c x = x

Tactic:
EmbeddingLike.apply_eq_iff_eq

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
⊢ c x = x ↔ c x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inl
α : 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 ∈ σ.cycleFactorsFinset
⊢ (τ * σ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset ∪ σ.cycleFactorsFinset \ {f}

pp: case refine_3.inl
α : 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 ∈ σ.cycleFactorsFinset
⊢ f ∉ τ.cycleFactorsFinset

Tactic:
mul_assoc,

Goal state after:
case refine_3.inl
α : 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 ∈ σ.cycleFactorsFinset
⊢ (τ * (σ * f⁻¹)).cycleFactorsFinset = τ.cycleFactorsFinset ∪ σ.cycleFactorsFinset \ {f}

case refine_3.inl
α : 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 ∈ σ.cycleFactorsFinset
⊢ f ∉ τ.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : g.support = {a, g a, g (g a)}
⊢ [a, g a, g (g a)].Nodup

Tactic:
suffices g.support.card = 3 by grind

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : g.support = {a, g a, g (g a)}
⊢ #g.support = 3
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inr
α : 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 ∈ τ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset \ {f}

pp: case refine_3.inr
α : 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 ∈ τ.cycleFactorsFinset
⊢ f ∉ σ.cycleFactorsFinset

Tactic:
mul_assoc,

Goal state after:
case refine_3.inr
α : 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 ∈ τ.cycleFactorsFinset
⊢ (σ * (τ * f⁻¹)).cycleFactorsFinset = σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset \ {f}

case refine_3.inr
α : 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 ∈ τ.cycleFactorsFinset
⊢ f ∉ σ.cycleFactorsFinset
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
⊢ f m = 0

Tactic:
classical
    have : (0 : R) • (0 : M₁ i) = 0 := by simp
    rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]

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
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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M
⊢ (domDomCongr σ.symm (domDomCongr σ f)) x✝ = f x✝

Tactic:
simp [Function.comp_def]

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
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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
x✝ : ι' → M
⊢ (domDomCongr σ (domDomCongr σ.symm m)) x✝ = m x✝

Tactic:
simp [Function.comp_def]

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
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
M₂ : Type u_10
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
M₃ : Type u_11
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_12
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M
⊢ (domDomCongr σ.symm (domDomCongr σ f)) x✝ = f x✝

Tactic:
simp [Function.comp_def]

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
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
M₂ : Type u_10
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
M₃ : Type u_11
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_12
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
x✝ : ι' → M
⊢ (domDomCongr σ (domDomCongr σ.symm m)) x✝ = m x✝

Tactic:
simp [Function.comp_def]

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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
c : R
⊢ c ^ Fintype.card n * a * detp 1 A + c ^ Fintype.card n * b * detp (-1) A =
    c ^ Fintype.card n * b * detp 1 A + c ^ Fintype.card n * a * detp (-1) A

Tactic:
mul_assoc,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
c : R
⊢ c ^ Fintype.card n * (a * detp 1 A) + c ^ Fintype.card n * (b * detp (-1) A) =
    c ^ Fintype.card n * (b * detp 1 A) + c ^ Fintype.card n * (a * detp (-1) A)
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 : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
s t : ℤˣ
⊢ ∀ (i : Perm n), i ∈ ofSign 1 ↔ (Equiv.mulRight (swap p q)) i ∈ ofSign (-1)

Tactic:
simp [hpq]

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
inst✝ : Subsingleton n
A : Matrix n n R
k : n
⊢ A.det = A k k

Tactic:
have := uniqueOfSubsingleton k
  convert! det_unique A

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

Goal state before:
pp: case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → Nonempty (X ⟶ S)
⊢ ∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ ∅ → f ≫ T mY = T mX

Tactic:
exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩

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
σ : Perm n
M : Matrix n n R
⊢ (M.submatrix id ⇑σ).det = ↑↑(sign σ) * M.det

Tactic:
← det_transpose,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
σ : Perm n
M : Matrix n n R
⊢ (M.submatrix id ⇑σ)ᵀ.det = ↑↑(sign σ) * M.det
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
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ M.det = 0

Tactic:
← det_transpose,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ Mᵀ.det = 0
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
j : n
u v : n → R
⊢ (M.updateCol j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det

Tactic:
← det_transpose,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ (M.updateCol j (u + v))ᵀ.det = (M.updateCol j u).det + (M.updateCol j v).det
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
j : n
s : R
u : n → R
⊢ (M.updateCol j (s • u)).det = s * (M.updateCol j u).det

Tactic:
← det_transpose,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ (M.updateCol j (s • u))ᵀ.det = s * (M.updateCol j u).det
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
j : n
s : R
u : n → R
⊢ ((s • M).updateCol j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

Tactic:
← det_transpose,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ ((s • M).updateCol j u)ᵀ.det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det
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
j : n
c : n → R
⊢ (A.updateCol j fun k ↦ ∑ i, c i • A k i).det = c j • A.det

Tactic:
← det_transpose,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ (A.updateCol j fun k ↦ ∑ i, c i • A k i)ᵀ.det = c j • A.det
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
i j : n
hij : i ≠ j
⊢ (A.updateCol i fun k ↦ A k i + A k j).det = A.det

Tactic:
← det_transpose,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (A.updateCol i fun k ↦ A k i + A k j)ᵀ.det = A.det
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
i j : n
hij : i ≠ j
c : R
⊢ (A.updateCol i fun k ↦ A k i + c • A k j).det = A.det

Tactic:
← det_transpose,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (A.updateCol i fun k ↦ A k i + c • A k j)ᵀ.det = A.det
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → Nonempty (S ⟶ X)
⊢ ∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ ∅ → T mX ≫ f = T mY

Tactic:
exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ Function.Bijective (f ∘ F.descColimitType c)

Tactic:
convert! hc'.bijective

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
c' : F.CoconeTypes
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ f ∘ F.descColimitType c = F.descColimitType c'
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

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

Tactic:
by
  rw [isColimit_eq_iff _ ht]
  constructor
  · rintro ⟨k, f, g, h⟩
    refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩
    conv_rhs => rw [IsFiltered.coeq_condition]
    simp [h]
  · rintro ⟨j, f, h⟩
    exact ⟨j, f, f, h⟩

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
C : Matrix n m R
D : Matrix n n R
⊢ (fromBlocks A 0 C D).det = A.det * D.det

Tactic:
← det_transpose,

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
C : Matrix n m R
D : Matrix n n R
⊢ (fromBlocks A 0 C D)ᵀ.det = A.det * D.det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    -1 * ↑↑(sign i.cycleRange) * A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det

Tactic:
mul_assoc,

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    -1 * ↑↑(sign i.cycleRange) * (A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    -1 * ↑↑(sign i.cycleRange) * (A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det)

Tactic:
mul_assoc,

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    -1 * (↑↑(sign i.cycleRange) * (A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ∑ x, (-1) ^ ↑i * (-1) ^ ↑x * A i x * (A.submatrix i.succAbove x.succAbove).det

Tactic:
mul_assoc,

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ∑ x, (-1) ^ ↑i * ((-1) ^ ↑x * (A i x * (A.submatrix i.succAbove x.succAbove).det))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * A.submatrix (⇑i.cycleRange⁻¹) id 0 j *
      ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)

Tactic:
mul_assoc,

Goal state after:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j *
      (A.submatrix (⇑i.cycleRange⁻¹) id 0 j * ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det) =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ A.det = ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
← det_transpose,

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ Aᵀ.det = ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ (↑i + ↑j) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
← det_transpose,

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ (↑i + ↑j) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
    (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
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
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ { app := fun Y_1 ↦ colimit.ι (F.flip.obj Y_1) Y, naturality := ⋯ } =
    { app := fun Y ↦ colimit.ι (F.flip.obj Y) X, naturality := ⋯ } ≫ ((const J).obj (F.flip ⋙ colim)).map f

Tactic:
by
      ext x
      simp only [Functor.const_obj_obj, Functor.comp_obj, colim_obj, NatTrans.comp_app,
        Functor.const_obj_map, Category.comp_id]
      change (F.flip.obj x).map f ≫ _ = _
      rw [colimit.w]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategoryStruct C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)
id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), 𝟙 X ⊗ₘ f = X ◁ f
tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), f ⊗ₘ 𝟙 Y = f ▷ Y
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)
leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (𝟙_ C) ⊗ₘ f) ≫ (λ_ Y).hom = (λ_ X).hom ≫ f
rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (𝟙_ C)) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f
pentagon :
  ∀ (W X Y Z : C),
    ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).hom) =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
triangle : ∀ (X Y : C), (α_ X (𝟙_ C) Y).hom ≫ (𝟙 X ⊗ₘ (λ_ Y).hom) = (ρ_ X).hom ⊗ₘ 𝟙 Y
W✝ X✝ Y✝ Z✝ : C
⊢ (α_ W✝ X✝ Y✝).hom ▷ Z✝ ≫ (α_ W✝ (X✝ ⊗ Y✝) Z✝).hom ≫ W✝ ◁ (α_ X✝ Y✝ Z✝).hom =
    (α_ (W✝ ⊗ X✝) Y✝ Z✝).hom ≫ (α_ W✝ X✝ (Y✝ ⊗ Z✝)).hom

Tactic:
simp [← id_tensorHom, ← tensorHom_id, pentagon]

Goal state after: