mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
⊢ Function.RightInverse (fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ })
    fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X)

Tactic:
intro ξ

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
ξ : F.obj X
⊢ (fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X))
      ((fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ }) ξ) =
    ξ
Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi g

Tactic:
by
    rw [Arrow.iso_w' e]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ (H.map (limMap α) ≫ post G H) ≫ π (G ⋙ H) j✝ = (post F H ≫ limMap (whiskerRight α H)) ≫ π (G ⋙ H) j✝

Tactic:
simp only [whiskerRight_app, limMap_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero
⊢ F.map fst ≫ s.ι.app left ≫ i.hom = t.ι.app none

Tactic:
w₁,

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero
⊢ F.map fst ≫ t.ι.app WalkingCospan.left = t.ι.app none
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryProduct A B
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
H : C ⥤ D
inst✝ : HasBinaryProduct (H.obj A) (H.obj B)
α : F ⟶ H
⊢ α.app (A ⨯ B) ≫ prodComparison H A B = prodComparison F A B ≫ prod.map (α.app A) (α.app B)

Tactic:
rw [prodComparison, prodComparison, prod.lift_map, prod.comp_lift, α.naturality, α.naturality]

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryCoproduct A B
inst✝⁴ : HasBinaryCoproduct A' B'
inst✝³ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝² : HasBinaryCoproduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (coprodComparison F A B)
inst✝ : IsIso (coprodComparison F A' B')
⊢ inv (coprodComparison F A B) ≫ coprod.map (F.map f) (F.map g) =
    F.map (coprod.map f g) ≫ inv (coprodComparison F A' B')

Tactic:
by
  rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, coprodComparison_natural]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ IsIso (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

Tactic:
by
  refine ⟨⟨pushout.map _ _ _ _ (inv i₁) (inv i₂) (inv i₃) ?_ ?_, ?_, ?_⟩⟩
  · rw [IsIso.comp_inv_eq, Category.assoc, eq₁, IsIso.inv_hom_id_assoc]
  · rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
  · cat_disch
  · cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
h : F.FullyFaithful
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
⊢ F.map (A.hom ≫ h.preimage (Hom.right f)) = F.map B.hom

Tactic:
simpa using Under.w f

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f✝ g : Under X✝
φ : f✝ ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
x✝¹ x✝ : Under (F.obj ((𝟭 T).obj X))
f : x✝¹ ⟶ x✝
⊢ ((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x✝.right) ⋯ =
    homMk (a.counit.app x✝¹.right) ⋯ ≫ (𝟭 (Under (F.obj ((𝟭 T).obj X)))).map f

Tactic:
by
    ext
    exact (a.counit_naturality f.right)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ pushout.inr f g ≫ inv (pushout.inl f g) = inv g ≫ f

Tactic:
by
  rw [IsIso.eq_inv_comp, ← pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ (pushoutSymmetry f f).hom = 𝟙 (pushout f f)

Tactic:
ext <;> simp [inl_eq_inr_of_epi_eq]

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
t : Fork f g
⊢ t.π.app one = t.ι ≫ g

Tactic:
← t.app_one_eq_ι_comp_right

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
t : Fork f g
⊢ t.π.app one = t.π.app one
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ IsZero Y ↔ f = 0

Tactic:
rw [iff_id_eq_zero]
  constructor
  · intro h
    rw [← Category.comp_id f, h, comp_zero]
  · intro h
    rw [← IsSplitEpi.id f]
    simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: case calc_2
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
G : C ⥤ D
inst✝ : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 =
    adj.unit.app (G.obj X) ≫ G.map (G.leftAdjoint.map 0) ≫ G.map 0

Tactic:
simp only [← G.map_comp, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (F.mapCone c✝)

Tactic:
apply isLimitOfReflects G
    apply isLimitOfPreserves (F ⋙ G) h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor (F.mapCocone c))

Tactic:
exact IsColimit.whiskerEquivalence t _

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
W : C
k : W ⟶ X
h : k ≫ f = 0
inst✝ : Mono k
Z : C
g g' : Z ⟶ W
w : g ≫ lift f k h = g' ≫ lift f k h
⊢ g = g'

Tactic:
replace w := w =≫ kernel.ι f

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
W : C
k : W ⟶ X
h : k ≫ f = 0
inst✝ : Mono k
Z : C
g g' : Z ⟶ W
w : (g ≫ lift f k h) ≫ ι f = (g' ≫ lift f k h) ≫ ι f
⊢ g = g'
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasProduct f
inst✝¹ : HasProduct fun j ↦ G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (piComparison G f)

Tactic:
rw [← PreservesProduct.iso_hom]
  infer_instance

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
h : IsZero M
x : ↑M
⊢ x = 0

Tactic:
rw [← LinearMap.id_apply (R := R) x, ← ModuleCat.hom_id]

Goal state after:
R : Type u
inst✝ : Ring R
M : ModuleCat R
h : IsZero M
x : ↑M
⊢ (Hom.hom (𝟙 M)) x = 0
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
X Y : AlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgCat R)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (AlgCat.{v} R)).map f)

Goal state after:
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
X Y : AlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgCat R)).map f)
i : (forget (AlgCat R)).obj X ≅ (forget (AlgCat R)).obj Y := asIso ((forget (AlgCat R)).map f)
⊢ IsIso f
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case e_4
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.invEmbedding ((c.embedding i) y) ≍ y

Tactic:
Fin.heq_ext_iff

Goal state after:
case e_4
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ ↑(c.invEmbedding ((c.embedding i) y)) = ↑y

case e_4.h
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.blocksFun (c.index ((c.embedding i) y)) = c.blocksFun i
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
⊢ ∀ i ∈ (ones n).blocks, i = 1

Tactic:
exact fun i => eq_of_mem_replicate

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

Goal state before:
pp: n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
j : Fin c.length
i_blocks : 1 < c.blocksFun j
hj : c.blocksFun j = i
⊢ ∑ i, 1 < ∑ i, c.blocksFun i

Tactic:
exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
h : (x :: y :: xs).Nodup
⊢ (x :: y :: xs).formPerm x = y

Tactic:
simp [formPerm_apply_of_notMem h.notMem]

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

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ f x = hd (tl.prod x)

Tactic:
← IH h hl.right _ hx,

Goal state after:
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ f x = hd (f x)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬f a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : #{a} = 1
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = a
ha' : f a = x ∨ f a = a
⊢ f a = (swap x a) a

Tactic:
Or.resolve_right ha' ha,

Goal state after:
case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬f a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : #{a} = 1
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = a
ha' : f a = x ∨ f a = a
⊢ x = (swap x a) a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y z : α
x✝¹ : f.SameCycle x y
x✝ : f.SameCycle y z
i : ℤ
hi : (f ^ i) x = y
j : ℤ
hj : (f ^ j) y = z
⊢ (f ^ (j + i)) x = z

Tactic:
rw [zpow_add, mul_apply, hi, hj]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1

Tactic:
rw [← formPerm_apply_mem_eq_self_iff _ hl hd mem_cons_self]
    constructor
    · simp +contextual
    · intro h
      simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd mem_cons_self,
        add_le_iff_nonpos_left, length, nonpos_iff_eq_zero, length_eq_zero_iff] at h
      simp [h]

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

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

Tactic:
intro h; use a, b

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ (Equiv.symm f ^ (n + 1)) x = (Equiv.symm f) b

Tactic:
simpa [pow_succ', eq_symm_apply] using! h

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

Goal state before:
pp: case pos
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
hg : ↑g.support ⊆ Set.ofPred p
x : α
hx : g x = x
⊢ p (g x) ↔ p x

Tactic:
rw [hx]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

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

Tactic:
have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
x : ι
hx : x ∈ s
this : K x ≤ ⨆ i ∈ ↑s, K i
⊢ f x ∈ ⨆ i ∈ ↑s, K i
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
rw [notMem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa

Goal state after:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : f x = x
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case left.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ sign (swap (Sum.inl a₁) (Sum.inl a₂)) * sign σa' = sign (swap a₁ a₂) * sign σa'

Tactic:
sign_swap ha,

Goal state after:
case left.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ sign (swap (Sum.inl a₁) (Sum.inl a₂)) * sign σa' = -1 * sign σa'
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ _root_.Disjoint (ofSign 1) (ofSign (-1))

Tactic:
rw [Finset.disjoint_iff_ne]
  rintro σ hσ τ hτ rfl
  rw [mem_ofSign] at hσ hτ
  have := hσ.symm.trans hτ
  contradiction

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

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

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

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ i) ((c ^ j) a) = g ((c ^ j) a)

Tactic:
simp only [← mul_apply, Commute.eq (Commute.zpow_right hgc j)]

Goal state after:
case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ i * c ^ j) a = (c ^ j * g) a
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
inst✝ : DecidableRel f.SameCycle
x a : α
ha : a ∈ ↑(f.cycleOf x).support
b : α
hb : b ∈ ↑(f.cycleOf x).support
⊢ f.SameCycle a b

Tactic:
by
      rw [mem_coe, mem_support_cycleOf_iff_aux] at ha hb
      exact ha.1.symm.trans hb.1

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

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

Tactic:
exact
      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)

Goal state after:
Module: Mathlib.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)

Goal state after:
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
f' : (i : ι) → M₁ i →ₗ[R] M₁' i := fun i ↦ ↑(f i)
⊢ g.compLinearMap f' = 0 ↔ g = 0
Module: Mathlib.LinearAlgebra.Matrix.Reindex

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : Fintype o
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq o
inst✝¹ : Semiring A
inst✝ : Algebra R A
e : m ≃ n
x✝ : R
⊢ (reindexRingEquiv A e).toFun ((algebraMap R (Matrix m m A)) x✝) = (algebraMap R (Matrix n n A)) x✝

Tactic:
simp [algebraMap]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : D ⥤ C
R : C ⥤ D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ f ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g)) =
    g ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g))

Tactic:
rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]

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
A : Matrix n n R
j : n
c : n → R
⊢ (Aᵀ.updateRow j fun k ↦ ∑ i, c i • A k i).det = c j • A.det

Tactic:
← det_transpose A

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ (Aᵀ.updateRow j fun k ↦ ∑ i, c i • A k i).det = c j • Aᵀ.det
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
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (Aᵀ.updateRow i fun k ↦ A k i + A k j).det = A.det

Tactic:
← det_transpose A

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (Aᵀ.updateRow i fun k ↦ A k i + A k j).det = Aᵀ.det
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
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (Aᵀ.updateRow i fun k ↦ A k i + c • A k j).det = A.det

Tactic:
← det_transpose A

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (Aᵀ.updateRow i fun k ↦ A k i + c • A k j).det = Aᵀ.det