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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
⊢ sign (prodCongrRight σ) = ∏ k, sign (σ k)

Tactic:
have l_to_finset : l.toFinset = Finset.univ := by
    apply eq_top_iff.mpr
    intro b _
    exact List.mem_toFinset.mpr (mem_l b)

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
l_to_finset : l.toFinset = univ
⊢ sign (prodCongrRight σ) = ∏ k, sign (σ k)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
hi' : ∀ x ∈ c.support, g x = (c ^ i) x
⊢ g (c x) = c (g x)

Tactic:
by
        rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]
        simp only [← mul_apply, ← zpow_add_one, ← zpow_one_add, add_comm]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ c.subtypePerm ⋯ ^ k = g.subtypePerm ⋯ ↔ c ^ k = ofSubtype (g.subtypePerm ⋯)

Tactic:
subtypePerm_zpow c k

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ (c ^ k).subtypePerm ⋯ = g.subtypePerm ⋯ ↔ c ^ k = ofSubtype (g.subtypePerm ⋯)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ {#σ.support}.sum = #σ.support

Tactic:
Multiset.sum_singleton

Goal state after:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ #σ.support = #σ.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ y ∈ List.iterate (⇑f) x (Fintype.card α) ↔ f.SameCycle x y

Tactic:
simp only [List.mem_iterate, iterate_eq_pow, eq_comm (a := y)]
    constructor
    · rintro ⟨n, _, hn⟩
      exact ⟨n, hn⟩
    · intro hxy
      by_cases hx : x ∈ f.support
      case pos =>
        -- we can't invoke the aux lemmas above without obtaining the decidable instance we are
        -- already building; but now we've left the data, so we can do this non-constructively
        -- without sacrificing computability.
        let _inst (f : Perm α) : DecidableRel (SameCycle f) := Classical.decRel _
        rcases hxy.exists_pow_eq_of_mem_support_aux hx with ⟨i, hixy, hi⟩
        refine ⟨i, lt_of_lt_of_le hixy (card_le_univ _), hi⟩
      case neg =>
        have : Nonempty α := ⟨x⟩
        rw [notMem_support] at hx
        exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ σ.cycleType.card = σ.cycleType.card - 1 + 1

pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ

Tactic:
· rw [tsub_add_cancel_of_le]
    rw [Nat.succ_le_iff, card_cycleType_pos, Ne, ← orderOf_eq_one_iff]
    exact hσ.ne_one

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ Multiset.map (Finset.card ∘ support) {f}.val ≤ Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Tactic:
refine map_le_map ?_

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
hf' : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ {f}.val ≤ g.cycleFactorsFinset.val
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.sum_insert hi]
    rw [Disjoint.cycleType_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: case h
n : ℕ
i j : Fin n
h : i < j
⊢ j ∉ Set.range ⇑(castLEEmb ⋯)

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, τ x = l.prod x
x : α
hx : x ∈ σ.support ∩ τ.support
⊢ σ x = τ x

Tactic:
h x (mem_support.mp (mem_of_mem_inter_left hx)),

Goal state after:
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, τ x = l.prod x
x : α
hx : x ∈ σ.support ∩ τ.support
⊢ l.prod x = τ x
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case neg
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this✝ :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
this : subNat (↑i) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ (↑k - ↑i + 1) % (n - ↑i) + (n - (n - ↑i)) = (↑k + 1) % n

Tactic:
rw [Nat.mod_eq_of_lt (by lia), Nat.mod_eq_of_lt (by lia)]

Goal state after:
case neg
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this✝ :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
this : subNat (↑i) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ ↑k - ↑i + 1 + (n - (n - ↑i)) = ↑k + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ {3}.sum = 3

Tactic:
Multiset.sum_singleton

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ 3 = 3
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : {n}.sum = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle

Tactic:
Multiset.sum_singleton

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : (swap a b * swap a c).support = {a, b, c}
⊢ (swap a b * swap a c).IsThreeCycle

Tactic:
rw [← card_support_eq_three_iff, h]
    simp [ab, ac, bc]

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp : ¬((f p) fun i ↦ (x i) (p i)) = 0
i : ι
⊢ ¬(x i) (p i) = 0

Tactic:
exact mt ((f p).map_coord_zero (m := fun i => x i _) i) hp

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 : 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' : MultilinearMap R M₁ M₂
inst✝⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝⁴ : (i : ι) → Module R (M₁' i)
inst✝³ : (i : ι) → AddCommMonoid (M₁'' i)
inst✝² : (i : ι) → Module R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → β i → Type u_2
inst✝¹ : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst✝ : (i : ι) → (b : β i) → Module R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N i.fst i.snd) (i : (i : ι) × β i) (x y : N i.fst i.snd),
    (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i (x + y)) i_1)) =
      (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i x) i_1)) + g fun i_1 ↦ (f i_1) (Sigma.curry (update m i y) i_1)

Tactic:
simp +instances [Subsingleton.elim hDecEqSigma Sigma.instDecidableEqSigma,
      Sigma.curry_update, Function.apply_update (fun i ↦ f i)]

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 : 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' : MultilinearMap R M₁ M₂
inst✝⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝⁴ : (i : ι) → Module R (M₁' i)
inst✝³ : (i : ι) → AddCommMonoid (M₁'' i)
inst✝² : (i : ι) → Module R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → β i → Type u_2
inst✝¹ : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst✝ : (i : ι) → (b : β i) → Module R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N i.fst i.snd) (i : (i : ι) × β i) (c : R) (x : N i.fst i.snd),
    (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i (c • x)) i_1)) =
      c • g fun i_1 ↦ (f i_1) (Sigma.curry (update m i x) i_1)

Tactic:
simp +instances [Subsingleton.elim hDecEqSigma Sigma.instDecidableEqSigma,
      Sigma.curry_update, Function.apply_update (fun i ↦ f i)]

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
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
⊢ ∑ j ∈ A i, g i j = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j) i

Tactic:
rw [hi, update_self]
      have : A i₀ = B i₀ ∪ C i₀ := by
        simp only [B, C, Function.update_self, Finset.sdiff_union_self_eq_union]
        symm
        simp only [hj₂, Finset.singleton_subset_iff, Finset.union_eq_left]
      rw [this]
      refine Finset.sum_union <| Finset.disjoint_right.2 fun j hj => ?_
      have : j = j₂ := by
        simpa [C] using hj
      rw [this]
      simp only [B, Finset.mem_sdiff, not_true, not_false_iff, Finset.mem_singleton,
        update_self, and_false]

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
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ A.det = 0

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
h : ∀ (i : n), A i j = 0
⊢ Aᵀ.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
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']

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 = ∏ x, ∑ σ, ↑↑(sign σ) * ∏ i, M x (σ i) i
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
a : α
z : (i : ι) → M₁ i
⊢ (fun i ↦ update m a z (e.symm i) ↑i) = fun i ↦ update (fun j ↦ m (e.symm j) ↑j) (e a) (z ↑(e a)) i

Tactic:
by
  ext i
  rcases eq_or_ne a (e.symm i) with rfl | hne
  · rw [Equiv.apply_symm_apply e i, update_self, update_self]
  · rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]

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
B : Matrix m n R
D : Matrix n n R
⊢ (fromBlocks A B 0 D).det = A.det * D.det

Tactic:
simp_rw [det_apply']

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
B : Matrix m n R
D : Matrix n n R
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i =
    (∑ σ, ↑↑(sign σ) * ∏ i, A (σ i) i) * ∑ σ, ↑↑(sign σ) * ∏ i, D (σ i) i
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_4.e_a
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
σ₂ : Perm n
⊢ ↑↑(sign σ₁) * ↑↑(sign σ₂) = ↑↑(sign σ₁ * sign σ₂)

Tactic:
Units.val_mul,

Goal state after:
case e'_3.refine_4.e_a
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
σ₂ : Perm n
⊢ ↑↑(sign σ₁) * ↑↑(sign σ₂) = ↑(↑(sign σ₁) * ↑(sign σ₂))
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:
by
  rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,
    det_transpose]

Goal state after:
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
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det

Tactic:
← det_transpose

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ)ᵀ.det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.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
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ)ᵀ.det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det

Tactic:
simp only [transpose_apply, transpose_submatrix, transpose_transpose]

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.Full
inst✝ : F.Faithful
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (K.map f ≫ F.preimage (l.ι.app Z ≫ i.inv)) = F.map (F.preimage (l.ι.app Y ≫ i.inv) ≫ ((const J).obj X).map f)

Tactic:
by
              simpa [← cancel_mono i.hom] using l.w f

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
⊢ (flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj lim).map η ≫ (limitIsoFlipCompLim G).symm.hom =
    (limitIsoFlipCompLim F).symm.hom ≫ lim.map η

Tactic:
by
    ext k
    apply limit_obj_ext
    intro j
    simp [comp_evaluation, ← NatTrans.comp_app (limMap η)]

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 Z Z' : C
h : Z ⟶ Z'
⊢ (𝟙 (X ⊗ Y) ⊗ₘ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h)

Tactic:
by
  rw [← id_tensorHom_id, associator_naturality]

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 X Y : C
f g : X ⟶ Y
h : f ▷ 𝟙_ C = g ▷ 𝟙_ C
⊢ f = g

Tactic:
simpa using h

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 X Y : C
f g : X ⟶ Y
h : ((curriedTensor C).obj (𝟙_ C)).map f = ((curriedTensor C).obj (𝟙_ C)).map g
⊢ f = g

Tactic:
simpa using h

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y : J
f : X ⟶ Y
X' : J
⊢ F.map f ▷ G.obj X' ≫ (α.app Y ⊗ₘ β.app X') = (α.app X ⊗ₘ β.app X') ≫ F'.map f ▷ G'.obj X'

Tactic:
by
  simpa using tensor_naturality α β f (𝟙 X')

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
⊢ ∀ (r : R) {Y Z : D} (f : Y ⟶ Z) (X : D), (r • f) ▷ X = r • f ▷ X

Tactic:
by
      intro r X Y f Z
      apply F.map_injective
      rw [Functor.Monoidal.map_whiskerRight]
      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
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ≫ G.map (μ F x✝² x✝¹)) ▷ (F ⋙ G).obj x✝ ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ (F ⋙ G).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((F ⋙ G).obj x✝²) ((F ⋙ G).obj x✝¹) ((F ⋙ G).obj x✝)).hom ≫
      (F ⋙ G).obj x✝² ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
dsimp
    simp_rw [comp_whiskerRight, assoc, μ_natural_left_assoc, MonoidalCategory.whiskerLeft_comp,
      assoc, μ_natural_right_assoc, ← associativity_assoc, ← G.map_comp, associativity]

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
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
c : PushoutCocone f g
X : C
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
              (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).π.app
        j =
      (Iso.refl
            ((Cone.postcompose (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)).hom).obj
                (Cone.whisker walkingSpanOpEquiv.symm.functor ((yoneda.obj X).mapCone (Cocone.op c)))).pt).hom ≫
        ((yoneda.obj X).mapCone c.op).π.app j

Tactic:
rintro (_ | _ | _) <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ F.map (X✝ ◁ f✝ ≫ (β X✝ Z✝).hom) = F.map ((β X✝ Y✝).hom ≫ f✝ ▷ X✝)

Tactic:
refine (cancel_epi (μ F ?_ ?_)).1 ?_

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ Z✝
⊢ μ F X✝ Y✝ ≫ F.map (X✝ ◁ f✝ ≫ (β X✝ Z✝).hom) = μ F X✝ Y✝ ≫ F.map ((β X✝ Y✝).hom ≫ f✝ ▷ X✝)