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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
⊢ f a = (swap x y) a

Tactic:
have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
⊢ f a = (swap x y) a
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : Function.Injective l.get
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False

Tactic:
Function.Injective

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : ∀ ⦃a₁ a₂ : Fin l.length⦄, l.get a₁ = l.get a₂ → a₁ = a₂
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False
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
⊢ x :: y :: l ~r x' :: y' :: l'

Tactic:
use n

Goal state after:
case h
α : 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
⊢ (x :: y :: l).rotate n = x' :: y' :: l'
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ : Perm α
h✝ : σ = τ ∨ σ = swap i j * τ
h : σ = swap i j * τ
⊢ τ = swap i j * σ

Tactic:
by rw [h, swap_mul_self_mul]

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:
swap_mul_swap_mul_swap hwz.symm hyz.symm

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 y z = swap y z
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
have : x ∉ { x | (l.formPerm ^ l.length) x ≠ x } := by
      intro H
      refine hx ?_
      replace H := set_support_zpow_subset l.formPerm l.length H
      simpa using support_formPerm_le' _ H
    simpa using this

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
h₁ : List.map (⇑sign) l = List.replicate l.length (-1)
⊢ sign l.prod = (-1) ^ l.length

Tactic:
rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]

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

Goal state before:
pp: case nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ a ∈ [] ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) []).prod (a, b) = (a, (σ a) b) ∨
    a ∉ [] ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) []).prod (a, b) = (a, b)

Tactic:
refine Or.inr ⟨List.not_mem_nil, ?_⟩
    rw [List.map_nil, List.prod_nil, one_apply]

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

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Tactic:
have := hs.coe_sort
    exact isCycleOn_of_subsingleton _ _

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

Goal state before:
pp: case left
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr 1) = sign σa

Tactic:
induction σa using swap_induction_on with
    | one => simp
    | swap_mul σa' a₁ a₂ ha ih =>
      rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ l.formPerm.IsCycleOn {a | a ∈ l}

Tactic:
by
  refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩
  rw [Set.mem_ofPred, ← List.idxOf_lt_length_iff] at ha hb
  rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb]
  refine ⟨l.idxOf b - l.idxOf a, ?_⟩
  simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_natCast,
    Equiv.Perm.coe_mul, List.formPerm_pow_apply_getElem _ h, Function.comp]
  rw [add_comm]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: 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
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
⊢ orderOf ((ϕ i) g') ∣ Fintype.card (H i)

Tactic:
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card

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

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

Tactic:
by_cases hx : f x = x
  · rw [(cycleOf_eq_one_iff _).mpr hx]
    simp [hx]
  · rw [mem_support, cycleOf_apply]
    split_ifs with hy
    · simp only [hx, hy, Ne, not_false_iff, and_self_iff, mem_support]
      rcases hy with ⟨k, rfl⟩
      rw [← notMem_support]
      simpa using hx
    · simpa [hx] using hy

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: 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
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf ((noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g) ∣ Fintype.card ((i_1 : { j // j ≠ i }) → H ↑i_1)

Tactic:
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card

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

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ (∃ m < Fintype.card α, (f ^ m) x = y) → f.SameCycle x y

Tactic:
rintro ⟨n, _, hn⟩

Goal state after:
case mp
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
n : ℕ
left✝ : n < Fintype.card α
hn : (f ^ n) x = y
⊢ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

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

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

Goal state before:
pp: case neg
α : 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 → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Tactic:
· rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← notMem_support]
    · exact Finset.notMem_mono (support_zpow_le c k) ha
    · exact ha

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ Function.Injective ⇑(noncommPiCoprod hcomm)

Tactic:
apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep

Goal state after:
case hind
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ iSupIndep fun i ↦ (H i).subtype.range

case hinj
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ ∀ (i : ι), Function.Injective ⇑(H i).subtype
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i < j
⊢ (if i = j then 0 else i + 1) = i + 1

Tactic:
if_neg h.ne

Goal state after:
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i < j
⊢ i + 1 = i + 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
h : i < j
⊢ (if i = j then 0 else ↑i + 1) = ↑i + 1

Tactic:
if_neg h.ne

Goal state after:
n : ℕ
i j : Fin n
h : i < j
⊢ ↑i + 1 = ↑i + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3
ι : 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
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
⊢ (g.cycleOf x) y = y ∨ g' y = y

Tactic:
by_contra! ⟨hgy, hg'y⟩

Goal state after:
case refine_3
ι : 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
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
⊢ False
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p : Fin (n + 1)
⊢ cons (x p) (p.removeNth x) = x ∘ ⇑(Equiv.symm p.cycleRange)

Tactic:
by
  ext i
  cases i using Fin.cons <;> simp [Fin.removeNth_apply]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
⊢ sign σ = if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)

Tactic:
sign_of_cycleType',

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
⊢ (Multiset.map (fun n ↦ -(-1) ^ n) σ.cycleType).prod =
    if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : List.Vector G n
⊢ (v.toList.prod⁻¹ ::ᵥ v).toList.prod = 1

Tactic:
Vector.toList_cons,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : List.Vector G n
⊢ (v.toList.prod⁻¹ :: v.toList).prod = 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inl
n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : x < i
⊢ ↑((⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k)) x) = ↑((i.cycleIcc k) x)

Tactic:
simp [cycleIcc_of_lt (lt_of_lt_of_le ch hij), cycleIcc_of_lt ch]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ IsConj σ τ ↔ σ.partition = τ.partition

Tactic:
rw [isConj_iff_cycleType_eq]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ σ.cycleType = τ.cycleType ↔ σ.partition = τ.partition
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inl
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
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : x₂ < x₁
hlt : σ x₁ < σ x₂
⊢ f (σ ⟨x₁, x₂⟩.snd) (σ ⟨x₁, x₂⟩.fst) =
    ↑↑(if
              σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd <
                σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst then
            1
          else -1) *
      f ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd
        ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst

pp: case 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
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : x₂ < x₁
hle : σ x₂ ≤ σ x₁
⊢ f (σ ⟨x₁, x₂⟩.snd) (σ ⟨x₁, x₂⟩.fst) =
    ↑↑(if
              σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd <
                σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst then
            1
          else -1) *
      f ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd
        ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst

Tactic:
· simp [inf_eq_left.2 hlt.le, sup_eq_right.2 hlt.le, hx.not_gt, ← hf]

Goal state after:
case 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
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x✝ : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : x₂ < x₁
hle : σ x₂ ≤ σ x₁
⊢ f (σ ⟨x₁, x₂⟩.snd) (σ ⟨x₁, x₂⟩.fst) =
    ↑↑(if
              σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd <
                σ⁻¹ ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst then
            1
          else -1) *
      f ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.snd
        ⟨max (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd), min (σ ⟨x₁, x₂⟩.fst) (σ ⟨x₁, x₂⟩.snd)⟩.fst
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y).cycleType + (swap z t).cycleType = {2, 2}

Tactic:
isSwap_iff_cycleType.mp ?_,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ {2} + (swap z t).cycleType = {2, 2}

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y).IsSwap
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
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬Injective v
⊢ f v = 0

Tactic:
Function.Injective

Goal state after:
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
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬∀ ⦃a₁ a₂ : ι⦄, v a₁ = v a₂ → a₁ = a₂
⊢ f v = 0
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✝² : DistribSMul S M₂
inst✝¹ : SMulCommClass R S M₂
c : S
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
l : (i : ι) → M₁ i
i : ι
x : R
d : M₁ i
⊢ c • f (update l i (x • d)) = x • c • f (update l i d)

Tactic:
simp [← smul_comm x c (_ : M₂)]

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

Goal state before:
pp: ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ f (update v i (g i • v i)) = 0

Tactic:
rw [h, f.map_update_neg, f.map_update_sum, neg_eq_zero]

Goal state after:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ ∑ a ∈ s.erase i, f (update v i (g a • v a)) = 0
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 : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
⊢ f (t.piecewise (m + m'') m'') + f (t.piecewise (m + m') m') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')

Tactic:
Finset.sum_powerset_insert hit,

Goal state after:
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
⊢ f (t.piecewise (m + m'') m'') + f (t.piecewise (m + m') m') =
    ∑ t ∈ t.powerset, f (t.piecewise m m') + ∑ t ∈ t.powerset, f ((insert i t).piecewise m m')
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : j = i
⊢ (insert i s).piecewise m m' i = s.piecewise m m'' i

Tactic:
simp [m'', Finset.notMem_of_mem_powerset_of_notMem hs hit]

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

Goal state before:
pp: case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' ((ConcreteCategory.hom (F.map f)) x)) = descFunLift F s (Prequotient.of j x)

Tactic:
exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x

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 : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ adjp s A none (some i) = detp (-s) (A.submatrix (Function.update some i none) some)

Tactic:
rw [← detp_transpose]

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ adjp s A none (some i) = detp (-s) (A.submatrix (Function.update some i none) some)ᵀ
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (x.mul (y.add z)) = descFunLift F s ((x.mul y).add (x.mul z))

Tactic:
| left_distrib x y z =>

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

Goal state before:
pp: case a.map
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' ((ConcreteCategory.hom (F.map f)) x)) = descFunLift F s (Prequotient.of j x)

Tactic:
exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x

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

Goal state before:
pp: case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s (x.mul (y.add z)) = descFunLift F s ((x.mul y).add (x.mul z))

Tactic:
| left_distrib x y z =>

Goal state after: