mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (s : Finset α), #(permsOfFinset s) = (#s)!

Tactic:
by
  rintro ⟨⟨l⟩, hs⟩; exact length_permsOfList l

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ swap x (f x) * (swap x (f x) * f) = f

Tactic:
← mul_assoc,

Goal state after:
α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ swap x (f x) * swap x (f x) * f = f
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ x ∈ Submonoid.closure {σ | σ.IsSwap}

Tactic:
rw [← h1]

Goal state after:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ (↑x.truncSwapFactors.out).prod ∈ Submonoid.closure {σ | σ.IsSwap}
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| (x :: y :: l)[(k + 1 + n) % (x :: y :: l).length] = (x' :: y' :: l')[k + 1]

Tactic:
congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * (swap z w * swap w y) = swap y z

Tactic:
← mul_assoc,

Goal state after:
α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap z w * swap w y = swap y z
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l[(k + 1) % l.length] = l[k] ↔ l.length ≤ 1

Tactic:
hl.getElem_inj_iff

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ (k + 1) % l.length = k ↔ l.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
a : (_ : Fin (n + 2)) × Fin (n + 2)
ha₁ : a ∈ finPairsLT (n + 2)
ha₂ : a ∉ {⟨1, 0⟩}
⊢ (if (swap 0 1) a.fst ≤ (swap 0 1) a.snd then -1 else 1) = 1

Tactic:
rcases a with ⟨a₁, a₂⟩

Goal state after:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₁ : ⟨a₁, a₂⟩ ∈ finPairsLT (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
⊢ (if (swap 0 1) ⟨a₁, a₂⟩.fst ≤ (swap 0 1) ⟨a₁, a₂⟩.snd then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
b : β
hb : (g.extendDomain f) b ≠ b
⊢ b = ↑(f (f.symm ⟨b, ⋯⟩))

Tactic:
rw [apply_symm_apply, Subtype.coe_mk]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : x ∈ {x | (l.formPerm ^ n) x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
← set_support_apply_mem

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | (l.formPerm ^ n) x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ #(swap x (f x) * f).support + 1 = #(insert x (f.support.erase x))

Tactic:
support_swap_mul_eq _ _ h1,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ #(f.support \ {x}) + 1 = #(insert x (f.support.erase x))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → f x ≠ x → β
h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y
x : { x // f x ≠ x }
⊢ g (i ↑x ⋯) ≠ i ↑x ⋯

Tactic:
have : f (f x) ≠ f x := mt (fun h => f.injective h) x.2

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → f x ≠ x → β
h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y
x : { x // f x ≠ x }
this : f (f ↑x) ≠ f ↑x
⊢ g (i ↑x ⋯) ≠ i ↑x ⋯
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
this : f ^ (b - a) = 1
⊢ f ^ a = f ^ b

Tactic:
by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]

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

Goal state before:
pp: x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.lcm y' = d
⊢ x.lcm y = d

Tactic:
by subst_vars; rw [Int.lcm_def]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
⊢ (fun i ↦ (ϕ i).range) i ⊓ ⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (ϕ i).range) j ≤ ⊥

Tactic:
rintro f ⟨hxi, hxp⟩

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ ↑((fun i ↦ (ϕ i).range) i).toSubmonoid
hxp : f ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (ϕ i).range) j).toSubmonoid
⊢ f ∈ ⊥
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
hxp : f ∈ ↑(noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯).range
⊢ f ∈ ⊥

Tactic:
obtain ⟨g, hgf⟩ := hxp

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
⊢ f ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
⊢ (∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport) →
    Commute g c

Tactic:
rintro ⟨hc', ⟨i, hi⟩⟩
    ext x
    simp only [coe_mul, Function.comp_apply]
    by_cases hx : x ∈ c.support
    · suffices hi' : ∀ x ∈ c.support, g x = (c ^ i) x 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]
      intro x hx
      have hix := Perm.congr_fun hi ⟨x, hx⟩
      simp only [← Subtype.coe_inj, subtypePermOfSupport, subtypePerm_apply,
        subtypePerm_apply_zpow_of_mem] at hix
      exact hix.symm
    · rw [notMem_support.mp hx, eq_comm, ← notMem_support]
      contrapose hx
      exact (hc' x).mp hx

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

Goal state before:
pp: α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ x ∈ (f.cycleOf x).support

Tactic:
rw [mem_support_cycleOf_iff'_aux hx]

Goal state after:
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 : α
hxy : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
have : Nonempty α := ⟨x⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Tactic:
by_cases hx : f x = x
  · rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
  · rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      pow_mod_orderOf]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Injective cycleFactorsFinset

Tactic:
intro f g h
  rw [← cycleFactorsFinset_noncommProd f]
  simpa [h] using cycleFactorsFinset_noncommProd g

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

Goal state before:
pp: case refine_2.inr
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
hle : (Equiv.symm σ) x2 ≤ (Equiv.symm σ) x1
⊢ ∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2

Tactic:
exact ⟨_, _, hle.lt_of_ne (by simp [hlt.ne]), by simp [hlt.le]⟩

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

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

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))

pp: case pos.inr.inr
α : 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 (g a)) = (swap a (g a)) ((swap (g a) (g (g a))) (g (g a)))

Tactic:
· rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]
      simp

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)) ((swap (g a) (g (g a))) (g a))

case pos.inr.inr
α : 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 (g a)) = (swap a (g a)) ((swap (g a) (g (g a))) (g (g a)))
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
| (freeDFinsuppEquiv (DFinsupp.single p r)) x

Tactic:
← mul_one r,

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
| (freeDFinsuppEquiv (DFinsupp.single p (r * 1))) x
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_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
N'₂ : Type u_10
inst✝³ : AddCommGroup N'₂
inst✝² : Module R N'₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap R (fun x ↦ M) N'
⊢ MultilinearMap.alternatization (g.compMultilinearMap f) = g.compAlternatingMap (MultilinearMap.alternatization f)

Tactic:
by
  ext
  simp [MultilinearMap.alternatization_def]

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
c : R
⊢ a * (c ^ Fintype.card n * detp 1 A) + b * (c ^ Fintype.card n * detp (-1) A) =
    b * (c ^ Fintype.card n * detp 1 A) + a * (c ^ Fintype.card n * detp (-1) A)

Tactic:
← mul_assoc,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
c : R
⊢ a * c ^ Fintype.card n * detp 1 A + b * c ^ Fintype.card n * detp (-1) A =
    b * c ^ Fintype.card n * detp 1 A + a * c ^ Fintype.card n * detp (-1) A
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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
s t : ℤˣ
⊢ ∑ i ∈ ofSign s, ∑ j ∈ ofSign t, (∏ k, A k (i k)) * ∏ k, B k (j k) =
    ∑ x ∈ ofSign s, ∑ x_1 ∈ ofSign (t * s), (∏ x_2, A x_2 (x x_2)) * ∏ x_2, B (x x_2) (x_1 x_2)

Tactic:
refine sum_congr rfl fun σ hσ ↦ ?_

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
s t : ℤˣ
σ : Perm n
hσ : σ ∈ ofSign s
⊢ ∑ j ∈ ofSign t, (∏ k, A k (σ k)) * ∏ k, B k (j k) = ∑ x ∈ ofSign (t * s), (∏ x, A x (σ x)) * ∏ x_1, B (σ x_1) (x x_1)
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
M : Matrix n n R
j : n
s : R
u : n → R
⊢ ((s • M).updateCol j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, transpose_smul, det_updateRow_smul_left]

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ s ^ (Fintype.card n - 1) * (Mᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : (σ * τ) l ≠ l
hl2 : l ≠ τ⁻¹ j
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
ne_comm

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ) l
hl2 : l ≠ τ⁻¹ j
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))
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
hAB : A * B = 1
key : A * (B * adjp 1 B) + A * detp (-1) B • 1 = A * (B * adjp (-1) B) + A * detp 1 B • 1
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Tactic:
← mul_assoc,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
key : A * B * adjp 1 B + A * detp (-1) B • 1 = A * B * adjp (-1) B + A * detp 1 B • 1
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case empty
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ S T, ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ ∅ → T mX ≫ f = T mY

Tactic:
obtain ⟨S, f⟩ := inf_objs_exists O
    exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x : c.pt
f₁ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := true }
f₂ : (F.coconeTypesEquiv c).pt ⟶ ULift.{u, 0} Bool := ↾fun x ↦ { down := decide (∃ a, F.descColimitType c a = x) }
this✝ : f₁ = f₂
this : (ConcreteCategory.hom f₁) x = (ConcreteCategory.hom f₂) x
⊢ ∃ a, F.descColimitType c a = x

Tactic:
simpa [f₁, f₂] using this

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ¬∃ j y, (hom (t.ι.app j)) y = x
⊢ False

Tactic:
not_exists

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬(hom (t.ι.app x_1)) x_2 = x
⊢ False
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 ∘ F.coconeTypes.ι j = c.ι j

Tactic:
coconeTypes_ι,

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
j : J
⊢ F.descColimitType c ∘ (fun j ↦ F.ιColimitType j) j = c.ι j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // ¬P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
c : M₁ ↑i
⊢ (fun j ↦ if h : P j then x ⟨j, h⟩ else update z i c ⟨j, h⟩) =
    update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c

Tactic:
simpa only [dite_not] using domDomRestrict_aux _ z (fun j ↦ x ⟨j.1, not_not.mp j.2⟩) i c

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
x₁ x₂ : t.pt
⊢ ∃ j x₁' x₂', (hom (t.ι.app j)) x₁' = x₁ ∧ (hom (t.ι.app j)) x₂' = x₂

Tactic:
obtain ⟨j₁, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₁

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
x₂ : t.pt
j₁ : J
x₁ : F.obj j₁
⊢ ∃ j x₁' x₂', (hom (t.ι.app j)) x₁' = (hom (t.ι.app j₁)) x₁ ∧ (hom (t.ι.app j)) x₂' = x₂
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_2
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
⊢ Set.InjOn (fun σ ↦ σ.1.sumCongr σ.2) ↑univ

Tactic:
intro σ₁ _ σ₂ _

Goal state after:
case e'_3.refine_2
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
a✝¹ : σ₁ ∈ ↑univ
σ₂ : Perm m × Perm n
a✝ : σ₂ ∈ ↑univ
⊢ (fun σ ↦ σ.1.sumCongr σ.2) σ₁ = (fun σ ↦ σ.1.sumCongr σ.2) σ₂ → σ₁ = σ₂
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

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

Tactic:
intro x y z

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y z : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
      (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z) =
    Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel y +
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel z
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type (max v u)
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
x : x✝¹.pt
j : J
⊢ ↑((hom x✝).toFun x) j = ↑((hom (↾fun v ↦ ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩)).toFun x) j

Tactic:
exact congr_hom (w j) x

Goal state after: