mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGrpCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget CommGrpCat).map f)
    let e : X ≃* Y := { i.toEquiv with map_mul' := by simp [Iso.toEquiv, i] }
    exact e.toCommGrpIso.isIso_hom

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F✝ : J ⥤ C
t✝ : Cone F✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ G.map (e.counit.app (e.functor.obj j)) ≫ w.hom.app j =
    s.π.app j

Tactic:
rw [counit_app_functor, ← Functor.comp_map, ← w.inv.naturality_assoc]

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F✝ : J ⥤ C
t✝ : Cone F✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫ F.map (e.unitInv.app j) ≫ w.inv.app ((𝟭 J).obj j) ≫ w.hom.app j =
    s.π.app j
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ homOfCone h (coneOfHom h f) = f

Tactic:
by
  simp [coneOfHom, homOfCone]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y Y' : C
e : F.RepresentableBy Y
e' : F.RepresentableBy Y'
ε : {X : C} → (X ⟶ Y) ≃ (X ⟶ Y') := fun {X} ↦ e.homEquiv.trans e'.homEquiv.symm
⊢ ∀ {Z Z' : C} (f : Z' ⟶ Z) (g : Z ⟶ Y), ε (f ≫ g) = f ≫ ε g

Tactic:
simp [ε, comp_homEquiv_symm, homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X X' : C
e : F.CorepresentableBy X
e' : F.CorepresentableBy X'
ε : {Y : C} → (X ⟶ Y) ≃ (X' ⟶ Y) := fun {Y} ↦ e.homEquiv.trans e'.homEquiv.symm
⊢ ∀ {Z Z' : C} (f : X' ⟶ Z) (g : Z ⟶ Z'), ε.symm (f ≫ g) = ε.symm f ≫ g

Tactic:
by simp [ε, homEquiv_symm_comp, homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type v₁) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
by
      intro Y Z f
      ext F g
      simpa [← ULift.down_inj] using! (yonedaEquiv_naturality _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
⊢ IsIso f

Tactic:
obtain ⟨g, hg : f ≫ g = 𝟙 X⟩ := (hf X).2 (𝟙 X)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ IsIso f
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ (adj.homEquiv A X).symm ((adj.homEquiv A X) u) = u

Tactic:
apply (adj.homEquiv _ _).left_inv

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : ⋯.LiftStruct
⊢ (adj.homEquiv B Y).symm ((adj.homEquiv B Y) v) = v

Tactic:
apply (adj.homEquiv _ _).left_inv

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ a = b

Tactic:
rw [this a, this b]

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasCoproduct F.obj
Z✝ : C
x✝¹ x✝ : colimit F ⟶ Z✝
h : Sigma.desc (colimit.ι F) ≫ x✝¹ = Sigma.desc (colimit.ι F) ≫ x✝
⊢ x✝¹ = x✝

Tactic:
refine colimit.hom_ext fun j => ?_

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasCoproduct F.obj
Z✝ : C
x✝¹ x✝ : colimit F ⟶ Z✝
h : Sigma.desc (colimit.ι F) ≫ x✝¹ = Sigma.desc (colimit.ι F) ≫ x✝
j : J
⊢ colimit.ι F j ≫ x✝¹ = colimit.ι F j ≫ x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Tactic:
by
  have w := t.ι.naturality WalkingSpan.Hom.fst
  dsimp at w; simpa using w.symm

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
inst✝¹ : S.Full
inst✝ : S.Faithful
⊢ ∀ (s : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))) (m : s.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt),
    (∀ (j : Discrete PEmpty.{1}), m ≫ (asEmptyCone (mk (𝟙 (S.obj Y)))).π.app j = s.π.app j) →
      m = homMk (S.preimage s.pt.hom) ⋯

Tactic:
by
    rintro c m -
    ext
    apply S.map_injective
    simpa only [homMk_left, S.map_preimage, ← w m] using! (Category.comp_id _).symm

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
Z Y : Over (op X)
f : Z ⟶ Y
⊢ Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop

Tactic:
← unop_comp,

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Over (op X)
f : Z ⟶ Y
⊢ (Hom.left f ≫ Y.hom).unop = Z.hom.unop
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
Z Y : Under (op X)
f : Z ⟶ Y
⊢ (Hom.right f).unop ≫ Z.hom.unop = Y.hom.unop

Tactic:
← unop_comp,

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Under (op X)
f : Z ⟶ Y
⊢ (Z.hom ≫ Hom.right f).unop = Y.hom.unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝³ : HasEqualizers C
inst✝² : HasImage g
inst✝¹ : HasImage (f ≫ g)
inst✝ : Epi f
⊢ Epi (preComp f g)

Tactic:
apply @epi_of_epi_fac _ _ _ _ _ _ _ _ ?_ (image.factorThruImage_preComp _ _)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝³ : HasEqualizers C
inst✝² : HasImage g
inst✝¹ : HasImage (f ≫ g)
inst✝ : Epi f
⊢ Epi (f ≫ factorThruImage g)
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : m₁.toMonoid = m₂.toMonoid
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ ZPow.zpow = ZPow.zpow

Tactic:
ext m x

Goal state after:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : m₁.toMonoid = m₂.toMonoid
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
m : ℤ
x : M
⊢ ZPow.zpow m x = ZPow.zpow m x
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
D : Type u'
inst✝² : Category.{v, u'} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ ∀ {X_1 Y_1 : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1),
    (parallelPair f 0 ⋙ F).map f_1 ≫ (app Y_1).hom = (app X_1).hom ≫ (parallelPair (F.map f) 0).map f_1

Tactic:
rintro ⟨i⟩ ⟨j⟩

Goal state after:
case zero.zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u'
inst✝² : Category.{v, u'} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ ∀ (f_1 : zero ⟶ zero),
    (parallelPair f 0 ⋙ F).map f_1 ≫ (app zero).hom = (app zero).hom ≫ (parallelPair (F.map f) 0).map f_1

case zero.one
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u'
inst✝² : Category.{v, u'} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ ∀ (f_1 : zero ⟶ one),
    (parallelPair f 0 ⋙ F).map f_1 ≫ (app one).hom = (app zero).hom ≫ (parallelPair (F.map f) 0).map f_1

case one.zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u'
inst✝² : Category.{v, u'} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ ∀ (f_1 : one ⟶ zero),
    (parallelPair f 0 ⋙ F).map f_1 ≫ (app zero).hom = (app one).hom ≫ (parallelPair (F.map f) 0).map f_1

case one.one
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u'
inst✝² : Category.{v, u'} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ ∀ (f_1 : one ⟶ one),
    (parallelPair f 0 ⋙ F).map f_1 ≫ (app one).hom = (app one).hom ≫ (parallelPair (F.map f) 0).map f_1
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
F : MonoFactorisation f
⊢ kernel.ι f ≫ F.e = 0

Tactic:
by
  rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive C
inst✝ : Preadditive D
F : C ⥤ D
hF : IsZero F
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ IsZero (F.obj x✝²)

Tactic:
by
      rw [IsZero.iff_id_eq_zero]
      exact NatTrans.congr_app ((IsZero.iff_id_eq_zero _).1 hF) _

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
⊢ a = b

Tactic:
apply Preadditive.ext

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
⊢ homGroup = homGroup
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d : ℕ
n : μ
h : n = 0
⊢ ∀ (f : Fin 0 → μ), f ∈ {0} ↔ ∑ i, f i = n

Tactic:
by simp [h, Subsingleton.elim _ ![]]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    (antidiagonal 0)

Tactic:
rw [antidiagonal_zero]
      exact List.pairwise_singleton _ _

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
x : n.Partition
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ x.parts.Nodup

Tactic:
Multiset.nodup_iff_count_le_one

Goal state after:
n : ℕ
x : n.Partition
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ ∀ (a : ℕ), count a x.parts ≤ 1
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x

Tactic:
by
  induction k with
  | zero => simp
  | succ k hk =>
    intro x hx
    rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]
    rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]

Goal state after:
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: α : 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 b : α
⊢ f b ≠ b ↔ ?m.105 b

Tactic:
rw [← mem_support, ← hins, mem_insert, mem_singleton]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ (l.rotate 1).formPerm (l.rotate 1)[k] = l.formPerm (l.rotate 1)[k]

Tactic:
formPerm_apply_getElem _ h',

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ (l.rotate 1)[(k + 1) % (l.rotate 1).length] = l.formPerm (l.rotate 1)[k]
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
this : ¬b₁ < b₂
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

Tactic:
split_ifs at h <;>
  simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

Goal state after:
case neg
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : f b₁ < f b₂
h✝ : f b₁ ≤ f b₂
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂

case pos
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : f b₂ ≤ f b₁
h✝ : f b₂ < f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
split_ifs <;> simp [symm_apply_eq, eq_symm_apply] at *

Goal state after:
case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝ : b = f (f x)
⊢ ¬x = b

case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝¹ : ¬b = f (f x)
h✝ : b = f x
⊢ ¬f x = b

case neg
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝¹ : ¬b = f (f x)
h✝ : ¬b = f x
⊢ ¬b = f b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
simp only [support_inv, imp_self, implies_true]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
h1' : (σ ^ n).IsCycle
⊢ ⊤ ≤ closure {σ, swap x ((σ ^ n) x)}

Tactic:
← closure_cycle_adjacent_swap h1' h2' x,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
h1' : (σ ^ n).IsCycle
⊢ closure {σ ^ n, swap x ((σ ^ n) x)} ≤ closure {σ, swap x ((σ ^ n) x)}
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
key : (∀ i ∈ S, _root_.Disjoint (↑i.support) (⋃ b ∈ T, ↑b.support)) → _root_.Disjoint ↑a.support ↑b.support
⊢ _root_.Disjoint a.support b.support

Tactic:
Set.disjoint_iUnion_right,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
key : (∀ i ∈ S, ∀ i_2 ∈ T, _root_.Disjoint ↑i.support ↑i_2.support) → _root_.Disjoint ↑a.support ↑b.support
⊢ _root_.Disjoint a.support b.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Tactic:
by
  intro a ha b hb
  have key1 := support_closure_subset_union S a ha
  have key2 := support_closure_subset_union T b hb
  have key := Set.disjoint_of_subset key1 key2
  simp_rw [Set.disjoint_iUnion_left, Set.disjoint_iUnion_right, Finset.disjoint_coe] at key
  exact key h

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ (ϕ i) (f i) ∈ ⨆ i, mrange (ϕ i)

Tactic:
apply Submonoid.mem_sSup_of_mem

Goal state after:
case hs
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ?a.s✝ ∈ Set.range fun i ↦ mrange (ϕ i)

case a.a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ (ϕ i) (f i) ∈ ?a.s✝

case a.s
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ Submonoid M
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
⊢ ↑(i.castLT ⋯) = ↑(last ↑j)

Tactic:
by simp [ch]

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

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

Tactic:
extendDomain_one,

Goal state after:
case base_one
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ cycleType 1 = cycleType 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inr.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

pp: case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
· rw [heq, Fin.cycleRange_self, Fin.succAbove_of_castSucc_lt, swap_apply_right, Fin.castSucc_zero]
    · rw [Fin.castSucc_zero]
      apply Fin.succ_pos

Goal state after:
case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: case pos
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : Function.Injective v
⊢ (↑f fun i ↦ e (v i)) = ↑g fun i ↦ e (v i)

Tactic:
exact h v hi

Goal state after: