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

Goal state before:
pp: case neg
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
h✝¹ : ¬x = j
h✝ : ¬x = k
⊢ ↑(x + 1) = ↑(x + 1)

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
h : ¬x = k
⊢ ↑x + 1 < n

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
x : α
hx : x ∈ p.support
⊢ f x ≠ x

Tactic:
← h.right x hx,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
x : α
hx : x ∈ p.support
⊢ p x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
m : ℕ
h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3
hm : m ∈ σ.cycleType.erase n
⊢ ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
swap_apply_left,

Goal state after:
case pos.inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
⊢ g (g a) = (swap a (g a)) (g (g a))
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

Tactic:
exact fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))

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
ι : Type u_7
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M₂
⊢ (f.compLinearMap 0) x✝ = 0 x✝

Tactic:
simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]

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

Goal state before:
pp: case neg
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : ¬j = i
⊢ (insert i s).piecewise m m' j = s.piecewise m m'' j

Tactic:
by_cases h' : j ∈ s <;> simp [m'', h, h']

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

Goal state before:
pp: case pos
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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
i : ι
hi : i = i₀
⊢ C i ⊆ A i

Tactic:
rw [hi]
      simp only [C, hj₂, Finset.singleton_subset_iff, update_self]

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
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
⊢ (A * adjp s A) i i = detp s A

Tactic:
simp_rw [mul_apply, adjp_apply, mul_sum, detp, ← key]

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
⊢ ∑ x, ∑ i_1 ∈ ofSign s with i_1 i = x, A i x * ∏ k ∈ {i}ᶜ, A k (i_1 k) =
    ∑ j, ∑ σ ∈ ofSign s with σ i = j, ∏ k, A k (σ k)
Module: Mathlib.CategoryTheory.Filtered.Basic

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

Tactic:
obtain ⟨s, ls, l's, hs₁, hs₂⟩ := bowtie g₁ (f₁ ≫ k₁l) g₂ (f₄ ≫ k₂l)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ ∃ s α β γ, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case empty
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
i j : n
⊢ B i j + 0 * B k j = B i j

Tactic:
zero_mul,

Goal state after:
case empty
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
i j : n
⊢ B i j + 0 = B i j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < 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
i✝ j : Fin n.succ
i : Fin n
⊢ N i.succ j + 0 * M i.castSucc j = N i.succ j

Tactic:
zero_mul,

Goal state after:
case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < 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
i✝ j : Fin n.succ
i : Fin n
⊢ N i.succ j + 0 = N i.succ j
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
j : J
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j

Tactic:
rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι]

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

Goal state before:
pp: 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
⊢ M' i.succ j = N i.succ j + 0 * M' i.castSucc j

Tactic:
zero_mul,

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
⊢ M' i.succ j = N i.succ j + 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: 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
⊢ M' i.succ j = N i.succ j + 0 * M' i.castSucc j

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
⊢ M' i.succ j = N i.succ j + c i * M' i.castSucc j

Tactic:
· rw [zero_mul, add_zero, hM', hik, updateRow_self]

Goal state after:
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
⊢ M' i.succ j = N i.succ j + c i * M' i.castSucc j
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:
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)

Goal state after:
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 : J
g : IsFiltered.max i j ⟶ k
hg :
  (hom (F.map g)) ((hom (F.map (IsFiltered.leftToMax i j))) xi) =
    (hom (F.map g)) ((hom (F.map (IsFiltered.rightToMax i j))) xj)
⊢ ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: 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)

Tactic:
exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm

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
⊢ (blockDiagonal M).det = ∏ k, (M k).det

Tactic:
simp_rw [det_apply']
  -- The right-hand side is a product of sums, rewrite it as a sum of products.
  rw [Finset.prod_sum]
  simp_rw [Finset.prod_attach_univ, Finset.univ_pi_univ]
  -- We claim that the only permutations contributing to the sum are those that
  -- preserve their second component.
  let preserving_snd : Finset (Equiv.Perm (n × o)) := {σ | ∀ x, (σ x).snd = x.snd}
  have mem_preserving_snd :
    ∀ {σ : Equiv.Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ x, (σ x).snd = x.snd := fun {σ} =>
    Finset.mem_filter.trans ⟨fun h => h.2, fun h => ⟨Finset.mem_univ _, h⟩⟩
  rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _]
  -- And that these are in bijection with `o → Equiv.Perm m`.
  · refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).symm
    · intro σ _
      rw [mem_preserving_snd]
      rintro ⟨-, x⟩
      simp only [prodCongrLeft_apply]
    · intro σ _ σ' _ eq
      ext x hx k
      have :
        ∀ k x,
          prodCongrLeft (fun k => σ k (Finset.mem_univ _)) (k, x) =
            prodCongrLeft (fun k => σ' k (Finset.mem_univ _)) (k, x) :=
        fun k x => by rw [eq]
      simp only [prodCongrLeft_apply, Prod.mk_inj] at this
      exact (this k x).1
    · intro σ hσ
      rw [mem_preserving_snd] at hσ
      have hσ' x : (σ.symm x).snd = x.snd := by simpa [eq_comm] using hσ (σ.symm x)
      have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k) := by
        intro k x
        ext
        · simp only
        · simp only [hσ]
      have mk_inv_apply_eq : ∀ k x, ((σ.symm (x, k)).fst, k) = σ.symm (x, k) := by grind
      refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩
      · intro x
        simp [mk_apply_eq]
      · intro x
        simp [mk_inv_apply_eq]
      · apply Finset.mem_univ
      · ext ⟨k, x⟩
        · simp only [coe_fn_mk, prodCongrLeft_apply]
        · simp only [prodCongrLeft_apply, hσ]
    · intro σ _
      rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right]
      simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq,
        prodCongrLeft_apply]
  · intro σ _ hσ
    rw [mem_preserving_snd] at hσ
    obtain ⟨⟨k, x⟩, hkx⟩ := not_forall.mp hσ
    rw [Finset.prod_eq_zero (Finset.mem_univ (k, x)), mul_zero]
    rw [blockDiagonal_apply_ne]
    exact hkx

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

Goal state before:
pp: case convert_2.inl
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
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
a2 : m
hx : σ (Sum.inl a) = Sum.inl a2
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0

Tactic:
have hn := (not_exists.mp ha) a2

Goal state after:
case convert_2.inl
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
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
a2 : m
hx : σ (Sum.inl a) = Sum.inl a2
hn : ¬Sum.inl a2 = σ (Sum.inl a)
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0
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 ι
f : MultilinearMap R (fun x ↦ R) M₂
⊢ MultilinearMap.mkPiRing R ι (f fun x ↦ 1) = f

Tactic:
ext
  simp

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

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j

Tactic:
rw [if_pos hjs]; by_cases hji : j < i
    · rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]
    rw [if_neg (Classical.not_imp.mpr ⟨hjs, hji⟩), if_neg hji]
    obtain rfl | hij := eq_or_ne i j
    · rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]
    · rw [if_neg hij, if_neg hij.symm]

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

Goal state before:
pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∉ s
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j

Tactic:
· rw [if_neg hjs, if_pos fun h ↦ (hjs h).elim, s.piecewise_eq_of_notMem _ _ hjs]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Ulift

Goal state before:
pp: J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ Type u
c : Cone K
hc : IsLimit c
s : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hs : s ∈ (K ⋙ uliftFunctor.{v, u}).sections
x : c.pt
hx₁ : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) x = ↑((sectionsEquiv K).symm ⟨s, ⋯⟩) j
hx₂ :
  ∀ (y : c.pt), (fun x ↦ ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) x = ↑((sectionsEquiv K).symm ⟨s, ⋯⟩) j) y → y = x
⊢ ∃! x, ∀ (j : J), (ConcreteCategory.hom ((uliftFunctor.{v, u}.mapCone c).π.app j)) x = s j

Tactic:
exact ⟨⟨x⟩, fun i => ULift.ext _ _ (hx₁ i),
          fun y hy => ULift.ext _ _ (hx₂ y.down fun i ↦ ULift.ext_iff.mp (hy i))⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this✝ : (Cocone.functoriality K F).map f = i.hom
this : IsIso ((Cocone.functoriality K F).map f)
⊢ IsColimit d

Tactic:
haveI := isIso_of_reflects_iso f (Cocone.functoriality K F)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this✝¹ : (Cocone.functoriality K F).map f = i.hom
this✝ : IsIso ((Cocone.functoriality K F).map f)
this : IsIso f
⊢ IsColimit d
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
m : c.pt ⟶ s.pt
w : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : K
⊢ m.app x =
    { app := fun k ↦ (t k).desc { pt := s.pt.obj k, ι := whiskerRight s.ι ((evaluation K C).obj k) },
          naturality := ⋯ }.app
      x

Tactic:
exact (t x).hom_ext fun j =>
      (congr_app (w j) x).trans
        ((t x).fac ⟨s.pt.obj _, whiskerRight s.ι ((evaluation K C).obj _)⟩ j).symm

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom =
    (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
ext
  simp

Goal state after: