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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ IsIso 0 ≃ (X ≅ 0) × (Y ≅ 0)

Tactic:
by
  -- This is lame, because `Prod` can't cope with `Prop`, so we can't use `Equiv.prodCongr`.
  refine (isIsoZeroEquiv X Y).trans ?_
  symm
  fconstructor
  · rintro ⟨eX, eY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X).symm eX
    · exact (idZeroEquivIsoZero Y).symm eY
  · rintro ⟨hX, hY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X) hX
    · exact (idZeroEquivIsoZero Y) hY
  · cat_disch
  · cat_disch

Goal state after:
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✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
s : KernelFork (f ≫ g)
m : ?m.112 s ⟶ kernel (?m.117 s)
w : m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m = kernel.lift g (Fork.ι s ≫ f) ⋯

Tactic:
← w

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
s : KernelFork (f ≫ g)
m : ?m.112 s ⟶ kernel (?m.117 s)
w : m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯
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✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel (?m.116 s) ⟶ ?m.118 s
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ m = cokernel.desc f (g ≫ Cofork.π s) ⋯

Tactic:
← w

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel (?m.116 s) ⟶ ?m.118 s
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ m = cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
⊢ fromSubtype f p ≫ toSubtype f p = 𝟙 (⨁ Subtype.restrict p f)

Tactic:
refine biproduct.hom_ext _ _ fun j => ?_
  rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]

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
inst✝ : HasFiniteBiproducts C
f g : J → C
h : (j : J) → f j ⟶ g j
⊢ map h = ∑ j, π f j ≫ h j ≫ ι g j

Tactic:
ext
  simp [biproduct.ι_π, biproduct.ι_π_assoc, sum_comp, comp_dite, dite_comp]

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
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)).desc
        (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) ≫
      retraction f =
    0

Tactic:
isColimitCoforkOfCokernelCofork_desc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (isCokernelEpiComp i (retraction f) ⋯).desc (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ≫
      retraction f =
    0
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
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      Cofork.π c ≫
        (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)).desc
          (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) =
    𝟙 Y

Tactic:
isColimitCoforkOfCokernelCofork_desc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      Cofork.π c ≫
        (isCokernelEpiComp i (retraction f) ⋯).desc (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) =
    𝟙 Y
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ ι f j ≫ (bicone f).π j'.as = (ι f j ≫ desc b.ι) ≫ b.toCone.π.app j'

Tactic:
biproduct.bicone_π,

Goal state after:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ ι f j ≫ π f j'.as = (ι f j ≫ desc b.ι) ≫ b.toCone.π.app j'
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝¹ : IsIso f₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
⊢ IsIso (biprod.map f₁₁ g)

Tactic:
← w

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝¹ : IsIso f₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
⊢ IsIso (L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ map length (l.splitWrtComposition c)
⊢ 0 < l'.length

Tactic:
rw [map_length_splitWrtComposition] at this

Goal state after:
α : Type u_1
l l' : List α
c : Composition l.length
h : l' ∈ l.splitWrtComposition c
this : l'.length ∈ c.blocks
⊢ 0 < l'.length
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
⊢ Fintype.card { x // x ∈ s } = Fintype.card { x // x ∈ t }

Tactic:
convert! h

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
⊢ c.blocks.length ≤ c.boundaries.card

Tactic:
simp [blocks, length]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
hzx : ¬z = x
hzf : z = f x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
hzx : ¬z = x
hzf : ¬z = f x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
· simp [hzf, hx, h, swap_apply_of_ne_of_ne]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
hzx : ¬z = x
hzf : ¬z = f x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ∀ (x : α), ¬g x = x → ¬f.asEmbedding x = b

Tactic:
rintro a _ rfl

Goal state after:
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
a : α
a✝ : ¬g a = a
pb : ¬p (f.asEmbedding a)
⊢ False
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ ↑(u ^ 2) = ↑1

Tactic:
Units.val_pow_eq_pow_val,

Goal state after:
u : ℤˣ
⊢ ↑u ^ 2 = ↑1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ p x ∈ fixedPoints ⇑g ↔ x ∈ fixedPoints ⇑g

Tactic:
simp only [Function.mem_fixedPoints_iff]

Goal state after:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ g (p x) = p x ↔ g x = x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
⊢ _root_.Disjoint (ofSubtype x).support σ.support

Tactic:
rw [Finset.disjoint_iff_ne]
  rintro a ha b hb rfl
  rw [mem_support] at ha hb
  exact ha (ofSubtype_apply_of_not_mem x (mt Function.mem_fixedPoints_iff.mp hb))

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

Goal state before:
pp: case h
k : ℕ
a✝ : List ℕ
⊢ k.Coprime (Multiset.prod ⟦a✝⟧) ↔ ∀ n ∈ ⟦a✝⟧, k.Coprime n

Tactic:
simpa using coprime_list_prod_right_iff

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : y = f x
⊢ f y = (swap x (f x)) y

Tactic:
by simp [hfyx, hffx]

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

Goal state before:
pp: x y : ℤ
⊢ x.lcm y = x.natAbs.lcm y.natAbs

Tactic:
Int.lcm_def

Goal state after:
x y : ℤ
⊢ x.natAbs.lcm y.natAbs = x.natAbs.lcm y.natAbs
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ σ.cycleType = Multiset.map (Finset.card ∘ support) s.val

Tactic:
cycleType_def

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ 2 ≤ n

Tactic:
by
  simp only [cycleType_def, ← Finset.mem_def, Function.comp_apply, Multiset.mem_map,
    mem_cycleFactorsFinset_iff] at h
  obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h
  exact hc.two_le_card_support

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ σ ^ p = 1 ↔ ∀ c ∈ σ.cycleType, c = p

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, ← lcm_cycleType, Multiset.lcm_dvd]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (∀ b ∈ σ.cycleType, b ∣ p) ↔ ∀ c ∈ σ.cycleType, c = p
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
← card_cycleType_eq_one,

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
⊢ sign σ = if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)

Tactic:
rw [sign_of_cycleType', hσ, Multiset.map_replicate, Multiset.prod_replicate]
  obtain h | h := Nat.even_or_odd n
  · rw [if_neg (Nat.not_odd_iff_even.mpr h), h.neg_one_pow, σ.card_fixedPoints,
      Nat.sub_sub_self σ.sum_cycleType_le,
      show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,
        Nat.mul_div_cancel _ hn]
  · rw [if_pos h, h.neg_one_pow, neg_neg, one_pow]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
⊢ sign σ = (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2)

Tactic:
sign_of_cycleType_eq_replicate zero_lt_two (cycleType_of_pow_prime_eq_one hσ),

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
⊢ (if Odd 2 then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2)) =
    (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2)
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
⊢ ∃ x, orderOf x = p

Tactic:
have Scard :=
    calc
      p ∣ Fintype.card G ^ (p - 1) := hdvd.trans (dvd_pow (dvd_refl _) hp')
      _ = Fintype.card (vectorsProdEqOne G p) := (VectorsProdEqOne.card G p).symm

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)
⊢ ∃ 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)
⊢ (↑univ).Pairwise (Commute on fun i ↦ ((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) i) (v i))

pp: case hom
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ (a b : Perm α), (ofSubtype u).Disjoint a → (ofSubtype u).Disjoint b → (ofSubtype u).Disjoint (a * b)

pp: case unit
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ (ofSubtype u).Disjoint 1

pp: case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ univ, (ofSubtype u).Disjoint (((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) x) (v x))

Tactic:
· intro a _ b _ h
    apply f.pairwise_commute_of_mem_zpowers h <;> simp only [Subgroup.coe_subtype, SetLike.coe_mem]

Goal state after:
case hom
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ (a b : Perm α), (ofSubtype u).Disjoint a → (ofSubtype u).Disjoint b → (ofSubtype u).Disjoint (a * b)

case unit
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ (ofSubtype u).Disjoint 1

case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ univ, (ofSubtype u).Disjoint (((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) x) (v x))
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case base
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
u : Perm ↑(fixedPoints ⇑f)
v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ univ, (ofSubtype u).Disjoint (((fun i ↦ ((fun i ↦ Subgroup.zpowers ↑i) i).subtype) x) (v x))

Tactic:
intro c _
    simp only [Subgroup.coe_subtype]
    exact Disjoint.mono (disjoint_ofSubtype_of_memFixedPoints_self u)
      le_rfl (support_zpowers_of_mem_cycleFactorsFinset_le (v c))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.IsCycle

Tactic:
← card_cycleType_eq_one,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.cycleType.card = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ g.support = {a, g a, g (g a)} ↔ a ∈ g.support

Tactic:
by
  constructor
  · intro hg; simp [hg]
  · intro ha
    symm
    apply Finset.eq_of_subset_of_card_le
    · apply Finset.insert_subset ha
      apply Finset.insert_subset
      · rwa [Perm.apply_mem_support]
      simpa only [Finset.singleton_subset_iff, Perm.apply_mem_support]
    · rw [hg3.card_support]
      simp only [mem_support, ne_eq] at ha
      rw [Finset.card_insert_eq_ite, if_neg]
      · rw [Finset.card_insert_eq_ite, if_neg]
        · simp
        · simpa using Ne.symm ha
      · simp only [Finset.mem_insert, Finset.mem_singleton]
        contrapose ha
        rcases ha with ha | ha
        · exact ha.symm
        · suffices (g ^ 3) a = a by simpa [pow_succ, ← ha] using this
          simp [← hg3.orderOf]

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:
simp_rw [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.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:
rw [IsDetpBalanced] at *

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 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:
@w' _ _ mX' mY' f' _

Goal state after:
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')
⊢ T' mX' ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'

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')
⊢ ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ H'
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 : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h' : (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)
H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
nmf : h' ∉ H'
h'' : ∃ S T, ∀ {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 Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ insert h' H' → f ≫ T mY = T mX

Tactic:
| insert h' H' nmf h'' =>

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type w
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
⊢ f M.det = (f.mapMatrix M).det

Tactic:
by
  simp [Matrix.det_apply', map_sum f, map_prod f]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ (M.updateCol j (s • u)).det = s * (M.updateCol j u).det

Tactic:
by
  rw [← det_transpose, ← updateRow_transpose, det_updateRow_smul]
  simp [updateRow_transpose, det_transpose]

Goal state after: