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✝
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W'✝ : C
s : W'✝ ⟶ X'
hs : s ≫ g' = 0
⊢ (s ≫ e.inv) ≫ g = 0

Tactic:
iff,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W'✝ : C
s : W'✝ ⟶ X'
hs : s ≫ g' = 0
⊢ (s ≫ e.inv) ≫ e.hom ≫ g' = 0
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
h : f = f
⊢ kernelIsoOfEq h = Iso.refl (kernel f)

Tactic:
ext
  simp [kernelIsoOfEq]

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✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z'✝ : C
s : Y' ⟶ Z'✝
hs : f' ≫ s = 0
⊢ f ≫ e.inv ≫ s = 0

Tactic:
iff,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z'✝ : C
s : Y' ⟶ Z'✝
hs : f' ≫ s = 0
⊢ f' ≫ e.hom ≫ e.inv ≫ s = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ map f f' p q h₁ ≫ desc f' g' w' = desc f g w ≫ r

Tactic:
by
  ext; simp [h₂]

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

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

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

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
w : biproduct.fromSubtype f p ≫ g' = 0
j : K
⊢ biproduct.ι f j ≫ biproduct.toSubtype f pᶜ ≫ biproduct.fromSubtype f pᶜ ≫ g' = biproduct.ι f j ≫ g'

Tactic:
simp only [biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply, 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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
w : biproduct.fromSubtype f p ≫ g' = 0
j : K
⊢ (if (p j)ᶜ then 𝟙 (f j) else 0) ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k n : ℕ
⊢ Pairwise (Pi.Lex (fun x1 x2 ↦ x1 < x2) fun x x1 x2 ↦ x1 < x2) (antidiagonalTuple (k + 1) n)

Tactic:
by
    simp_rw [antidiagonalTuple, List.pairwise_flatMap, List.pairwise_map, List.mem_map,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    simp only [mem_antidiagonal, Prod.forall]
    simp only [Fin.pi_lex_lt_cons_cons, true_and, lt_self_iff_false,
      false_or]
    refine ⟨fun _ _ _ => antidiagonalTuple_pairwise_pi_lex k _, ?_⟩
    induction n with
    | zero =>
      rw [antidiagonal_zero]
      exact List.pairwise_singleton _ _
    | succ n n_ih =>
      simp
      grind

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

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

Tactic:
rw [← not_imp_not]
    intro h
    exact Set.disjoint_right.1 (c.disjoint_range h) (c.mem_range_embedding j)

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

Goal state before:
pp: case left
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (g.sum fun a b ↦ e b) = e n

Tactic:
← hsum,

Goal state after:
case left
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (g.sum fun a b ↦ e b) = e (g.sum fun x x_1 ↦ x_1)
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
by
  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)

pp: case neg
α : 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:
· rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
    · exact hf x (Finset.mem_coe.2 hx)

Goal state after:
case neg
α : 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)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : 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
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
extendDomain_apply_subtype _ _ pb

Goal state after:
case pos
α : 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
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b
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 α
a : α
a✝ : ¬g a = a
pb : ¬p (f.asEmbedding a)
⊢ False

Tactic:
exact pb (Subtype.prop _)

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
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ x' ∈ {z | (x :: y :: l).formPerm z ≠ z}

Tactic:
rw [Set.mem_ofPred_eq, h x', formPerm_apply_head _ _ _ hd']

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ y' ≠ x'
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : ¬(Equiv.symm f) a₂ < (Equiv.symm f) a₁
⊢ f.signBijAux ⟨(Equiv.symm f) a₂, (Equiv.symm f) a₁⟩ = ⟨a₁, a₂⟩

Tactic:
by
              simp [signBijAux, if_neg (mem_finPairsLT.1 ha).le.not_gt]

Goal state after:
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, (f ^ ↑i) x = y

Tactic:
obtain ⟨i, hi, hx⟩ := SameCycle.exists_pow_eq' h

Goal state after:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
i : ℕ
hi : i < orderOf f
hx : (f ^ i) x = y
⊢ ∃ i, (f ^ ↑i) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).IsSwap → a ≠ b

pp: case mpr
α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ a ≠ b → (swap a b).IsSwap

Tactic:
· intro h hab
    apply h.isCycle.ne_one
    aesop

Goal state after:
case mpr
α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ a ≠ b → (swap a b).IsSwap
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ sign f⁻¹ = sign f

Tactic:
by
  rw [map_inv sign f, Int.units_inv_eq_self]

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
⊢ f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x

Tactic:
classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : a ∈ l
b : α
hb : b ∈ l
⊢ l.formPerm.SameCycle a b

Tactic:
← List.idxOf_lt_length_iff

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
a : α
ha : idxOf a l < l.length
b : α
hb : idxOf b l < l.length
⊢ l.formPerm.SameCycle a b
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := ⋯
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ 1 = orderOf f * c

Tactic:
← hc

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ 1 = (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i))
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
⊢ #σ.support = #τ.support

Tactic:
rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i j : Fin n
⊢ i.cycleRange j = if j < i then j + 1 else if j = i then 0 else j

Tactic:
split_ifs with h₁ h₂
  · exact cycleRange_of_lt h₁
  · exact cycleRange_of_eq h₂
  · exact cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n) → n ∈ σ.cycleType

Tactic:
rintro ⟨c, t, rfl, hd, hc, rfl⟩

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c t : Perm α
hd : c.Disjoint t
hc : c.IsCycle
⊢ #c.support ∈ (c * t).cycleType
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ σ.cycleType ↔ ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
constructor
  · intro h
    obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ
    rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h
    obtain ⟨c, cl, rfl⟩ := h
    rw [(List.perm_cons_erase cl).pairwise_iff symm] at hld
    refine ⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩
    · rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]
    · exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld
  · rintro ⟨c, t, rfl, hd, hc, rfl⟩
    simp [hd.cycleType_mul, hc.cycleType]

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

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

Tactic:
h.neg_one_pow,

Goal state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (-1) ^ σ.cycleType.card = (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ (-(-1) ^ n) ^ σ.cycleType.card = 1

Tactic:
h.neg_one_pow,

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ (- -1) ^ σ.cycleType.card = 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ sign σ = ∏ i, ∏ j > i, if σ i < σ j then 1 else -1

Tactic:
rw [σ.sign_eq_prod_prod_Iio]
  apply Finset.prod_comm' (by simp)

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
this : (∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2) ↔ x2 < x1
⊢ ⟨x1, x2⟩ ∈ Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D ↔ ⟨x1, x2⟩ ∈ D

Tactic:
by simpa [hD]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ (swap a b * swap a c).IsThreeCycle

Tactic:
suffices h : support (swap a b * swap a c) = {a, b, c} by
    rw [← card_support_eq_three_iff, h]
    simp [ab, ac, bc]
  apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_
  · simp [ab, ac]
  · simp only [mem_support, coe_mul]
    grind

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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
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 : ι'
hv : v i = v j
hij : i ≠ j
⊢ (v ∘ ⇑σ) (σ.symm i) = (v ∘ ⇑σ) (σ.symm j)

Tactic:
by simpa using hv

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

Goal state before:
pp: case pos
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
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : Function.Injective g
f' : m ≃ n := ofBijective f ⋯
g' : m ≃ n := ofBijective g ⋯
⊢ (A.submatrix (⇑f') g).IsDetpBalanced a b

Tactic:
show g = g' by rfl,

Goal state after:
case pos
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
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : Function.Injective g
f' : m ≃ n := ofBijective f ⋯
g' : m ≃ n := ofBijective g ⋯
⊢ (A.submatrix ⇑f' ⇑g').IsDetpBalanced a b
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 ι
inst✝ : Fintype ι
m m' : (i : ι) → M₁ i
⊢ f (m + m') = ∑ s, f (s.piecewise m m')

Tactic:
by
  simpa using f.map_piecewise_add m m' Finset.univ

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 (Option n) (Option n) R
i : Option n
σ : Perm (Option n)
x✝ : sign σ = s ∧ σ none = i
⊢ sign (removeNone σ) = sign (swap none i) * s ∧ decomposeOption.symm (i, removeNone σ) = σ

Tactic:
rw [← optionCongr_sign]; aesop

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
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s with True, ∏ k, A k (i k)
⊢ (A * adjp s A) i i = detp s A

Tactic:
filter_true

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
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
⊢ (A * adjp s A) i i = detp s A
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * N * ↑M⁻¹).det = N.det

Tactic:
det_mul_right_comm,

Goal state after:
m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * ↑M⁻¹ * N).det = N.det
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 = (Aᵀ * (adjp s A)ᵀ) i i

Tactic:
← transpose_mul,

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 = (adjp s A * 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
⊢ IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B))

Tactic:
suffices h : ∀ {s t}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B)) from
    (h (by decide)).add (h (by decide))
  intro s t h
  rw [isAddUnit_iff]
  intro i j
  simp_rw [smul_apply, smul_eq_mul, mul_apply, detp, adjp_apply, mul_sum, sum_mul,
    IsAddUnit.sum_iff]
  intro k hk σ hσ τ hτ
  rw [mem_filter] at hσ
  rw [mem_ofSign] at hσ hτ
  rw [← hσ.1, ← hτ, ← sign_inv] at h
  replace h := ne_of_apply_ne sign h
  rw [ne_eq, eq_comm, eq_inv_iff_mul_eq_one] at h
  obtain ⟨l, hl1, hl2⟩ := exists_mem_ne (one_lt_card_support_of_ne_one h) (τ⁻¹ j)
  rw [mem_support, ne_comm] at hl1
  rw [ne_eq, ← mem_singleton, ← mem_compl] at hl2
  rw [← prod_mul_prod_compl {τ⁻¹ j}, mul_mul_mul_comm, mul_comm, ← smul_eq_mul]
  apply IsAddUnit.smul_right
  have h0 : ∀ k, k ∈ ({τ⁻¹ j} : Finset n)ᶜ ↔ τ k ∈ ({j} : Finset n)ᶜ := by
    simp [inv_def, eq_symm_apply]
  rw [← prod_equiv τ h0 fun _ _ ↦ rfl, ← prod_mul_distrib, ← mul_prod_erase _ _ hl2, ← smul_eq_mul]
  exact (isAddUnit_mul hAB l (σ (τ l)) (τ l) hl1).smul_right _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
s : C
ts : s ⟶ t
hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂
⊢ ∃ s α β, α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂

Tactic:
exact ⟨s, ts ≫ k₁t, ts ≫ k₂t, by simp only [Category.assoc, ht],
    by simp only [Category.assoc, hs]⟩

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

Goal state before:
pp: case neg
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
i j : Fin n.succ
hi : ¬i = k.succ
⊢ M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j

Tactic:
rw [updateRow_ne hi, hM', updateRow_ne hi]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : F.ColimitType → ULift.{u, 0} Bool := fun z ↦ { down := decide (x = z) }
this :
  ∀ (z : F.ColimitType),
    (ConcreteCategory.hom (hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f)))) (F.descColimitType c z) = f z
⊢ f x = f y

Tactic:
by rw [← this x, h, ← this y]

Goal state after: