mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.comap (↑(map (AlgHom.id S A) g)) (RingHom.ker (map f (AlgHom.id R D))) =
    Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.comap (map (AlgHom.id R A) g) ⊥

Tactic:
rw [← Ideal.comap_map_of_surjective (map (AlgHom.id R A) g) (LinearMap.lTensor_surjective A hg)]

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.comap (↑(map (AlgHom.id S A) g)) (RingHom.ker (map f (AlgHom.id R D))) =
    Ideal.comap (map (AlgHom.id R A) g) (Ideal.map (map (AlgHom.id R A) g) (Ideal.map includeLeft (RingHom.ker f)))
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ ↑j ≠ last k

Tactic:
grind [val_cast_of_lt]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝¹ : Semifield K
inst✝ : CharZero K
s : Finset ι
f : ι → K
⊢ (↑↑(#s))⁻¹ * ∑ i ∈ s, f i = (↑(#s))⁻¹ * ∑ i ∈ s, f i

Tactic:
NNRat.cast_natCast

Goal state after:
ι : Type u_1
K : Type u_3
inst✝¹ : Semifield K
inst✝ : CharZero K
s : Finset ι
f : ι → K
⊢ (↑(#s))⁻¹ * ∑ i ∈ s, f i = (↑(#s))⁻¹ * ∑ i ∈ s, f i
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
a✝ : ℤ
⊢ a✝ ∈ Icc (-(↑m + 1)) (↑n + 1) ↔ a✝ ∈ Icc (-↑m) ↑n ∪ {-(↑m + 1), ↑n + 1}

Tactic:
simp only [mem_Icc, union_insert, union_singleton, mem_insert]

Goal state after:
m n : ℕ
a✝ : ℤ
⊢ -(↑m + 1) ≤ a✝ ∧ a✝ ≤ ↑n + 1 ↔ a✝ = -(↑m + 1) ∨ a✝ = ↑n + 1 ∨ -↑m ≤ a✝ ∧ a✝ ≤ ↑n
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
⊢ Nat.card ↑(f ⁻¹' ↑s) = ∑ b ∈ s, Nat.card { a // f a = b }

Tactic:
rw [show Nat.card (f ⁻¹' s) = Nat.card (f ⁻¹' t) by simp [t]]

Goal state after:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
⊢ Nat.card ↑(f ⁻¹' ↑t) = ∑ b ∈ s, Nat.card { a // f a = b }
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Tactic:
by
  cases n
  · exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim
  · refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
    rintro ⟨_, rfl⟩
    exact sym_empty _

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: α : Type ?u.3
inst✝ : LinearOrder α
a b : α
x✝ : a ≤ b ∨ b ≤ a
⊢ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = a ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = b ∨
    (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = b ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = a

Tactic:
cases le_total a b with

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)

Tactic:
rw [Nat.multichoose_succ_succ, length_cons, add_comm]

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤

Tactic:
induction s using Finset.cons_induction <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
⊢ ∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥

Tactic:
induction s using Finset.cons_induction <;> simp [*]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ s(a, Mem.other h) = z

Tactic:
other_spec

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ z = z
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ (insert a s).sym2 = (fun b ↦ s(a, b)) '' insert a s ∪ s.sym2

Tactic:
by
  ext ⟨x, y⟩; aesop

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ ⇑(hom (𝟙 X)) = id

Tactic:
ext
  simp [ConcreteCategory.id_apply]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure = P

Tactic:
apply le_antisymm
  · intro X ⟨Y, hY, ⟨e⟩⟩
    exact prop_of_iso P e.symm hY
  · exact le_isoClosure P

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y : C
f : Y ⟶ X
h : W = Y
⊢ eqToHom h ≫ f ≍ f

Tactic:
by
  rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (𝟙 ((𝟭 C).obj (e.inverse.obj Y))))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))

Tactic:
dsimp only [Functor.id_obj]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (𝟙 (e.inverse.obj Y)))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : Cᵒᵖ
⊢ e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫ (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X) =
    𝟙 (e.functor.op.obj X)

Tactic:
by
    apply Quiver.Hom.unop_inj
    simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h k : c ⟶ d
η : h ≅ k
⊢ f ◁ g ◁ η.hom ≫ f ◁ g ◁ η.inv = 𝟙 (f ≫ g ≫ h)

Tactic:
by
  simp [← whiskerLeft_comp]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h k : c ⟶ d
η : h ≅ k
⊢ f ◁ g ◁ η.inv ≫ f ◁ g ◁ η.hom = 𝟙 (f ≫ g ≫ k)

Tactic:
by
  simp [← whiskerLeft_comp]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
k : c ⟶ d
⊢ f ◁ η.hom ▷ k ≫ f ◁ η.inv ▷ k = 𝟙 (f ≫ g ≫ k)

Tactic:
by
  simp [← whiskerLeft_comp]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
k : c ⟶ d
⊢ f ◁ η.inv ▷ k ≫ f ◁ η.hom ▷ k = 𝟙 (f ≫ h ≫ k)

Tactic:
by
  simp [← whiskerLeft_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
intro η

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
η : yoneda.obj X ⟶ F
⊢ (fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ })
      ((fun η ↦ (ConcreteCategory.hom (η.app (op X))) (𝟙 X)) η) =
    η
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯ ≫
      Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯ =
    𝟙 (Arrow.mk f.op)

Tactic:
ext <;> simp [← op_comp]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ Function.RightInverse (fun u ↦ { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ }) fun t X ↦
    {
      default :=
        t.lift { pt := X, π := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } },
      uniq := ⋯ }

Tactic:
dsimp [Function.RightInverse, Function.LeftInverse]
    subsingleton

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
⊢ IsLimit (mk X fun x ↦ e.hom)

Tactic:
refine Fan.IsLimit.mk _ (fun s ↦ s.proj default ≫ e.inv) (fun s j ↦ ?_) fun s m hm ↦ ?_
  · obtain rfl : j = default := Subsingleton.elim _ _
    simp
  · simpa [← cancel_mono e.hom] using hm default

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

Goal state before:
pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s.π.app (some WalkingPair.right) = i.hom ≫ t.π.app (some WalkingPair.right)

Tactic:
exact w₂

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

Goal state before:
pp: case some.right
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
⊢ s.ι.app (some WalkingPair.right) ≫ i.hom = t.ι.app (some WalkingPair.right)

Tactic:
exact w₂

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingCospan ⥤ C
t : Cone F
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose (diagramIsoCospan F).hom).obj t).π.app j =
      (Iso.refl ((Cone.postcompose (diagramIsoCospan F).hom).obj t).pt).hom ≫
        (mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯).π.app j

Tactic:
rintro (_ | (_ | _)) <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
F : WalkingSpan ⥤ C
t : Cocone F
⊢ ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan F).inv).obj t).ι.app j ≫
        (Iso.refl ((Cocone.precompose (diagramIsoSpan F).inv).obj t).pt).hom =
      (mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯).ι.app j

Tactic:
rintro (_ | (_ | _)) <;> simp

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 f
⊢ IsIso (pushout.inr f g)

Tactic:
refine ⟨⟨pushout.desc (inv f ≫ g) (𝟙 _) (by simp), by simp, ?_⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = 𝟙 (pushout f g)
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 × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
⊢ (Over.forget X.1).map (((proj (Functor.diag T) X).toOver X.1 (fun g ↦ g.hom.1) ⋯).map m) ≫ Z✝.hom.2 = Y✝.hom.2

Tactic:
by have := congrArg (·.2) m.w; cat_disch

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

Goal state before:
pp: case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
| _ j
       => 

Goal state after:
case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ (imageMonoIsoSource f).inv ≫ image.ι f = image.ι f

Tactic:
rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]

Goal state after:
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
F : MonoFactorisation f.hom
F' : MonoFactorisation g.hom
hF' : IsImage F'
map : F.I ⟶ F'.I
map_ι : map ≫ F'.m = F.m ≫ Arrow.Hom.right sq
⊢ (image.lift F ≫ map ≫ hF'.lift (Image.monoFactorisation g.hom)) ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq

Tactic:
by simp [map_ι]

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

Goal state before:
pp: case invFun
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ 𝟙 X = 0 ∧ 𝟙 Y = 0 → (X ≅ 0) × (Y ≅ 0)

Tactic:
rintro ⟨hX, hY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X) hX
    · exact (idZeroEquivIsoZero Y) hY

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn j' (Option.casesOn j {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
        if h : some j' = j then ⋯.mpr {Hom.id j} else ∅

Tactic:
rintro (_ | _)
    · cases j <;> simp
    · simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn j (Option.casesOn j' {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
        if h : some j = j' then ⋯.mpr {Hom.id j'} else ∅

Tactic:
rintro (_ | _)
    · cases j <;> simp
    · simp

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
g₁ g₂ : Group G
h_mul : HMul.hMul = HMul.hMul
h₁ : One.one = One.one
⊢ g₁ = g₂

Tactic:
let f : @MonoidHom G G g₁.toMulOne g₂.toMulOne :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)

Goal state after:
G : Type u_1
g₁ g₂ : Group G
h_mul : HMul.hMul = HMul.hMul
h₁ : One.one = One.one
f : G →* G := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ g₁ = 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
s : CokernelCofork f
⊢ f ≫ Cofork.π s = 0

Tactic:
Cofork.condition,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : CokernelCofork f
⊢ 0 ≫ Cofork.π s = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : CokernelCofork f
⊢ f ≫ Cofork.π s = 0

Tactic:
by
  rw [Cofork.condition, zero_comp]

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
W : C
g : W ⟶ X
h : W ⟶ Y
c : CokernelCofork h
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h
s : Cofork f 0
⊢ Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ i.desc (CokernelCofork.ofπ s.π ⋯) = s.π

Tactic:
simp only [CokernelCofork.π_ofπ, Cofork.IsColimit.π_desc]

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✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel (?m.116 s) ⟶ ?m.118 s
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ m = cokernel.desc f (g ≫ Cofork.π s) ⋯

Tactic:
simp_rw [← w]
            apply coequalizer.hom_ext
            simp

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ fst.op ≫ (opIso P Q).hom = inl

Tactic:
ext <;> simp [← op_comp]

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ snd.op ≫ (opIso P Q).hom = inr

Tactic:
ext <;> simp [← op_comp]

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (opIso P Q).inv ≫ inl.op = fst

Tactic:
ext <;> simp [← op_comp]

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
P Q : C
inst✝ : HasBinaryBiproduct P Q
⊢ (opIso P Q).inv ≫ inr.op = snd

Tactic:
ext <;> simp [← op_comp]

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q₁ q₂ : (j : Fin (n + 1)) → α j
⊢ i.insertNth x p ∈ Icc q₁ q₂ ↔ x ∈ Icc (q₁ i) (q₂ i) ∧ p ∈ Icc (fun j ↦ q₁ (i.succAbove j)) fun j ↦ q₂ (i.succAbove j)

Tactic:
simp only [mem_Icc, insertNth_le_iff, le_insertNth_iff, and_assoc, @and_left_comm (x ≤ q₂ i)]

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.boundaries.card = c.length + 1

Tactic:
simp [boundaries]

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

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

Tactic:
rw [sum_mapRange_index (fun _ ↦ rfl), ← hsum, _root_.map_finsuppSum]

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

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : (n :: ns).sum = l.length
⊢ (l.splitWrtCompositionAux (n :: ns)).flatten = l

Tactic:
sum_cons

Goal state after:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ (l.splitWrtCompositionAux (n :: ns)).flatten = l
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ #{x | σ x = x} < Fintype.card α - 1

Tactic:
by
  rw [Nat.lt_sub_iff_add_lt, ← Nat.lt_sub_iff_add_lt', ← Finset.card_compl, Finset.compl_filter]
  exact one_lt_card_support_of_ne_one h

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

Goal state before:
pp: case intro.refine_2.inl.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
h : g (τ ((Equiv.symm g) (f x))) = f x
⊢ τ x = (Equiv.symm f) (g (τ ((Equiv.symm g) (f x))))

Tactic:
rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| (k + 1 + n) % (x :: y :: l).length

Tactic:
rw [← Nat.mod_eq_of_lt hk']

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length