mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.x.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
hab : q < q
⊢ q.insertNth x f q < q.insertNth x f q

pp: case refine_4.x.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝ : Fin n
hab : q < q.succAbove j✝
⊢ q.insertNth x f q < q.insertNth x f (q.succAbove j✝)

pp: case refine_4.p.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝ : Fin n
hab : q.succAbove j✝ < q
⊢ q.insertNth x f (q.succAbove j✝) < q.insertNth x f q

pp: case refine_4.p.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝¹ j✝ : Fin n
hab : q.succAbove j✝¹ < q.succAbove j✝
⊢ q.insertNth x f (q.succAbove j✝¹) < q.insertNth x f (q.succAbove j✝)

Tactic:
· simp at hab

Goal state after:
case refine_4.x.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝ : Fin n
hab : q < q.succAbove j✝
⊢ q.insertNth x f q < q.insertNth x f (q.succAbove j✝)

case refine_4.p.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝ : Fin n
hab : q.succAbove j✝ < q
⊢ q.insertNth x f (q.succAbove j✝) < q.insertNth x f q

case refine_4.p.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝¹ j✝ : Fin n
hab : q.succAbove j✝¹ < q.succAbove j✝
⊢ q.insertNth x f (q.succAbove j✝¹) < q.insertNth x f (q.succAbove j✝)
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case a.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
⊢ (∃ a, ∑ i, a i = n ∧ (fun i ↦ if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) → s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
rintro ⟨f, ⟨hf, rfl⟩, rfl⟩
    rw [sum_dite_of_true fun _ ↦ id]
    exact ⟨Fintype.sum_equiv e _ _ (by simp), by simp +contextual⟩

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x : Fin (k + 1) → ℕ
hx₁ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id a)
hx₂ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id b)
⊢ False

Tactic:
rw [List.mem_map] at hx₁ hx₂
      obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
      dsimp at h₁₂
      rw [Fin.cons_inj, Nat.succ_inj] at h₁₂
      obtain ⟨h₁₂, rfl⟩ := h₁₂
      rw [Function.onFun, h₁₂] at h
      exact h (List.mem_map_of_mem hx₁) (List.mem_map_of_mem hx₂)

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ p = q

Tactic:
Nat.Partition.ext_iff,

Goal state after:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ p.parts = q.parts
Module: Mathlib.Data.Fintype.Perm

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

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

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

Goal state before:
pp: n : ℕ
⊢ (∏ x ∈ finPairsLT n, if 1 x.fst ≤ 1 x.snd then -1 else 1) = 1

Tactic:
conv => rhs; rw [← @Finset.prod_const_one _ _ (finPairsLT n)]

Goal state after:
n : ℕ
⊢ (∏ x ∈ finPairsLT n, if 1 x.fst ≤ 1 x.snd then -1 else 1) = ∏ _x ∈ finPairsLT n, 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
⊢ signAux ((e.symm.trans f).trans e) = if x = f x then signAux2 l f else -signAux2 l (swap x (f x) * f)

Tactic:
have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l := fun y hy =>
        have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
        List.mem_of_ne_of_mem this.2 (h _ this.1)

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
⊢ signAux ((e.symm.trans f).trans e) = if x = f x then signAux2 l f else -signAux2 l (swap x (f x) * f)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
⊢ ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ (n + 1)) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
intro b x f hb h

Goal state after:
case succ
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y ↦ (swap x y).signAux3 hs = -1

Tactic:
by
  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin α
  induction s using Quotient.inductionOn with | _ l => ?_
  change
    signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧
    Pairwise fun x y => signAux2 l (swap x y) = -1
  have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e :=
    Equiv.ext fun h => by simp [mul_apply]
  constructor
  · rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]
  · intro x y hxy
    rw [← e.injective.ne_iff] at hxy
    rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hxy]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
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 ι
i : ι
y : N i
⊢ ∀ x ∈ Finset.univ.erase i, (ϕ x) (Pi.mulSingle i y x) = 1

Tactic:
intro j hj
    simp only [Finset.mem_erase] at hj
    simp [hj]

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

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : (↑s).Subsingleton
⊢ (↑(range #s)).Subsingleton

Tactic:
Set.Subsingleton,

Goal state after:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : ∀ ⦃x : α⦄, x ∈ ↑s → ∀ ⦃y : α⦄, y ∈ ↑s → x = y
⊢ ∀ ⦃x : ℕ⦄, x ∈ ↑(range #s) → ∀ ⦃y : ℕ⦄, y ∈ ↑(range #s) → x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
a✝ : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
⊢ (τ * σ * τ⁻¹ * (τ * π * τ⁻¹)).cycleType = σ.cycleType + π.cycleType

Tactic:
(hd.conj _).cycleType_mul,

Goal state after:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
a✝ : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
⊢ (τ * σ * τ⁻¹).cycleType + (τ * π * τ⁻¹).cycleType = σ.cycleType + π.cycleType
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ (Multiset.map (fun n ↦ -(-1) ^ n) (a ::ₘ s)).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
    simp only [pow_add, pow_one, neg_mul, mul_neg, mul_assoc, mul_one]

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

Goal state before:
pp: case hg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x).IsCycle

pp: case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x) x ≠ x

Tactic:
· exact isCycle_cycleOf g hx

Goal state after:
case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x) x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case h
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ Commute g⁻¹ (g.cycleOf x)

Tactic:
Commute.inv_left_iff,

Goal state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ Commute g (g.cycleOf x)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

Tactic:
let σ : α ≃ α := ⟨f, f ^ (p ^ n - 1),
    leftInverse_iff_comp.mpr ((pow_sub_mul_pow f (Nat.one_le_pow n p hp.out.pos)).trans hf),
    leftInverse_iff_comp.mpr ((pow_mul_pow_sub f (Nat.one_le_pow n p hp.out.pos)).trans hf)⟩

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.partition = τ.partition

Tactic:
Nat.Partition.ext_iff,

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.partition.parts = τ.partition.parts
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ [a, g a, g (g a)].Nodup ↔ a ∈ g.support

Tactic:
by
  constructor
  · intro ha
    rw [mem_support]
    grind
  rw [← support_eq_iff_mem_support hg3]
  intro ha
  suffices g.support.card = 3 by grind
  exact hg3.card_support

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ (Function.update m i (c • x) i_1) (p i_1)) = c • (f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1)

Tactic:
simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.smul_apply,
      (f p).map_update_smul]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute z c ↔ ∃ (hc : ∀ (x : α), z x ∈ c.support ↔ x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c

Tactic:
exact IsCycle.commute_iff (mem_cycleFactorsFinset_iff.mp hc).1

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
c : R
x : M 0
⊢ f (Fin.cons (c • x) m) = c • f (Fin.cons x m)

Tactic:
by
  simp_rw [← update_cons_zero x m (c • x), f.map_update_smul, update_cons_zero]

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
d : n → R
σ : Perm n
hσ : σ = 1
⊢ σ ∉ ofSign (-1)

Tactic:
rw [hσ, mem_ofSign, sign_one]

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
σ : Perm n
hσ : σ = 1
⊢ ¬1 = -1
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
s t : ℤˣ
⊢ a * detp s A + b * detp t A = b * detp s A + a * detp t A

Tactic:
obtain rfl | rfl := Int.units_eq_one_or s <;> obtain rfl | rfl := Int.units_eq_one_or t

Goal state after:
case inl.inl
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
⊢ a * detp 1 A + b * detp 1 A = b * detp 1 A + a * detp 1 A

case inl.inr
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
⊢ a * detp 1 A + b * detp (-1) A = b * detp 1 A + a * detp (-1) A

case inr.inl
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
⊢ a * detp (-1) A + b * detp 1 A = b * detp (-1) A + a * detp 1 A

case inr.inr
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
⊢ a * detp (-1) A + b * detp (-1) A = b * detp (-1) A + a * 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
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))

Tactic:
of_apply,

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
⊢ ∑ σ ∈ ofSign s with σ none = i, ∏ k ∈ {none}ᶜ, A k (σ k) =
    detp (sign (swap none i) * s) (A.submatrix some (⇑(swap none i) ∘ some))
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₂
α : ι → 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
A_eq_BC : (fun 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)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
i : ι
hi : ¬i = i₀
⊢ update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) i = ∑ j ∈ C i, g i j

Tactic:
· simp only [C, hi, update_of_ne, Ne, not_false_iff]

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 : c.IsColimit
s : Cocone F
j : J
⊢ ((F.coconeTypesEquiv c).ι.app j ≫ ↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x) = s.ι.app j

Tactic:
by
          ext x
          exact congr_fun (hc.fac (F.coconeTypesEquiv.symm s) j) x

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 : c.IsColimit
s : Cocone F
m : (F.coconeTypesEquiv c).pt ⟶ s.pt
hm : ∀ (j : J), (F.coconeTypesEquiv c).ι.app j ≫ m = s.ι.app j
x : (F.coconeTypesEquiv c).pt
j : J
y : F.obj j
⊢ ((ConcreteCategory.hom m).toFun ∘ c.ι j) y =
    ((ConcreteCategory.hom (↾fun x ↦ hc.desc (F.coconeTypesEquiv.symm s) x)).toFun ∘ c.ι j) y

Tactic:
by simp [← hm j]

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

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
⊢ c.IsColimit → Nonempty (Limits.IsColimit (F.coconeTypesEquiv c))

Tactic:
intro hc
    exact
     ⟨{ desc s := ↾fun x => hc.desc (F.coconeTypesEquiv.symm s) x
        fac s j := by
          ext x
          exact congr_fun (hc.fac (F.coconeTypesEquiv.symm s) j) x
        uniq s m hm := by
          ext x
          exact congr_fun (hc.funext fun j ↦ funext fun y ↦ by simp [← hm j]) x }⟩

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
x✝ : Nonempty (IsLimit c)
s : (j : J) → F.obj j
hs : s ∈ F.sections
t : IsLimit c
cs : Cone F := coneOfSection ⋯
x : c.pt
hx : (fun x ↦ ∀ (j : J), (hom (c.π.app j)) x = s j) x
j : J
⊢ (↾fun x_1 ↦ x) ≫ c.π.app j = cs.π.app j

Tactic:
by ext; exact hx j

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0

Tactic:
simp only [det_succ_row_zero, det_unique, Fin.default_eq_zero, submatrix_apply,
    Fin.succ_zero_eq_one, Fin.sum_univ_succ, Fin.val_zero, Fin.zero_succAbove, univ_unique,
    Fin.val_succ, Fin.val_eq_zero, Fin.succ_succAbove_zero, sum_singleton]

Goal state after:
R : Type v
inst✝ : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ (-1) ^ 0 * A 0 0 * A 1 1 + (-1) ^ (0 + 1) * A 0 1 * A 1 0 = A 0 0 * A 1 1 - A 0 1 * A 1 0
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : uncurry.obj F₁ = uncurry.obj F₂
⊢ curry.obj (uncurry.obj F₁) = F₂

Tactic:
← curry_obj_uncurry_obj F₂,

Goal state after:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : uncurry.obj F₁ = uncurry.obj F₂
⊢ curry.obj (uncurry.obj F₁) = curry.obj (uncurry.obj F₂)
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
x✝ : Cᵒᵖ
⊢ Small.{w, v} ((yoneda.obj X).obj x✝)

Tactic:
by dsimp; infer_instance

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ᵒᵖ
x✝ : C
⊢ Small.{w, v} ((coyoneda.obj X).obj x✝)

Tactic:
by dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
s : Cocone F
k : J
⊢ (coconeOfIsFiltered hc j).ι.app k ≫
      ofHom
        (let __spread.0 := RingCat.Hom.hom (hc.desc ((forget₂ (AlgCat R) RingCat).mapCocone s));
        { toRingHom := __spread.0, commutes' := ⋯ }) =
    s.ι.app k

Tactic:
by
    ext
    apply elementwise_of% hc.fac

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 : C
⊢ (α_ X (𝟙_ C) Y).inv ≫ (α_ X (𝟙_ C) Y).hom ≫ X ◁ (λ_ Y).hom = X ◁ (λ_ Y).hom

Tactic:
Iso.inv_hom_id_assoc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ (λ_ Y).hom = X ◁ (λ_ Y).hom
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = ε G ≫ G.map (ε F)

Tactic:
← unit_app_unit_comp_map_η adj,

Goal state after:
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
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ adj.unit.app (𝟙_ C) = (adj.unit.app (𝟙_ C) ≫ G.map (η F)) ≫ G.map (ε F)
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv

Tactic:
by
  rw [← associativity_assoc, ← F.map_comp, Iso.hom_inv_id, map_id, Category.comp_id]

Goal state after: