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

Goal state before:
pp: case zero
α : 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
⊢ swap ((σ ^ 0) x) ((σ ^ (0 + 1)) x) ∈ H

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : 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
⊢ swap x ((σ ^ 0) x) ∈ H

Tactic:
| zero =>

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

Goal state before:
pp: case right
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
y : α
hy : y ∈ σ.support
⊢ ∃ a, (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) a = ⟨y, hy⟩

Tactic:
rw [mem_support] at hy

Goal state after:
case right
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
y : α
hy✝ : y ∈ σ.support
hy : σ y ≠ y
⊢ ∃ a, (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) a = ⟨y, hy✝⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case zero
α : Type u_4
inst✝ : DecidableEq α
⊢ ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ 0) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
| zero =>

Goal state after:
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
h6 : x = (σ ^ (n + 1)) 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
h6 : ¬x = (σ ^ (n + 1)) x
⊢ swap x ((σ ^ (n + 1)) x) ∈ H

Tactic:
· rw [← h6, swap_self]
        exact H.one_mem

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
h6 : ¬x = (σ ^ (n + 1)) x
⊢ swap x ((σ ^ (n + 1)) x) ∈ H
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
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
h6 : ¬x = (σ ^ (n + 1)) x
⊢ swap ((σ ^ n) x) ((σ ^ (n + 1)) x) * swap x ((σ ^ n) x) * swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H

Tactic:
exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)

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

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
intro a

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a : Perm α
⊢ ∀ (y : Perm α),
    a ∈ closure S →
      y ∈ closure S →
        ↑a.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(a * y).support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Tactic:
intro a

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
⊢ a ∈ closure S → ∀ b ∈ closure T, _root_.Disjoint a.support b.support
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ closure {σ, swap x ((σ ^ n) x)} = ⊤

Tactic:
by
  rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0
  obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h0
  have h2' : (σ ^ n).support = univ := Eq.trans (support_pow_coprime h0) h2
  have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1
  replace h1' : IsCycle (σ ^ n) :=
    h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm)))
  rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset_iff]
  exact
    ⟨Subgroup.pow_mem (closure _) (subset_closure (Set.mem_insert σ _)) n,
      Set.singleton_subset_iff.mpr (subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _)))⟩

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case zero
α : Type u_1
f : α → α
n : ℕ
a : α
⊢ iterate f a (0 + n) = iterate f a 0 ++ iterate f (f^[0] a) n

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
obtain hfxb | hfxb := eq_or_ne (f x) b
    · exact ⟨0, hfxb⟩
    obtain ⟨hfb, hbx⟩ : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
    replace hb : (swap x (f.symm x) * f⁻¹) (f.symm b) ≠ f.symm b := by
      rw [mul_apply, swap_apply_def]
      split_ifs <;> simp [symm_apply_eq, eq_symm_apply] at * <;> tauto
    obtain ⟨i, hi⟩ := isCycle_swap_mul_aux₁ n hb <| by
      rw [← mul_apply, ← pow_succ]; simpa [pow_succ', eq_symm_apply] using! h
    refine ⟨-i, (swap x (f⁻¹ x) * f⁻¹).injective ?_⟩
    convert! hi using 1
    · rw [zpow_neg, ← inv_zpow, ← mul_apply, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul]
      simp [swap_comm _ x, ← mul_apply, -coe_mul, ← inv_def, -coe_inv, ← inv_def, mul_assoc _ f⁻¹,
        ← mul_zpow_mul, mul_assoc _ _ f]
      simp
    · exact swap_apply_of_ne_of_ne (by simpa [eq_comm, eq_symm_apply, symm_apply_eq] using! hfxb)
        (by simpa [eq_comm, eq_symm_apply, symm_apply_eq])

Goal state after:
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: k : ℕ
m : Multiset ℕ
⊢ k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n

Tactic:
induction m using Quotient.inductionOn; simpa using coprime_list_prod_right_iff

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

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

Tactic:
by
                have : f (f x) ≠ f x := mt (fun h => f.injective h) x.2
                rw [← h _ x.2 this]
                exact mt (hi _ _ this x.2) x.2

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

Goal state before:
pp: α : Type u_2
f : Perm α
⊢ f.IsCycle ↔ ∃ s, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s

Tactic:
by
  refine ⟨fun hf => ⟨{ x | f x ≠ x }, ?_, hf.isCycleOn, fun _ => id⟩, ?_⟩
  · obtain ⟨a, ha⟩ := hf
    exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩
  · rintro ⟨s, hs, hf, hsf⟩
    obtain ⟨a, ha⟩ := hs.nonempty
    exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩

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

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
obtain rfl | hs := Finset.eq_singleton_or_nontrivial ha

Goal state after:
case inl
α : Type u_2
f : Perm α
a : α
n : ℕ
hf : f.IsCycleOn ↑{a}
ha : a ∈ {a}
⊢ (f ^ n) a = a ↔ #{a} ∣ n

case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
⊢ (f ^ n) a = a ↔ #s ∣ n
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (↑n).num * (↑d)⁻¹.num / ↑(((↑n).num * (↑d)⁻¹.num).natAbs.gcd (1 * d)) = ↑n

Tactic:
Rat.inv_natCast_num_of_pos this,

Goal state after:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (↑n).num * 1 / ↑(((↑n).num * 1).natAbs.gcd (1 * d)) = ↑n
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ 1 * d / ((↑n).num * (↑d)⁻¹.num).natAbs.gcd (1 * d) = ↑d

Tactic:
Rat.inv_natCast_num_of_pos this,

Goal state after:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ 1 * d / ((↑n).num * 1).natAbs.gcd (1 * d) = ↑d
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ d / n.natAbs.gcd d = ↑d

Tactic:
Nat.cast_id,

Goal state after:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ d / n.natAbs.gcd d = d
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ hs'.toFinset.toList.formPerm.IsCycleOn s

Tactic:
convert! hs'.toFinset.nodup_toList.isCycleOn_formPerm

Goal state after:
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ s = {a | a ∈ hs'.toFinset.toList}
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
⊢ ∀ c ∈ Finset.univ, (ϕ c) (f c) ∈ ⨆ i, (ϕ i).range

Tactic:
intro i _hi

Goal state after:
case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ (ϕ i) (f i) ∈ ⨆ i, (ϕ i).range
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
⊢ ∀ (a : α), a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Tactic:
intro a

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
⊢ a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
induction f.cycleType using Multiset.induction_on with

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∈ Multiset.map (Finset.card ∘ support) f.cycleFactorsFinset.val

Tactic:
Multiset.mem_map

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ σ.cycleType.card = σ.cycleType.card - 1 + 1

Tactic:
tsub_add_cancel_of_le

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ σ.cycleType.card = σ.cycleType.card

case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ 1 ≤ σ.cycleType.card
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : ↑(n + 1) * orderOf σ < 2 * orderOf σ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle

Tactic:
Nat.cast_id,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : (n + 1) * orderOf σ < 2 * orderOf σ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case zero
⊢ sign (finRotate 0) = (-1) ^ (0 - 1)

Tactic:
| zero =>

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

Goal state before:
pp: case succ.zero
⊢ sign (finRotate (0 + 1)) = (-1) ^ (0 + 1 - 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n : ℕ
hx : 0 < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨0, hx⟩) 0) = ↑⟨0, hx⟩

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
⊢ (cycleRange 2).IsThreeCycle

Tactic:
rw [IsThreeCycle, cycleType_cycleRange two_ne_zero]
  simp

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ∈ (f.cycleOf x).support
⊢ (f.cycleOf x) y = f y

Tactic:
rw [mem_support] at hy

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
⊢ (f.cycleOf x) y = f y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case comm
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ (↑univ).Pairwise (Commute on fun i ↦ ((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) i) (v i))

Tactic:
intro a

Goal state after:
case comm
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
a : ↥f.cycleFactorsFinset
⊢ a ∈ ↑univ →
    ∀ ⦃y : ↥f.cycleFactorsFinset⦄,
      y ∈ ↑univ → a ≠ y → (Commute on fun i ↦ ((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) i) (v i)) a y
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
⊢ ∏ x ∈ Finset.univ.sigma Finset.Iio, f (σ x.snd) (σ x.fst) =
    (∏ i ∈ Finset.univ.sigma Finset.Iio, ↑↑(if σ⁻¹ i.snd < σ⁻¹ i.fst then 1 else -1)) *
      ∏ x ∈ Finset.univ.sigma Finset.Iio, f x.snd x.fst

Tactic:
← Finset.prod_mul_distrib

Goal state after:
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
⊢ ∏ x ∈ Finset.univ.sigma Finset.Iio, f (σ x.snd) (σ x.fst) =
    ∏ x ∈ Finset.univ.sigma Finset.Iio, ↑↑(if σ⁻¹ x.snd < σ⁻¹ x.fst then 1 else -1) * f x.snd x.fst
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support + ↑(Fintype.card α - #σ.support) * 1 = Fintype.card α

Tactic:
Nat.cast_id,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support + (Fintype.card α - #σ.support) * 1 = Fintype.card α
Module: Mathlib.LinearAlgebra.Multilinear.Finsupp

Goal state before:
pp: case zero
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : CommSemiring R
inst✝⁴ : DecidableEq R
inst✝³ : DecidableEq ι'
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : Fintype ι'
x : (i : ι) → κ i →₀ R
⊢ (freeFinsuppEquiv 0) x = ∑ p, 0 p • Finsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
| zero =>

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
hv : ∃ a₁ a₂, v a₁ = v a₂ ∧ a₁ ≠ a₂
⊢ f v = 0

Tactic:
rcases hv with ⟨i₁, i₂, heq, hne⟩

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
i₁ i₂ : ι
heq : v i₁ = v i₂
hne : i₁ ≠ i₂
⊢ f v = 0
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x ↦ M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ (∑ σ, Perm.sign σ • domDomCongr σ m) v = 0

Tactic:
sum_apply

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x ↦ M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ ∑ i, (Perm.sign i • domDomCongr i m) v = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
| add_assoc x y z =>

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

Goal state before:
pp: case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) zero) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) zero)

Tactic:
| zero =>

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

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

Tactic:
| add_assoc x y z =>

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

Goal state before:
pp: case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F) x y
⊢ descFunLift F s x = descFunLift F s y

Tactic:
induction r with
    | refl => rfl
    | symm x y _ ih => exact ih.symm
    | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
    | map j j' f x => exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x
    | zero j => simp +instances
    | one j => simp +instances
    | neg j x => simp +instances
    | add j x y => simp +instances
    | mul j x y => simp +instances
    | neg_1 x x' r ih => dsimp; rw [ih]
    | add_1 x x' y r ih => dsimp; rw [ih]
    | add_2 x y y' r ih => dsimp; rw [ih]
    | mul_1 x x' y r ih => dsimp; rw [ih]
    | mul_2 x y y' r ih => dsimp; rw [ih]
    | zero_add x => dsimp; rw [zero_add]
    | add_zero x => dsimp; rw [add_zero]
    | one_mul x => dsimp; rw [one_mul]
    | mul_one x => dsimp; rw [mul_one]
    | neg_add_cancel x => dsimp; rw [neg_add_cancel]
    | add_comm x y => dsimp; rw [add_comm]
    | mul_comm x y => dsimp; rw [mul_comm]
    | add_assoc x y z => dsimp; rw [add_assoc]
    | mul_assoc x y z => dsimp; rw [mul_assoc]
    | left_distrib x y z => dsimp; rw [mul_add]
    | right_distrib x y z => dsimp; rw [add_mul]
    | zero_mul x => dsimp; rw [zero_mul]
    | mul_zero x => dsimp; rw [mul_zero]

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

Goal state before:
pp: case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) zero) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) zero)

Tactic:
| zero =>

Goal state after:
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 u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |((A.submatrix id ⇑(e₁.symm.trans e₂)).submatrix ⇑e₁ ⇑e₁).det| = |A.det|

Tactic:
Matrix.det_submatrix_equiv_self,

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |(A.submatrix id ⇑(e₁.symm.trans e₂)).det| = |A.det|
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ M.det = 0

Tactic:
by
  rw [← det_transpose, det_zero_of_row_eq i_ne_j]
  exact funext hij

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ j₃ j₄ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
f₄ : j₄ ⟶ k₁
g₄ : j₄ ⟶ k₂
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β

Tactic:
by
  obtain ⟨s, α, β, H⟩ := crown ![j₁, j₂, j₃, j₄]
      (Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ (Fin.cons f₄ nofun))))
     (Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ (Fin.cons g₄ nofun))))
  exact ⟨s, α, β, H 0, H 1, H 2, H 3⟩

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
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (A.updateCol i fun k ↦ A k i + A k j).det = A.det

Tactic:
rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]
  exact det_updateRow_add_self Aᵀ hij

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
I : Type u_1
inst✝ : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
⊢ ∃ k fik g, ∀ (x : I), f x ≫ g x = fik

Tactic:
by
  have : IsFiltered C := { nonempty := ⟨i⟩ }
  classical
  cases nonempty_fintype I
  obtain ⟨k, fk, hk⟩ := sup_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨i, j x, by simp, by simp, f x⟩)
  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩

Goal state after: