mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
e : m ≃ n
⊢ detp s (A.submatrix ⇑e ⇑e) = detp s A

Tactic:
by
  simp

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
⊢ Aᵀ.IsDetpBalanced a b ↔ A.IsDetpBalanced a b

Tactic:
simp [IsDetpBalanced]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ m'
eₙ : n ≃ n'
M : Matrix m n A
⊢ (reindexLinearEquiv R A eₘ eₙ) M = (reindex eₘ eₙ) M

Tactic:
by
  simp

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

Goal state before:
pp: m : Type u_2
m' : Type u_6
R : Type u_11
A : Type u_12
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
inst✝² : DecidableEq m
inst✝¹ : DecidableEq m'
inst✝ : One A
e : m ≃ m'
⊢ (reindexLinearEquiv R A e e) 1 = 1

Tactic:
by
  simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
m' : Type u_6
n' : Type u_7
o' : Type u_8
R : Type u_11
A : Type u_12
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Fintype n
inst✝ : Fintype n'
eₘ : m ≃ m'
eₙ : n ≃ n'
eₒ : o ≃ o'
M : Matrix m n A
N : Matrix n o A
⊢ (reindexLinearEquiv R A eₘ eₙ) M * (reindexLinearEquiv R A eₙ eₒ) N = (reindexLinearEquiv R A eₘ eₒ) (M * N)

Tactic:
by
  simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_11
A : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring A
inst✝ : Algebra R A
e : m ≃ n
M : Matrix m m A
⊢ (reindexAlgEquiv R A e) M = (reindex e e) M

Tactic:
by
  simp

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 B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
⊢ ∀ a ∈ {x ∈ ofSign t | x j = k}, ∀ a_2 ∈ ofSign s, IsAddUnit ((∏ k, A k (a_2 k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (a k)))

Tactic:
σ

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
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
⊢ σ ∈ {x ∈ ofSign t | x j = k} → ∀ a ∈ ofSign s, IsAddUnit ((∏ k, A k (a k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))
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.IsColimitCore
c' : F.CoconeTypes
j : J
⊢ (Equiv.ulift.toFun ∘ hc.desc (c'.postcomp ⇑Equiv.ulift.symm)) ∘ c.ι j = c'.ι j

Tactic:
rw [Function.comp_assoc, hc.fac]
    rfl

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

Goal state before:
pp: case neg
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (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
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < 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' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
⊢ N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j

Tactic:
by_cases hik2 : k < i

Goal state after:
case pos
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (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
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < 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' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : k < i
⊢ N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j

case neg
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (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
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < 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' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
⊢ N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
⊢ ∀ (c : Fin n → R),
    (∀ (i : Fin n), k < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (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:
refine Fin.induction ?_ (fun k ih => ?_) k <;> intro c hc M N h0 hsucc
  · congr
    ext i j
    refine Fin.cases (h0 j) (fun i => ?_) i
    rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]
  set M' := updateRow M k.succ (N k.succ) with hM'
  have hM : M = updateRow M' k.succ (M' k.succ + c k • M (Fin.castSucc k)) := by
    ext i j
    by_cases hi : i = k.succ
    · simp [hi, hM', hsucc, updateRow_self]
    rw [updateRow_ne hi, hM', updateRow_ne hi]
  have k_ne_succ : (Fin.castSucc k) ≠ k.succ := Fin.castSucc_lt_succ.ne
  have M_k : M (Fin.castSucc k) = M' (Fin.castSucc k) := (updateRow_ne k_ne_succ).symm
  rw [hM, M_k, det_updateRow_add_smul_self M' k_ne_succ.symm, ih (Function.update c k 0)]
  · intro i hi
    rw [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff] at hi
    rw [Function.update_apply]
    split_ifs with hik
    · rfl
    exact hc _ (Fin.succ_lt_succ_iff.mpr (lt_of_le_of_ne hi (Ne.symm hik)))
  · rwa [hM', updateRow_ne (Fin.succ_ne_zero _).symm]
  intro i j
  rw [Function.update_apply]
  split_ifs with hik
  · rw [zero_mul, add_zero, hM', hik, updateRow_self]
  rw [hM', updateRow_ne ((Fin.succ_injective _).ne hik), hsucc]
  by_cases hik2 : k < i
  · simp [hc i (Fin.succ_lt_succ_iff.mpr hik2)]
  rw [updateRow_ne]
  apply ne_of_lt
  rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : ↑(G F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a)⁻¹ *
        Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a =
      1

Tactic:
clear x

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a)⁻¹ *
        Quot.mk ((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).ColimitTypeRel a =
      1
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : ↑(R F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    0 * Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a = 0

Tactic:
clear x

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    0 * Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a = 0
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : ↑(R F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a * 0 = 0

Tactic:
clear x

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a * 0 = 0
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
z : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
      (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z) =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z

Tactic:
obtain ⟨j₃, z⟩ := z

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
      (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩) =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
z : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
⊢ (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩) *
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z

Tactic:
obtain ⟨j₃, z⟩ := z

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
⊢ (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩) *
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩ =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₁, x⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩ +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₂, y⟩ *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨j₃, z⟩
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✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
⊢ c • x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}

Tactic:
let := Classical.decEq ι

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
⊢ c • x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFilteredOrEmpty J
D : Cocone F
hD : IsColimit D
k j : J
y : ToType (F.obj j)
⊢ ∃ j_1 x y_1, (ConcreteCategory.hom (D.ι.app j_1)) y_1 = (ConcreteCategory.hom (D.ι.app j)) y

Tactic:
refine ⟨IsFiltered.max k j, IsFiltered.leftToMax _ _, F.map (IsFiltered.rightToMax _ _) y, ?_⟩

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFilteredOrEmpty J
D : Cocone F
hD : IsColimit D
k j : J
y : ToType (F.obj j)
⊢ (ConcreteCategory.hom (D.ι.app (IsFiltered.max k j))) ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax k j))) y) =
    (ConcreteCategory.hom (D.ι.app j)) y
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 G : J ⥤ K ⥤ C
η : F ⟶ G
⊢ colim.map η ≫ (colimitIsoFlipCompColim G).hom =
    (colimitIsoFlipCompColim F).hom ≫ (flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj colim).map η

Tactic:
by
    ext k
    apply colimit_obj_ext
    intro j
    simp [comp_evaluation, ← NatTrans.comp_app_assoc _ (colimMap η)]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ C₃ ⥤ C₄
f : G ⟶ G'
⊢ (bifunctorComp₁₂FunctorObj F₁₂).map f ≫
      {
        app := fun X₁ ↦
          { app := fun X₂ ↦ { app := fun X₃ ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun X₁ ↦
          { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ },
        naturality := ⋯ } ≫
      (bifunctorComp₁₂FunctorObj F₁₂').map f

Tactic:
ext X₁ X₂ X₃
    dsimp
    simp only [← NatTrans.comp_app, NatTrans.naturality]

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
X✝ Y✝ : C
⊢ X✝ ◁ 𝟙 Y✝ = 𝟙 (X✝ ⊗ Y✝)

Tactic:
simp [← id_tensorHom, ← id_tensorHom_id]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
⊢ inv f ▷ Z ≫ f ▷ Z = 𝟙 (Y ⊗ Z)

Tactic:
rw [← comp_whiskerRight, IsIso.inv_hom_id, id_whiskerRight]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f = (ρ_ X).inv ≫ f ▷ 𝟙_ C ≫ (ρ_ Y).hom

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ f ≫ g ⊗ₘ 𝟙 Z = (f ⊗ₘ 𝟙 Z) ≫ (g ⊗ₘ 𝟙 Z)

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ 𝟙 Z ⊗ₘ f ≫ g = (𝟙 Z ⊗ₘ f) ≫ (𝟙 Z ⊗ₘ g)

Tactic:
by
  simp

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

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

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

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ p ◁ Iso.refl f ≪≫ η_f = η_f

Tactic:
by
  simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
    μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g h : C
α : f ≅ g
β : g ≅ h
⊢ (α ≪≫ β).hom = (α ≪≫ β).hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g h i j : C
α : f ≅ g
β : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
⊢ α.hom ≫ β.hom ≫ η ≫ ηs = (α ≪≫ β).hom ≫ η ≫ ηs

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g : C
η : f ⟶ g
⊢ η = (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
α : g ≅ h
⊢ (f ◁ᵢ α).hom = (f ◁ᵢ α).hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
α : f ≅ g
h : C
⊢ (α ▷ᵢ h).hom = (α ▷ᵢ h).hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
η : f ⟶ g
h : C
⊢ η ▷ h = (Iso.refl (f ⊗ h)).hom ≫ η ▷ h ≫ (Iso.refl (g ⊗ h)).hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η : f ⟶ g
θ : h ⟶ i
⊢ η ⊗ₘ θ = (Iso.refl (f ⊗ h)).hom ≫ (η ⊗ₘ θ) ≫ (Iso.refl (g ⊗ i)).hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
α : f ≅ g
β : h ≅ i
⊢ (α ⊗ᵢ β).hom = (α ⊗ᵢ β).hom

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
η₁ : g ⊗ g' ⟶ h ⊗ g'
ηs₁ : h ⊗ g' ⟶ i ⊗ g'
η₂ : g ⊗ g' ⟶ i ⊗ g'
η₃ : f ⊗ f' ⟶ i ⊗ g'
e_η₁ : ((Iso.refl g).hom ≫ η ≫ (Iso.refl h).hom) ▷ g' = η₁
e_ηs₁ : ηs ▷ g' = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ⊗ᵢ β).hom ≫ η₂ = η₃
⊢ α.hom ≫ η ≫ ηs ⊗ₘ β.hom = η₃

Tactic:
simp_all [MonoidalCategory.tensorHom_def']

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inl (G.map f) (G.map g) ≫ (iso G f g).hom = G.map (pushout.inl f g)

Tactic:
by
  simp

Goal state after: