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

Goal state before:
pp: case left
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ y = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ y

Tactic:
by_cases hy : σ y = y

Goal state after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
hy : σ y = y
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ y = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ y

case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
y : α
hy : ¬σ y = y
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ y = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ y
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : x = (σ ^ (n + 1)) x
⊢ swap x ((σ ^ (n + 1)) x) ∈ H

Tactic:
rw [← h6, swap_self]

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : x = (σ ^ (n + 1)) x
⊢ Equiv.refl α ∈ H
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).support = f.support ↔ ¬orderOf f ∣ n

Tactic:
rw [orderOf_dvd_iff_pow_eq_one]
  constructor
  · intro h H
    refine hf.ne_one ?_
    rw [← support_eq_empty_iff, ← h, H, support_one]
  · intro H
    apply le_antisymm (support_pow_le _ n) _
    intro x hx
    contrapose H
    ext z
    by_cases hz : f z = z
    · rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]
    · obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)
      apply (f ^ k).injective
      rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply]
      simpa using H

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
⊢ (f ^ n).support = f.support

Tactic:
rw [hf.support_pow_eq_iff]

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
⊢ ¬orderOf f ∣ n
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ _root_.Disjoint (ofSign 1) (ofSign (-1))

Tactic:
by
  rw [Finset.disjoint_iff_ne]
  rintro σ hσ τ hτ rfl
  rw [mem_ofSign] at hσ hτ
  have := hσ.symm.trans hτ
  contradiction

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ ↑d

Tactic:
← h₃

Goal state after:
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ x * a + y * b
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝ : DecidableEq ι
f : ((i : ι) → N i) →* M
i : ι
x : N i
⊢ ((fun ϕ ↦ noncommPiCoprod ↑ϕ ⋯) ((fun f ↦ ⟨fun i ↦ f.comp (mulSingle N i), ⋯⟩) f)) (Pi.mulSingle i x) =
    f (Pi.mulSingle i x)

Tactic:
by
    simp only [noncommPiCoprod_mulSingle, coe_comp, Function.comp_apply, mulSingle_apply]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle a b

Tactic:
rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle l[idxOf a l] l[idxOf b l]
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case refine_1
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b

pp: case refine_2
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ (∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b) → a ∈ s ∧ b ∈ s

Tactic:
· obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2
    exact ⟨n, hn, a, hx.1, rfl, by rw [f.iterate_eq_pow]⟩

Goal state after:
case refine_2
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ (∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b) → a ∈ s ∧ b ∈ s
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : ¬f.SameCycle x y
⊢ (f.cycleOf x) y = f y

Tactic:
rw [cycleOf_apply_of_not_sameCycle h,
        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)

Tactic:
refine ⟨f.cycleOf x, ?_, ?_⟩

Goal state after:
case neg.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ f.cycleOf x ∈ f.cycleFactorsFinset.val

case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

pp: case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
· obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
    rcases k with - | k
    · refine ⟨#(f.cycleOf x).support, hk, self_le_add_right _ _, ?_⟩
      simp only [pow_zero, coe_one, id_eq] at hk'
      subst hk'
      rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]
    · exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩

Goal state after:
case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : σ (some x) = some val✝
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (some val✝)

Tactic:
· have hn : σ (some x) ≠ none := by simp [h]
        have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
        simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]

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

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
⊢ IsConj (σ * π) τ

Tactic:
have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm

Goal state after:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) τ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))

Tactic:
have hs : σ.cycleType = σ'.cycleType := by
      rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
      rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl

Goal state after:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ IsConj (σ * π) (σ' * (τ * σ'⁻¹))
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 ⋯
⊢ ↑(Fin.cast ⋯ ((⟨↑(Fin.cast ⋯ k) - ↑i, ⋯⟩ + 1).addNat (n - (n - ↑i)))) = ↑(k + 1)

Tactic:
simp only [val_cast, add_def, val_one', Nat.add_mod_mod, addNat_mk, cast_mk]

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 - ↑i) + (n - (n - ↑i)) = (↑k + 1) % n
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁵ : Semiring R✝
M : Type u_2
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R✝ M
N : Type u_3
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R✝ N
P : Type u_4
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R✝ P
M' : Type u_5
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R✝ M'
N' : Type u_6
inst✝⁶ : AddCommGroup N'
inst✝⁵ : Module R✝ N'
ι✝ : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι✝]→ₗ[R✝] N
g g₂ : M [⋀^ι✝]→ₗ[R✝] N'
g' : M' [⋀^ι✝]→ₗ[R✝] N'
v✝ : ι✝ → M
v' : ι✝ → M'
R : Type u_10
M₁ : Type u_11
M₂ : Type u_12
ι : Type u_13
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
f : M₁ [⋀^ι]→ₗ[R] R
z : M₂
v : ι → M₁
i j : ι
h : v i = v j
hne : i ≠ j
⊢ ((↑f).smulRight z).toFun v = 0

Tactic:
by simp [f.map_eq_zero_of_eq v h hne]

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 (Option n) (Option n) R
i : Option n
⊢ adjp s A i none = detp (sign (swap none i) * s) (A.submatrix some (⇑(swap none i) ∘ some))

Tactic:
adjp,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
⊢ of (fun i j ↦ ∑ σ ∈ ofSign s with σ j = i, ∏ k ∈ {j}ᶜ, A k (σ k)) i none =
    detp (sign (swap none i) * s) (A.submatrix some (⇑(swap none i) ∘ some))
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
s t : ℤˣ
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
⊢ sign τ = t * s ↔ sign τ = t * sign σ

Tactic:
mem_ofSign.mp hσ

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → descFunLift F s a = descFunLift F s b

Tactic:
· intro x y r
    induction r with
    | refl => rfl
    | symm x y _ ih => exact ih.symm
    | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
    | map j j' f x => exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x
    | zero j => simp +instances
    | one j => simp +instances
    | neg j x => simp +instances
    | add j x y => simp +instances
    | mul j x y => simp +instances
    | neg_1 x x' r ih => dsimp; rw [ih]
    | add_1 x x' y r ih => dsimp; rw [ih]
    | add_2 x y y' r ih => dsimp; rw [ih]
    | mul_1 x x' y r ih => dsimp; rw [ih]
    | mul_2 x y y' r ih => dsimp; rw [ih]
    | zero_add x => dsimp; rw [zero_add]
    | add_zero x => dsimp; rw [add_zero]
    | one_mul x => dsimp; rw [one_mul]
    | mul_one x => dsimp; rw [mul_one]
    | neg_add_cancel x => dsimp; rw [neg_add_cancel]
    | add_comm x y => dsimp; rw [add_comm]
    | add_assoc x y z => dsimp; rw [add_assoc]
    | mul_assoc x y z => dsimp; rw [mul_assoc]
    | left_distrib x y z => dsimp; rw [mul_add]
    | right_distrib x y z => dsimp; rw [add_mul]
    | zero_mul x => dsimp; rw [zero_mul]
    | mul_zero x => dsimp; rw [mul_zero]

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
d : n → R
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, diagonal d (σ i) i = ∏ i, d i

Tactic:
refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_

Goal state after:
case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∀ b ∈ univ, b ≠ 1 → ↑↑(sign b) * ∏ i, diagonal d (b i) i = 0

case refine_2
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ 1 ∉ univ → ↑↑(sign 1) * ∏ i, diagonal d (1 i) i = 0

case refine_3
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(sign 1) * ∏ i, diagonal d (1 i) i = ∏ i, d i
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_4
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 σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) * ∏ x, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) x) x

Tactic:
Fintype.prod_sum_type

Goal state after:
case e'_3.refine_4
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 σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) *
      ((∏ a₁, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) (Sum.inl a₁)) (Sum.inl a₁)) *
        ∏ a₂, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) (Sum.inr a₂)) (Sum.inr a₂))
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 ι
z₁ z₂ : M₂
⊢ (∀ (x : ι → R), (MultilinearMap.mkPiRing R ι z₁) x = (MultilinearMap.mkPiRing R ι z₂) x) ↔ z₁ = z₂

Tactic:
mkPiRing_apply

Goal state after:
R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
z₁ z₂ : M₂
⊢ (∀ (x : ι → R), (∏ i, x i) • z₁ = (∏ i, x i) • z₂) ↔ z₁ = z₂
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j
⊢ IsLimit c

Tactic:
have := fun c y ↦ h _ (sectionOfCone c y).2

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j
this : ∀ (c_1 : Cone F) (y : c_1.pt), ∃! x, ∀ (j : J), (hom (c.π.app j)) x = ↑(sectionOfCone c_1 y) j
⊢ IsLimit c
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
X✝ Y✝ : J ⥤ Type (max u v)
f : X✝ ⟶ Y✝
x : lim.obj X✝
⊢ (hom (lim.map f ≫ (limitEquivSections Y✝).toIso.hom)).toFun x =
    (hom ((limitEquivSections X✝).toIso.hom ≫ (Functor.sectionsFunctor J).map f)).toFun x

Tactic:
exact Subtype.ext (funext fun j ↦ congr_hom (limMap_π f j) x)

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) + (f x + ∑ x_1, f (update x x_1 (h x_1))) =
    f x + (f.linearDeriv x) h + ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x)

Tactic:
linearDeriv_apply,

Goal state after:
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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) + (f x + ∑ x_1, f (update x x_1 (h x_1))) =
    f x + ∑ x_1, f (update x x_1 (h x_1)) + ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
eq :
  (hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s) ≫ ((yoneda.obj (unop s.pt)).mapCone c).π.app j))
      (𝟙 (unop s.pt)) =
    (hom (((yoneda.obj (unop s.pt)).mapCone s).π.app j)) (𝟙 (unop s.pt))
⊢ ↑((Types.isLimitEquivSections (hc (unop s.pt))) m.unop) j =
    ↑((Types.isLimitEquivSections (hc (unop s.pt)))
          (Quiver.Hom.op ((hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s))) (𝟙 (unop s.pt)))).unop)
      j

Tactic:
dsimp [Types.isLimitEquivSections, Types.sectionOfCone]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
eq :
  (hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s) ≫ ((yoneda.obj (unop s.pt)).mapCone c).π.app j))
      (𝟙 (unop s.pt)) =
    (hom (((yoneda.obj (unop s.pt)).mapCone s).π.app j)) (𝟙 (unop s.pt))
⊢ (c.π.app j).unop ≫ m.unop =
    (c.π.app j).unop ≫ (hom ((hc (unop s.pt)).lift ((yoneda.obj (unop s.pt)).mapCone s))) (𝟙 (unop s.pt))
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
⊢ ↑((Types.isLimitEquivSections (hc (op s.pt))) m) j =
    ↑((Types.isLimitEquivSections (hc (op s.pt)))
          ((hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s))) (𝟙 (unop (op s.pt)))))
      j

Tactic:
dsimp [Types.isLimitEquivSections, Types.sectionOfCone]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
⊢ m ≫ c.π.app j = (hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s))) (𝟙 s.pt) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w', v, u} C
K : Cᵒᵖ
J : Type w
x✝ : Category.{t, w} J
⊢ PreservesLimitsOfShape J (shrinkYoneda.{w', v, u} ⋙ (evaluation Cᵒᵖ (Type w')).obj K)

Tactic:
have := preservesLimitsOfShape_of_natIso (J := J) (Functor.associator _ _ _ ≪≫
      shrinkYonedaCompEvaluationCompUliftFunctorIsoUliftFunctor.{w'} K).symm
    exact preservesLimitsOfShape_of_reflects_of_preserves _ uliftFunctor.{v}

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
τ : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
Y : C
f : (yoneda.obj Y).obj X
⊢ (ConcreteCategory.hom
          (((fun x ↦
                  { app := fun Y ↦ ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x,
                    naturality := ⋯ })
                ((fun τ ↦
                    (ConcreteCategory.hom (τ.app (unop X))) ((equivShrink ((yoneda.obj (unop X)).obj X)) (𝟙 (unop X))))
                  τ)).app
            Y)).toFun
      ((equivShrink ((yoneda.obj Y).obj X)) f) =
    (ConcreteCategory.hom (τ.app Y)).toFun ((equivShrink ((yoneda.obj Y).obj X)) f)

Tactic:
simpa [shrinkYoneda] using ((τ.naturality_apply f) (equivShrink _ (𝟙 X.unop))).symm

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

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X₁✝ Y₁✝ X₂✝ Y₂✝ : Discrete M
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
⊢ { as := X₁✝.as * X₂✝.as } = { as := Y₁✝.as * Y₂✝.as }

Tactic:
by rw [eq_of_hom f, eq_of_hom g]

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

Goal state before:
pp: case η
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ (εIso F).hom ≫ η F = ε F ≫ η F

Tactic:
exact congr(($eq.symm).ε ≫ _)

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 : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : g ⊗ f ⟶ h ⊗ f
ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'
ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ f ⊗ g'
ηθ₂ : g ⊗ f ⊗ f' ⟶ h ⊗ f ⊗ g'
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ₘ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom = ηθ
e_ηθ₁ : ηθ ≫ (α_ h f g').hom = ηθ₁
e_ηθ₂ : (α_ g f f').inv ≫ ηθ₁ = ηθ₂
⊢ η ⊗ₘ f ◁ θ = ηθ₂

Tactic:
simp only [← e_η₁, ← e_ηθ, ← e_ηθ₁, ← e_ηθ₂]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : g ⊗ f ⟶ h ⊗ f
ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'
ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ f ⊗ g'
ηθ₂ : g ⊗ f ⊗ f' ⟶ h ⊗ f ⊗ g'
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ₘ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom = ηθ
e_ηθ₁ : ηθ ≫ (α_ h f g').hom = ηθ₁
e_ηθ₂ : (α_ g f f').inv ≫ ηθ₁ = ηθ₂
⊢ η ⊗ₘ f ◁ θ = (α_ g f f').inv ≫ (η ▷ f ⊗ₘ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom) ≫ (α_ h f g').hom