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✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x✝ : M ⊗[R] N'
hx : (lTensor M L) x✝ = 0
x : N'
⊢ L x = 0 ↔ x ∈ Set.range ⇑0

Tactic:
Set.mem_range,

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x✝ : M ⊗[R] N'
hx : (lTensor M L) x✝ = 0
x : N'
⊢ L x = 0 ↔ ∃ y, 0 y = x
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✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ x ∈ Set.range ⇑0

Tactic:
Set.mem_range,

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ ∃ y, 0 y = x
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:
simp [dens, Fintype.card_congr e]

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

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
s : Finset α
⊢ ↑(Fintype.card α) * s.dens = ↑(#s)

Tactic:
by
  cases isEmpty_or_nonempty α
  · simp [Subsingleton.elim s ∅]
  rw [dens, mul_div_cancel₀]
  exact mod_cast Fintype.card_ne_zero

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s \ t).dens + (s ∩ t).dens = s.dens

Tactic:
← dens_union_of_disjoint (disjoint_sdiff_inter _ _),

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s \ t ∪ s ∩ t).dens = s.dens
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 : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (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)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧) =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ / DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧

Tactic:
div₀_def,

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 : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (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)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x / y⟩⟧ =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ / DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧
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 : ι) → Mul (G i)
inst✝³ : (i : ι) → SMul R (G i)
inst✝² : ∀ (i : ι), IsScalarTower R (G i) (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝¹ x✝ : G i
⊢ (r • ⟦⟨i, x✝¹⟩⟧) • ⟦⟨i, x✝⟩⟧ = r • ⟦⟨i, x✝¹⟩⟧ • ⟦⟨i, x✝⟩⟧

Tactic:
by
    simp_rw [smul_eq_mul, smul_def, mul_def, smul_def, smul_mul_assoc]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
G : Type u_6
inst✝¹ : DistribSMul G M
inst✝ : SMulCommClass G ℚ≥0 M
a : G
s : Finset ι
f : ι → M
⊢ a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i

Tactic:
simp only [expect, smul_sum, smul_comm]

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
M' : Type u_5
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M
inst✝ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
f' : M₁ →ₗ[R] M₂ →ₗ[R] M'
x₁ : M₁
x₂ : M₂
⊢ (h.lift f') ((f x₁) x₂) = (f' x₁) x₂

Tactic:
by
  simp [lift]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ a * (n / a) ≤ n % a + a * (n / a)

Tactic:
simp only [le_add_iff_nonneg_left]

Goal state after:
case inr.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ 0 ≤ n % a
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
M' : Type u_5
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M
inst✝ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
ist : Function.Bijective ⇑(TensorProduct.lift f)
e : M ≃ₗ[R] M'
⊢ Function.Bijective ⇑(TensorProduct.lift (f.compr₂ ↑e))

Tactic:
rw [TensorProduct.lift_compr₂]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M
inst✝ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
ist : Function.Bijective ⇑(TensorProduct.lift f)
e : M ≃ₗ[R] M'
⊢ Function.Bijective ⇑(↑e ∘ₗ TensorProduct.lift f)
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
N₁ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₁
inst✝ : Module R N₂
ist : IsTensorProduct f
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ IsTensorProduct ((f ∘ₗ ↑e₁).compl₂ ↑e₂)

Tactic:
simp only [IsTensorProduct] at ist ⊢
  rw [← TensorProduct.lift_comp_map, ← LinearMap.rTensor_comp_lTensor]
  exact ist.comp ((e₁.rTensor M₂).bijective.comp (e₂.lTensor N₁).bijective)

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

Goal state before:
pp: α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, y) :: s(y, x) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
enter [

Goal state after:
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, y) :: s(y, x) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ xs.sym2))
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).prod = ∏ d ∈ s, d ^ Multiset.count d ↑k

Tactic:
rw [Finset.prod_multiset_count_of_subset _ s]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ ∏ i ∈ s, i ^ Multiset.count i ↑k = ∏ d ∈ s, d ^ Multiset.count d ↑k

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).toFinset ⊆ s
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
obtain hab | hba := le_total a b <;> obtain hcd | hdc := le_total c d <;>
    aesop (add unsafe le_antisymm)

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

Goal state before:
pp: case inj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Function.Injective fun p ↦ x ::ₛ p

pp: case disj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)

Tactic:
case inj =>
      intro z z'
      simp

Goal state after:
case disj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a b c : α
⊢ s(a, b) = s(a, c) ↔ b = c

Tactic:
by
  simp +contextual

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

Goal state before:
pp: α : Type u_1
a b c : α
⊢ s(b, a) = s(c, a) ↔ b = c

Tactic:
by
  simp +contextual

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

Goal state before:
pp: case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(b, a)

Tactic:
rw [eq_swap]

Goal state after:
case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(a, b)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
⊢ ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = i

Tactic:
let := Module.compHom Q (algebraMap S T)

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
this : Module S Q := Module.compHom Q (algebraMap S T)
⊢ ∃! g', ↑R g' ∘ₗ ↑R g ∘ₗ f = i
Module: Mathlib.Data.Sym.Sym2

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

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

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
X : C
F : C ⥤ D
⊢ (singleton X).strictMap F = singleton (F.obj X)

Tactic:
ext
  simp [strictMap_iff]

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
t : V
C : Path a t
D : t ⟶ x✝
h : (p.cons f).toList = (C.cons D).toList
⊢ p.cons f = C.cons D

Tactic:
simp only [toList, List.cons.injEq] at h

Goal state after:
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
t : V
C : Path a t
D : t ⟶ x✝
h : c = t ∧ p.toList = C.toList
⊢ p.cons f = C.cons D
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ F.mapPath (p.comp (q.cons e)) = (F.mapPath p).comp (F.mapPath (q.cons e))

Tactic:
dsimp; rw [mapPath_comp p q]

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

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X : I
⊢ ∀ (Y : Discrete I) (f : { as := X } ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
⟨Y⟩

Goal state after:
case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
⊢ ∀ (f : { as := X } ⟶ { as := Y }), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
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₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)

Tactic:
dsimp [funInvIdAssoc]
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ofHoms P.homFamily = P

Tactic:
by
  ext _ _ f
  constructor
  · intro hf
    rw [ofHoms_iff] at hf
    obtain ⟨⟨f, hf⟩, ⟨_, _⟩⟩ := hf
    exact hf
  · intro hf
    exact ⟨(⟨f, hf⟩ : P.toSet)⟩

Goal state after:
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 : InfSet.sInf W x✝
⊢ InfSet.sInf W (x✝¹ ≫ x✝)

Tactic:
sInf_iff

Goal state after:
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✝)
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'.RespectsRight Q
X✝ Y✝ Z✝ : C
x✝¹ : Y✝ ⟶ Z✝
hi : Q x✝¹
x✝ : X✝ ⟶ Y✝
hf : InfSet.sInf W x✝
⊢ InfSet.sInf W (x✝ ≫ x✝¹)

Tactic:
sInf_iff

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsRight Q
X✝ Y✝ Z✝ : C
x✝¹ : Y✝ ⟶ Z✝
hi : Q x✝¹
x✝ : X✝ ⟶ Y✝
hf : ∀ W_1 ∈ W, W_1 x✝
⊢ ∀ W_1 ∈ W, W_1 (x✝ ≫ x✝¹)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
⊢ φ = ψ

Tactic:
by
    let aux : (Z ⟶ f.left) → (Arrow.mk (𝟙 Z) ⟶ f) := fun φ =>
      { left := φ
        right := φ ≫ f.hom }
    have : ∀ g, (aux g).right = g ≫ f.hom := fun g => rfl
    change (aux φ).left = (aux ψ).left
    congr 1
    rw [← cancel_mono sq]
    ext
    · exact h
    · simp [this, ← Arrow.w_mk_right, reassoc_of% h]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
P : MorphismProperty C
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.map F).inverseImage F = P

Tactic:
((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)),

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
P : MorphismProperty C
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.map F).map F.asEquivalence.inverse = P
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget CommSemiRingCat).map f)

Goal state after:
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (ConcreteCategory.hom (e'.hom.app (op X))) ((ConcreteCategory.hom (F.map f.op)) (e.homEquiv g)) =
    (ConcreteCategory.hom (F'.map f.op)) ((ConcreteCategory.hom (e'.hom.app (op X'))) (e.homEquiv g))

Tactic:
apply e'.hom.naturality_apply

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : C ⥤ Type v
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
⊢ (ConcreteCategory.hom (e'.hom.app Y')) ((ConcreteCategory.hom (F.map g)) (e.homEquiv f)) =
    (ConcreteCategory.hom (F'.map g)) ((ConcreteCategory.hom (e'.hom.app Y)) (e.homEquiv f))

Tactic:
apply e'.hom.naturality_apply

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

Goal state before:
pp: B C : Cat
F : B ⟶ C
⊢ toNatIso (ρ_ F) = eqToIso ⋯ ≪≫ F.toFunctor.rightUnitor ≪≫ eqToIso ⋯

Tactic:
simp; rfl

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

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
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ (unop X).unop.ι.app j ≫ f.unop.hom.unop = (unop Y).unop.ι.app j

Tactic:
by
            apply Quiver.Hom.op_inj
            dsimp
            apply ConeMorphism.w

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ ∀ ⦃X_1 Y : J⦄ (f : X_1 ⟶ Y),
    F.map f ≫ inv (F.map (hX.to Y)) = inv (F.map (hX.to X_1)) ≫ ((Functor.const J).obj (F.obj X)).map f

Tactic:
intro i j f
        dsimp
        simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.comp_id, ← F.map_comp,
          hX.hom_ext (hX.to i ≫ f) (hX.to j)]

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ (ι (F ⋙ G) j✝ ≫ post F G) ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)

Tactic:
colimit.ι_post,

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (ι F j✝) ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ (ι ((F ⋙ G) ⋙ H) j ≫ post (F ⋙ G) H) ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Tactic:
colimit.ι_post,

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ H.map (ι (F ⋙ G) j) ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
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
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ (ι ((E ⋙ F) ⋙ G) j ≫ post (E ⋙ F) G) ≫ G.map (pre F E) = ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E ≫ post F G

Tactic:
colimit.ι_post,

Goal state after:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ G.map (ι (E ⋙ F) j) ≫ G.map (pre F E) = ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E ≫ post F G
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
e : K ≌ J
inst✝ : HasColimit (e.functor ⋙ F)
⊢ HasColimit F

Tactic:
have : HasColimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasColimit_equivalence_comp e.symm
  apply hasColimit_of_iso (e.invFunIdAssoc F).symm

Goal state after: