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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
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✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
ext x

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
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✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
x : DirectLimit G f
⊢ g₁ x = g₂ x
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding a)) (range (b + 1 - a).toNat) ↔ a ≤ x ∧ x ≤ b

Tactic:
by
    simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]
    constructor
    · lia
    · intro
      use (x - a).toNat
      lia

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

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding a)) (range (b - a).toNat) ↔ a ≤ x ∧ x < b

Tactic:
by
    simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]
    constructor
    · lia
    · intro
      use (x - a).toNat
      lia

Goal state after:
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
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
⊢ g₁ = g₂

Tactic:
ext x

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
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ g₁ x = g₂ x
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
⊢ s = t

Tactic:
ext x

Goal state after:
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
x : α
⊢ x ∈ s ↔ x ∈ t
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case inj
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
⊢ Function.Injective fun y ↦ s(x, y)

Tactic:
case inj =>
      intro a b
      simp only [Sym2.eq_iff, true_and]
      rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map (fun p ↦ f x ::ₛ p) (List.sym n (map f (x :: xs))) ++ List.sym (n + 1) (map f xs) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))

Tactic:
sym_map f n (x :: xs),

Goal state after:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map (fun p ↦ f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))) ++ List.sym (n + 1) (map f xs) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ ↑R (↑ULift.moduleEquiv.symm ∘ₗ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g) ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ f

Tactic:
ext x

Goal state after:
case refine_1
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
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := ⋯
f'' : S ⊗[R] M →ₗ[S] N := ⋯
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
x : M
⊢ ((↑R (↑ULift.moduleEquiv.symm ∘ₗ f'' ∘ₗ ↑ULift.moduleEquiv ∘ₗ g) ∘ₗ f) x).down =
    ((↑ULift.moduleEquiv.symm ∘ₗ f) x).down
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
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
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ (↑ULift.moduleEquiv ∘ₗ g) ∘ₗ f'' = LinearMap.id

Tactic:
ext x

Goal state after:
case refine_2
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
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
x : M
⊢ ((AlgebraTensorModule.curry ((↑ULift.moduleEquiv ∘ₗ g) ∘ₗ f'')) 1) x = ((AlgebraTensorModule.curry LinearMap.id) 1) x
Module: Mathlib.Algebra.BigOperators.WithTop

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

Tactic:
simp only [WithBot.bot_lt_iff_ne_bot, ne_eq, sum_eq_bot_iff, not_exists, not_and]

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

Goal state before:
pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)

pp: case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨y, hy⟩)

Tactic:
· exfalso
          simp at hx

Goal state after:
case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨y, hy⟩)
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
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y : N
⊢ ∀ (x_1 : S) (y : M),
    (IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x))
        (((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) x_1) y) =
      (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x)))
        (((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) x_1) y)

Tactic:
intro s m

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
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y : N
s : S
m : M
⊢ (IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x))
      (((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) s) m) =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x)))
      (((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) s) m)
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:
rw [← other_eq_other']
  exact other_mem h

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ f x = g x
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
⊢ ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
x : R'
⊢ (↑R (toAlgHom S S' T').toLinearMap ∘ₗ f) x = (toAlgHom R R' T').toLinearMap x
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
h : α = β
X : C
⊢ α.app X = β.app X

Tactic:
by rw [h]

Goal state after:
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
inst✝ : F.Faithful
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
by rw [h]

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
H I : D ⥤ E
α : G ⟶ F
β : I ⟶ H
⊢ { app := fun X ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ } =
    mk' (fun X ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯

Tactic:
ext x

Goal state after:
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 G : C ⥤ D
H I : D ⥤ E
α : G ⟶ F
β : I ⟶ H
x : C
⊢ { app := fun X ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ }.app x =
    (mk' (fun X ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯).app x
Module: Mathlib.Tactic.CategoryTheory.Elementwise

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
x✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f g : X ⟶ Y
h : f = g
x : CC X
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Tactic:
by rw [h]

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

Goal state before:
pp: case refine_1.nil
V : Type u_1
inst✝ : Quiver V
a : V
h : nil.length ≠ 0
⊢ ∃ c p' e, nil = p'.cons e

Tactic:
simp at h

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

Goal state before:
pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c p' e, p = p'.cons e) → p.length ≠ 0

Tactic:
· rintro ⟨c, p', e, rfl⟩
    simp

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

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

Tactic:
rintro X ⟨X', hX', ⟨e⟩⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
X X' : C
hX' : P X'
e : X ≅ X'
⊢ Q.isoClosure X
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
h : F = G
X : C
⊢ F.obj X = G.obj X

Tactic:
by rw [h]

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X Y : I
g x✝ : { as := X }.as = { as := Y }.as
⊢ F.map { down := { down := g } } ≫ f { as := Y } = f { as := X } ≫ G.map { down := { down := g } }

Tactic:
rcases g

Goal state after:
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X : I
x✝ : { as := X }.as = { as := X }.as
⊢ F.map { down := { down := ⋯ } } ≫ f { as := X } = f { as := X } ≫ G.map { down := { down := ⋯ } }
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X✝ Y✝ : I
g x✝ : { as := X✝ }.as = { as := Y✝ }.as
⊢ F.map { down := { down := g } } ≫ (f { as := Y✝ }).hom = (f { as := X✝ }).hom ≫ G.map { down := { down := g } }

Tactic:
rcases g

Goal state after:
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X✝ : I
x✝ : { as := X✝ }.as = { as := X✝ }.as
⊢ F.map { down := { down := ⋯ } } ≫ (f { as := X✝ }).hom = (f { as := X✝ }).hom ≫ G.map { down := { down := ⋯ } }
Module: Mathlib.CategoryTheory.Comma.Arrow

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

Tactic:
by
  simp [← Arrow.comp_right]

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ X.left = Y.left

Tactic:
by rw [h]

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ X.right = Y.right

Tactic:
by rw [h]

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

Goal state before:
pp: case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
h : mk f = mk f'
⊢ f = eqToHom ⋯ ≫ f' ≫ eqToHom ⋯

Tactic:
simpa [eqToHom_left, eqToHom_right] using! iso_w (eqToIso h.symm)

Goal state after:
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✝¹ : IsIso sq
inst✝ : IsIso f.hom
⊢ IsIso g.hom

Tactic:
rw [iso_w (asIso sq)]

Goal state after:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝¹ : IsIso sq
inst✝ : IsIso f.hom
⊢ IsIso (Hom.left (asIso sq).inv ≫ f.hom ≫ Hom.right (asIso sq).hom)
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
⊢ ⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm

Tactic:
ext x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
x : (fun X ↦ X) (G.obj j)
⊢ (⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f))) x = (⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm) x
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾_root_.Functor.map ⇑(Hom.hom (f ≫ g)) = ↾_root_.Functor.map ⇑(Hom.hom f) ≫ ↾_root_.Functor.map ⇑(Hom.hom g)

Tactic:
ext x

Goal state after:
m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : m X✝
⊢ (ConcreteCategory.hom (↾_root_.Functor.map ⇑(Hom.hom (f ≫ g)))).toFun x =
    (ConcreteCategory.hom (↾_root_.Functor.map ⇑(Hom.hom f) ≫ ↾_root_.Functor.map ⇑(Hom.hom g))).toFun x
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X✝ Y✝ : Type u
f : X✝ ⟶ Y✝
hf : Epi f
⊢ ↾Function.surjInv ⋯ ≫ f = 𝟙 Y✝

Tactic:
ext x

Goal state after:
X✝ Y✝ : Type u
f : X✝ ⟶ Y✝
hf : Epi f
x : Y✝
⊢ (ConcreteCategory.hom (↾Function.surjInv ⋯ ≫ f)).toFun x = (ConcreteCategory.hom (𝟙 Y✝)).toFun x
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 : F ⊣ G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)

Tactic:
simp only [homEquiv_naturality_right, Equiv.apply_symm_apply]

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

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ x ≤ y

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X✝ : C
R : F.RepresentableBy X✝
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (uliftYoneda.{w, v₁, u₁}.obj X✝).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
    (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
ext x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X✝ : C
R : F.RepresentableBy X✝
X Y : Cᵒᵖ
f : X ⟶ Y
x : (uliftYoneda.{w, v₁, u₁}.obj X✝).obj X
⊢ (ConcreteCategory.hom
          ((uliftYoneda.{w, v₁, u₁}.obj X✝).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom)).toFun
      x =
    (ConcreteCategory.hom ((equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f)).toFun x
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X✝ : C
R : F.CorepresentableBy X✝
X Y : C
f : X ⟶ Y
⊢ (uliftCoyoneda.{w, v₁, u₁}.obj (op X✝)).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
    (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
ext x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X✝ : C
R : F.CorepresentableBy X✝
X Y : C
f : X ⟶ Y
x : (uliftCoyoneda.{w, v₁, u₁}.obj (op X✝)).obj X
⊢ (ConcreteCategory.hom
          ((uliftCoyoneda.{w, v₁, u₁}.obj (op X✝)).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom)).toFun
      x =
    (ConcreteCategory.hom ((equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f)).toFun x
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: C : Cat
⊢ ↾Quot.map (𝟙 C).toFunctor.obj ⋯ = 𝟙 (Quotient (isIsomorphicSetoid ↑C))

Tactic:
ext x

Goal state after:
C : Cat
x : Quotient (isIsomorphicSetoid ↑C)
⊢ (ConcreteCategory.hom (↾Quot.map (𝟙 C).toFunctor.obj ⋯)).toFun x =
    (ConcreteCategory.hom (𝟙 (Quotient (isIsomorphicSetoid ↑C)))).toFun x
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: C D E : Cat
f : C ⟶ D
g : D ⟶ E
⊢ ↾Quot.map (f ≫ g).toFunctor.obj ⋯ = ↾Quot.map f.toFunctor.obj ⋯ ≫ ↾Quot.map g.toFunctor.obj ⋯

Tactic:
ext x

Goal state after:
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quotient (isIsomorphicSetoid ↑C)
⊢ (ConcreteCategory.hom (↾Quot.map (f ≫ g).toFunctor.obj ⋯)).toFun x =
    (ConcreteCategory.hom (↾Quot.map f.toFunctor.obj ⋯ ≫ ↾Quot.map g.toFunctor.obj ⋯)).toFun x
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: _X _Y : Type u
_f _g : _X ⟶ _Y
h : typeToCat.map _f = typeToCat.map _g
⊢ _f = _g

Tactic:
ext x

Goal state after:
_X _Y : Type u
_f _g : _X ⟶ _Y
h : typeToCat.map _f = typeToCat.map _g
x : _X
⊢ (ConcreteCategory.hom _f).toFun x = (ConcreteCategory.hom _g).toFun x