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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
f g : Arrow C
inst✝⁵ : HasImage f.hom
inst✝⁴ : HasImage g.hom
sq : f ⟶ g
inst✝³ : HasImageMap sq
h : Arrow C
inst✝² : HasImage h.hom
sq' : g ⟶ h
inst✝¹ : HasImageMap sq'
inst✝ : HasImageMap (sq ≫ sq')
⊢ HasImageMap.imageMap (sq ≫ sq') = imageMapComp sq sq'

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImageMap (𝟙 f)
⊢ HasImageMap.imageMap (𝟙 f) = imageMapId f

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case e_a
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ default = default

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case e_a
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y Z : C
f : Y ⟶ Z
⊢ default ≫ f = default

Tactic:
simp only [eq_iff_true_of_subsingleton]

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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ IsLimit (F.mapCone c)

Tactic:
apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit

Goal state after:
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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := ⋯
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ (Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c))) ≅ F.mapCone c
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ HasZeroObject C

Tactic:
by
  refine ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by cat_disch⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩⟩
  calc
    f = f ≫ 𝟙 _ := (Category.comp_id _).symm
    _ = f ≫ 0 := by congr!; subsingleton
    _ = 0 := HasZeroMorphisms.comp_zero _ _

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

Goal state before:
pp: 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
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
⊢ F.map 0 = 0

Tactic:
let adj := Adjunction.ofIsLeftAdjoint F
    calc
      dsimp% F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
      _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
      _ = 0 := ?_
    · rw [Adjunction.left_triangle_components]
      exact (Category.comp_id _).symm
    · simp only [← Category.assoc, ← F.map_comp, zero_comp]
    · simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
⊢ HasLimitsOfShape (Discrete ι) C

Tactic:
by
  rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
  have : HasLimitsOfShape (Discrete (Fin n)) C := HasFiniteProducts.out n
  exact hasLimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (lift f g)

Tactic:
← biprod.map_lift_mapBiprod,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ (F.map (lift f g) ≫ (F.mapBiprod X Y).hom) ≫ (F.mapBiprod X Y).inv = F.map (lift f g)
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
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
⊢ image.ι f ≫ cokernel.π f = 0

Tactic:
have w := cokernel.condition f
        conv at w =>
          lhs
          congr
          rw [← image.fac f]
        rw [← HasZeroMorphisms.comp_zero (Limits.factorThruImage f), Category.assoc,
          cancel_epi] at w
        exact w

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
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
⊢ Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ (fromSubtype f fun j ↦ j ≠ i) ≫ s.π = s.π

Tactic:
apply biproduct.hom_ext'

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),
    ι f j ≫ Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ (fromSubtype f fun j ↦ j ≠ i) ≫ s.π =
      ι f j ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case refine_1
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : ⨁ Empty.elim ⟶ X
⊢ a = default

Tactic:
apply biproduct.hom_ext'

Goal state after:
case refine_1
J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
a : ⨁ Empty.elim ⟶ X
⊢ ∀ (j : Empty), biproduct.ι Empty.elim j ≫ a = biproduct.ι Empty.elim j ≫ default
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin n → α
a : α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) (cons a f) (cons a f) ↔ (∀ (i : Fin n), r a (f i)) ∧ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
by
  match n with
  | 0 => simp [Relator.LiftFun]
  | n + 1 =>
    apply (liftFun_vecCons r).trans
    simp only [forall_iff_succ, and_congr_left_iff, iff_self_and]
    intro h r0 i
    exact _root_.trans r0 (h (by grind))

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈ s.piAntidiag n ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
rw [piAntidiag]

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈
      Trunc.lift
        (fun e ↦ map { toFun := fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n))
        ⋯ (Fintype.truncEquivFinOfCardEq ⋯) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ f ≫ (biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst = 0

Tactic:
conv_lhs =>
      slice 2 3
      rw [comp_add]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ ((f ≫ biprod.fst ≫ biprod.inl + f ≫ biprod.snd ≫ biprod.inr) ≫ inv f) ≫ biprod.fst = 0
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ (f ^ (n + 1)) x = x

Tactic:
rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]

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

Goal state before:
pp: n i : ℕ
⊢ (ones n).sizeUpTo i = min i n

Tactic:
simp [sizeUpTo, ones_blocks, take_replicate]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ g (c x) = g x ↔ c x = x

Tactic:
Equiv.apply_eq_iff_eq

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ c x = x ↔ c x = x
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Epi (F.biprodComparison' X Y)
⊢ PreservesBinaryBiproduct X Y F

Tactic:
have : Epi (splitEpiBiprodComparison F X Y).section_ := by simpa
  have : IsIso (biprodComparison F X Y) :=
    IsIso.of_epi_section' (splitEpiBiprodComparison F X Y)
  apply preservesBinaryBiproduct_of_mono_biprodComparison

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

Goal state before:
pp: n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ ↑((d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩) = (take i c.blocks).sum

Tactic:
← Composition.sizeUpTo,

Goal state after:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ ↑((d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩) = c.sizeUpTo i
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case pos.refine_1
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ σ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (σ.extendDomain f) b = b

Tactic:
· intro h
        rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]

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

Goal state before:
pp: case pos.refine_2
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ τ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (τ.extendDomain f) b = b

Tactic:
· intro h
        rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]

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

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

Tactic:
have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
      rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]

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

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

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

Tactic:
· have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
      rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False

Tactic:
nodup_iff_injective_get,

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : Function.Injective l.get
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: x : ℤ
⊢ x.natAbs = 1 ↔ ↑x.natAbs = ↑1

Tactic:
natCast_inj

Goal state after:
x : ℤ
⊢ x.natAbs = 1 ↔ x.natAbs = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
⊢ f.SameCycle x y → ∃ i < orderOf f, (f ^ i) x = y

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
⊢ ∃ i < orderOf f, (f ^ i) x = (f ^ k) x
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : ¬x = (σ ^ (n + 1)) x
⊢ swap ((σ ^ (n + 1)) x) x ∈ H

Tactic:
← swap_mul_swap_mul_swap h5 h6

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : ¬x = (σ ^ (n + 1)) x
⊢ swap ((σ ^ n) x) ((σ ^ (n + 1)) x) * swap x ((σ ^ n) x) * swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ sign l.prod = (-1) ^ l.length

Tactic:
have h₁ : l.map sign = List.replicate l.length (-1) :=
    List.eq_replicate_iff.2
      ⟨by simp, fun u hu =>
        let ⟨g, hg⟩ := List.mem_map.1 hu
        hg.2 ▸ (hl _ hg.1).sign_eq⟩

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
h₁ : List.map (⇑sign) l = List.replicate l.length (-1)
⊢ sign l.prod = (-1) ^ l.length
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
⊢ f.IsCycle

Tactic:
obtain ⟨x, hx1, hx2⟩ := h1

Goal state after:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h2 : f.support ⊆ (f ^ n).support
key : ∀ (x : α), (f ^ n) x ≠ x ↔ f x ≠ x
x : α
hx1 : (f ^ n) x ≠ x
hx2 : ∀ ⦃y : α⦄, (f ^ n) y ≠ y → (f ^ n).SameCycle x y
⊢ f.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
⊢ ¬orderOf f ∣ n

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
k : ℕ
h : (f ^ (orderOf f * k)).IsCycle
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
x : α
hx : x = a ∨ x = b
y : α
hy : y = a ∨ y = b
⊢ (swap a b).SameCycle x y

Tactic:
obtain rfl | rfl := hx <;> obtain rfl | rfl := hy

Goal state after:
case inl.inl
α : Type u_2
b : α
inst✝ : DecidableEq α
y : α
hab : y ≠ b
⊢ (swap y b).SameCycle y y

case inl.inr
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ (swap x y).SameCycle x y

case inr.inl
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : y ≠ x
⊢ (swap y x).SameCycle x y

case inr.inr
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y).SameCycle y y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ (f.subtypePerm ⋯).IsCycle

Tactic:
by
  obtain ⟨a, ha⟩ := hs.nonempty
  exact
    ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
      (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩

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

Goal state before:
pp: case pos
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
z : ℤ
⊢ ((f * g) ^ (z + 1)) x = (f.cycleOf x) (((f * g) ^ z) x)

Tactic:
simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]

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

Goal state before:
pp: case neg
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
z : ℤ
⊢ ((f * g) ^ z) x = (f ^ z) x

Tactic:
simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]

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

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

Tactic:
| base_cycles σ hσ =>

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

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

Tactic:
| base_cycles σ hσ =>

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

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ sign σ = (Multiset.map (fun n ↦ -(-1) ^ n) σ.cycleType).prod

Tactic:
| base_cycles σ hσ =>

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

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

Tactic:
| base_cycles σ hσ =>

Goal state after:
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
⊢ IsConj σ τ

Tactic:
| base_cycles σ hσ =>

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

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ : Perm α
hσ : σ.IsCycle
⊢ (σ.extendDomain f).cycleType = σ.cycleType

Tactic:
| base_cycles σ hσ =>

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
inst✝ : IsEmpty n
⊢ detp (-1) A = 0

Tactic:
rw [detp, ofSign, univ_unique]

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
inst✝ : IsEmpty n
⊢ ∑ σ ∈ {default} with sign σ = -1, ∏ k, A k (σ k) = 0
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
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : ¬Function.Injective f
p q : m
eq : f p = f q
ne : p ≠ q
x✝ : m
⊢ (A.submatrix f g).row p x✝ = (A.submatrix f g).row q x✝

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.Algebra.BrauerGroup.Defs

Goal state before:
pp: K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
hAB : IsBrauerEquivalent A B
hBC : IsBrauerEquivalent B C
⊢ IsBrauerEquivalent A C

Tactic:
obtain ⟨n, m, hn, hm, ⟨iso1⟩⟩ := hAB
  obtain ⟨p, q, hp, hq, ⟨iso2⟩⟩ := hBC
  exact ⟨p * n, m * q, by simp_all, by simp_all,
    ⟨reindexAlgEquiv _ _ finProdFinEquiv |>.symm.trans <| compAlgEquiv _ _ _ _|>.symm.trans <|
    iso1.mapMatrix (m := Fin p)|>.trans <| compAlgEquiv _ _ _ _|>.trans <|
    reindexAlgEquiv K B (.prodComm (Fin p) (Fin m))|>.trans <| compAlgEquiv _ _ _ _|>.symm.trans <|
    iso2.mapMatrix.trans <| compAlgEquiv _ _ _ _|>.trans <| reindexAlgEquiv _ _ finProdFinEquiv⟩⟩

Goal state after:
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
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : ¬Function.Injective g
p q : m
eq : g p = g q
ne : p ≠ q
x✝ : m
⊢ (A.submatrix f g).col p x✝ = (A.submatrix f g).col q x✝

Tactic:
simp [eq]

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
l : n
hl1 : l ≠ (σ * τ) l
hl2 : l ∈ {τ⁻¹ j}ᶜ
⊢ ∀ (k : n), k ∈ {τ⁻¹ j}ᶜ ↔ τ k ∈ {j}ᶜ

Tactic:
simp [inv_def, eq_symm_apply]

Goal state after: