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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ f = Fork.ι s ≫ 0

Tactic:
← cancel_mono g,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ (Fork.ι s ≫ f) ≫ g = (Fork.ι s ≫ 0) ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : CokernelCofork f
⊢ f ≫ Cofork.π s = 0

Tactic:
rw [Cofork.condition, zero_comp]

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

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
P Q : C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : BinaryBicone P Q
t : (functoriality P Q F).obj X✝ ⟶ (functoriality P Q F).obj Y✝
⊢ F.map (F.preimage t.hom ≫ Y✝.snd) = F.map X✝.snd

Tactic:
simpa using! t.wsnd

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → f j ⟶ T
⊢ desc g = ∑ j, π f j ≫ g j

Tactic:
by
  classical
  ext j
  simp [comp_sum, biproduct.ι_π_assoc, dite_comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N A✝ B✝ : ModuleCat R
f : A✝ ⟶ B✝
x✝ : IsIso ((forget₂ (ModuleCat R) AddCommGrpCat).map f)
⊢ IsIso f

Tactic:
have : IsIso ((forget _).map f) := by
      change IsIso ((forget _).map ((forget₂ _ AddCommGrpCat).map f))
      infer_instance

Goal state after:
R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N A✝ B✝ : ModuleCat R
f : A✝ ⟶ B✝
x✝ : IsIso ((forget₂ (ModuleCat R) AddCommGrpCat).map f)
this : IsIso ((forget (ModuleCat R)).map f)
⊢ IsIso f
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) →
    ∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t ↦ if t = i then a else 0) a_1 = f

Tactic:
rintro ⟨hn, hf⟩
    refine ⟨_, _, hn, update f i 0, ⟨sum_update_of_notMem hi _ _, fun j ↦ ?_⟩, by aesop⟩
    grind

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ (∑ a ∈ s, f a • {a}).card = s.sum f ∧ ∀ (x : ι), Multiset.count x (∑ a ∈ s, f a • {a}) = f x

Tactic:
· simpa [Multiset.count_sum', Multiset.count_singleton, not_imp_comm, eq_comm (a := 0)] using hf

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

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ (take (i + 1) c.blocks).sum = (take i c.blocks).sum + c.blocks[i]

Tactic:
sum_take_succ _ _ h

Goal state after:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ (take i c.blocks).sum + c.blocks[i] = (take i c.blocks).sum + c.blocks[i]
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
x : ι
hx : x ∈ s
⊢ Function.update (⇑g) a n1 x = g x

Tactic:
rw [update_of_ne (ne_of_mem_of_not_mem hx h) n1 ⇑g]

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

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ i = c.index j → j ∈ Set.range ⇑(c.embedding i)

Tactic:
· intro h
    rw [h]
    exact c.mem_range_embedding j

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ PreservesBinaryBiproduct X Y F

Tactic:
have that :
    prodComparison F X Y =
      (F.mapIso (biprod.isoProd X Y)).inv ≫ biprodComparison F X Y ≫ (biprod.isoProd _ _).hom := by
    ext <;> simp [← Functor.map_comp]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
that :
  prodComparison F X Y =
    (F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom
⊢ PreservesBinaryBiproduct X Y F
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl

Tactic:
· rintro ⟨a, rfl⟩
    obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
    grind

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

Goal state before:
pp: α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1

Tactic:
hστ.commute.mul_pow,

Goal state after:
α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
⊢ σ ^ n * τ ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.toFinset ⊆ {x | l.formPerm x ≠ x}

Tactic:
intro x hx
    simp only [Finset.mem_coe, mem_toFinset] at hx
    obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
    rw [Set.mem_ofPred_eq, formPerm_apply_getElem _ h]
    intro H
    rw [nodup_iff_injective_get, Function.Injective] at h
    specialize h H
    rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'
    · simp only [← hn', Nat.mod_self] at h
      refine not_exists.mpr h' ?_
      rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]
    · simp [Nat.mod_eq_of_lt hn'] at h

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ swap x (f x) * swap x (f x) * f = f

Tactic:
mul_def (swap x (f x)),

Goal state after:
α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ Equiv.trans (swap x (f x)) (swap x (f x)) * f = f
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f (g a) ≤ (f * g) b then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
mul_apply

Goal state after:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
i : ℕ
left✝ : i < orderOf f
hi : (f ^ i) x = y
⊢ ∃ i, (f ^ i) x = y

Tactic:
exact ⟨i, hi⟩

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

Goal state before:
pp: α : Type u_2
f g : Perm α
⊢ f.IsCycle → (g * f * g⁻¹).IsCycle

Tactic:
rintro ⟨x, hx, h⟩

Goal state after:
α : Type u_2
f g : Perm α
x : α
hx : f x ≠ x
h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ (g * f * g⁻¹).IsCycle
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:
simp only [pow_zero, coe_one, id_eq, swap_self]

Goal state after:
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
⊢ Equiv.refl α ∈ H
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ n * f ^ k) z = (f ^ k) (1 z)

Tactic:
mul_apply

Goal state after:
case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ n) ((f ^ k) z) = (f ^ k) (1 z)
Module: Mathlib.GroupTheory.Perm.Sign

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

Tactic:
mul_apply

Goal state after:
case cons
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hmem : ∀ x ∈ insert i s, f x ∈ K x
⊢ (insert i s).noncommProd f comm = 1 → ∀ i_1 ∈ insert i s, f i_1 = 1

Tactic:
| insert i s hnotMem ih =>

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

Goal state before:
pp: case succ
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f ((f ^ n) x) = (f * f ^ n) x

pp: case succ.hc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f.SameCycle x ((f ^ n) x)

Tactic:
mul_apply

Goal state after:
case succ
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f ((f ^ n) x) = f ((f ^ n) x)

case succ.hc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f.SameCycle x ((f ^ n) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
mul_apply

Goal state after:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f ((f ^ k) x) = f ((f ^ k) 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 σ)
⊢ 1 ≤ σ.cycleType.card

Tactic:
Nat.succ_le_iff,

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ 0 < σ.cycleType.card
Module: Mathlib.GroupTheory.Perm.Fin

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

Tactic:
ext j
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, σ a = a

Tactic:
contrapose! hα

Goal state after:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
hα : ∀ (a : α), σ a ≠ a
⊢ p ∣ Fintype.card α
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)
⊢ ∃ x, orderOf x = p

Tactic:
let f : ℕ → vectorsProdEqOne G p → vectorsProdEqOne G p := fun k v =>
    VectorsProdEqOne.rotate v k

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
⊢ ∃ x, orderOf x = p
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)
a : ↥f.cycleFactorsFinset
a✝¹ : a ∈ ↑univ
b : ↥f.cycleFactorsFinset
a✝ : b ∈ ↑univ
h : a ≠ b
⊢ (Commute on fun i ↦ ((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) i) (v i)) a b

Tactic:
apply f.pairwise_commute_of_mem_zpowers h

Goal state after:
case comm.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
a : ↥f.cycleFactorsFinset
a✝¹ : a ∈ ↑univ
b : ↥f.cycleFactorsFinset
a✝ : b ∈ ↑univ
h : a ≠ b
⊢ (fun i ↦ ((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) i) (v i)) a ∈ Subgroup.zpowers ↑a

case comm.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
a : ↥f.cycleFactorsFinset
a✝¹ : a ∈ ↑univ
b : ↥f.cycleFactorsFinset
a✝ : b ∈ ↑univ
h : a ≠ b
⊢ (fun i ↦ ((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) i) (v i)) b ∈ Subgroup.zpowers ↑b
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c = f.cycleOf a

Tactic:
rw [this]
    apply symm
    exact
      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
⊢ (g ^ m) x ∈ (↑c).support ↔ x ∈ (↑c).support

Tactic:
← g.eq_cycleOf_of_mem_cycleFactorsFinset_iff _ c.prop,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
m : ℤ
c : ↥g.cycleFactorsFinset
⊢ ↑c = g.cycleOf ((g ^ m) x) ↔ x ∈ (↑c).support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : σ x = x
hfx : ¬f x = x
⊢ (σ * f⁻¹) x = x

Tactic:
mul_apply

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : σ x = x
hfx : ¬f x = x
⊢ σ (f⁻¹ x) = x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
hfx : ¬f x = x
⊢ (τ * f⁻¹) x = x

Tactic:
mul_apply

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
hfx : ¬f x = x
⊢ τ (f⁻¹ x) = x
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
P : Type u_4
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
M' : Type u_5
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
N' : Type u_6
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v✝ : ι → M
v' : ι → M'
S : Type u_10
inst✝² : Monoid S
inst✝¹ : DistribMulAction S N
inst✝ : SMulCommClass R S N
c : S
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (c • ↑f).toFun v = 0

Tactic:
simp [f.map_eq_zero_of_eq v h hij]

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
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v✝ : ι → M
v' : ι → M'
f : M [⋀^ι]→ₗ[R] N'
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (-↑f).toFun v = 0

Tactic:
simp [f.map_eq_zero_of_eq v h hij]

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
P : Type u_4
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type u_5
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
S : Type u_10
N₂ : Type u_11
inst✝¹ : AddCommMonoid N₂
inst✝ : Module R N₂
g : N →ₗ[R] N₂
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (g.compMultilinearMap ↑f).toFun v = 0

Tactic:
simp [f.map_eq_zero_of_eq v h hij]

Goal state after:
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 ι
⊢ ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')

Tactic:
refine Finset.induction_on t (by simp) ?_

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 ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (m' : (i : ι) → M₁ i), f (s.piecewise (m + m') m') = ∑ s ∈ s.powerset, f (s.piecewise m m')) →
        ∀ (m' : (i : ι) → M₁ i),
          f ((insert a s).piecewise (m + m') m') = ∑ s ∈ (insert a s).powerset, f (s.piecewise m m')
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 (update (t.piecewise (m + m') m') i (m i)) + f (t.piecewise (m + m') m') =
    ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')

Tactic:
C,

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') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')