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

Goal state before:
pp: 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 B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ a ⊗ₜ[R] ↑b ∈ ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
by
          rw [this]
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          apply Ideal.mul_mem_left
          -- Note: adding `includeRight` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeRight
          exact Submodule.coe_mem b

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

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
s : Set (M ⊗[R] N)
hs : s.Finite
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(map w✝.subtype N'.subtype).range
⊢ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range

Tactic:
← LinearMap.lTensor_comp_rTensor

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
s : Set (M ⊗[R] N)
hs : s.Finite
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.lTensor M N'.subtype ∘ₗ LinearMap.rTensor (↥N') w✝.subtype).range
⊢ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

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₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
w✝¹ : Submodule R M
N' : Submodule R N
w✝ : w✝¹ ≤ M₁
hN : N' ≤ N₁
left✝ : Module.Finite R ↥w✝¹
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(map (inclusion w✝) (inclusion hN)).range
⊢ s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN)).range

Tactic:
← LinearMap.lTensor_comp_rTensor

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₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
w✝¹ : Submodule R M
N' : Submodule R N
w✝ : w✝¹ ≤ M₁
hN : N' ≤ N₁
left✝ : Module.Finite R ↥w✝¹
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN) ∘ₗ LinearMap.rTensor (↥N') (inclusion w✝)).range
⊢ s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN)).range
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
x✝ : IsNilpotent (f r)
k : ℕ
hk : f r ^ k = 0
⊢ f (r ^ k) = 0

Tactic:
rwa [map_pow]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
s : Set ℕ := {k | x ^ k = 0}
⊢ s.Nonempty

Tactic:
change 0 < sInf s at hx

Goal state after:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
s : Set ℕ := {k | x ^ k = 0}
hx : 0 < sInf s
⊢ s.Nonempty
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : Flat R M
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
⊢ Flat R N

Tactic:
by
  rw [iff_rTensor_injectiveₛ] at *
  refine fun P _ _ Q ↦ .of_comp (f := lTensor P i) ?_
  rw [← coe_comp, lTensor_comp_rTensor, ← rTensor_comp_lTensor, coe_comp]
  refine (f Q).comp (Function.RightInverse.injective (g := lTensor Q r) fun x ↦ ?_)
  simp [← comp_apply, ← lTensor_comp, h]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst✝¹ : Module.Flat R M
inst✝ : Module.Flat R Q
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(map f g)

Tactic:
← LinearMap.lTensor_comp_rTensor

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
inst✝¹ : Module.Flat R M
inst✝ : Module.Flat R Q
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
⊢ Function.Injective ⇑(LinearMap.lTensor M g ∘ₗ LinearMap.rTensor Q f)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
e : α ≃ β
⊢ (map e.toEmbedding s).dens = s.dens

Tactic:
by
  simp [dens, Fintype.card_congr e]

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

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f g : ι → G
⊢ balance (f + g) = balance f + balance g

Tactic:
by
  simp only [balance, expect_add_distrib, ← const_add, add_sub_add_comm, Pi.add_apply]

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h✝ : ∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = (↑(#s))⁻¹ • a

Tactic:
simp [expect, sum_ite_zero _ _ h, *]

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h✝ : ¬∃ i ∈ s, p i
⊢ (𝔼 i ∈ s, if p i then a else 0) = 0

Tactic:
simp [expect, sum_ite_zero _ _ h, *]

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

Goal state before:
pp: ι : 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 : ι) → DivisionSemiring (G i)
inst✝² : DivisionSemiring C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ≥0
i : ι
⊢ (g ⟨?i, ↑q⟩.fst) ⟨?i, ↑q⟩.snd = ↑q

pp: case i
ι : 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 : ι) → DivisionSemiring (G i)
inst✝² : DivisionSemiring C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ≥0
i : ι
⊢ ι

Tactic:
map_nnratCast (g i)

Goal state after:
ι : 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 : ι) → DivisionSemiring (G i)
inst✝² : DivisionSemiring C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ≥0
i : ι
⊢ ↑q = ↑q
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : Semiring M
inst✝¹ : Module ℚ≥0 M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
⊢ a * (↑(#s))⁻¹ • ∑ i ∈ s, f i = (↑(#s))⁻¹ • ∑ i ∈ s, a * f i

Tactic:
mul_smul_comm,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : Semiring M
inst✝¹ : Module ℚ≥0 M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
⊢ (↑(#s))⁻¹ • (a * ∑ i ∈ s, f i) = (↑(#s))⁻¹ • ∑ i ∈ s, a * f i
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
have hk : k - 1 + 1 = k := by omega

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
by
  simp only [List.sym2, map_cons, cons_append, mem_cons, mem_append, mem_map]
  simp only [eq_comm]

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

Goal state before:
pp: case cons
α : Type u_1
x : α
xs : List α
ih : xs.sym2.length = (xs.length + 1).choose 2
⊢ (x :: xs).sym2.length = ((x :: xs).length + 1).choose 2

Tactic:
rw [List.sym2, length_append, length_map, length_cons,
        Nat.choose_succ_succ, ← ih, Nat.choose_one_right]

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

Goal state before:
pp: α : Type u_1
⊢ ∅.sym2 = ∅

Tactic:
by ext ⟨x, y⟩; simp

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

Goal state before:
pp: α : Type u_1
⊢ univ.sym2 = univ

Tactic:
by ext ⟨x, y⟩; simp

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.sym2 = {s(a, a)}

Tactic:
by ext ⟨x, y⟩; simp

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P Q : ObjectProperty C
h : P ≤ Q
F : C ⥤ D
⊢ P.map F ≤ Q.map F

Tactic:
by
  rintro X ⟨Y, hY, ⟨e⟩⟩
  exact ⟨Y, h _ hY, ⟨e⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ (α ≫ h).app X = α.app X ≫ h.app X

Tactic:
comp_app

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ α.app X ≫ h.app X = α.app X ≫ h.app X
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ IsIso f

Tactic:
simpa using (hF.preimageIso (asIso (F.map f))).isIso_hom

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ (G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ (G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯ ≫ eqToHom ⋯
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 (e.unit.app (e.inverse.obj Y))) ≫
    e.inverse.map (e.counitIso.inv.app (e.functor.obj (e.inverse.obj (e.functor.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.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (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.inverse.map (e.functor.map (e.unitInv.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.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)

Tactic:
rw [← map_comp e.inverse, ← e.counitInv_naturality, map_comp]

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.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.inverse.map (e.functor.map (e.unit.app (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.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (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.inverse.map (e.functor.map (e.unitInv.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.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)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
l : f.right ≅ g.right
r : f.left ≅ g.left
h : g.hom = (r.inv ≫ f.hom) ≫ l.hom
⊢ r.hom ≫ g.hom = f.hom ≫ l.hom

Tactic:
Category.assoc,

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
l : f.right ≅ g.right
r : f.left ≅ g.left
h : g.hom = r.inv ≫ f.hom ≫ l.hom
⊢ r.hom ≫ g.hom = f.hom ≫ l.hom
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
W X Y Z : T
f : X ⟶ W
g : Z ⟶ Y
e₁ : W ≅ Y
e₂ : X ≅ Z
h : g = (e₂.inv ≫ f) ≫ e₁.hom
⊢ e₂.hom ≫ g = f ≫ e₁.hom

Tactic:
Category.assoc,

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
W X Y Z : T
f : X ⟶ W
g : Z ⟶ Y
e₁ : W ≅ Y
e₂ : X ≅ Z
h : g = e₂.inv ≫ f ≫ e₁.hom
⊢ e₂.hom ≫ g = f ≫ e₁.hom
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
⊢ i = (g.inv ≫ f) ≫ h.hom

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
⊢ i = g.inv ≫ f ≫ h.hom
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
⊢ (f ≫ f') ≫ h' = (g ≫ i) ≫ i'

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
⊢ f ≫ f' ≫ h' = (g ≫ i) ≫ i'
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
hi : Q x✝¹
x✝ : Y✝ ⟶ Z✝
hf : ∀ W_1 ∈ W, W_1 x✝
⊢ ∀ W_1 ∈ W, W_1 (x✝¹ ≫ x✝)

Tactic:
exact fun _ hW' ↦ (h _ hW').precomp _ hi _ (hf _ hW')

Goal state after:
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ X.hom = (X.hom ≫ R₁.map r.hom) ≫ R₁.map r.inv

Tactic:
Category.assoc,

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
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ X.hom = X.hom ≫ R₁.map r.hom ≫ R₁.map r.inv
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ α.inv ≫ (f ≫ β.hom) ≫ β.inv = f
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ α.inv ≫ (f ≫ β.hom) ≫ β.inv = f

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ α.inv ≫ f ≫ β.hom ≫ β.inv = f
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ α.inv ≫ α.hom ≫ (f ≫ β.inv) ≫ β.hom = f
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ α.inv ≫ α.hom ≫ (f ≫ β.inv) ≫ β.hom = f

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X₁ ⟶ Y₁
⊢ α.inv ≫ α.hom ≫ f ≫ β.inv ≫ β.hom = f
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h s) = s

Tactic:
← coconeOfHom_homOfCocone h s

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h (coconeOfHom h (homOfCocone h s))) = coconeOfHom h (homOfCocone h s)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type v₁
g : ((coyoneda.rightOp ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((coyoneda.rightOp ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                  (evaluation C (Type v₁) ⋙
                        (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                    f).app
              F)).toFun
        g).down

Tactic:
simpa using (coyonedaEquiv_naturality _ _).symm

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst✝ : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
⊢ (u ≫ Arrow.Hom.left h.i) ≫ f = u ≫ f' ≫ Arrow.Hom.right h.i

Tactic:
Category.assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst✝ : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
⊢ u ≫ Arrow.Hom.left h.i ≫ f = u ≫ f' ≫ Arrow.Hom.right h.i
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : (c.inl ≫ l) ≫ c.inl = 𝟙 X ≫ c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl

Tactic:
Category.assoc,

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : c.inl ≫ l ≫ c.inl = 𝟙 X ≫ c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

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

Tactic:
Category.assoc,

Goal state after:
case none
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
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero
⊢ F.map fst ≫ s.ι.app left ≫ i.hom = t.ι.app none