mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ N', ∃ (hN : N' ≤ N₁), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN)).range

Tactic:
refine ⟨N', hN, hfin, ?_⟩

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 ⊆ ↑(map (inclusion w✝) (inclusion hN)).range
⊢ s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN)).range
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx' : nilpotencyClass x = 0
hx : x ^ 0 = 0
⊢ False

Tactic:
pow_zero

Goal state after:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx' : nilpotencyClass x = 0
hx : 1 = 0
⊢ False
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
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R N
⊢ Injective ⇑(baseChangeHom R S M N)

Tactic:
intro f

Goal state after:
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
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R N
f : M →ₗ[R] N
⊢ ∀ ⦃a₂ : M →ₗ[R] N⦄, (baseChangeHom R S M N) f = (baseChangeHom R S M N) a₂ → f = a₂
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → Mul (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarMul (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, star (x✝¹ * x✝)⟩⟧ = ⟦⟨i, star x✝⟩⟧ * ⟦⟨i, star x✝¹⟩⟧

Tactic:
star_mul,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → Mul (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarMul (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, star x✝ * star x✝¹⟩⟧ = ⟦⟨i, star x✝⟩⟧ * ⟦⟨i, star x✝¹⟩⟧
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : ι → κ
hi : ∀ a ∈ s, i a ∈ t
h : ∀ a ∈ s, f a = g (i a)
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
⊢ (↑(#t))⁻¹ • ∑ x ∈ s, f x = (↑(#t))⁻¹ • ∑ x ∈ t, g x

Tactic:
sum_nbij i hi i_inj i_surj h

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
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
s : S
n : N
⊢ g₁ n = g₂ n → g₁ (s • n) = g₂ (s • n)

Tactic:
e'

Goal state after:
case refine_3
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
s : S
n : N
e' : g₁ n = g₂ n
⊢ g₁ (s • n) = g₂ (s • n)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
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
s : S
n : N
e' : g₁ n = g₂ n
⊢ s • g₁ n = s • g₂ n

Tactic:
e'

Goal state after:
case refine_3
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
s : S
n : N
e' : g₁ n = g₂ n
⊢ s • g₂ n = s • g₂ n
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
this :
  ∀ (i : ℕ),
    f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
        -∑ x ∈ Ico m (n - 1), (f (x + 1) - f x) • ∑ i ∈ range (x + 1), g i) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ x ∈ Ico m (n - 1), (f (x + 1) - f x) • ∑ i ∈ range (x + 1), g i

Tactic:
sum_range_succ,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
this :
  ∀ (i : ℕ),
    f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)
⊢ f m • g m +
      (f (n - 1) • ∑ i ∈ range n, g i - f m • (∑ i ∈ range m, g i + g m) +
        -∑ x ∈ Ico m (n - 1), (f (x + 1) - f x) • (∑ i ∈ range x, g i + g x)) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ x ∈ Ico m (n - 1), (f (x + 1) - f x) • (∑ i ∈ range x, g i + g x)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a b : α
⊢ a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s.val ∧ b ∈ s

Tactic:
mem_mk

Goal state after:
α : Type u_1
s : Finset α
a b : α
⊢ a ∈ s.val ∧ b ∈ s.val ↔ a ∈ s.val ∧ b ∈ s.val
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty

Tactic:
contrapose!; exact sym_eq_empty

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
g : M →ₗ[R] Q
I₄ : IsScalarTower R R Q
⊢ (fun g' ↦ ↑R g' ∘ₗ ↑e = g) (g ∘ₗ ↑e.symm)

Tactic:
by
      ext
      simp

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ Std.Irrefl r → ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

Tactic:
intro ⟨h⟩; apply Sym2.ind; aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
⊢ (fun z ↦ ⟨map Subtype.val ↑z.snd, ⋯⟩)
      ((fun z ↦ fromRelNdrec ↑z ⋯ (fun a₁ a₂ h ↦ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯) z) =
    z

Tactic:
rcases z with ⟨⟨a₁, a₂⟩, h⟩

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
val✝ : Sym2 α
a₁ a₂ : α
h : Quot.mk (Rel α) (a₁, a₂) ∈ fromRel sym
⊢ (fun z ↦ ⟨map Subtype.val ↑z.snd, ⋯⟩)
      ((fun z ↦ fromRelNdrec ↑z ⋯ (fun a₁ a₂ h ↦ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯) ⟨Quot.mk (Rel α) (a₁, a₂), h⟩) =
    ⟨Quot.mk (Rel α) (a₁, a₂), h⟩
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ [a₁, b₁].Perm [a₂, b₂]

Tactic:
by
          rw [h₁, h₂]
          first | done | constructor

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

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [a₁, b₁].Perm [a₂, b₂]

Tactic:
by
          rw [h₁, h₂]
          first | done | constructor

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : (fun {Z} h ↦ f ≫ h) = fun {Z} h ↦ g ≫ h
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
by convert! congr_fun (congr_fun w Z) h

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝¹ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝ : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toPrefunctor =
    { obj := obj, map := map', map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor
⊢ map = map'

Tactic:
simpa [Functor.toPrefunctor] using h

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3.e_a
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'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) = g ((algebraMap S S') s)

Tactic:
exact (AlgHom.congr_fun h₂ s :)

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

Goal state before:
pp: case mk.mk
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
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝¹ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
⊢ { preimage := f₁, map_preimage := hf₁, preimage_map := preimage_map✝¹ } =
    { preimage := f₂, map_preimage := hf₂, preimage_map := preimage_map✝ }

Tactic:
simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]

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

Goal state before:
pp: case mp
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g

pp: case mpr
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g

Tactic:
· rintro h
    simpa using congr_arg Quiver.reverse h

Goal state after:
case mpr
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g
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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : F.map f ≍ G.map f
hg : F.map g ≍ G.map g
⊢ F.map (f ≫ g) ≍ G.map (f ≫ g)

Tactic:
rw [F.map_comp, G.map_comp]
  congr

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : Cᵒᵖ
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
simp only [← op_comp_unop, Quiver.Hom.unop_op, assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a
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 : D ≌ E
X : C
| f.functor.map (e.counitIso.inv.app (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
    f.functor.map (e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X))))

pp: case a.a
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 : D ≌ E
X : C
| f.counitIso.hom.app (f.functor.obj (e.functor.obj X))

pp: case a
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 : D ≌ E
X : C
| f.functor.map (f.unitIso.hom.app (e.functor.obj X))

Tactic:
← Functor.map_comp,

Goal state after:
case a.a
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 : D ≌ E
X : C
| f.functor.map
    (e.counitIso.inv.app (f.inverse.obj (f.functor.obj (e.functor.obj X))) ≫
      e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X))))

case a.a
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 : D ≌ E
X : C
| f.counitIso.hom.app (f.functor.obj (e.functor.obj X))

case a
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 : D ≌ E
X : C
| f.functor.map (f.unitIso.hom.app (e.functor.obj X))
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : C ⥤ D
⊢ F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : C ⥤ D
⊢ F.map (se.section_ ≫ f) = 𝟙 (F.obj Y)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.map (𝟭 C) = P

Tactic:
rw [map_id_eq_isoClosure, P.isoClosure_eq_self]

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁸ : ConcreteCategory C FC
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
E : Type u_5
inst✝⁴ : Category.{v_3, u_5} E
FE : E → E → Type u_6
CE : E → Type w
inst✝³ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
inst✝² : ConcreteCategory E FE
inst✝¹ : HasForget₂ C D
inst✝ : HasForget₂ D E
⊢ (CategoryTheory.forget₂ C D ⋙ CategoryTheory.forget₂ D E) ⋙ forget E = forget C

Tactic:
change (CategoryTheory.forget₂ _ D) ⋙ (CategoryTheory.forget₂ D E ⋙ CategoryTheory.forget E) = _
    simp only [HasForget₂.forget_comp]

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
FC : C → C → Type t₁
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
FD : D → D → Type t₂
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
⊢ IsIso f

Tactic:
by
      have i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
      have : IsIso ((forget C).map f) := by
        rwa [← @HasForget₂.forget_comp (C := C) (D := D)]
      apply isIso_of_reflects_iso f (forget C)

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty i' p

Tactic:
rw [Arrow.iso_w' e]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B A' B' X Y : C
i : A ⟶ B
i' : A' ⟶ B'
e : Arrow.mk i ≅ Arrow.mk i'
p : X ⟶ Y
hip : HasLiftingProperty i p
⊢ HasLiftingProperty (Arrow.Hom.left e.inv ≫ i ≫ Arrow.Hom.right e.hom) p
Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi g

Tactic:
rw [Arrow.iso_w' e]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ Epi (Arrow.Hom.left e.inv ≫ f ≫ Arrow.Hom.right e.hom)
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ ∀ {f : A ⟶ F.obj X} {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), sq.HasLift

Tactic:
intro f

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
⊢ ∀ {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), sq.HasLift
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ ∀ {f : G.obj A ⟶ X} {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), sq.HasLift

Tactic:
intro f

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
⊢ ∀ {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), sq.HasLift
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
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
⊢ ∀ {Z : D} (g h : F.obj Y ⟶ Z), F.map f ≫ g = F.map f ≫ h → g = h

Tactic:
intro Z g h H
    replace H := congr_arg (adj.homEquiv X Z) H
    rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
      Equiv.apply_eq_iff_eq] at H

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
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
s : SplitEpi (F.map f)
⊢ F.map (F.preimage s.section_ ≫ f) = F.map (𝟙 Y)

Tactic:
simp only [map_comp, map_preimage, map_id]

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
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
s : SplitEpi (F.map f)
⊢ s.section_ ≫ F.map f = 𝟙 (F.obj Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
t : Fan fun p ↦ X p.1 p.2
m : t.pt ⟶ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).pt
hm : ∀ (j : ι × ι'), m ≫ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).proj j = t.proj j
i : ι
j : ι'
⊢ (m ≫ c'.proj i) ≫ (c i).proj j = ((lift hc' fun i ↦ lift (hc i) fun j ↦ t.proj (i, j)) ≫ c'.proj i) ≫ (c i).proj j

Tactic:
by simpa using hm (i, j)

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
m : (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt
hm : ∀ (j : ι × ι'), (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ m = t.inj j
i : ι
j : ι'
⊢ (c i).inj j ≫ c'.inj i ≫ m = (c i).inj j ≫ c'.inj i ≫ desc hc' fun i ↦ desc (hc i) fun j ↦ t.inj (i, j)

Tactic:
by simpa using hm (i, j)

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

Goal state before:
pp: case none.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f ≫ inl = g ≫ inr
⊢ ∀ (f_1 : none ⟶ none),
    ((span f g).map f_1 ≫ Option.casesOn none (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
      (Option.casesOn none (f ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫
        ((Functor.const WalkingSpan).obj W).map f_1

Tactic:
intro f

Goal state after:
case none.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
W : C
inl : Y ⟶ W
inr : Z ⟶ W
eq : f✝ ≫ inl = g ≫ inr
f : none ⟶ none
⊢ ((span f✝ g).map f ≫ Option.casesOn none (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) =
    (Option.casesOn none (f✝ ≫ inl) fun j' ↦ WalkingPair.casesOn j' inl inr) ≫ ((Functor.const WalkingSpan).obj W).map f