mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: case mk
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (↑((addConGen (Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun (r • Quot.mk (⇑(moduleCon f).toSetoid) x) =
    (RingHom.id R) r •
      (↑((addConGen (Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun (Quot.mk (⇑(moduleCon f).toSetoid) x)

Tactic:
exact map_smul (DirectSum.toModule R ι P g) r x

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
p : P
q : Q
⊢ ∃ a, (rTensor Q g) a = p ⊗ₜ[R] q

Tactic:
obtain ⟨n, rfl⟩ := hg p
    exact ⟨n ⊗ₜ[R] q, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Small.{u, u_1} R
s : Set M
inst✝ : Small.{u, u_2} ↑s
⊢ Small.{u, u_2} ↥(span R s)

Tactic:
suffices span R s = iSup (fun i : s ↦ span R ({(↑i : M)} : Set M)) by
    rw [this]
    apply small_iSup

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Small.{u, u_1} R
s : Set M
inst✝ : Small.{u, u_2} ↑s
⊢ span R s = ⨆ i, R ∙ ↑i
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
⊢ ↑(LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range ⊆
    ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
· rintro x ⟨y, rfl⟩
    induction y with
    | zero =>
        rw [map_zero]
        apply zero_mem
    | tmul a b =>
        simp only [LinearMap.rTensor_tmul, Submodule.coe_subtype]
        suffices (a : A) ⊗ₜ[R] b = ((1 : A) ⊗ₜ[R] b) * ((a : A) ⊗ₜ[R] (1 : B)) by
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          rw [this]
          apply Ideal.mul_mem_left
          -- Note: adding `includeLeft` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeLeft
          exact Submodule.coe_mem a
        simp only [Algebra.TensorProduct.tmul_mul_tmul,
          mul_one, one_mul]
    | add x y hx hy =>
        rw [map_add]
        apply Submodule.add_mem _ hx hy

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → AddGroupWithOne (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
n : ℕ
⊢ ⟦⟨Classical.arbitrary ι, (fun x ↦ ↑↑n) (Classical.arbitrary ι)⟩⟧ =
    ⟦⟨Classical.arbitrary ι, (fun x ↦ ↑n) (Classical.arbitrary ι)⟩⟧

Tactic:
simp_rw [Int.cast_natCast]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : (a : ι) → a ∈ s → κ
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ (↑(#t))⁻¹ • ∑ x ∈ s, f x = (↑(#t))⁻¹ • ∑ x ∈ t, g x

Tactic:
sum_bij i hi i_inj i_surj h

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

Goal state before:
pp: case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ ∃ a ∈ xs, s(x', a) = s(x, x')

Tactic:
exact ⟨_, h, Sym2.eq_swap⟩

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

Goal state before:
pp: case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ s(x, x') :: map (fun y ↦ s(x, y)) xs <+ s(x', x') :: (map (fun y ↦ s(x', y)) xs ++ xs.sym2)

Tactic:
| tail _ h =>

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

Goal state before:
pp: case succ.refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
h : ∀ a ∈ m, a ∈ s
⊢ ∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)

Tactic:
obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ

Goal state after:
case succ.refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
m : Sym α n
h : ∀ a_1 ∈ a ::ₛ m, a_1 ∈ s
⊢ ∃ i ∈ s, a ::ₛ m ∈ image (Sym.cons i) (s.sym n)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
⊢ (r • 1) • q = (r * 1) • q

Tactic:
smul_eq_mul

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
⊢ (r * 1) • q = (r * 1) • q
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
h_eq : p₁.comp q₁ = p₂.comp q₂
⊢ p₂.length + q₁.length = p₂.length + q₂.length

Tactic:
simpa [h] using congr_arg length h_eq

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

Goal state before:
pp: case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : (p.cons q).length = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
· rw [length_cons, Nat.add_right_cancel_iff] at hp
      obtain ⟨x, q'', p'', hl, rfl⟩ := h hp
      exact ⟨x, q'', p''.cons q, by simpa, rfl⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
⊢ (∃ i, Arrow.mk g = Arrow.mk (f i)) → ofHoms f g

Tactic:
rintro ⟨i, h⟩
    rw [← (ofHoms f).arrow_mk_mem_toSet_iff, h, arrow_mk_mem_toSet_iff]
    constructor

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : F.IsCorepresentable
X : C
f : F.coreprX ⟶ X
⊢ (ConcreteCategory.hom (F.coreprW.hom.app X)) f = (ConcreteCategory.hom (F.map f)) F.coreprx

Tactic:
by
  apply CorepresentableBy.homEquiv_eq

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

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
⊢ (fromSkeleton C).Full

Tactic:
by
  apply InducedCategory.full

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ c.π.app j ≫ F.map f = c.π.app j'

Tactic:
by
  simpa using (c.π.naturality f).symm

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

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
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfAdj adj F).pt
hm : ∀ (j : J), m ≫ (coneOfAdj adj F).π.app j = s.π.app j
⊢ (adj.homEquiv s.pt F).symm m = (adj.homEquiv s.pt F).symm ((adj.homEquiv s.pt F) s.π)

Tactic:
ext j; simpa using! hm j

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom ⋯ = π f j'

Tactic:
by
  simp [*]

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

Goal state before:
pp: case refine_2
β : 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
s : Cofan fun x ↦ X
m : (mk Y fun x ↦ e.hom).pt ⟶ s.pt
hm : ∀ (j : J), (mk Y fun x ↦ e.hom).inj j ≫ m = s.inj j
⊢ m = e.inv ≫ s.inj default

Tactic:
simpa [← cancel_epi e.hom] using hm default

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
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasProduct F.obj
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ limit F
h : x✝¹ ≫ Pi.lift (limit.π F) = x✝ ≫ Pi.lift (limit.π F)
j : J
⊢ x✝¹ ≫ limit.π F j = x✝ ≫ limit.π F j

Tactic:
simpa using h =≫ Pi.π _ j

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Over Y
⊢ (map (𝟙 Y)).obj x✝ = (𝟭 (Over Y)).obj x✝

Tactic:
simp [map, Comma.mapRight]

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Over Y
⊢ { left := x✝.left, right := x✝.right, hom := x✝.hom } = x✝
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
x✝ : Over X
⊢ (map (f ≫ g)).obj x✝ = (map f ⋙ map g).obj x✝

Tactic:
simp [map, Comma.mapRight]

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 : Over X
φ : f ⟶ g
F✝ : T ⥤ D
Y : D
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
A : Over (G.obj Y)
⊢ (post F ⋙ map (a.counit.app Y)).map ({ app := fun A ↦ homMk (a.unit.app A.left) ⋯, naturality := ⋯ }.app A) ≫
      { app := fun A ↦ homMk (a.counit.app A.left) ⋯, naturality := ⋯ }.app ((post F ⋙ map (a.counit.app Y)).obj A) =
    𝟙 ((post F ⋙ map (a.counit.app Y)).obj A)

Tactic:
by
    ext
    simp [-Functor.id_obj]

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 : Over X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
x✝ : t.pt ⟶ (liftCone D s c p hp).pt
hm : ∀ (j : J), x✝ ≫ (liftCone D s c p hp).π.app j = t.π.app j
j : J
⊢ Hom.left x✝ ≫ c.π.app j = Hom.left (homMk (hc.lift ((forget X).mapCone t)) ⋯) ≫ c.π.app j

Tactic:
simp [dsimp% hc.fac ((forget X).mapCone t) j, ← hm]

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
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
this : l' = homMk m ⋯
⊢ l = m

Tactic:
by apply congrArg CommaMorphism.right this

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

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

Tactic:
by
    ext
    simp [-Functor.id_obj]

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

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

Tactic:
by
    ext
    simp [-Functor.id_obj]

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

Tactic:
rw [← Under.w f.unop, op_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : IsIsomorphic X 0
⊢ 0 ≫ 0 = 𝟙 X

Tactic:
have P := P.some

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P✝ : IsIsomorphic X 0
P : X ≅ 0
⊢ 0 ≫ 0 = 𝟙 X
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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
A : Bicone F
i j : J
⊢ G.map (A.ι i ≫ A.π j) = if h : i = j then eqToHom ⋯ else 0

Tactic:
rw [A.ι_π]

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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
A : Bicone F
i j : J
⊢ G.map (if h : i = j then eqToHom ⋯ else 0) = if h : i = j then eqToHom ⋯ else 0
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : (c.whisker g).IsBilimit
⊢ IsLimit c.toCone

Tactic:
let := IsLimit.ofIsoLimit hc.isLimit (Bicone.whiskerToCone c g)
    let := (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _) this
    exact IsLimit.ofWhiskerEquivalence (Discrete.equivalence g) this

Goal state after:
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
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom ⋯ = π f j'

Tactic:
by
  simp [*]

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

Goal state before:
pp: case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ ι g k ≫ (desc fun k ↦ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j ↦ π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
· simp only [ι_desc_assoc, Category.assoc, lift_π]
    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
    · simp
    · exact h
    · rintro rfl
      simp at h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ m ≫ ∑ j, b.π j ≫ b.ι j = ∑ j, s.π.app { as := j } ≫ b.ι j

Tactic:
comp_sum

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ ∑ j, m ≫ b.π j ≫ b.ι j = ∑ j, s.π.app { as := j } ≫ b.ι j
Module: Mathlib.Algebra.Category.AlgCat.Basic

Goal state before:
pp: R✝ : Type u
inst✝³ : CommRing R✝
X₁ X₂ : Type v
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
gf : R →+* T
hfg : gf = g.comp f
A : AlgCat T
x✝ : R
⊢ (RingEquiv.refl ↑((restrictScalars gf).obj A)) ((algebraMap R ↑((restrictScalars gf).obj A)) x✝) =
    (algebraMap R ↑((restrictScalars f).obj ((restrictScalars g).obj A))) x✝

Tactic:
by subst hfg; rfl

Goal state after:
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
⊢ False

Tactic:
have h₁ : x = 𝟙 W := by simp [x]

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
⊢ False
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case elim0
k n : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 n ↔ ∑ i, i.elim0 = n

Tactic:
| elim0 =>

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

Goal state before:
pp: case refine_1
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
⊢ ∀ {i : ℕ}, i ∈ (↑p).parts.erase a → 0 < i

Tactic:
intro _ hi

Goal state after:
case refine_1
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
i✝ : ℕ
hi : i✝ ∈ (↑p).parts.erase a
⊢ 0 < i✝
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f g h : Perm α
x✝ : α
⊢ (h * f * h⁻¹) x✝ = x✝ ∨ (h * g * h⁻¹) x✝ = x✝ ↔ f (h⁻¹ x✝) = h⁻¹ x✝ ∨ g (h⁻¹ x✝) = h⁻¹ x✝

Tactic:
by simp only [mul_apply, eq_inv_iff_eq]

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
constructor
  · intro hj
    rcases (c.boundaries.orderIsoOfFin rfl).surjective ⟨j, hj⟩ with ⟨i, hi⟩
    rw [Subtype.ext_iff, Subtype.coe_mk] at hi
    refine ⟨i.1, i.2, ?_⟩
    dsimp at hi
    rw [← hi, c.blocks_partial_sum i.2]
    rfl
  · rintro ⟨i, hi, H⟩
    convert! (c.boundaries.orderIsoOfFin rfl ⟨i, hi⟩).2
    have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
    exact this.symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

Tactic:
replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
      simp [formPerm_apply_of_notMem hx, ← h]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
z : α
xs : List α
IH : ∀ (x y : α), (x :: (xs ++ [y])).formPerm y = x
x y : α
⊢ (x :: (z :: xs ++ [y])).formPerm y = x

Tactic:
simp [IH]

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

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

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

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

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
⊢ ↑a.support ⊆ ⋃ b ∈ S, ↑b.support → ↑b.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(a * b).support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
hc

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(a * b).support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
h : Fin n
⊢ ((e.symm.trans (f * g)).trans e) h = ((e.symm.trans f).trans e * (e.symm.trans g).trans e) h

Tactic:
simp [mul_apply]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.List

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
l✝ : List α
inst✝ : Std.Symm r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : (a :: l).Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Tactic:
rw [List.nodup_cons] at hl

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
l✝ : List α
inst✝ : Std.Symm r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ l.Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case h2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ (↑l.toFinset).Pairwise Disjoint

pp: case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ l.toFinset.noncommProd id ⋯ = σ

Tactic:
· simpa [hl] using h2

Goal state after:
case h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
l : List (Perm α)
h0 : l.prod = σ
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
hl : l.Nodup
⊢ l.toFinset.noncommProd id ⋯ = σ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
by_cases hx : x ∈ f.support

Goal state after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ m < Fintype.card α, (f ^ m) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
by_cases hx : x ∈ f.support

Goal state after:
case pos
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

case neg
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y