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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(rTensor M f) ⇑(rTensor M π)
⊢ Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)

Tactic:
rw [show g = ι.comp π from rfl, rTensor_comp]

Goal state after:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(rTensor M f) ⇑(rTensor M π)
⊢ Function.Exact ⇑(rTensor M f) ⇑(rTensor M ι ∘ₗ rTensor M π)
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✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧)

Tactic:
by simp_rw [mul_def, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R M
inst✝⁷ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
⊢ Function.Injective ⇑(hf.map hg LinearMap.id i)

Tactic:
have h : hf.map hg LinearMap.id i = hg.equiv ∘ i.lTensor M₁ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R M
inst✝⁷ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
h : ⇑(hf.map hg LinearMap.id i) = ⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(hf.map hg LinearMap.id i)
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
⊢ ((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f = LinearMap.id f

Tactic:
apply (Matrix.stdBasis _ _ _).ext

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
⊢ ∀ (i : n × n),
    (((mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n) f) ((stdBasis R n n) i) =
      (LinearMap.id f) ((stdBasis R n n) i)
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 : ι) → NonUnitalNonAssocSemiring (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ (⟦⟨i, x✝²⟩⟧ + ⟦⟨i, x✝¹⟩⟧) * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝⟩⟧ + ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧

Tactic:
simp_rw [add_def, mul_def, right_distrib, add_def]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
n : ℕ
⊢ hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α n
⊢ m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s

Tactic:
induction n with

Goal state after:
case succ
α : 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)
⊢ m ∈ s.sym (n + 1) ↔ ∀ a ∈ m, a ∈ s
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
⊢ (map g s).sym n = map { toFun := Sym.map ⇑g, inj' := ⋯ } (s.sym n)

Tactic:
ext d
  simp only [mem_sym_iff, mem_map, Function.Embedding.coeFn_mk]
  refine ⟨fun hd ↦ ?_, fun ⟨b, hb, hd'⟩ d' hd ↦ ?_⟩
  · let g' : {x // x ∈ d} → α := fun ⟨x, hx⟩ ↦ (hd x hx).choose
    refine ⟨(fun p ↦ Sym.map g' p) d.attach, ?_, ?_⟩
    · simp only [Sym.mem_map, Sym.mem_attach, true_and, Subtype.exists, forall_exists_index, g']
      intro i e he hi
      rw [← hi]
      exact (hd e he).choose_spec.1
    · simp only [Sym.map_map, Function.comp_apply, g']
      convert! Sym.attach_map_coe d with ⟨x, hx⟩ hx'
      exact (hd x hx).choose_spec.2
  · rw [← hd', Sym.mem_map] at hd
    obtain ⟨a, ha, rfl⟩ := hd
    exact ⟨a, hb a ha, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
⊢ z.toFinset ≠ ∅

Tactic:
exact Finset.ne_empty_of_mem (Sym2.mem_toFinset.mpr (Sym2.out_fst_mem _))

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
inst✝ : Epi (f ≫ g)
Z✝ : C
x✝¹ x✝ : Z ⟶ Z✝
w : g ≫ x✝¹ = g ≫ x✝
⊢ (f ≫ g) ≫ x✝¹ = (f ≫ g) ≫ x✝

Tactic:
simp only [Category.assoc, w]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other' h ∈ z

Tactic:
← other_eq_other'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ refl Y ≪≫ β = β

Tactic:
refl_trans

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : Y ≅ Z
⊢ β = β
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ refl X ≪≫ β = β

Tactic:
refl_trans

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ β = β
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
v w : V
p q : Path v w
a✝² x✝³ b✝ : V
a✝¹ : Path a✝² b✝
a✝ : b✝ ⟶ x✝³
x✝² : Path a✝² x✝³
x✝¹ x✝ : BoundedPaths a✝² x✝³ 0
hp : (a✝¹.cons a✝).length ≤ 0
hq : x✝².length ≤ 0
⊢ ⟨a✝¹.cons a✝, hp⟩ = ⟨x✝², hq⟩

Tactic:
by simp [Quiver.Path.length] at hp

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

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

Tactic:
rw [← h]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case mpr
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
⊢ (P.ι ⋙ F).essImage Y

Tactic:
exact ⟨⟨X, hX⟩, ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ G.IsEquivalence

Tactic:
rw [isEquivalence_iff_of_iso (G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G)]
  exact (F.asEquivalence.symm.trans (F ⋙ G).asEquivalence).isEquivalence_functor

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Y)

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ Arrow.mk (F.map (F.preimage ?refine_1)) ≅ Arrow.mk f

Tactic:
· exact (Functor.objObjPreimageIso F X).hom ≫ f ≫ (Functor.objObjPreimageIso F Y).inv

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ Arrow.mk (F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv))) ≅ Arrow.mk f
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left (𝟙 f) = 𝟙 f.left

Tactic:
id_left

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ 𝟙 f.left = 𝟙 f.left
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left e.hom ≫ Hom.left e.inv = 𝟙 f.left

Tactic:
rw [← comp_left, e.hom_inv_id, id_left]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left (𝟙 g) = 𝟙 g.left

Tactic:
id_left

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ 𝟙 g.left = 𝟙 g.left
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ (𝟙 X).left = 𝟙 X.left

Tactic:
id_left

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ 𝟙 X.left = 𝟙 X.left
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
A' : Type u₄
inst✝³ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝² : Category.{v₅, u₅} B'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝ : Category.{v₄, u₄} C
L : A ⥤ T
R : B ⥤ T
F : T ⥤ C
X✝ Y✝ : Comma L R
f : X✝ ⟶ Y✝
⊢ (L ⋙ F).map f.left ≫ { left := Y✝.left, right := Y✝.right, hom := F.map Y✝.hom }.hom =
    { left := X✝.left, right := X✝.right, hom := F.map X✝.hom }.hom ≫ (R ⋙ F).map f.right

Tactic:
by simp only [Functor.comp_map, ← F.map_comp, f.w]

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 : CoreHomEquiv F G
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ (G ⋙ F).map f✝ ≫ (adj.homEquiv (G.obj Y✝) ((𝟭 D).obj Y✝)).invFun (𝟙 (G.obj Y✝)) =
    (adj.homEquiv (G.obj X✝) ((𝟭 D).obj X✝)).invFun (𝟙 (G.obj X✝)) ≫ (𝟭 D).map f✝

Tactic:
simp [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by
    intro X Y f
    ext a b
    simp [yonedaEquiv, ← NatTrans.naturality_apply]

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
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
⊢ (fun s ↦ { app := fun j ↦ ↾fun x ↦ ↑s j, naturality := ⋯ })
      ((fun τ ↦ ⟨fun j ↦ (ConcreteCategory.hom (τ.app j)) default, ⋯⟩) τ) =
    τ

Tactic:
by
    ext _ (x : X)
    rw [Unique.eq_default x]
    rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f : Y ⟶ X
⊢ Epi f

Tactic:
by
  have := t.isSplitEpi_to f; infer_instance

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

Goal state before:
pp: case none
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
h₁ : s.π.app one = s.π.app left ≫ F.map inl
h₂ : t.π.app one = t.π.app left ≫ F.map inl
⊢ s.π.app none = (i.hom ≫ t.π.app left) ≫ F.map inl

Tactic:
← w₁,

Goal state after:
case none
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
h₁ : s.π.app one = s.π.app left ≫ F.map inl
h₂ : t.π.app one = t.π.app left ≫ F.map inl
⊢ s.π.app none = s.π.app left ≫ F.map inl
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁹ : Category.{w, u₂} D
E : Type u₃
inst✝⁸ : Category.{w', u₃} E
F✝ : C ⥤ D
G : D ⥤ E
A✝ A' B B' : C
inst✝⁷ : HasBinaryProduct A✝ B
inst✝⁶ : HasBinaryProduct A' B'
inst✝⁵ : HasBinaryProduct (F✝.obj A✝) (F✝.obj B)
inst✝⁴ : HasBinaryProduct (F✝.obj A') (F✝.obj B')
inst✝³ : HasBinaryProduct (G.obj (F✝.obj A✝)) (G.obj (F✝.obj B))
inst✝² : HasBinaryProduct ((F✝ ⋙ G).obj A✝) ((F✝ ⋙ G).obj B)
inst✝¹ : HasBinaryProducts C
inst✝ : HasBinaryProducts D
F : C ⥤ D
A f : C
⊢ ∀ ⦃Y : C⦄ (f_1 : f ⟶ Y),
    (prod.functor.obj A ⋙ F).map f_1 ≫ prodComparison F A Y =
      prodComparison F A f ≫ (F ⋙ prod.functor.obj (F.obj A)).map f_1

Tactic:
by simp [prodComparison_natural]

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 g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l ≫ f.hom = (mk (m ≫ f.hom)).hom

Tactic:
dsimp; rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc]

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✝
U V W : Under X
f : U.right ⟶ V.right
g : V.right ⟶ W.right
w_f : U.hom ≫ f = V.hom
w_g : V.hom ≫ g = W.hom
⊢ U.hom ≫ f ≫ g = W.hom

Tactic:
by simp only [reassoc_of% w_f, w_g]

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
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ (h ≫ y) ≫ s.inr = g ≫ s.inr

Tactic:
apply congrArg (· ≫ inr s) hhy

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasBinaryProducts D
i : ∀ {X Y : C}, IsIso (prodComparison G X Y)
K : Discrete WalkingPair ⥤ C
this : PreservesLimit (pair (K.obj { as := WalkingPair.left }) (K.obj { as := WalkingPair.right })) G
⊢ PreservesLimit K G

Tactic:
apply preservesLimit_of_iso_diagram G (diagramIsoPair K).symm

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
            (F.mapBicone b.toBicone).toCone).π.app
      j =
    (Iso.refl
          ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (F.mapBicone b.toBicone).toCone).pt).hom ≫
      (F.mapBinaryBicone b).toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).ι.app
        j ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

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

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
X Y : C
b : Bicone (pairFunction X Y)
j : Discrete WalkingPair
⊢ b.toBinaryBicone.toCone.π.app j = (Iso.refl b.toBinaryBicone.toCone.pt).hom ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

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

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
X Y : C
b : Bicone (pairFunction X Y)
j : Discrete WalkingPair
⊢ b.toBinaryBicone.toCocone.ι.app j ≫ (Iso.refl b.toBinaryBicone.toCocone.pt).hom = b.toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
j : Discrete WalkingPair
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app j = s.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
j : Discrete WalkingPair
⊢ b.toCocone.ι.app j ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) = s.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
i : b.IsBilimit
j : Discrete WalkingPair
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

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

Goal state before:
pp: case refine_1
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inl ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inl ≫ desc b.inl b.inr) ≫ b.toCone.π.app j

Tactic:
simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
    rcases j with ⟨⟨⟩⟩

Goal state after:
case refine_1.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_1.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case refine_2
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ (inr ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j =
    (inr ≫ desc b.inl b.inr) ≫ b.toCone.π.app j

Tactic:
simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
    rcases j with ⟨⟨⟩⟩

Goal state after:
case refine_2.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_2.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cocone (pair X Y)
ht : IsColimit t
j : Discrete WalkingPair
⊢ t.ι.app j ≫ (Iso.refl t.pt).hom = (BinaryBicone.ofColimitCocone ht).toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩ <;> simp

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; funext X Y; apply AddCommGroup.ext; funext f g
    have h₁ := @biprod.add_eq_lift_id_desc _ _ a _ _ f g
      (by convert! (inferInstance : HasBinaryBiproduct X X); subsingleton)
    have h₂ := @biprod.add_eq_lift_id_desc _ _ b _ _ f g
      (by convert! (inferInstance : HasBinaryBiproduct X X); subsingleton)
    refine h₁.trans (Eq.trans ?_ h₂.symm)
    congr! 2 <;> subsingleton

Goal state after: