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

Goal state before:
pp: case refine_2
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✝ : HasFiniteBiproducts C
X : C
a : X ⟶ ⨁ Empty.elim
⊢ a = default

Tactic:
apply biproduct.hom_ext

Goal state after:
case refine_2
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✝ : HasFiniteBiproducts C
X : C
a : X ⟶ ⨁ Empty.elim
⊢ ∀ (j : Empty), a ≫ biproduct.π Empty.elim j = default ≫ biproduct.π Empty.elim j
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
by
  simp only [sizeUpTo]
  rw [sum_take_succ _ _ h]

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

Goal state before:
pp: n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h ↔ c.length = 1

Tactic:
constructor
  · intro H
    rw [H]
    exact single_length h
  · intro H
    ext1
    have A : c.blocks.length = 1 := H ▸ c.blocks_length
    have B : c.blocks.sum = n := c.blocks_sum
    rw [eq_cons_of_length_one A] at B ⊢
    simpa [single_blocks] using B

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

Goal state before:
pp: n m : ℕ
c : Composition m
hmn : m = n
⊢ c.cast hmn = cast ⋯ c

Tactic:
subst m
  rfl

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
i : ℕ
hi : i < (l.splitWrtCompositionAux []).length
⊢ (l.splitWrtCompositionAux [])[i] = drop (take i []).sum (take (take (i + 1) []).sum l)

Tactic:
cases hi

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

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ (f ^ (k + 1)) x = (g ^ (k + 1)) x

Tactic:
rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]

Goal state after:
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ g x ∈ f.support ∩ g.support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.boundary ⟨c.length, ⋯⟩ = Fin.last n

Tactic:
convert! Finset.orderEmbOfFin_last rfl c.card_boundaries_pos
  exact le_antisymm (Finset.le_max' _ _ c.getLast_mem) (Fin.le_last _)

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

Goal state before:
pp: case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ f.extendSubtype (σ x) = τ (f.extendSubtype x)

Tactic:
Equiv.extendSubtype_apply_of_mem,

Goal state after:
case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ ↑(f ⟨σ x, ?pos.hx✝⟩) = τ (f.extendSubtype x)

case pos.hx
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ σ x ∈ ↑σ.support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.toCompositionAsSet.blocks = c.blocks

Tactic:
by
  let d := c.toCompositionAsSet
  change d.blocks = c.blocks
  have length_eq : d.blocks.length = c.blocks.length := by simp [d, blocks_length]
  suffices H : ∀ i ≤ d.blocks.length, (d.blocks.take i).sum = (c.blocks.take i).sum from
    eq_of_sum_take_eq length_eq H
  intro i hi
  have i_lt : i < d.boundaries.card := by
    simpa [CompositionAsSet.blocks, length_ofFn,
      d.card_boundaries_eq_succ_length] using Nat.lt_succ_iff.2 hi
  have i_lt' : i < c.boundaries.card := i_lt
  have i_lt'' : i < c.length + 1 := by rwa [c.card_boundaries_eq_succ_length] at i_lt'
  have A :
    d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ =
      c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
    rfl
  have B : c.sizeUpTo i = c.boundary ⟨i, i_lt''⟩ := rfl
  rw [d.blocks_partial_sum i_lt, CompositionAsSet.boundary, ← Composition.sizeUpTo, B, A,
    c.orderEmbOfFin_boundaries]

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)

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:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ (g.extendDomain f).support = map f.asEmbedding g.support

Tactic:
ext b
  simp only [mem_map, Ne,
    mem_support]
  by_cases pb : p b
  · rw [extendDomain_apply_subtype _ _ pb]
    grind [asEmbedding_apply]
  · rw [extendDomain_apply_not_subtype _ _ pb]
    simp only [not_exists, false_iff, not_and, not_true]
    rintro a _ rfl
    exact pb (Subtype.prop _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
a✝ : α
⊢ a✝ ∈ (σ * τ * σ⁻¹).support ↔ a✝ ∈ map (Equiv.toEmbedding σ) τ.support

Tactic:
simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne, Perm.mem_support,
    Equiv.eq_symm_apply, inv_def]

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

Goal state before:
pp: n : ℕ
a : (_ : Fin n) × Fin n
⊢ a ∈ finPairsLT n ↔ a.snd < a.fst

Tactic:
simp only [finPairsLT, Fin.lt_def, true_and, mem_attachFin, mem_range, mem_univ,
    mem_sigma]

Goal state after:
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:
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.Data.List.Iterate

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → α
a : α
⊢ map (fun x ↦ f^[x] a) (range n) = iterate f a n

Tactic:
by
  apply List.ext_getElem <;> simp

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ |↑(sign f)| = 1

Tactic:
by
  rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
this : ∀ {f : Perm α}, f.IsSwap → s f = -1
f : Perm α
l : List (Perm α)
hl₁ : l.prod = f
hl₂ : ∀ g ∈ l, g.IsSwap
hsl : ∀ a ∈ List.map (⇑s) l, a = -1
⊢ (-1) ^ l.length = sign l.prod

Tactic:
sign_prod_list_swap hl₂

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
this : ∀ {f : Perm α}, f.IsSwap → s f = -1
f : Perm α
l : List (Perm α)
hl₁ : l.prod = f
hl₂ : ∀ g ∈ l, g.IsSwap
hsl : ∀ a ∈ List.map (⇑s) l, a = -1
⊢ (-1) ^ l.length = (-1) ^ l.length
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
val✝ : Fintype β
this : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle

Tactic:
exact (pow_iff hf).mpr this

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ : α × β
a' : α
b : β
hab : (prodExtendRight a σ) (a', b) ≠ (a', b)
x✝ : (prodExtendRight a σ) ((prodExtendRight a σ) (a', b)) ≠ (prodExtendRight a σ) (a', b)
⊢ ((prodExtendRight a σ) (a', b)).2 = σ (a', b).2

Tactic:
simp [eq_of_prodExtendRight_ne hab]

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

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

Tactic:
coe_singleton,

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
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: case h₂
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ y * b

Tactic:
exact (Int.gcd_dvd_right ..).mul_right _

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ∃ f, f.IsCycleOn ↑s ∧ f.support ⊆ s

Tactic:
by
  refine ⟨s.toList.formPerm, ?_, fun x hx => by
    simpa using List.mem_of_formPerm_apply_ne (Perm.mem_support.1 hx)⟩
  convert! s.nodup_toList.isCycleOn_formPerm
  simp

Goal state after:
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 ^ (k + 1)) x

pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k) x)

Tactic:
· rw [add_comm, zpow_add, zpow_one, mul_apply]

Goal state after:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
⊢ (if f.SameCycle x y then f y else y) = y

Tactic:
by_cases hy : f y = y

Goal state after:
case pos
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : f y = y
⊢ (if f.SameCycle x y then f y else y) = y

case neg
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : ¬f y = y
⊢ (if f.SameCycle x y then f y else y) = y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ (g * f⁻¹ * f).cycleType = g.cycleType - f.cycleType + f.cycleType

Tactic:
inv_mul_cancel_right,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ g.cycleType = g.cycleType - f.cycleType + f.cycleType
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
⊢ σ ∈ l ↔ ∀ (a : α), σ a ≠ a → σ a = l.prod a

Tactic:
cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert! hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

Tactic:
by
  let σ : α ≃ α := ⟨f, f ^ (p ^ n - 1),
    leftInverse_iff_comp.mpr ((pow_sub_mul_pow f (Nat.one_le_pow n p hp.out.pos)).trans hf),
    leftInverse_iff_comp.mpr ((pow_mul_pow_sub f (Nat.one_le_pow n p hp.out.pos)).trans hf)⟩
  have hσ : σ ^ p ^ n = 1 := by
    rw [DFunLike.ext'_iff, coe_pow]
    exact (hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf
  suffices Fintype.card f.fixedPoints = (support σ)ᶜ.card from
    this ▸ (card_compl_support_modEq hσ).symm
  suffices f.fixedPoints = (support σ)ᶜ by
    simp only [this]; apply Fintype.card_coe
  simp [σ, Set.ext_iff, IsFixedPt]

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
s : ↑(vectorsProdEqOne G p)
⊢ f (p - 1) (f 1 s) = s

Tactic:
hf2,

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
s : ↑(vectorsProdEqOne G p)
⊢ f (1 + (p - 1)) s = s
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
s : ↑(vectorsProdEqOne G p)
⊢ f 1 (f (p - 1) s) = s

Tactic:
hf2,

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
s : ↑(vectorsProdEqOne G p)
⊢ f (p - 1 + 1) s = s
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
⊢ ↑((i.cycleIcc i) k) = ↑(1 k)

Tactic:
simp only [Perm.coe_one, id_eq]

Goal state after:
n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
⊢ ↑((i.cycleIcc i) k) = ↑k
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inl
α : 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 ∈ σ.cycleFactorsFinset
⊢ f ∉ τ.cycleFactorsFinset

Tactic:
exact fun H =>
        notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
s : (i : ι) → { s // ∀ (i_1 : κ i), i_1 ∈ s ∨ (x i).toFun i_1 = 0 }
p : (i : ι) → κ i
⊢ (∃ a, (∀ (a_1 : ι), a a_1 ⋯ ∈ ↑(s a_1)) ∧ (fun i ↦ a i ⋯) = p) ∨ ((f p) fun i ↦ (x i) (p i)) = 0

Tactic:
or_iff_not_imp_right

Goal state after:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
s : (i : ι) → { s // ∀ (i_1 : κ i), i_1 ∈ s ∨ (x i).toFun i_1 = 0 }
p : (i : ι) → κ i
⊢ ¬((f p) fun i ↦ (x i) (p i)) = 0 → ∃ a, (∀ (a_1 : ι), a a_1 ⋯ ∈ ↑(s a_1)) ∧ (fun i ↦ a i ⋯) = p
Module: Mathlib.LinearAlgebra.Multilinear.Basis

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
val✝ : Fintype ι
x : (i : ι) → ιM i →₀ R
⊢ (f fun i ↦ (Finsupp.linearCombination R ⇑(e i)) (x i)) = g fun i ↦ (Finsupp.linearCombination R ⇑(e i)) (x i)

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
val✝ : Fintype ι
x : (i : ι) → ιM i →₀ R
⊢ (f fun i ↦ (x i).sum fun i_1 a ↦ a • (e i) i_1) = g fun i ↦ (x i).sum fun i_1 a ↦ a • (e i) i_1
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Fintype (κ i)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι'
f : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
⊢ (freeDFinsuppEquiv f) x = ∑ p, f p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
by
  apply DFinsupp.induction f
  · simp
  · rintro p r f - - hfx
    simp [Finset.sum_add_distrib, add_smul, hfx]

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 : Matrix n n R
a b c : R
inst✝ : IsCancelAdd R
hab : A.IsDetpBalanced a b
hbc : A.IsDetpBalanced b c
⊢ A.IsDetpBalanced a c

Tactic:
IsDetpBalanced

Goal state after:
n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
a b c : R
inst✝ : IsCancelAdd R
hab : a * detp 1 A + b * detp (-1) A = b * detp 1 A + a * detp (-1) A
hbc : b * detp 1 A + c * detp (-1) A = c * detp 1 A + b * detp (-1) A
⊢ a * detp 1 A + c * detp (-1) A = c * detp 1 A + a * detp (-1) A
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
X : C
O' : Finset C
nm : X ∉ O'
h : ∃ S, ∀ {X : C}, X ∈ O' → Nonempty (X ⟶ S)
⊢ ∃ S, ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty (X_1 ⟶ S)

Tactic:
| insert X O' nm h =>

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

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
h : ¬(X = X' ∧ Y = Y')
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'

Tactic:
· rw [@w' _ _ mX' mY' f' _]
      apply Finset.mem_of_mem_insert_of_ne mf'
      contrapose h
      obtain ⟨rfl, h⟩ := h
      trivial

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
⊢ (adjp s A * A) i i = detp s Aᵀ

Tactic:
← mul_adjp_apply_eq _ _ i,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
⊢ (adjp s A * A) i i = (Aᵀ * adjp s Aᵀ) i i
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
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
⊢ IsAddUnit (∑ i ∈ ofSign s, ∑ j ∈ ofSign t, (∏ k, A k (i k)) * ∏ k, B k (j k))

Tactic:
IsAddUnit.sum_iff

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
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
⊢ ∀ a ∈ ofSign s, ∀ a_2 ∈ ofSign t, IsAddUnit ((∏ k, A k (a k)) * ∏ k, B k (a_2 k))