mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : DirectLimit F₁ f₁
w : DirectLimit F₂ f₂
x✝⁵ : (i : ι) × F₁ i
x✝⁴ : (i : ι) × F₂ i
x✝³ : (i : ι) × F₁ i
x✝² : (i : ι) × F₂ i
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
j : ι
hx : x✝⁵.fst ≤ j
hyj : x✝³.fst ≤ j
jeq : (f₁ x✝⁵.fst j hx) x✝⁵.snd = (f₁ x✝³.fst j hyj) x✝³.snd
k : ι
hyk : x✝⁴.fst ≤ k
hz : x✝².fst ≤ k
keq : (f₂ x✝⁴.fst k hyk) x✝⁴.snd = (f₂ x✝².fst k hz) x✝².snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) ((f₁ x✝³.fst j hyj) x✝³.snd)) ((f₂ x✝⁴.fst i ⋯) x✝⁴.snd) =
    ih i ((f₁ x✝³.fst i ⋯) x✝³.snd) ((f₂ k i hki) ((f₂ x✝².fst k hz) x✝².snd))

Tactic:
← keq,

Goal state after:
ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : DirectLimit F₁ f₁
w : DirectLimit F₂ f₂
x✝⁵ : (i : ι) × F₁ i
x✝⁴ : (i : ι) × F₂ i
x✝³ : (i : ι) × F₁ i
x✝² : (i : ι) × F₂ i
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
j : ι
hx : x✝⁵.fst ≤ j
hyj : x✝³.fst ≤ j
jeq : (f₁ x✝⁵.fst j hx) x✝⁵.snd = (f₁ x✝³.fst j hyj) x✝³.snd
k : ι
hyk : x✝⁴.fst ≤ k
hz : x✝².fst ≤ k
keq : (f₂ x✝⁴.fst k hyk) x✝⁴.snd = (f₂ x✝².fst k hz) x✝².snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) ((f₁ x✝³.fst j hyj) x✝³.snd)) ((f₂ x✝⁴.fst i ⋯) x✝⁴.snd) =
    ih i ((f₁ x✝³.fst i ⋯) x✝³.snd) ((f₂ k i hki) ((f₂ x✝⁴.fst k hyk) x✝⁴.snd))
Module: Mathlib.Algebra.Colimit.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M (Module.DirectLimit.of R { N // N.FG } (fun i ↦ ↥↑i) (Module.fgSystem R P) N)) x) =
    (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M (Module.DirectLimit.of R { N // N.FG } (fun i ↦ ↥↑i) (Module.fgSystem R P) N)) y)
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
directLimitLeft_rTensor_of

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (Module.DirectLimit.of R { N // N.FG } (fun i ↦ ↥↑i ⊗[R] M)
        (fun i j h ↦ LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      x =
    (Module.DirectLimit.of R { N // N.FG } (fun i ↦ ↥↑i ⊗[R] M)
        (fun i j h ↦ LinearMap.rTensor M (Module.fgSystem R P i j h)) N)
      y
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y
Module: Mathlib.RingTheory.Finiteness.Small

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

Tactic:
rw [this]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ Exact ⇑(rTensor Q f) ⇑(rTensor Q g)

Tactic:
rTensor_exact_iff_lTensor_exact

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ Exact ⇑(lTensor Q f) ⇑(lTensor Q g)
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 A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ ↑a ⊗ₜ[R] b ∈ map includeLeft I

Tactic:
rw [this]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1 ∈ map includeLeft I
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:
rw [this]

Goal state after:
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] 1 * 1 ⊗ₜ[R] ↑b ∈ ↑(Submodule.restrictScalars R (map includeRight I))
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ RingHom.ker (map f g) = Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.map includeRight (RingHom.ker g)

Tactic:
rw [this]

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ RingHom.ker ((map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)) =
    Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.map includeRight (RingHom.ker g)
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ f x = 0

Tactic:
exact (hx.map f).eq_zero

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R M
this : ⇑((TensorProduct.mk R S M) 1) = ⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm
⊢ Injective ⇑((TensorProduct.mk R S M) 1)

Tactic:
rw [this]

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R M
this : ⇑((TensorProduct.mk R S M) 1) = ⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm
⊢ Injective (⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Set.InjOn (insert a) ↑s.powerset

Tactic:
exact insert_erase_invOn.2.injOn.mono fun t ht ↦ notMem_mono (mem_powerset.1 ht) ha

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
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
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
hF : ∀ (s : S) (m : M), (IsTensorProduct.lift h F) (s • f m) = s • g m
x₁ x₂ : N
e₁ : (IsTensorProduct.lift h F) (r • x₁) = r • (IsTensorProduct.lift h F) x₁
e₂ : (IsTensorProduct.lift h F) (r • x₂) = r • (IsTensorProduct.lift h F) x₂
⊢ (IsTensorProduct.lift h F) (r • (x₁ + x₂)) = r • (IsTensorProduct.lift h F) (x₁ + x₂)

Tactic:
rw [map_add, smul_add, map_add, smul_add, e₁, e₂]

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

Goal state before:
pp: α : Type u_1
s : Finset α
a b : α
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s

Tactic:
by
  rw [mem_mk, sym2_val, Multiset.mk_mem_sym2_iff, mem_mk, mem_mk]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ univ.sym2

Tactic:
by rw [mem_sym2_iff]; exact (fun a _ ↦ mem_univ a)

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

Goal state before:
pp: case succ.refine_1
α : 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)
⊢ (∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)) → ∀ a ∈ m, a ∈ s

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

Tactic:
· rintro ⟨a, ha, he⟩ b hb
    rw [mem_image] at he
    obtain ⟨m, he, rfl⟩ := he
    rw [Sym.mem_cons] at hb
    obtain rfl | hb := hb
    · exact ha
    · exact ih.1 he _ hb

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

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
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
⊢ IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x) = ↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))

Tactic:
ext y
  refine IsTensorProduct.inductionOn hf y (by simp) ?_ (fun _ _ ha hb ↦ by simp [ha, hb])
  intro s m
  rw [hf.map_eq hf]
  simpa using smul_comm x s (f m)

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 : ObjectProperty C
F : C ⥤ D
X : C
hX : P X
⊢ ∃ X_1, P X_1 ∧ F.obj X_1 = F.obj X

Tactic:
exact ⟨X, hX, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.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.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.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.unitInv.app (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.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)

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.functor.map (e.unit.app (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.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))

Tactic:
← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)

Goal state after:
case a.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.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).hom ≫
    (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
      e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.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.unitInv.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.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)

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

Goal state before:
pp: case mk.mk.mk
α : Type u₁
as✝¹ as✝ : α
g : ULift.{u₁, 0} (PLift ({ as := as✝¹ }.as = { as := as✝ }.as))
⊢ ULift.{u₁, 0} (PLift ({ as := as✝¹ }.as = { as := as✝ }.as))

Tactic:
exact g

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
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) =
    𝟙 (F.obj X)

Tactic:
rw [this]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

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
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)

Tactic:
rw [this]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

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
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
rw [this]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

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
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
rw [this]

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✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ F.IsEquivalence

Tactic:
by
  rw [isEquivalence_iff_of_iso (F.rightUnitor.symm ≪≫ isoWhiskerLeft F (G.asEquivalence.unitIso))]
  exact ((F ⋙ G).asEquivalence.trans G.asEquivalence.symm).isEquivalence_functor

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : coyoneda.obj X ⟶ coyoneda.obj Y),
    coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop X))) (𝟙 (unop X)))) = f

Tactic:
intro Z W f
    ext X x
    have := f.naturality_apply x (𝟙 (unop Z))
    cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton D
⊢ (map R ⋙ map L).obj X ⟶ (𝟭 (ThinSkeleton D)).obj X

Tactic:
letI := isIsomorphicSetoid D
        exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩

Goal state after:
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:
by
    ext x
    exact congrArg Discrete.as (Functor.congr_obj congr(($h).toFunctor) ⟨x⟩)

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

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 : C ⥤ D
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
x✝ : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map (h ≫ f) = F.map h ≫ F.map f

Tactic:
F.map_comp

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 : C ⥤ D
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
x✝ : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map h ≫ F.map f = F.map h ≫ F.map f
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ IsSplitEpi (F.map f) ↔ IsSplitEpi f

Tactic:
constructor
  · intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)
  · intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

Tactic:
refine ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro ?_⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
⊢ Unique (x ⟶ y)
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
inst✝¹ : HasColimit F
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ colimit.ι F j ≫ (isoOfEquivalence e w).hom =
    F.map (e.unit.app j) ≫
      w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫ colimit.ι G (e.functor.obj ((e.functor ⋙ e.inverse).obj j))

Tactic:
by
  simp [HasColimit.isoOfEquivalence]

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

Goal state before:
pp: case id
J : Type w
X✝ Z✝ : WidePullbackShape J
g : X✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
exact g

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

Goal state before:
pp: case id
J : Type w
X✝ Z✝ : WidePushoutShape J
g : X✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
exact g

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ m = (P.lift s.unop).op

Tactic:
dsimp
    rw [← P.uniq s.unop m.unop]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ m = (P.desc s.unop).op

Tactic:
dsimp
    rw [← P.uniq s.unop m.unop]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
i : ι
⊢ s.π i ≫ f i = s.base

Tactic:
by
  simpa using! ((Cone.π s).naturality (.term i)).symm

Goal state after: