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
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
j : J
⊢ ι f j ≫ (map fun j ↦ if j ≠ i then 𝟙 (f j) else 0) ≫ s.π = ι f j ≫ s.π

Tactic:
biproduct.ι_map_assoc

Goal state after:
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
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
j : J
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
j : K
h : ¬(p j)ᶜ
w :
  (g' ≫ biproduct.toSubtype f p) ≫ biproduct.π (Subtype.restrict p f) ⟨j, ⋯⟩ =
    0 ≫ biproduct.π (Subtype.restrict p f) ⟨j, ⋯⟩
⊢ g' ≫ biproduct.π f j ≫ 0 = g' ≫ biproduct.π f j

Tactic:
simpa using w.symm

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

Goal state before:
pp: case neg
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
j : K
h : ¬(p j)ᶜ
w :
  biproduct.ι (Subtype.restrict p f) ⟨j, ⋯⟩ ≫ biproduct.fromSubtype f p ≫ g' =
    biproduct.ι (Subtype.restrict p f) ⟨j, ⋯⟩ ≫ 0
⊢ 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'

Tactic:
simpa using w.symm

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
⊢ StrictMono (q.insertNth x f) ↔
    StrictMono f ∧ (∀ (i : Fin n), i.castSucc < q → f i < x) ∧ ∀ (i : Fin n), q ≤ i.castSucc → x < f i

Tactic:
refine ⟨fun h ↦ ⟨fun a b hab ↦ ?_, ⟨fun i hlt ↦ ?_, fun i hlt ↦ ?_⟩⟩, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
a b : Fin n
hab : a < b
⊢ f a < f b

case refine_2
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : i.castSucc < q
⊢ f i < x

case refine_3
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : q ≤ i.castSucc
⊢ x < f i

case refine_4
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
⊢ (StrictMono f ∧ (∀ (i : Fin n), i.castSucc < q → f i < x) ∧ ∀ (i : Fin n), q ≤ i.castSucc → x < f i) →
    StrictMono (q.insertNth x f)
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False

Tactic:
Function.onFun,

Goal state after:
case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h :
  (map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple k a.2)).Disjoint
    (map (fun x ↦ Fin.cons b.1 x) (antidiagonalTuple k b.2))
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ n • s.piAntidiag m = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Tactic:
ext f
  refine mem_smul_finset.trans ?_
  simp only [mem_filter, mem_piAntidiag, and_assoc]
  constructor
  · rintro ⟨f, rfl, hf, rfl⟩
    simpa [← mul_sum, hn] using hf
  rintro ⟨hfsum, hfsup, hfdvd⟩
  have (i : _) : n ∣ f i := by
    by_cases hi : i ∈ s
    · exact hfdvd _ hi
    · rw [not_imp_comm.1 (hfsup _) hi]
      exact dvd_zero _
  refine ⟨fun i ↦ f i / n, ?_⟩
  simp [funext_iff, Nat.mul_div_cancel', ← Nat.sum_div, *]
  grind

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ (∑ j, biproduct.ι S s ≫ f ≫ biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0

Tactic:
grind [CategoryTheory.Limits.zero_comp, Finset.sum_const_zero]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ ofSubtype f = swap x y

Tactic:
rw [hxy.2, ofSubtype_swap_eq]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = swap ⟨x, hx⟩ ⟨y, hy⟩
⊢ ofSubtype f = swap x y

Tactic:
by
    rw [hxy.2, ofSubtype_swap_eq]

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

Goal state before:
pp: case cons._
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : (∀ f ∈ l, f x = x) → l.prod x = x
hx : ∀ f_1 ∈ f :: l, f_1 x = x
⊢ f ∈ f :: l

Tactic:
simp only [List.mem_cons, true_or]

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

Goal state before:
pp: case mpr
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
A : c.blocks.length = 1
B : [c.blocks.get ⟨0, ⋯⟩].sum = n
⊢ [c.blocks.get ⟨0, ⋯⟩] = (single n h).blocks

Tactic:
simpa [single_blocks] using B

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

Goal state before:
pp: case mp.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.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr

Tactic:
rintro _

Goal state after:
case mp.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.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
a✝ : x ∈ Set.range Sum.inr
⊢ Sum.inr r ∈ Set.range Sum.inr
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr.inl
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
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

Tactic:
rintro _

Goal state after:
case mpr.inl
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
l : m
hx : σ x = Sum.inl l
a✝ : x ∈ Set.range Sum.inl
⊢ Sum.inl l ∈ Set.range Sum.inl
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
congr
    ext
    simp [h.support_mul]

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

Goal state before:
pp: case intro.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
⊢ { x // x ∈ ↑(σ * τ).support } ≃ { x // x ∈ ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support }

pp: case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
⊢ ∀ (x : α) (hx : x ∈ ↑(σ * τ).support),
    ↑(?intro.refine_1 ⟨(σ * τ) x, ⋯⟩) = (f * σ * f⁻¹ * (g * τ * g⁻¹)) ↑(?intro.refine_1 ⟨x, hx⟩)

Tactic:
· refine ((Equiv.setCongr hd1').trans (Equiv.Set.union hd1'')).trans <|
      (Equiv.sumCongr (subtypeEquiv f fun a => ?_) <| subtypeEquiv g fun a => ?_).trans
        ((Equiv.setCongr hd2').trans (Equiv.Set.union hd2'')).symm <;>
      simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
        apply_eq_iff_eq]

Goal state after:
case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
⊢ ∀ (x : α) (hx : x ∈ ↑(σ * τ).support),
    ↑((((setCongr hd1').trans (Set.union hd1'')).trans
            (((subtypeEquiv f ⋯).sumCongr (subtypeEquiv g ⋯)).trans ((setCongr hd2').trans (Set.union hd2'')).symm))
          ⟨(σ * τ) x, ⋯⟩) =
      (f * σ * f⁻¹ * (g * τ * g⁻¹))
        ↑((((setCongr hd1').trans (Set.union hd1'')).trans
              (((subtypeEquiv f ⋯).sumCongr (subtypeEquiv g ⋯)).trans ((setCongr hd2').trans (Set.union hd2'')).symm))
            ⟨x, hx⟩)
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : (l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
· simpa [h] using hx

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case ofNat
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.ofNat a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.ofNat a✝).support
⊢ f.IsCycle

pp: case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.negSucc a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a✝).support
⊢ f.IsCycle

Tactic:
· exact h1.of_pow h2

Goal state after:
case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.negSucc a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a✝).support
⊢ f.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
⊢ f.IsCycleOn ∅

Tactic:
simp [IsCycleOn]

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ (fun x ↦ d * x) (x.lcm y) = (fun x ↦ d * x) m

Tactic:
dsimp only
    rw [← dm, ← hd, Nat.gcd_mul_lcm]

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
m n : ℕ
⊢ (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD #s]

Tactic:
rw [Nat.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
  simp [sub_eq_neg_add, zpow_add, eq_symm_apply, eq_comm]

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
m n : ℤ
⊢ (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD ↑(#s)]

Tactic:
rw [Int.modEq_iff_dvd, ← hf.zpow_apply_eq ha]

Goal state after:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℤ
⊢ (f ^ m) a = (f ^ n) a ↔ (f ^ (n - m)) a = a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
a : α
ha : a ∈ s
⊢ s.Countable

Tactic:
exact (Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)

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

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
z : α
hz : ¬f.SameCycle x z
⊢ z = (f.cycleOf y) z

Tactic:
exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ sign f = (-1) ^ (f.cycleType.sum + f.cycleType.card)

Tactic:
by
  rw [sign_of_cycleType']
  induction f.cycleType using Multiset.induction_on with
  | empty => rfl
  | cons a s ihs =>
    rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
    simp only [pow_add, pow_one, neg_mul, mul_neg, mul_assoc, mul_one]

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

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

Tactic:
constructor
  · intro h
    ext ⟨x, hx⟩
    simpa [Perm.congr_fun h _] using ofSubtype_subtypePerm_of_mem _ hx
  · intro h; ext x
    rw [← h]
    by_cases hx : x ∈ s
    · rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]
    · rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,
        ← notMem_support]
      exact fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))

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

Goal state before:
pp: case neg
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑i.succ + 1 = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Tactic:
rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]

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

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i ≤ j
inst✝ : NeZero n
⊢ j.cycleIcc i = 1

Tactic:
rcases Fin.lt_or_eq_of_le hij with hij | hij

Goal state after:
case inl
n : ℕ
i j : Fin n
hij✝ : i ≤ j
inst✝ : NeZero n
hij : i < j
⊢ j.cycleIcc i = 1

case inr
n : ℕ
i j : Fin n
hij✝ : i ≤ j
inst✝ : NeZero n
hij : i = j
⊢ j.cycleIcc i = 1
Module: Mathlib.GroupTheory.Perm.Fin

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

Tactic:
rcases Fin.lt_or_eq_of_le hij with hij | hij

Goal state after:
case inl
n : ℕ
i j : Fin n
hij✝ : i ≤ j
hij : i < j
⊢ Perm.sign (j.cycleIcc i) = 1

case inr
n : ℕ
i j : Fin n
hij✝ : i ≤ j
hij : i = j
⊢ Perm.sign (j.cycleIcc i) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType = {2} → σ.IsSwap

Tactic:
· intro h
    simp [← card_support_eq_two, ← sum_cycleType, h]

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

Goal state before:
pp: case refine_3
α : 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 α
⊢ f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}

Tactic:
hd.cycleFactorsFinset_mul_eq_union,

Goal state after:
case refine_3
α : 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 α
⊢ f ∈ σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset →
    (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ a ∈ g.support → [a, g a, g (g a)].Nodup

Tactic:
rw [← support_eq_iff_mem_support hg3]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ g.support = {a, g a, g (g a)} → [a, g a, g (g a)].Nodup
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i ≃ₗ[R] M₁' i
⊢ (g.compLinearMap fun i ↦ ↑(f i)) = 0 ↔ g = 0

Tactic:
set f' := fun i => (f i : M₁ i →ₗ[R] M₁' i)
  rw [← zero_compLinearMap f', compLinearMap_inj f' fun i => (f i).surjective]

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

Goal state before:
pp: case inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
t : ℤˣ
⊢ a * detp 1 A + b * detp t A = b * detp 1 A + a * detp t A

Tactic:
obtain rfl | rfl := Int.units_eq_one_or t

Goal state after:
case inl.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp 1 A + b * detp 1 A = b * detp 1 A + a * detp 1 A

case inl.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp 1 A + b * detp (-1) A = b * detp 1 A + a * detp (-1) A
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
t : ℤˣ
⊢ a * detp (-1) A + b * detp t A = b * detp (-1) A + a * detp t A

Tactic:
obtain rfl | rfl := Int.units_eq_one_or t

Goal state after:
case inr.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp 1 A = b * detp (-1) A + a * detp 1 A

case inr.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
⊢ a * detp (-1) A + b * detp (-1) A = b * detp (-1) A + a * detp (-1) A
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
e₁ e₂ : m ≃ n
h : A.IsDetpBalanced a b
⊢ (A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b

Tactic:
simp_rw [IsDetpBalanced, detp_submatrix_equiv_equiv]
  apply h.mul_add_mul_eq

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

Goal state before:
pp: case inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
t : ℤˣ
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp t A

Tactic:
obtain rfl | rfl := Int.units_eq_one_or t

Goal state after:
case inl.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp 1 A

case inl.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp 1 A = detp (-1) A
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
t : ℤˣ
this : detp 1 A = detp (-1) A
⊢ detp (-1) A = detp t A

Tactic:
obtain rfl | rfl := Int.units_eq_one_or t

Goal state after:
case inr.inl
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp (-1) A = detp 1 A

case inr.inr
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
this : detp 1 A = detp (-1) A
⊢ detp (-1) 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
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
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      ⟨X_1, ⟨Y_1, ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' → f_1 ≫ T mY_1 = T mX_1

Tactic:
refine ⟨coeq (f ≫ T' mY) (T' mX), fun mZ => T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX), ?_⟩

Goal state after:
case insert
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_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
    ⟨X_1, ⟨Y_1, ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
      f_1 ≫ (fun {X_2} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY_1 =
        (fun {X_2} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX_1