mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f fun j ↦ if h : P j then update z i a ⟨j, h⟩ else z✝ ⟨j, h⟩

Tactic:
]

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✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f fun j ↦ if h : P j then update z i a ⟨j, h⟩ else z✝ ⟨j, h⟩
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
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i =
    ∑ p ∈ univ.pi fun x ↦ univ, ∏ x ∈ univ.attach, ↑↑(sign (p ↑x ⋯)) * ∏ i, M (↑x) ((p ↑x ⋯) i) i

Tactic:
]

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
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i =
    ∑ p ∈ univ.pi fun x ↦ univ, ∏ x ∈ univ.attach, ↑↑(sign (p ↑x ⋯)) * ∏ i, M (↑x) ((p ↑x ⋯) i) i
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
x : t.pt
⊢ (hom m) ((hom (t.ι.app (α x))) (f x)) = (hom (s.ι.app (α x))) (f x)

Tactic:
]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
x : t.pt
⊢ (hom m) ((hom (t.ι.app (α x))) (f x)) = (hom (s.ι.app (α x))) (f x)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) a)

Tactic:
]

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✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝¹ : DecidablePred P
z✝ : (i : { a // ¬P a }) → M₁ ↑i
inst✝ : DecidableEq { a // P a }
z : (i : { a // P a }) → M₁ ↑i
i : { a // P a }
c : R
a : M₁ ↑i
⊢ f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) (c • a)) =
    c • f (update (fun j ↦ if h : P j then z ⟨j, h⟩ else z✝ ⟨j, h⟩) (↑i) a)
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
⊢ m = ↾fun x ↦ (hom (s.ι.app (α x))) (f x)

Tactic:
ext x
        dsimp
        nth_rw 1 [hf x]
        simp [← hm, comp_apply]

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
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
⊢ ∑ x ∈ preserving_snd, ↑↑(sign x) * ∏ i, blockDiagonal M (x i) i =
    ∑ x, ∏ x_1, ↑↑(sign (x x_1 ⋯)) * ∏ x_2, M x_1 ((x x_1 ⋯) x_2) x_2

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
⊢ ∀ x ∈ univ, x ∉ preserving_snd → ↑↑(sign x) * ∏ i, blockDiagonal M (x i) i = 0

Tactic:
]

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
⊢ ∑ x ∈ preserving_snd, ↑↑(sign x) * ∏ i, blockDiagonal M (x i) i =
    ∑ x, ∏ x_1, ↑↑(sign (x x_1 ⋯)) * ∏ x_2, M x_1 ((x x_1 ⋯) x_2) x_2

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
⊢ ∀ x ∈ univ, x ∉ preserving_snd → ↑↑(sign x) * ∏ i, blockDiagonal M (x i) i = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_1
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
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∀ (x : n × o), ((prodCongrLeft fun k ↦ σ k ⋯) x).2 = x.2

Tactic:
]

Goal state after:
case refine_1
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
σ : (a : o) → a ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∀ (x : n × o), ((prodCongrLeft fun k ↦ σ k ⋯) x).2 = x.2
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
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i : J) (x y : (fun X ↦ X) (F.obj i)),
    (hom (t.ι.app i)) x = (hom (t.ι.app i)) y → ∃ k f, (hom (F.map f)) x = (hom (F.map f)) y
i j : J
xi : (fun X ↦ X) (F.obj i)
xj : (fun X ↦ X) (F.obj j)
h : (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj
⊢ ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj

Tactic:
by
    obtain ⟨k, g, hg⟩ := hinj (IsFiltered.max i j) (F.map (IsFiltered.leftToMax i j) xi)
      (F.map (IsFiltered.rightToMax i j) xj)
      (by set_option backward.isDefEq.respectTransparency true in simp_all)
    exact ⟨k, IsFiltered.leftToMax i j ≫ g, IsFiltered.rightToMax i j ≫ g, by simpa using hg⟩

Goal state after:
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
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map (fl ≫ n))) ((hom (F.map g)) y.snd) = (hom (F.map (fl ≫ n))) ((hom (F.map g)) y.snd)

Tactic:
]

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
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
σ : (a : o) → a ∈ univ → Perm n
ha₁✝ : σ ∈ univ
σ' : (a : o) → a ∈ univ → Perm n
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k ↦ σ k ⋯) = prodCongrLeft fun k ↦ σ' k ⋯
x✝ : o
hx : x✝ ∈ univ
k✝ k : n
x : o
⊢ (prodCongrLeft fun k ↦ σ' k ⋯) (k, x) = (prodCongrLeft fun k ↦ σ' k ⋯) (k, x)

Tactic:
]

Goal state after:
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
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map ((f' ≫ gl) ≫ n))) y.snd = (hom (F.map ((f' ≫ gl) ≫ n))) y.snd

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι'
m : (i : ι') → M₁ (σ.symm i)
i : ι'
this : DecidableEq ι := σ.decidableEq
⊢ ∀ (x y : M₁ (σ.symm (σ (σ.symm i)))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x) +
        (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) y)

Tactic:
]

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✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι'
m : (i : ι') → M₁ (σ.symm i)
i : ι'
this : DecidableEq ι := σ.decidableEq
⊢ ∀ (x y : M₁ (σ.symm (σ (σ.symm i)))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x) +
        (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) y)
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
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map (gl ≫ n))) ((hom (F.map g')) z.snd) = (hom (F.map (gl ≫ n))) ((hom (F.map g')) z.snd)

Tactic:
]

Goal state after:
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σ : ∀ (x : n × o), (σ x).2 = x.2
⊢ ∃ a, ∃ (_ : a ∈ univ), (prodCongrLeft fun k ↦ a k ⋯) = σ

Tactic:
]

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.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✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι'
m : (i : ι') → M₁ (σ.symm i)
i : ι'
c : R
this : DecidableEq ι := σ.decidableEq
⊢ ∀ (x : M₁ (σ.symm (σ (σ.symm i)))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (c • x)) =
      c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x)

Tactic:
]

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✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι'
m : (i : ι') → M₁ (σ.symm i)
i : ι'
c : R
this : DecidableEq ι := σ.decidableEq
⊢ ∀ (x : M₁ (σ.symm (σ (σ.symm i)))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) (c • x)) =
      c • (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm) (update m (σ (σ.symm i)) x)
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩ → Relation.EqvGen (FilteredColimit.Rel F) ⟨j, x⟩ ⟨j', y⟩

Tactic:
]

Goal state after:
case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩ → Relation.EqvGen (FilteredColimit.Rel F) ⟨j, x⟩ ⟨j', y⟩
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
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ Relation.EqvGen F.ColimitTypeRel ⟨i, xi⟩ ⟨j, xj⟩ ↔ Relation.EqvGen F.ColimitTypeRel ⟨i, xi⟩ ⟨j, xj⟩

Tactic:
]

Goal state after:
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 : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app i)) xi) =
      (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app j)) xj) ↔
    (hom ((colimitCocone F).ι.app i)) xi = (hom ((colimitCocone F).ι.app j)) xj

Tactic:
]

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app i)) xi) =
      (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app j)) xj) ↔
    (hom ((colimitCocone F).ι.app i)) xi = (hom ((colimitCocone F).ι.app j)) xj
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✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
⊢ ∀ (x y : M₁ (σ.symm (σ i))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x) +
        (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) y)

Tactic:
]

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✝¹² : Semiring R
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : (i : ι) → Module R (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Semiring S
inst✝⁶ : Module S M₂
inst✝⁵ : SMulCommClass R S M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module S M₃
inst✝² : Module R M₃
inst✝¹ : SMulCommClass R S M₃
ι' : Type u_1
σ : ι ≃ ι'
f : MultilinearMap R (fun i ↦ M₁ (σ.symm i)) M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
this : DecidableEq ι' := σ.symm.decidableEq
⊢ ∀ (x y : M₁ (σ.symm (σ i))),
    (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) (x + y)) =
      (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) x) +
        (⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ)) (update m (σ.symm (σ i)) y)
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 : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app i)) xi) =
      (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app j)) xj) ↔
    (hom ((colimitCocone F).ι.app i)) xi = (hom ((colimitCocone F).ι.app j)) xj

Tactic:
convert! Iff.rfl

Goal state after:
case e'_2.e'_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : (fun X ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i) = (colimitCocone F).pt
⊢ (hom ((colimitCocone F).ι.app i)) xi =
    (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app i)) xi)

case e'_2.e'_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : (fun X ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i) = (colimitCocone F).pt
⊢ (hom ((colimitCocone F).ι.app j)) xj =
    (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app j)) xj)
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
⊢ (∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y) ↔ ∃ j f, (hom (F.map f)) x = (hom (F.map f)) y

Tactic:
]

Goal state after:
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
⊢ (∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y) ↔ ∃ j f, (hom (F.map f)) x = (hom (F.map f)) y