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

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k ⋯).support = (insert i s).biUnion fun i ↦ (k i).support

Tactic:
| insert i s hi hrec =>

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

Goal state before:
pp: case h.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
a : m
⊢ ((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2) (Sum.inl a) = σ (Sum.inl a)

pp: case h.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
b : n
⊢ ((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2) (Sum.inr b) = σ (Sum.inr b)

Tactic:
· rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inl_injective, ofInjective_apply]
    rfl

Goal state after:
case h.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
b : n
⊢ ((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2) (Sum.inr b) = σ (Sum.inr b)
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {s : Finset α} {f : Equiv.Perm α}, f ∈ permsOfFinset s ↔ ∀ {x : α}, f x ≠ x → x ∈ s

Tactic:
by
  rintro ⟨⟨l⟩, hs⟩ f; exact mem_permsOfList_iff

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

Goal state before:
pp: case h.h.succ.e_i
α : 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
⊢ ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length =
    ((k + n) % (x :: y :: l).length + 1) % (x :: y :: l).length

Tactic:
rw [hl, Nat.mod_eq_of_lt hk', add_right_comm]

Goal state after:
case h.h.succ.e_i
α : 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
⊢ (k + n + 1) % (x' :: y' :: l').length = ((k + n) % (x' :: y' :: l').length + 1) % (x' :: y' :: l').length
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
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔ x :: y :: l ~r x' :: y' :: l'

Tactic:
by
  refine ⟨fun h => ?_, fun hr => formPerm_eq_of_isRotated hd hr⟩
  rw [Equiv.Perm.ext_iff] at h
  have hx : x' ∈ x :: y :: l := by
    have : x' ∈ { z | formPerm (x :: y :: l) z ≠ z } := by
      rw [Set.mem_ofPred_eq, h x', formPerm_apply_head _ _ _ hd']
      simp only [mem_cons, nodup_cons] at hd'
      push Not at hd'
      exact hd'.left.left.symm
    simpa using support_formPerm_le' _ this
  obtain ⟨⟨n, hn⟩, hx'⟩ := get_of_mem hx
  have hl : (x :: y :: l).length = (x' :: y' :: l').length := by
    rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
    refine congr_arg Finset.card ?_
    rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ←
      support_formPerm_of_nodup' _ hd' (by simp)]
    simp only [h]
  use n
  apply List.ext_getElem
  · rw [length_rotate, hl]
  · intro k hk hk'
    rw [getElem_rotate]
    induction k with
    | zero =>
      refine Eq.trans ?_ hx'
      congr
      simpa using hn
    | succ k IH =>
      conv => congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])
      rw [← formPerm_apply_getElem _ hd' k (k.lt_succ_self.trans hk'),
        ← IH (k.lt_succ_self.trans hk), ← h, formPerm_apply_getElem _ hd]
      congr 1
      rw [hl, Nat.mod_eq_of_lt hk', add_right_comm]
      apply Nat.add_mod

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x

Tactic:
← zpow_apply_eq_self_of_apply_eq_self hy i,

Goal state after:
α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : (f ^ i) x = (f ^ i) y
⊢ f x = x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝ : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
⊢ IsConj (σ * τ) (π * ρ)

Tactic:
by
  classical
  cases nonempty_fintype α
  obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
  obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
  have hd1' := coe_inj.2 hd1.support_mul
  have hd2' := coe_inj.2 hd2.support_mul
  rw [coe_union] at *
  have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
  have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
  refine isConj_of_support_equiv ?_ ?_
  · refine ((Equiv.setCongr hd1').trans (Equiv.Set.union hd1'')).trans <|
      (Equiv.sumCongr (subtypeEquiv f fun a => ?_) <| subtypeEquiv g fun a => ?_).trans
        ((Equiv.setCongr hd2').trans (Equiv.Set.union hd2'')).symm <;>
      simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]
  intro x hx
  simp only [trans_apply, symm_trans_apply, Equiv.setCongr_apply, Equiv.setCongr_symm_apply,
    Equiv.sumCongr_apply]
  rw [hd1', Set.mem_union] at hx
  rcases hx with hxσ | hxτ
  · rw [mem_coe, mem_support] at hxσ
    rw [Set.union_apply_left, Set.union_apply_left]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
        Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq, coe_inv]
      have h := (hd2 (f x)).resolve_left ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]
  · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
    rw [Set.union_apply_right, Set.union_apply_right]
    · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
        Set.union_symm_apply_right, Subtype.coe_mk]
      have h := (hd2 (g (τ x))).resolve_right ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [coe_inv, coe_inv, symm_apply_apply, h, (hd1 (τ x)).resolve_right hxτ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]
    · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
    · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
        mem_coe, mem_support]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
⊢ ∀ a ∈ (ofSubtype x).support, ∀ b ∈ σ.support, a ≠ b

Tactic:
rintro a ha b hb rfl

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
a : α
ha : a ∈ (ofSubtype x).support
hb : a ∈ σ.support
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
obtain ⟨i, hi⟩ := isCycle_swap_mul_aux₁ n hb <| by
      rw [← mul_apply, ← pow_succ]; simpa [pow_succ', eq_symm_apply] using! h

Goal state after:
case inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) 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 α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
h : Fin n
⊢ ((e.symm.trans (f * g)).trans e) h = ((e.symm.trans f).trans e * (e.symm.trans g).trans e) h

Tactic:
by simp [mul_apply]

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

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : f ^ n = 1
⊢ ∃ x, f x ≠ x ∧ (f ^ n) x = x

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Goal state after:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : f ^ n = 1
x : β
hx : f x ≠ x
⊢ ∃ x, f x ≠ x ∧ (f ^ n) x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
⊢ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Goal state after:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
x : β
hx : f x ≠ x
⊢ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
b : α
a✝ : b ∈ ⊤
⊢ b ∈ l.toFinset

Tactic:
exact List.mem_toFinset.mpr (mem_l b)

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ (f.cycleOf x) (f x) = f (f x)

Tactic:
by
  convert! cycleOf_apply_apply_pow_self f x 1 using 1

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro.hcomm
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)
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ∀ (x : H ↑i✝) (y : H ↑j✝), Commute ((ϕ ↑i✝) x) ((ϕ ↑j✝) y)

Tactic:
apply hcomm

Goal state after:
case intro.hcomm
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 ι := ⋯
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ↑i✝ ≠ ↑j✝
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
mem_support_cycleOf_iff_aux,

Goal state after:
α : Type u_2
f : Perm α
x y : α
hx : f x ≠ x
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ f.SameCycle x y ∧ x ∈ f.support ↔ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p

Tactic:
← orderOf_dvd_iff_pow_eq_one,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ orderOf σ ∣ p ↔ ∀ c ∈ σ.cycleType, c = p
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case refine_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Tactic:
· intro i
    by_cases h : i = e x
    · simp [h, Equiv.Perm.decomposeFin]
    · simp [Equiv.Perm.decomposeFin, swap_apply_def, Ne.symm h]

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

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
⊢ ((insert i s).noncommProd k hs').cycleType = ∑ i ∈ insert i s, (k i).cycleType

Tactic:
| insert i s hi hrec =>

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ (- -1) ^ σ.cycleType.card = 1

Tactic:
neg_neg,

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ 1 ^ σ.cycleType.card = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑(vectorsProdEqOne G 1)

Tactic:
rw [one_eq]
  exact Set.uniqueSingleton (Vector.nil.cons 1)

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
⊢ l' ~ l

Tactic:
refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
⊢ l'.prod = l.prod
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
hlt : x2 < x1
hlt' : (Equiv.symm σ) x1 < (Equiv.symm σ) x2
⊢ max (σ ((Equiv.symm σ) x2)) (σ ((Equiv.symm σ) x1)) = x1 ∧ min (σ ((Equiv.symm σ) x2)) (σ ((Equiv.symm σ) x1)) = x2

Tactic:
by simp [hlt.le]

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
hlt : x2 < x1
hle : (Equiv.symm σ) x2 ≤ (Equiv.symm σ) x1
⊢ max (σ ((Equiv.symm σ) x1)) (σ ((Equiv.symm σ) x2)) = x1 ∧ min (σ ((Equiv.symm σ) x1)) (σ ((Equiv.symm σ) x2)) = x2

Tactic:
by simp [hlt.le]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : g.support = {a, g a, g (g a)}
⊢ #g.support = 3

Tactic:
exact hg3.card_support

Goal state after:
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
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M₂
⊢ 0 = 0 x✝

Tactic:
zero_apply

Goal state after:
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
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
m : M
⊢ update (update v i m) j m i = update (update v i m) j m j

Tactic:
rw [Function.update_self, Function.update_of_ne hij, Function.update_self]

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

Goal state before:
pp: case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)

Tactic:
| mul_1 x x' y r ih =>

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

Goal state before:
pp: case a.mul_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)

Tactic:
| mul_1 x x' y r ih =>

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 B : Matrix n n R
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) +
        (detp 1 A * detp (-1) B + detp (-1) A * detp (- -1) B) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
neg_neg,

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)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ f ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g)) =
    g ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g))

Tactic:
← h.homEquiv_naturality_left,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ (h.homEquiv X (coeq (L.map f) (L.map g))) (L.map f ≫ coeqHom (L.map f) (L.map g)) =
    g ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g))
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ (h.homEquiv X (coeq (L.map f) (L.map g))) (L.map f ≫ coeqHom (L.map f) (L.map g)) =
    g ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g))

Tactic:
← h.homEquiv_naturality_left,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ (h.homEquiv X (coeq (L.map f) (L.map g))) (L.map f ≫ coeqHom (L.map f) (L.map g)) =
    (h.homEquiv X (coeq (L.map f) (L.map g))) (L.map g ≫ coeqHom (L.map f) (L.map g))
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)
i : ι
hi : ¬i = i₀
⊢ update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) i = ∑ j ∈ B i, g i j

Tactic:
simp only [B, hi, update_of_ne, Ne, not_false_iff]

Goal state after: