mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ x = ((aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0)))⁻¹

Tactic:
inv_div,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ x = ((aeval x) p - (algebraMap K L) (p.coeff 0)) / (aeval x) p.divX
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
m : M
g : G i
⊢ (directLimitRight f M) (m ⊗ₜ[R] (of R ι G f i) g) =
    (of R ι (fun x ↦ M ⊗[R] G x) (fun i j h ↦ LinearMap.lTensor M (f i j h)) i) (m ⊗ₜ[R] g)

Tactic:
by
  simp [directLimitRight, congr_apply_of]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl
ι✝ : Type u_1
inst✝⁴ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝¹ j : ι✝
h : i✝¹ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝¹ : WellFoundedLT ι
inst✝ : InverseSystem f
hi : ¬IsMax i
e : PEquivOn f equivSucc (Iic i)
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i✝ : ι
hsj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hj : ¬IsMax i✝
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
cases (succ_eq_succ_iff_of_not_isMax hj hi).mp eq

Goal state after:
case inl.refl
ι✝ : Type u_1
inst✝⁴ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝¹ : WellFoundedLT ι
inst✝ : InverseSystem f
hi : ¬IsMax i
e : PEquivOn f equivSucc (Iic i)
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hsj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hj : ¬IsMax i
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
I : Ideal R
⊢ comap (↑(TensorProduct.lid R Q)) ((TensorProduct.mk R (R ⧸ I) Q) 1).ker = comap (↑(TensorProduct.lid R Q)) (I • ⊤)

Tactic:
← ker_comp

Goal state after:
R : Type u_1
inst✝² : CommRing R
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
I : Ideal R
⊢ ((TensorProduct.mk R (R ⧸ I) Q) 1 ∘ₗ ↑(TensorProduct.lid R Q)).ker = comap (↑(TensorProduct.lid R Q)) (I • ⊤)
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = 0

Tactic:
rw [← pow_nilpotencyClass this, hx, pow_one]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat R (M i)

Tactic:
by
  classical
  simp_rw [iff_rTensor_injectiveₛ, ← EquivLike.comp_injective _ (directSumRight R R _ _),
    ← LinearEquiv.coe_coe, ← coe_comp, directSumRight_comp_rTensor, coe_comp, LinearEquiv.coe_coe,
    EquivLike.injective_comp, lmap_injective]
  constructor <;> (intro h; intros; apply h)

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

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₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
⊢ Function.Injective ⇑(hf.map hg LinearMap.id i)

Tactic:
by
  have h : hf.map hg LinearMap.id i = hg.equiv ∘ i.lTensor M₁ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
  simpa [h] using Module.Flat.lTensor_preserves_injective_linearMap i hi

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

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

Tactic:
simp_rw [HPow.hPow, Pow.pow]

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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Monoid (G i)
inst✝² : Monoid C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝ : G i
⊢ map f f (fun x x_1 ↦ x_1 ^ 0) ⋯ ⟦⟨i, x✝⟩⟧ = 1
Module: Mathlib.Algebra.Colimit.DirectLimit

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

Tactic:
simp_rw [HPow.hPow, Pow.pow]

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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Monoid (G i)
inst✝² : Monoid C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x✝ : G i
⊢ map f f (fun x x_1 ↦ x_1 ^ (n + 1)) ⋯ ⟦⟨i, x✝⟩⟧ = map f f (fun x x_1 ↦ x_1 ^ n) ⋯ ⟦⟨i, x✝⟩⟧ * ⟦⟨i, x✝⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : (i : ι) → FunLike (H i) (G i) C
inst✝⁷ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁶ : IsDirectedOrder ι
inst✝⁵ : Nonempty ι
inst✝⁴ : Monoid R
inst✝³ : (i : ι) → Monoid (G i)
inst✝² : (i : ι) → MulDistribMulAction R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
⊢ ⟦⟨Classical.arbitrary ι, r • (fun x ↦ 1) (Classical.arbitrary ι)⟩⟧ = 1

Tactic:
by rw [smul_one]; rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ (𝔼 i, if p i then a else 0) = if ∃ i, p i then (↑(card ι))⁻¹ • a else 0

Tactic:
simp [univ.expect_ite_zero p (by simpa using h)]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
⊢ ∏ z ∈ F, f z.1 z.2 = ∏ i ∈ range k, f (F.intervalGapsWithin h a b ↑i).2 (F.intervalGapsWithin h a b ↑i.succ).1

Tactic:
set p := F.intervalGapsWithin h a b
  symm
  apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))
  · exact fun i _ ↦ F.intervalGapsWithin_mapsTo h a b (x := i) (by grind)
  · intro i hi j hj hij
    rw [mem_range] at hi hj
    apply F.intervalGapsWithin_injOn h a b <;> grind
  · intro z hz
    obtain ⟨i, hi₁, hi₂⟩ := F.intervalGapsWithin_surjOn h a b hz
    exact ⟨i, by grind, hi₂⟩
  · simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
n✝ : ℕ
a✝ : ∏ m ∈ Icc (-(↑n✝ + 1)) (↑n✝ + 1), f m = f (↑n✝ + 1) * f (-(↑n✝ + 1)) * ∏ m ∈ Icc (-↑n✝) ↑n✝, f m
⊢ ∏ m ∈ Icc (-(↑(n✝ + 1) + 1)) (↑(n✝ + 1) + 1), f m =
    f (↑(n✝ + 1) + 1) * f (-(↑(n✝ + 1) + 1)) * ∏ m ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f m

Tactic:
· rw [Icc_succ_succ, prod_union (by simp)]
    grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ {a | f a = m} ⊆ ↑ht.toFinset

Tactic:
intro _

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
a✝ : ι
⊢ a✝ ∈ {a | f a = m} → a✝ ∈ ↑ht.toFinset
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y : α × α
⊢ Rel α x y → Rel α y x

Tactic:
aesop (rule_sets := [Sym2])

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

Goal state before:
pp: α : Type u_1
x y z : α × α
a : Rel α x y
b : Rel α y z
⊢ Rel α x z

Tactic:
aesop (rule_sets := [Sym2])

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

Goal state before:
pp: α : Type u_1
p q : α × α
⊢ Rel α p q ↔ p = q ∨ p = q.swap

Tactic:
aesop (rule_sets := [Sym2])

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
⊢ ∀ ⦃a b : α × α⦄, Rel α a b → Rel β (Prod.map f f a) (Prod.map f f b)

Tactic:
intro _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ : α × α
⊢ ∀ ⦃b : α × α⦄, Rel α a✝ b → Rel β (Prod.map f f a✝) (Prod.map f f b)
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 R' S S'
T : Type u_8
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R' T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T
⊢ IsPushout R R' S T

Tactic:
isPushout_iff

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 : IsBaseChange R' (toAlgHom R S S').toLinearMap
T : Type u_8
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R' T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T
⊢ IsBaseChange R' (toAlgHom R S T).toLinearMap
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
ι : Type u'
X : ι → C
F : C ⥤ D
⊢ (ofObj X).strictMap F = ofObj (F.obj ∘ X)

Tactic:
ext Y

Goal state after:
C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
ι : Type u'
X : ι → C
F : C ⥤ D
Y : D
⊢ (ofObj X).strictMap F Y ↔ ofObj (F.obj ∘ X) Y
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n : ℕ
hp : (p.cons q).length = n + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
| @cons c d p q h =>

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
⊢ (P.ι ⋙ F).essImage = P.map F

Tactic:
ext Y

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ (P.ι ⋙ F).essImage Y ↔ P.map F Y
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ ⊤.map F = F.essImage

Tactic:
ext Y

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
⊢ ⊤.map F Y ↔ F.essImage Y
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

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

Goal state before:
pp: case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f → ∀ (i : I), IsIso (f i)

Tactic:
intro _

Goal state after:
case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : IsIso f
⊢ ∀ (i : I), IsIso (f i)
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → ⊤ ≤ isomorphisms C

Tactic:
intro _

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsGroupoid C
⊢ ⊤ ≤ isomorphisms C
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: case h₁
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := ⋯
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.left (aux φ ≫ sq) = Hom.left (aux ψ ≫ sq)

pp: case h₂
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := ⋯
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.right (aux φ ≫ sq) = Hom.right (aux ψ ≫ sq)

Tactic:
· exact h

Goal state after:
case h₂
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := ⋯
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.right (aux φ ≫ sq) = Hom.right (aux ψ ≫ sq)
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
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ e.left ≫ (inv e).left = 𝟙 X.left

Tactic:
rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
⊢ Function.Injective fun f ↦ ofHom f

Tactic:
intro _

Goal state after:
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ : X →* Y
⊢ ∀ ⦃a₂ : X →* Y⦄, (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂ → a₁✝ = a₂
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
⊢ Function.Injective fun f ↦ ofHom f

Tactic:
intro _

Goal state after:
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ : X →* Y
⊢ ∀ ⦃a₂ : X →* Y⦄, (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂ → a₁✝ = a₂
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ h.homEquiv f = (const J).map f ≫ h.homEquiv (𝟙 X)

Tactic:
conv_lhs => rw [← Category.comp_id f]

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ h.homEquiv (f ≫ 𝟙 X) = (const J).map f ≫ h.homEquiv (𝟙 X)
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: case mp
X : Type u
inst✝ : PartialOrder X
a b : X
f : a ⟶ b
⊢ IsIso f → a = b

Tactic:
intro _

Goal state after:
case mp
X : Type u
inst✝ : PartialOrder X
a b : X
f : a ⟶ b
a✝ : IsIso f
⊢ a = b
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).map f ≫
              (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                        (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).obj
                    X).map
                f)).toFun
        g).down

Tactic:
simpa using uliftYonedaEquiv_comp _ _

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {X_1 Y : C ⥤ Type v₁} (f : X_1 ⟶ Y),
    ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type v₁) ⋙
                  (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
intro Y Z f
        ext g
        rw [← ULift.down_inj]
        simpa using coyonedaEquiv_comp _ _

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map f) = { down := f.unop }

Tactic:
by
  simp [uliftCoyonedaEquiv, uliftYoneda]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p → ∀ (φ : mk i ⟶ mk p), Nonempty (LiftStruct φ)

Tactic:
intro _

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i p
⊢ ∀ (φ : mk i ⟶ mk p), Nonempty (LiftStruct φ)
Module: Mathlib.CategoryTheory.Functor.EpiMono

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
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi f

Tactic:
StrongEpi.iff_of_arrow_iso e

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
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi (F.inv.map (F.map f))
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
⊢ HasLimit F

Tactic:
have : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimit_equivalence_comp e.symm

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasLimit F
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✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ limMap (𝟙 F) = 𝟙 (limit F)

Tactic:
by
    apply Limits.limit.hom_ext; intro j
    simp

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

Goal state before:
pp: case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.id none) ≫
      match none with
      | none => f
      | some j => π j) =
    (match none with
      | none => f
      | some j => π j) ≫
      F.map (Hom.id none)

Tactic:
simp [w]

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

Goal state before:
pp: case some.none.term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.term val✝) ≫
      match none with
      | none => f
      | some j => π j) =
    (match some val✝ with
      | none => f
      | some j => π j) ≫
      F.map (Hom.term val✝)

Tactic:
simp [w]

Goal state after: