mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : Unique J
f : J → C
j : J
⊢ default = j

Tactic:
rw [← Unique.uniq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : Unique J
f : J → C
j : J
⊢ j = default

Tactic:
rw [← Unique.uniq]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ m = b.fst ≫ f + b.snd ≫ g

Tactic:
have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ m = b.fst ≫ f + b.snd ≫ g
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ m = b.fst ≫ f + b.snd ≫ g

Tactic:
have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ m = b.fst ≫ f + b.snd ≫ g
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
⊢ 𝟙 W = 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0

Tactic:
by_contra! ⟨nz, a₁, a₂⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
⊢ False
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
⊢ map { toFun := fun m a ↦ Multiset.count a ↑m, inj' := ⋯ } (s.sym n) = s.piAntidiag n

Tactic:
ext f
  simp only [Sym.val_eq_coe, mem_map, mem_sym_iff, Embedding.coeFn_mk, funext_iff, Sym.exists,
    Sym.mem_mk, Sym.coe_mk, exists_and_left, exists_prop, mem_piAntidiag, ne_eq]
  constructor
  · rintro ⟨m, hm, rfl, hf⟩
    simpa [← hf, Multiset.sum_count_eq_card hm]
  · rintro ⟨rfl, hf⟩
    refine ⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩
    · simp +contextual
    · simpa [Multiset.count_sum', Multiset.count_singleton, not_imp_comm, eq_comm (a := 0)] using hf

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support ↔ f x ≠ x

Tactic:
rw [support, mem_filter, and_iff_right (mem_univ x)]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ False

Tactic:
apply lt_irrefl (∑ k, c.blocksFun k)

Goal state after:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ ∑ k, c.blocksFun k < ∑ k, c.blocksFun k
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
ha : a ∈ s
⊢ ↑((g.subtypePerm hg) ⟨a, ha⟩) = g a

Tactic:
subtypePerm_apply

Goal state after:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
ha : a ∈ s
⊢ ↑⟨g ↑⟨a, ha⟩, ⋯⟩ = g a
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∈ s
⊢ ↑((g.subtypePerm hg) ⟨a, ha⟩) = g a

Tactic:
subtypePerm_apply

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∈ s
⊢ ↑⟨g ↑⟨a, ha⟩, ⋯⟩ = g a
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
hc : Fintype.card { x // x ∈ s \ t } = (ft \ fs).card
⊢ ↑(s \ t) ≃ ↑(t \ s)

Tactic:
← Fintype.subtype_card (ft \ fs) hts

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
hc : Fintype.card { x // x ∈ s \ t } = Fintype.card { x // x ∈ t \ s }
⊢ ↑(s \ t) ≃ ↑(t \ s)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x ↦ f i) x hx
⊢ (Equiv.symm f) y ∈ s

Tactic:
obtain ⟨y2, hy2, rfl⟩ := h0 y hy

Goal state after:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x ↦ f i) x hx
y2 : α
hy2 : y2 ∈ s
hy : (fun i x ↦ f i) y2 hy2 ∈ s
⊢ (Equiv.symm f) ((fun i x ↦ f i) y2 hy2) ∈ s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
by
  constructor
  · intro hj
    rcases (c.boundaries.orderIsoOfFin rfl).surjective ⟨j, hj⟩ with ⟨i, hi⟩
    rw [Subtype.ext_iff, Subtype.coe_mk] at hi
    refine ⟨i.1, i.2, ?_⟩
    dsimp at hi
    rw [← hi, c.blocks_partial_sum i.2]
    rfl
  · rintro ⟨i, hi, H⟩
    convert! (c.boundaries.orderIsoOfFin rfl ⟨i, hi⟩).2
    have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
    exact this.symm

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

Goal state before:
pp: α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
⊢ p ((Equiv.symm f) x)

Tactic:
by
  have : Finite { x | p x } := by simpa
  simpa using perm_symm_mapsTo_of_mapsTo (s := {x | p x}) f h hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
a : α
h : f a = a ∨ f a = a ∨ f a = a
⊢ f a = 1 a

Tactic:
or_self_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
a : α
h : f a = a ∨ f a = a
⊢ f a = 1 a
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
rcases n with (_ | _ | n)

Goal state after:
case zero
hn : 2 ≤ 0
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

case succ.zero
hn : 2 ≤ 0 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

case succ.succ
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
⊢ closure {σ, τ} = ⊤

Tactic:
rw [h5, ← hi]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
⊢ closure {σ, swap x ((σ ^ i) x)} = ⊤
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case e'_2
α : 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
⊢ (swap x (f⁻¹ x) * f⁻¹ * (swap (f⁻¹ x) (f⁻¹ (f x)) * f⁻¹) ^ i) (f x) =
    ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x)

Tactic:
simp [swap_comm _ x, ← mul_apply, -coe_mul, ← inv_def, -coe_inv, ← inv_def, mul_assoc _ f⁻¹,
        ← mul_zpow_mul, mul_assoc _ _ f]

Goal state after:
case e'_2
α : 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
⊢ ((swap x (f⁻¹ x) * f⁻¹) ^ i * swap x (f⁻¹ x)) x = ((swap x (f⁻¹ x) * f⁻¹) ^ i * f⁻¹) x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f✝ : Perm α
x✝¹ : f✝.IsSwap
x y : α
hxy : x ≠ y
hxy' : f✝ = swap x y
h : ¬s (swap x y) = -1
f : Perm α
x✝ : f.IsSwap
a b : α
hab : a ≠ b
hab' : f = swap a b
⊢ IsConj (s f) 1

Tactic:
← Or.resolve_right (Int.units_eq_one_or _) h,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f✝ : Perm α
x✝¹ : f✝.IsSwap
x y : α
hxy : x ≠ y
hxy' : f✝ = swap x y
h : ¬s (swap x y) = -1
f : Perm α
x✝ : f.IsSwap
a b : α
hab : a ≠ b
hab' : f = swap a b
⊢ IsConj (s f) (s (swap x y))
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ (swap a b).SameCycle x y

Tactic:
obtain rfl | rfl := hx

Goal state after:
case inl
α : Type u_2
b : α
inst✝ : DecidableEq α
x y : α
hab : x ≠ b
hy : y = x ∨ y = b
⊢ (swap x b).SameCycle x y

case inr
α : Type u_2
a : α
inst✝ : DecidableEq α
x y : α
hab : a ≠ x
hy : y = a ∨ y = x
⊢ (swap a x).SameCycle x y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ ∈ (ofSign 1).disjUnion (ofSign (-1)) ⋯ ↔ σ ∈ univ

Tactic:
mem_disjUnion,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ ∈ ofSign 1 ∨ σ ∈ ofSign (-1) ↔ σ ∈ univ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ σ.cycleFactorsFinset = s

Tactic:
rw [cycleFactorsFinset_eq_finset]

Goal state after:
case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
⊢ σ.cycleType = ↑(List.map (Finset.card ∘ support) l)

Tactic:
by
  have hl : l.Nodup := nodup_of_pairwise_disjoint_cycles h1 h2
  rw [cycleType_eq' l.toFinset]
  · simp [List.dedup_eq_self.mpr hl, Function.comp_def]
  · simpa using h1
  · simpa [hl] using h2
  · simp [hl, h0]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
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)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
j : ι
h : j ≠ i
⊢ (Fintype.card (H ↑⟨j, h⟩)).Coprime (Fintype.card (H i))

Tactic:
exact hcoprime h

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = ↑(((c ^ n).subtypePerm ⋯) ⟨x, hx⟩)

Tactic:
subtypePerm_apply

Goal state after:
case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = ↑⟨(c ^ n) ↑⟨x, hx⟩, ⋯⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : (σ.extendDomain f).cycleType = σ.cycleType
hτ : (τ.extendDomain f).cycleType = τ.cycleType
⊢ ((σ * τ).extendDomain f).cycleType = (σ * τ).cycleType

Tactic:
rw [hd.cycleType_mul, ← extendDomain_mul, (hd.extendDomain f).cycleType_mul, hσ, hτ]

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
x : α
hx : σ x ≠ x
⊢ l.prod x ≠ x

Tactic:
← h _ hx

Goal state after:
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
x : α
hx : σ x ≠ x
⊢ σ x ≠ x
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : k = j
⊢ ↑(subNat (↑i) (Fin.cast ⋯ j) ⋯) = ↑((j - i).castLT ⋯)

Tactic:
by simp [sub_val_of_le hij]

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
⊢ ∃ x, orderOf x = p

Tactic:
let σ :=
    Equiv.mk (f 1) (f (p - 1)) (fun s => by rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3])
      fun s => by rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]

Goal state after:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ ∃ x, orderOf x = p
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mp.refine_1
α : 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
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ ∀ f ∈ l, f.IsCycle

pp: case mp.refine_2
α : 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
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ List.Pairwise Disjoint l

pp: case mp.refine_3
α : 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
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ l.prod = σ

Tactic:
· exact fun _ h => hc' _ (hperm.subset h)

Goal state after:
case mp.refine_2
α : 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
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ List.Pairwise Disjoint l

case mp.refine_3
α : 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
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ l.prod = σ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr
n : ℕ
i j : Fin n
hij✝ : i ≤ j
hij : i = j
⊢ Perm.sign (j.cycleIcc j) = 1

Tactic:
sign_cycleIcc_of_eq

Goal state after:
case inr
n : ℕ
i j : Fin n
hij✝ : i ≤ j
hij : i = j
⊢ 1 = 1
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
⊢ ∏ j, ∏ i < j, f (σ i) (σ j) = ↑↑(sign σ) * ∏ j, ∏ i < j, f i j

Tactic:
simp_rw [← σ.sign_inv, σ⁻¹.sign_eq_prod_prod_Iio, Finset.prod_sigma', Units.coe_prod,
    Int.cast_prod, ← 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.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
rw [cycleFactorsFinset_eq_finset]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ ((∀ f ∈ {g}, f.IsCycle) ∧ ∃ (h : (↑{g}).Pairwise Disjoint), {g}.noncommProd id ⋯ = f) ↔ f.IsCycle ∧ f = g
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).cycleFactorsFinset = f.cycleFactorsFinset ∪ g.cycleFactorsFinset

Tactic:
rw [cycleFactorsFinset_eq_finset]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle) ∧
    ∃ (h : (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset)).Pairwise Disjoint),
      (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g
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✝¹ : DecidableEq ι
f : ((i : ι) → M₁ i) → M₂
h₁ : ∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), f (update m i (x + y)) = f (update m i x) + f (update m i y)
h₂ : ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (update m i (c • x)) = c • f (update m i x)
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i (x + y)) = f (update m i x) + f (update m i y)

Tactic:
by convert! h₁ m i x y

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
⊢ update v i (v j) i = update v i (v j) j

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

Goal state after: