mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
⊢ IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)))

Tactic:
convert! TensorProduct.isTensorProduct R S M using 1

Goal state after:
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
⊢ ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1)) = mk R S M
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
rw [Sym2.eq_swap] at h

Goal state after:
α : Type u_1
xs : List α
a b : α
h : s(b, a) ∈ xs.sym2
⊢ b ∈ xs
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a = x ∨ a ∈ xs

Tactic:
right

Goal state after:
case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a ∈ xs
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case inr
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs

Tactic:
· rw [mem_cons]
      right
      exact mem_of_mem_of_mem_sym ha hz

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Epi h
w : f ≫ g = h
⊢ Epi g

Tactic:
subst h; exact epi_of_epi f g

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁵⁰ : AddCommMonoid M✝
inst✝⁴⁹ : AddCommMonoid N
inst✝⁴⁸ : CommSemiring R
inst✝⁴⁷ : CommSemiring S
inst✝⁴⁶ : Algebra R S
inst✝⁴⁵ : Module R M✝
inst✝⁴⁴ : Module R N
inst✝⁴³ : Module S N
inst✝⁴² : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁴¹ : AddCommMonoid P
inst✝⁴⁰ : Module R P
inst✝³⁹ : AddCommMonoid Q
inst✝³⁸ : Module S Q
inst✝³⁷ : Module R Q
inst✝³⁶ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³⁵ : CommSemiring T
inst✝³⁴ : Algebra R T
inst✝³³ : Algebra S T
inst✝³² : IsScalarTower R S T
inst✝³¹ : AddCommMonoid O
inst✝³⁰ : Module R O
inst✝²⁹ : Module S O
inst✝²⁸ : Module T O
inst✝²⁷ : IsScalarTower S T O
inst✝²⁶ : IsScalarTower R S O
inst✝²⁵ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝²⁴ : CommSemiring R'
inst✝²³ : CommSemiring S'
inst✝²² : Algebra R R'
inst✝²¹ : Algebra S S'
inst✝²⁰ : Algebra R' S'
inst✝¹⁹ : Algebra R S'
inst✝¹⁸ : IsScalarTower R R' S'
inst✝¹⁷ : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra S B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : IsPushout R S A B
M : Type u_10
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ B ⊗[A] C ≃ₐ[S] S ⊗[R] C

Tactic:
by
  refine AlgEquiv.symm
    (AlgEquiv.ofLinearEquiv (IsPushout.cancelBaseChange R S A B C).symm ?_ ?_)
  · simp [TensorProduct.one_def]
  · apply LinearMap.map_mul_of_map_mul_tmul
    simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1) → p.length ≠ 0

Tactic:
rintro ⟨c, p', e, rfl, h⟩
    simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.inv.unop ≫ f.hom.unop = 𝟙 (Opposite.unop X)

Tactic:
simp only [← unop_comp, f.hom_inv_id, unop_id]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
X : C
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
rw [← adj.homEquiv_counit, (adj.homEquiv _ _).symm_apply_eq, adj.homEquiv_unit]
    simp

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✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
j : J
⊢ G.map m ≫ (G.mapCone t).π.app j = (G.mapCone s).π.app j

Tactic:
convert! ← congrArg (fun f => G.map f) (w j)

Goal state after:
case e'_2
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✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
j : J
e_1✝ : (G.obj s.pt ⟶ G.obj (F.obj j)) = ((G.mapCone s).pt ⟶ (F ⋙ G).obj j)
⊢ G.map (m ≫ t.π.app j) = G.map m ≫ (G.mapCone t).π.app j
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'

Tactic:
rhs
      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ g'
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
u : WalkingPair
⊢ (colimit.cocone (pair X Y)).ι.app { as := u } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    (BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := u }

Tactic:
cases u
    · dsimp; simp only [Category.comp_id]
    · dsimp; simp only [Category.comp_id]

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

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
left✝¹ : Discrete PUnit.{1}
right✝¹ : C
hom✝¹ : (Functor.fromPUnit S).obj left✝¹ ⟶ T.obj right✝¹
left✝ : Discrete PUnit.{1}
right✝ : C
hom✝ : (Functor.fromPUnit S).obj left✝ ⟶ T.obj right✝
hr : right { left := left✝¹, right := right✝¹, hom := hom✝¹ } = right { left := left✝, right := right✝, hom := hom✝ }
hh :
  hom { left := left✝¹, right := right✝¹, hom := hom✝¹ } ≫ T.map (eqToHom hr) =
    hom { left := left✝, right := right✝, hom := hom✝ }
⊢ { left := left✝¹, right := right✝¹, hom := hom✝¹ } = { left := left✝, right := right✝, hom := hom✝ }

Tactic:
cases hr

Goal state after:
case mk.mk.refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
left✝¹ : Discrete PUnit.{1}
right✝ : C
hom✝¹ : (Functor.fromPUnit S).obj left✝¹ ⟶ T.obj right✝
left✝ : Discrete PUnit.{1}
hom✝ : (Functor.fromPUnit S).obj left✝ ⟶ T.obj right✝
hh :
  hom { left := left✝¹, right := right✝, hom := hom✝¹ } ≫ T.map (eqToHom ⋯) =
    hom { left := left✝, right := right✝, hom := hom✝ }
⊢ { left := left✝¹, right := right✝, hom := hom✝¹ } = { left := left✝, right := right✝, hom := hom✝ }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } })) = 𝟙 t.pt

Tactic:
apply Q.hom_ext
    rintro ⟨⟨⟩⟩
    · simp
    · apply P.hom_ext
      rintro ⟨⟨⟩⟩

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 g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ g.hom ≫ l = g.hom ≫ m

Tactic:
rw [← Under.w k, Category.assoc, a, Category.assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : (mk s.inl s.inr ⋯).inl ≫ m✝ = t.inl
hr' : (mk s.inl s.inr ⋯).inr ≫ m✝ = t.inr
⊢ m✝ = hs.desc (mk t.inl t.inr ⋯)

Tactic:
apply PushoutCocone.IsColimit.hom_ext hs

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : (mk s.inl s.inr ⋯).inl ≫ m✝ = t.inl
hr' : (mk s.inl s.inr ⋯).inr ≫ m✝ = t.inr
⊢ s.inl ≫ m✝ = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : (mk s.inl s.inr ⋯).inl ≫ m✝ = t.inl
hr' : (mk s.inl s.inr ⋯).inr ≫ m✝ = t.inr
⊢ s.inr ≫ m✝ = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
f : F ⟶ G
X : C
H : MonoFactorisation f
x : F.obj X
⊢ (ConcreteCategory.hom (H.m.app X)) ((ConcreteCategory.hom (H.e.app X)) x) = (ConcreteCategory.hom (f.app X)) x

Tactic:
simp [← comp_apply, ← NatTrans.comp_app]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
A✝ B✝ : SemimoduleCat R
f : A✝ ⟶ B✝
x✝ : IsIso ((forget₂ (SemimoduleCat R) AddCommMonCat).map f)
this : IsIso ((forget (SemimoduleCat R)).map f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso _ (forget _)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² : x✝⁵ ⟶ x✝⁴
x✝¹ : R
x✝ : x✝⁴ ⟶ x✝³
⊢ x✝² ≫ (x✝¹ • x✝) = x✝¹ • x✝² ≫ x✝

Tactic:
by ext; apply comp_smul

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

Goal state before:
pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')

Tactic:
· exact ∅

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

Goal state before:
pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : ¬some j = j'
⊢ Finset (some j ⟶ j')

Tactic:
· exact ∅

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
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⟩ <;> rintro (g | g) <;> aesop

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ Y✝ : C ⥤ D
e : X✝ ≅ Y✝
h : leftExactFunctor C D X✝
⊢ leftExactFunctor C D Y✝

Tactic:
simp only [leftExactFunctor_iff] at h ⊢

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ Y✝ : C ⥤ D
e : X✝ ≅ Y✝
h : PreservesFiniteLimits X✝
⊢ PreservesFiniteLimits Y✝
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
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ IsZero c.pt

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]

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

Goal state before:
pp: case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : ↑i = j then eqToHom ⋯ else 0) = if h_1 : i = ⟨j, h⟩ then eqToHom ⋯ else 0

Tactic:
split_ifs with h₁ h₂ h₂

Goal state after:
case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ↑i = j
h₂ : i = ⟨j, h⟩
⊢ eqToHom ⋯ = eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ↑i = j
h₂ : ¬i = ⟨j, h⟩
⊢ eqToHom ⋯ = 0

case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬↑i = j
h₂ : i = ⟨j, h⟩
⊢ 0 = eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬↑i = j
h₂ : ¬i = ⟨j, h⟩
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
⊢ (if h : ↑j✝ = ↑j then eqToHom ⋯ else 0) = if h : j✝ = j then eqToHom ⋯ else 0

Tactic:
split_ifs with h₁ h₂ h₂

Goal state after:
case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
h₁ : ↑j✝ = ↑j
h₂ : j✝ = j
⊢ eqToHom ⋯ = eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
h₁ : ↑j✝ = ↑j
h₂ : ¬j✝ = j
⊢ eqToHom ⋯ = 0

case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
h₁ : ¬↑j✝ = ↑j
h₂ : j✝ = j
⊢ 0 = eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
h₁ : ¬↑j✝ = ↑j
h₂ : ¬j✝ = j
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : j = ↑i then eqToHom ⋯ else 0) = if h_1 : ⟨j, h⟩ = i then eqToHom ⋯ else 0

Tactic:
split_ifs with h₁ h₂ h₂

Goal state after:
case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : j = ↑i
h₂ : ⟨j, h⟩ = i
⊢ eqToHom ⋯ = eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : j = ↑i
h₂ : ¬⟨j, h⟩ = i
⊢ eqToHom ⋯ = 0

case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬j = ↑i
h₂ : ⟨j, h⟩ = i
⊢ 0 = eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬j = ↑i
h₂ : ¬⟨j, h⟩ = i
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
⊢ (if h : ↑j = ↑j✝ then eqToHom ⋯ else 0) = if h : j = j✝ then eqToHom ⋯ else 0

Tactic:
split_ifs with h₁ h₂ h₂

Goal state after:
case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
h₁ : ↑j = ↑j✝
h₂ : j = j✝
⊢ eqToHom ⋯ = eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
h₁ : ↑j = ↑j✝
h₂ : ¬j = j✝
⊢ eqToHom ⋯ = 0

case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
h₁ : ¬↑j = ↑j✝
h₂ : j = j✝
⊢ 0 = eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
h₁ : ¬↑j = ↑j✝
h₂ : ¬j = j✝
⊢ 0 = 0
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N A✝ B✝ : ModuleCat R
f : A✝ ⟶ B✝
x✝ : IsIso ((forget₂ (ModuleCat R) AddCommGrpCat).map f)
this : IsIso ((forget (ModuleCat R)).map f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso _ (forget _)

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

Goal state before:
pp: n : ℕ
⊢ antidiagonalTuple 1 n = [![n]]

Tactic:
simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton,
    Nat.sub_self, List.flatMap_append, List.flatMap_singleton, List.flatMap_map]

Goal state after:
n : ℕ
⊢ flatMap (fun a ↦ map (fun x ↦ Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) ++
      map (fun x ↦ Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: p : Partition 1
h : p.parts = replicate p.parts.card 1
⊢ p.parts.card = 1

Tactic:
simpa using (congrArg sum h.symm).trans p.parts_sum

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

Goal state before:
pp: case inr
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
this :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length},
    i₁ ≠ i₂ → i₁ < i₂ → _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
h' : ¬i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

pp: n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

Tactic:
· exact (this c h.symm (h.lt_or_gt.resolve_left h')).symm

Goal state after:
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
h' : i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ ↑((c.embedding i) j) - c.sizeUpTo ↑(c.index ((c.embedding i) j)) = ↑j

Tactic:
index_embedding,

Goal state after:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ ↑((c.embedding i) j) - c.sizeUpTo ↑i = ↑j
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∈ c.support
⊢ c x ∈ s ↔ x ∈ s

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∉ c.support
⊢ c x ∈ s ↔ x ∈ s

Tactic:
· simp only [hcs hx', hcs (apply_mem_support.mpr hx')]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∉ c.support
⊢ c x ∈ s ↔ x ∈ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k ⋯).support = (insert i s).biUnion fun i ↦ (k i).support

Tactic:
have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])

Goal state after:
case insert
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k ⋯).support = (insert i s).biUnion fun i ↦ (k i).support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.toComposition.length = c.length

Tactic:
by
  simp [CompositionAsSet.toComposition, Composition.length]

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

Goal state before:
pp: n✝ n : ℕ
c : CompositionAsSet n
⊢ ((fun c ↦ c.toCompositionAsSet) ((fun c ↦ c.toComposition) c)).boundaries = c.boundaries

Tactic:
exact c.toComposition_boundaries

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ ∀ x ∈ l, (List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)).Nodup

Tactic:
exact fun _ _ => hln'.map fun _ _ => mul_left_cancel

Goal state after: