mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
⊢ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d

Tactic:
p

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
⊢ p ∣ a → p ∣ b → ¬Prime p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ Associates.mk p ∣ 1

Tactic:
← hg

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ Associates.mk p ∣ Associates.mk a ⊓ Associates.mk b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
⊢ factors 1 = 0

Tactic:
apply FactorSet.unique
  rw [Associates.factors_prod]
  exact Multiset.prod_zero

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
a✝ : Nontrivial R
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (C (lcm p.content q.content)).content * r.content ∣ s.content ∧
      (C (lcm p.content q.content) * r).primPart ∣ s.primPart

Tactic:
rprim.content_eq_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
a✝ : Nontrivial R
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (C (lcm p.content q.content)).content * 1 ∣ s.content ∧ (C (lcm p.content q.content) * r).primPart ∣ s.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case e'_4
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
hph : p ^ Nat.find ⋯ ≠ 0
hα : Nontrivial α
⊢ Nat.find ⋯ = p.count (p ^ Nat.find ⋯).factors

Tactic:
rw [count_pow hp.ne_zero hp, count_self hp, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ g n ∈ Submodule.comap ((TensorProduct.mk R Q P) q) (lTensor Q g).range

Tactic:
exact ⟨q ⊗ₜ[R] n, rfl⟩

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

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
q : Q
n : N
⊢ ∃ a, (lTensor Q g) a = q ⊗ₜ[R] g n

Tactic:
exact ⟨q ⊗ₜ[R] n, rfl⟩

Goal state after:
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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ ∀ (x : Q) (y : N),
    (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ lTensor Q g) (x ⊗ₜ[R] y) = (lTensor Q f).range.mkQ (x ⊗ₜ[R] y)

Tactic:
intro n

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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
n : Q
⊢ ∀ (y : N), (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ lTensor Q g) (n ⊗ₜ[R] y) = (lTensor Q f).range.mkQ (n ⊗ₜ[R] 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
P : Submodule R M
hP : ∃ n s, span R (Set.range s) = P
⊢ Small.{u, u_2} ↥P

Tactic:
obtain ⟨n, s, rfl⟩ := hP

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
n : ℕ
s : Fin n → M
⊢ Small.{u, u_2} ↥(span R (Set.range s))
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
p m✝ : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy : y ∈ (restrictSupport R s).carrier
m : σ →₀ ℕ
hm : ¬∑ x_1 ∈ Finset.antidiagonal m, coeff x_1.1 x * coeff x_1.2 y = 0
⊢ m ∈ s

Tactic:
obtain ⟨⟨i, j⟩, hij, e⟩ := Finset.exists_ne_zero_of_sum_ne_zero hm

Goal state after:
σ : Type u
R : Type v
inst✝ : CommSemiring R
p m✝ : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy : y ∈ (restrictSupport R s).carrier
m : σ →₀ ℕ
hm : ¬∑ x_1 ∈ Finset.antidiagonal m, coeff x_1.1 x * coeff x_1.2 y = 0
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal m
e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0
⊢ m ∈ s
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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ ∀ (x : N) (y : Q),
    (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ rTensor Q g) (x ⊗ₜ[R] y) = (rTensor Q f).range.mkQ (x ⊗ₜ[R] y)

Tactic:
intro n

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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
⊢ ∀ (y : Q), (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ rTensor Q g) (n ⊗ₜ[R] y) = (rTensor Q f).range.mkQ (n ⊗ₜ[R] y)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = (LinearMap.lTensor A g.toLinearMap).ker
⊢ (LinearMap.lTensor A g.toLinearMap).ker =
    (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype).range

Tactic:
rw [(lTensor_exact A g.toLinearMap.exact_subtype_ker_map hg).linearMap_ker_eq]

Goal state after:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = (LinearMap.lTensor A g.toLinearMap).ker
⊢ (LinearMap.lTensor A g.toLinearMap.ker.subtype).range =
    (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype).range
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ (((F.orderEmbOfFin h) ⟨j, hj⟩).1, ((F.orderEmbOfFin h) ⟨j, hj⟩).2) ∈ F

Tactic:
convert! F.orderEmbOfFin_mem h ⟨j, hj⟩ using 1

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

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

Tactic:
by_cases hk : 0 = k

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f + g)

Tactic:
by
  intro a
  simp only [hf a, hg a, Pi.add_apply]

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

Goal state before:
pp: n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 1 [MOD n]
⊢ s.prod ≡ 1 [MOD n]

Tactic:
simpa using multisetProd_map_one h

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

Goal state before:
pp: n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 1 [ZMOD n]
⊢ s.prod ≡ 1 [ZMOD n]

Tactic:
simpa using multisetProd_map_one h

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

Goal state before:
pp: α : Type u_1
s : Finset α
m : Sym2 α
⊢ m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s

Tactic:
by
  rw [mem_mk, sym2_val, Multiset.mem_sym2_iff]
  simp only [mem_val]

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

Tactic:
rintro ⟨a, ha, he⟩ b hb

Goal state after:
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)
a : α
ha : a ∈ s
he : m ∈ image (Sym.cons a) (s.sym n)
b : α
hb : b ∈ m
⊢ b ∈ s
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
i : α
e : β
he : e ∈ d
hi : ⋯.choose = i
⊢ ⋯.choose ∈ s

Tactic:
exact (hd e he).choose_spec.1

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
n✝ : ℕ
left✝ : n✝ + 1 ≠ 0
⊢ ∅.sym (n✝ + 1) = ∅

Tactic:
exact sym_empty _

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

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F G : U ⥤q V
e : F = G
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
by
  subst e
  simp

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 : α → β
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧

Tactic:
exfalso
      simp at hx

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'
inst✝ : IsPushout R S R' S'
a : S
⊢ (equiv R S R' S').symm ((algebraMap S S') a) = a ⊗ₜ[R] 1

Tactic:
(equiv R S R' S').symm_apply_eq,

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'
inst✝ : IsPushout R S R' S'
a : S
⊢ (algebraMap S S') a = (equiv R S R' S') (a ⊗ₜ[R] 1)
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'
inst✝ : IsPushout R S R' S'
a : R'
⊢ (equiv R S R' S').symm ((algebraMap R' S') a) = 1 ⊗ₜ[R] a

Tactic:
(equiv R S R' S').symm_apply_eq,

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'
inst✝ : IsPushout R S R' S'
a : R'
⊢ (algebraMap R' S') a = (equiv R S R' S') (1 ⊗ₜ[R] a)
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : CategoryStruct.{v₁, u₁} C
X Y : C
p : X = Y
⊢ X ⟶ Y

Tactic:
p

Goal state after:
C : Type u₁
inst✝ : CategoryStruct.{v₁, u₁} C
X Y : C
p : X = Y
⊢ Y ⟶ Y
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (𝟙 (e.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.counitInv.app (e.functor.obj (e.inverse.obj Y)))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))

Tactic:
rw [map_id, map_id]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| 𝟙 (e.inverse.obj (e.functor.obj (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.counitInv.app (e.functor.obj (e.inverse.obj Y)))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ l.l.unop ≫ i.unop = f.unop

Tactic:
by rw [← unop_comp, l.fac_left]

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)

Tactic:
simp only [epimorphisms.iff]

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ Epi f → Epi (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)

Tactic:
simp only [epimorphisms.iff]

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ Epi f → Epi (f ≫ e.hom)
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ L₁.map l.inv ≫ X.hom = Y.hom ≫ R₁.map r.inv

Tactic:
rw [← L₁.mapIso_inv l, Iso.inv_comp_eq, L₁.mapIso_hom, ← Category.assoc, h,
          Category.assoc, ← R₁.map_comp]
        simp

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) = F.map (X.hom ≫ R.map (F₂.preimage φ.right))

Tactic:
rw [← cancel_mono (β.app _), ← cancel_epi (α.app _), F.map_comp, F.map_comp, assoc, assoc]
        calc
        _ = (F₁ ⋙ L').map (F₁.preimage φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right := by
          rw [← Functor.comp_map, ← α.naturality_assoc]
        _ = α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ (F₂ ⋙ R').map (F₂.preimage φ.right) := by
          simp only [Functor.comp_map, Functor.map_preimage, ← map_obj_hom α β Y, φ.w,
            map_obj_hom α β X, assoc]
        _ = _ := by rw [← Functor.comp_map, β.naturality]

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:
by
        letI := isIsomorphicSetoid D
        exact Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩

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
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ (coneOfDiagramInitial tX F).π.app j = s.π.app j
⊢ m = s.π.app X

Tactic:
simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)]
    simp

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
inst✝ : HasProducts C
X : C
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (yoneda.obj X ⋙ (piConst.obj X).rightOp).map x✝ ≫ (Pi.lift id).op = (Pi.lift id).op ≫ (𝟭 Cᵒᵖ).map x✝

Tactic:
apply Quiver.Hom.unop_inj; cat_disch

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
inst✝ : HasProducts C
X : C
x✝ : Type v
⊢ (piConst.obj X).rightOp.map ({ app := fun n ↦ ↾fun i ↦ Pi.π (fun x ↦ X) i, naturality := ⋯ }.app x✝) ≫
      { app := fun Y ↦ (Pi.lift id).op, naturality := ⋯ }.app ((piConst.obj X).rightOp.obj x✝) =
    𝟙 ((piConst.obj X).rightOp.obj x✝)

Tactic:
apply Quiver.Hom.unop_inj; cat_disch

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

Goal state before:
pp: case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ g ≫ inr ≫ i₁ = g ≫ inr ≫ i₂

Tactic:
simpa using congr_arg (fun f => coprod.inr ≫ f) h

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
F : T ⥤ D
inst✝ : F.Faithful
A B : Under X
f g : A ⟶ B
h : (post F).map f = (post F).map g
⊢ f = g

Tactic:
ext
    exact F.map_injective (congrArg CommaMorphism.right h)

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂

Tactic:
by
  constructor
  · intro h
    refine ⟨fun f => ?_⟩
    have : W₁.comp W₂ f := by simp only [h, top_apply]
    exact ⟨this.some⟩
  · intro
    ext X Y f
    simp only [top_apply, iff_true]
    exact ⟨factorizationData W₁ W₂ f⟩

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

Goal state before:

Tactic:
g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
    _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
    _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
    _ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
    _ = h := by rw [Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cone K
h : IsLimit c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (j : J),
    h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫ ((𝟭 C).mapCone c).π.app j = s.π.app j

Tactic:
by
            cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cocone K
h : IsColimit c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (j : J),
    ((𝟭 C).mapCocone c).ι.app j ≫ h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } = s.ι.app j

Tactic:
by
            cases K; rcases c with ⟨_, _, _⟩; intro s j; cases s; exact h.fac _ j

Goal state after: