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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x = x ↔ l.length ≤ 1

Tactic:
by
  obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  rw [formPerm_apply_getElem _ hl k hk, hl.getElem_inj_iff]
  cases hn : l.length
  · exact absurd k.zero_le (hk.trans_le hn.le).not_ge
  · rw [hn] at hk
    rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'
    · simp [← hk', eq_comm]
    · simpa [Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.succ_lt_succ_iff] using
        (k.zero_le.trans_lt hk').ne.symm

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

Goal state before:
pp: x y : Fin 1
⊢ x ≠ y → (swap x y).signAux = -1

Tactic:
dsimp [signAux, swap, swapCore]

Goal state after:
x y : Fin 1
⊢ ¬x = y →
    (∏ x_1 ∈ finPairsLT 1,
        if
            (if x_1.fst = x then y else if x_1.fst = y then x else x_1.fst) ≤
              if x_1.snd = x then y else if x_1.snd = y then x else x_1.snd then
          -1
        else 1) =
      -1
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
⊢ swap x ((σ ^ (n + 1)) x) ∈ H

pp: case neg
α : 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
⊢ swap x ((σ ^ (n + 1)) x) ∈ H

Tactic:
· rw [pow_succ', mul_apply, ← h5]
        exact h4

Goal state after:
case neg
α : 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
⊢ swap x ((σ ^ (n + 1)) x) ∈ H
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : ¬f.SameCycle x z
⊢ z = (f.cycleOf y) z

Tactic:
· exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm

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

Goal state before:
pp: α : Type u_2
g : Perm α
s : Finset α
hs : ∀ (x : α), g x ∈ s ↔ x ∈ s
i : ℤ
x : α
hx : x ∈ s
⊢ ↑((g.subtypePerm hs ^ i) ⟨x, hx⟩) = (g ^ i) x

Tactic:
by
  simp only [subtypePerm_zpow, subtypePerm_apply]

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

Goal state before:
pp: case neg.ha
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∉ c.support

Tactic:
· exact ha

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ Fintype.card α < 2 * orderOf σ

Tactic:
← one_mul (Fintype.card α),

Goal state after:
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ 1 * Fintype.card α < 2 * orderOf σ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i ≤ j
⊢ Perm.sign (i.cycleIcc j) = (-1) ^ (↑j - ↑i)

Tactic:
simp [hij, sub_val_of_le hij]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Perm.sign (i.cycleIcc i) = 1

Tactic:
rw [sign_cycleIcc_of_le (Fin.ge_of_eq rfl), tsub_self, pow_zero]

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

Goal state before:
pp: 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
this : (∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2) ↔ x2 < x1
⊢ ⟨x1, x2⟩ ∈ Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D ↔ ⟨x1, x2⟩ ∈ D

Tactic:
simpa [hD]

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 : ι
x y : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ (Function.update m i (x + y) i_1) (p i_1)) =
    ((f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1)) + (f p) fun i_1 ↦ (Function.update m i y i_1) (p i_1)

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

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

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

Tactic:
apply exists_congr

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ ∀ (a : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support),
    k.subtypePerm a ∈ Subgroup.zpowers c.subtypePermOfSupport ↔ k.subtypePerm a ∈ Subgroup.zpowers (g.subtypePerm ⋯)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
apply exists_congr

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support
⊢ ∀ (a : ℤ), c.subtypePermOfSupport ^ a = k.subtypePerm hc' ↔ g.subtypePerm ⋯ ^ a = k.subtypePerm hc'
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'✝ f f' : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update m i (c • x)) + f' (update m i (c • x)) = c • (f (update m i x) + f' (update m i x))

Tactic:
by
      simp [smul_add]

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✝¹ : Subsingleton ι
i : ι
f : M₂ →ₗ[R] M₃
inst✝ : DecidableEq ι
m✝ : ι → M₂
i✝ : ι
x✝ y✝ : M₂
⊢ f (update m✝ i✝ (x✝ + y✝) i) = f (update m✝ i✝ x✝ i) + f (update m✝ i✝ y✝ i)

Tactic:
simp [update_eq_const_of_subsingleton]

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✝¹ : Subsingleton ι
i : ι
f : M₂ →ₗ[R] M₃
inst✝ : DecidableEq ι
m✝ : ι → M₂
i✝ : ι
c✝ : R
x✝ : M₂
⊢ f (update m✝ i✝ (c✝ • x✝) i) = c✝ • f (update m✝ i✝ x✝ i)

Tactic:
simp [update_eq_const_of_subsingleton]

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
⊢ detp (-1) 1 = 0

Tactic:
rw [← diagonal_one, detp_neg_one_diagonal]

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
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
s t : ℤˣ
x✝¹ : Perm n
x✝ : x✝¹ ∈ ofSign 1
⊢ ∀ i ∈ univ, A i (x✝¹ i) = A ((swap p q) i) (((Equiv.mulRight (swap p q)) x✝¹) ((swap p q) i))

Tactic:
aesop (add simp row)

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

Goal state before:
pp: case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
hσ : σ ∈ ofSign 1
⊢ 1 • ∏ x, M (σ⁻¹ x) x = ∏ k, M k (σ k)

Tactic:
← Equiv.prod_comp σ

Goal state after:
case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
hσ : σ ∈ ofSign 1
⊢ 1 • ∏ i, M (σ⁻¹ (σ i)) (σ i) = ∏ k, M k (σ k)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
hσ : σ ∈ ofSign (-1)
⊢ -1 • ∏ x, M (σ⁻¹ x) x = -∏ k, M k (σ k)

Tactic:
← Equiv.prod_comp σ

Goal state after:
case refine_2
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
hσ : σ ∈ ofSign (-1)
⊢ -1 • ∏ i, M (σ⁻¹ (σ i)) (σ i) = -∏ k, M 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
⊢ detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
have hf {s t} {σ : Perm n} (hσ : σ ∈ ofSign s) :
      ofSign (t * s) = (ofSign t).map (mulRightEmbedding σ) := by
    ext τ
    simp_rw [mem_map, mulRightEmbedding_apply, ← eq_mul_inv_iff_mul_eq, exists_eq_right,
      mem_ofSign, map_mul, map_inv, mul_inv_eq_iff_eq_mul, mem_ofSign.mp hσ]
  have h {s t} : detp s A * detp t B =
      ∑ σ ∈ ofSign s, ∑ τ ∈ ofSign (t * s), ∏ k, A k (σ k) * B (σ k) (τ k) := by
    simp_rw [detp, sum_mul_sum, prod_mul_distrib]
    refine sum_congr rfl fun σ hσ ↦ ?_
    simp_rw [hf hσ, sum_map, mulRightEmbedding_apply, Perm.mul_apply]
    exact sum_congr rfl fun τ hτ ↦ (congr_arg (_ * ·) (Equiv.prod_comp σ _).symm)
  let ι : Perm n ↪ (n → n) := ⟨_, coe_fn_injective⟩
  have hι {σ x} : ι σ x = σ x := rfl
  let bij : Finset (n → n) := (disjUnion (ofSign 1) (ofSign (-1)) ofSign_disjoint).map ι
  replace h (s) : detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i : n, A i (σ i) * B (σ i) (τ i) +
        (detp 1 A * detp s B + detp (-1) A * detp (-s) B) := by
    simp_rw [h, neg_mul_neg, mul_one, detp, mul_apply, prod_univ_sum, Fintype.piFinset_univ]
    rw [sum_comm, ← sum_compl_add_sum bij, sum_map, sum_disjUnion]
    simp_rw [hι]
  rw [h, h, neg_neg, add_assoc]
  conv_rhs => rw [add_assoc]
  refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (add_comm _ _)
  replace hσ : ¬ Function.Injective σ := by
    contrapose hσ
    rw [notMem_compl, mem_map, ofSign_disjUnion]
    exact ⟨Equiv.ofBijective σ hσ.bijective_of_finite, mem_univ _, rfl⟩
  obtain ⟨i, j, hσ, hij⟩ := Function.not_injective_iff.mp hσ
  replace hσ k : σ (swap i j k) = σ k := by
    rw [swap_apply_def]
    split_ifs with h h <;> simp only [hσ, h]
  rw [← mul_neg_one, hf (mem_ofSign.mpr (sign_swap hij)), sum_map]
  simp_rw [prod_mul_distrib, mulRightEmbedding_apply, Perm.mul_apply]
  refine sum_congr rfl fun τ hτ ↦ congr_arg (_ * ·) ?_
  rw [← Equiv.prod_comp (swap i j)]
  simp only [hσ]

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
α : Type u_3
inst✝³ : Monoid α
inst✝² : MulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ (c • 1) ^ Fintype.card n * A.det = c ^ Fintype.card n • A.det

Tactic:
smul_pow,

Goal state after:
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
R : Type v
inst✝⁴ : CommRing R
α : Type u_3
inst✝³ : Monoid α
inst✝² : MulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ c ^ Fintype.card n • 1 ^ Fintype.card n * A.det = c ^ Fintype.card n • A.det
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:
by
  classical
    simp_rw [det_apply']
    convert!
      Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_
    · simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]
      refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
      · intro σ₁₂ _
        simp
      · intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x
      · intro σ hσ
        rw [mem_coe, Set.mem_toFinset] at hσ
        obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
        use σ₁₂
        rw [← hσ₁₂]
        simp
      · simp only [forall_prop_of_true, Prod.forall, mem_univ]
        intro σ₁ σ₂
        rw [Fintype.prod_sum_type]
        simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
        rw [mul_mul_mul_comm]
        congr
        rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
    · rintro σ - hσn
      have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by
        rw [Set.mem_toFinset] at hσn
        simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using
          mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn
      obtain ⟨a, ha⟩ := not_forall.mp h1
      rcases hx : σ (Sum.inl a) with a2 | b
      · have hn := (not_exists.mp ha) a2
        exact absurd hx.symm hn
      · rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]
        rw [hx, fromBlocks_apply₂₁, zero_apply]

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

Goal state before:
pp: case insert.e_a
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ f (update (s.piecewise b a) k (s.piecewise b a k - b k)) =
    f fun j ↦ if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j

Tactic:
congr; ext i; split_ifs with h₁ h₂
    · rw [update_of_ne, Finset.piecewise_eq_of_notMem]
      · exact fun h ↦ (hk i h).not_gt (h₁ <| .inr h)
      · exact fun h ↦ (h₁ <| .inl h).ne h
    · cases h₂
      rw [update_self, s.piecewise_eq_of_notMem _ _ (lt_irrefl _ <| hk k ·)]
    · push Not at h₁
      rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]

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

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

Tactic:
if_neg hji

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

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
x y : ↑s✝.1
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) x * (ConcreteCategory.hom (s✝.π.app j)) y, ⋯⟩ =
    (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) x, ⋯⟩ *
      (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) y, ⋯⟩

Tactic:
rw [← equivShrink_mul]

Goal state after:
case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
x y : ↑s✝.1
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) x * (ConcreteCategory.hom (s✝.π.app j)) y, ⋯⟩ =
    (equivShrink ↑(F ⋙ forget MonCat).sections)
      (⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) x, ⋯⟩ * ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) y, ⋯⟩)
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
x✝ : D
⊢ (λ_ (F.obj x✝)).hom = fData.εIso.hom ▷ F.obj x✝ ≫ (fData.μIso (𝟙_ D) x✝).hom ≫ F.map (λ_ x✝).hom

Tactic:
simp [fData.leftUnitor_eq]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.ZModuleEquivalence

Goal state before:
pp: A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
⊢ { toFun := ⇑(ConcreteCategory.hom f), map_add' := ⋯ }.toFun (n • x) =
    (RingHom.id ℤ) n • { toFun := ⇑(ConcreteCategory.hom f), map_add' := ⋯ }.toFun x

Tactic:
convert! AddMonoidHom.map_zsmul f.hom n x

Goal state after:
case e'_2.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
e_2✝ : ↑A = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A)
⊢ DistribMulAction.toDistribSMul.toSMul = ZSMul.toSMul

case e'_3.e'_4.e'_3
A B : ModuleCat ℤ
f : (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj A ⟶ (forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B
n : ℤ
x : ↑A
e_1✝ : ↑B = ↑((forget₂ (ModuleCat ℤ) AddCommGrpCat).obj B)
⊢ DistribMulAction.toDistribSMul.toSMul = ZSMul.toSMul
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
⊢ Mono f

Tactic:
have := PullbackCone.isLimitMkIdId (F.map f)

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono f
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ (ConcreteCategory.hom (F.map w✝¹ ≫ c.ι.app w✝²)) w✝ - (Hom.hom (c.ι.app w✝³)) w✝ = 0

Tactic:
c.ι.naturality

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ (ConcreteCategory.hom (c.ι.app w✝³ ≫ ((Functor.const J).obj c.pt).map w✝¹)) w✝ - (Hom.hom (c.ι.app w✝³)) w✝ = 0
Module: Mathlib.CategoryTheory.Functor.TwoSquare

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₃, u₃} C₃
inst✝⁵ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst✝⁴ : Category.{v₅, u₅} C₅
inst✝³ : Category.{v₆, u₆} C₆
inst✝² : Category.{v₇, u₇} C₇
inst✝¹ : Category.{v₈, u₈} C₈
T' : C₂ ⥤ C₅
R' : C₅ ⥤ C₆
B' : C₄ ⥤ C₆
L' : C₃ ⥤ C₇
R'' : C₄ ⥤ C₈
B'' : C₇ ⥤ C₈
C₉ : Type u₉
inst✝ : Category.{v₉, u₉} C₉
R₃ : C₆ ⥤ C₉
B₃ : C₈ ⥤ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
c : C₁
⊢ R₃.map (w₂.natTrans.app (T.obj c)) ≫
      R₃.map (B'.map (w₁.natTrans.app c)) ≫ w₄.natTrans.app (B.obj (L.obj c)) ≫ B₃.map (w₃.natTrans.app (L.obj c)) =
    R₃.map (w₂.natTrans.app (T.obj c)) ≫
      w₄.natTrans.app (R.obj (T.obj c)) ≫ B₃.map (R''.map (w₁.natTrans.app c)) ≫ B₃.map (w₃.natTrans.app (L.obj c))

Tactic:
slice_rhs 2 3 =>
    rw [← Functor.comp_map _ B₃, ← w₄.naturality]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₃, u₃} C₃
inst✝⁵ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst✝⁴ : Category.{v₅, u₅} C₅
inst✝³ : Category.{v₆, u₆} C₆
inst✝² : Category.{v₇, u₇} C₇
inst✝¹ : Category.{v₈, u₈} C₈
T' : C₂ ⥤ C₅
R' : C₅ ⥤ C₆
B' : C₄ ⥤ C₆
L' : C₃ ⥤ C₇
R'' : C₄ ⥤ C₈
B'' : C₇ ⥤ C₈
C₉ : Type u₉
inst✝ : Category.{v₉, u₉} C₉
R₃ : C₆ ⥤ C₉
B₃ : C₈ ⥤ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
c : C₁
⊢ R₃.map (w₂.natTrans.app (T.obj c)) ≫
      R₃.map (B'.map (w₁.natTrans.app c)) ≫ w₄.natTrans.app (B.obj (L.obj c)) ≫ B₃.map (w₃.natTrans.app (L.obj c)) =
    R₃.map (w₂.natTrans.app (T.obj c)) ≫
      ((B' ⋙ R₃).map (w₁.natTrans.app c) ≫ w₄.app (B.obj (L.obj c))) ≫ B₃.map (w₃.natTrans.app (L.obj c))