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

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : p.count (a ^ n).factors = n * p.count a.factors
⊢ p.count a.factors + n * p.count a.factors = (n + 1) * p.count a.factors

Tactic:
ring

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0

Tactic:
by rw [← aeval_comp, comp_eq_aeval, hp, map_zero]

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

Goal state before:
pp: case convert_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (algebraMap K L) 0

Tactic:
rw [RingHom.map_zero]

Goal state after:
case convert_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_3.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
x_eq,

Goal state after:
case refine_3.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑0)⁻¹ ∈ A
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
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
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective ⇑(g i)
⊢ Function.Injective ⇑(lift R ι G f g Hg)

Tactic:
by
  cases isEmpty_or_nonempty ι
  · apply Function.injective_of_subsingleton
  intro z w eq
  obtain ⟨i, x, y, rfl, rfl⟩ := exists_of₂ z w
  simp_rw [lift_of] at eq
  rw [injective _ eq]

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

Tactic:
by
  classical
  by_cases r = 0 <;> simp [mem_restrictSupport_iff, support_monomial, *]

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
hg : Surjective ⇑g
⊢ Exact ⇑(lTensor Q f) ⇑(lTensor Q g)

Tactic:
exact lTensor_exact Q hfg hg

Goal state after:
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
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range

Tactic:
obtain ⟨M', N', _, _, h⟩ := exists_finite_submodule_of_setFinite s hs

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
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ s.dens ≤ 1

Tactic:
simpa using dens_le_dens s.subset_univ

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype β
s : Finset α
inst✝ : DecidableEq α
f : β → α
t : Finset β
h : Set.MapsTo f ↑t ↑s
⊢ t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens

Tactic:
by
  simp [dens, ← sum_div, card_eq_sum_card_fiberwise h]

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 : ι) → Zero (G i)
inst✝¹ : (i : ι) → SMulZeroClass R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
⊢ ⟦⟨Classical.arbitrary ι, r • (fun x ↦ 0) (Classical.arbitrary ι)⟩⟧ = 0

Tactic:
smul_zero

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 : ι) → Zero (G i)
inst✝¹ : (i : ι) → SMulZeroClass R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
⊢ ⟦⟨Classical.arbitrary ι, 0⟩⟧ = 0
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
⊢ |b - a| + 1 = |b - a| + ↑1

Tactic:
Int.ofNat_one

Goal state after:
a b : ℤ
⊢ |b - a| + 1 = |b - a| + 1
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this :
  ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j' - 1)).1 ≤
    ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j' - 1)).2
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ (F.intervalGapsWithin h a b ↑j').1

Tactic:
simp only [Nat.succ_eq_add_one, hj'₀] at this

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ (F.intervalGapsWithin h a b ↑j').1
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
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
⊢ 0 = r • 0

Tactic:
smul_zero

Goal state after:
case zero
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
⊢ 0 = 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : 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
r : S
x : S ⊗[R] M
⊢ 0 = r • 0

Tactic:
smul_zero

Goal state after:
case refine_1
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : 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
r : S
x : S ⊗[R] M
⊢ 0 = 0
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ ↑x✝¹.sym2 = ↑x✝.sym2

Tactic:
rw [coe_eq_coe]

Goal state after:
α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ x✝¹.sym2.Perm x✝.sym2
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
h : xs.Nodup
⊢ xs.sym2.Nodup

Tactic:
induction xs with
  | nil => simp only [List.sym2, nodup_nil]
  | cons x xs ih =>
    rw [List.sym2]
    specialize ih h.of_cons
    rw [nodup_cons] at h
    refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
    case disj =>
      intro z hz hz'
      simp only [mem_cons, mem_map] at hz
      obtain ⟨_, (rfl | _), rfl⟩ := hz
        <;> simp [left_mem_of_mk_mem_sym2 hz'] at h
    case notmem =>
      intro h'
      simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'
    case inj =>
      intro a b
      simp only [Sym2.eq_iff, true_and]
      rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x : S ⊗[R] M
⊢ 0 = s • 0

Tactic:
smul_zero

Goal state after:
case refine_1
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x : S ⊗[R] M
⊢ 0 = 0
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
h : z.IsDiag
⊢ #z.toFinset = 1

Tactic:
induction z
  rw [Sym2.mk_isDiag_iff] at h
  simp [Sym2.toFinset_mk_eq, h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
h : ¬z.IsDiag
⊢ #z.toFinset = 2

Tactic:
induction z
  rw [Sym2.mk_isDiag_iff] at h
  simp [Sym2.toFinset_mk_eq, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
h : Rel α (b, c) (d, e)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ = fun x ↦ if a = d then e else d

Tactic:
ext hy

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
h : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ hy = if a = d then e else d
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X✝ Y✝ : D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hfg : F.map a₁✝ = F.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by
    rw [← cancel_mono (L.objObjPreimageIso _).inv, ← cancel_epi (L.objObjPreimageIso _).hom]
    exact h _ _ (by simp [hfg])

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f

Tactic:
by
    rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝)).op ≫ (α.inv.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))

Tactic:
rw [← op_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.inv.app (unop x✝) ≫ α.hom.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.inv.app (unop x✝)).op ≫ (α.hom.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))

Tactic:
rw [← op_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝) ≫ α.inv.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).map f)
⊢ IsIso f

Tactic:
let e : X ≃* Y := { f.hom, i.toEquiv with }

Goal state after:
X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
i : (forget MonCat).obj X ≅ (forget MonCat).obj Y := asIso ((forget MonCat).map f)
e : ↑X ≃* ↑Y :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
i : (forget CommMonCat).obj X ≅ (forget CommMonCat).obj Y := asIso ((forget CommMonCat).map f)
⊢ IsIso f

Tactic:
let e : X ≃* Y := { f.hom, i.toEquiv with }

Goal state after:
X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
i : (forget CommMonCat).obj X ≅ (forget CommMonCat).obj Y := asIso ((forget CommMonCat).map f)
e : ↑X ≃* ↑Y :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.IsLimit

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
r t : Cone F
P : IsLimit r
i : IsIso (P.lift t)
⊢ r ≅ t

Tactic:
haveI : IsIso (P.liftConeMorphism t).hom := i
    haveI : IsIso (P.liftConeMorphism t) := Cone.cone_iso_of_hom_iso _
    symm
    apply asIso (P.liftConeMorphism t)

Goal state after:
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

Tactic:
← 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)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
X : C
f : X ⟶ Y
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
e.homEquiv_eq,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
X : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f.op)) (e.homEquiv (𝟙 Y)) = e'.homEquiv f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X✝ : C
e e' : F.CorepresentableBy X✝
h : e.homEquiv (𝟙 X✝) = e'.homEquiv (𝟙 X✝)
X : C
f : X✝ ⟶ X
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
e.homEquiv_eq,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X✝ : C
e e' : F.CorepresentableBy X✝
h : e.homEquiv (𝟙 X✝) = e'.homEquiv (𝟙 X✝)
X : C
f : X✝ ⟶ X
⊢ (ConcreteCategory.hom (F.map f)) (e.homEquiv (𝟙 X✝)) = e'.homEquiv f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type (max w v₁)
t : F.obj X
⊢ uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) =
    uliftYoneda.{w, v₁, u₁}.map f.unop ≫ uliftYonedaEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := uliftYonedaEquiv.surjective t

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type (max w v₁)
u : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F
⊢ uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) (uliftYonedaEquiv u)) =
    uliftYoneda.{w, v₁, u₁}.map f.unop ≫ uliftYonedaEquiv.symm (uliftYonedaEquiv u)
Module: Mathlib.CategoryTheory.LiftingProperties.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ sq.HasLift

Tactic:
simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
    infer_instance

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

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
D : Type u₄
inst✝³ : Category.{v₄, u₄} D
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : J ⥤ C
G : C ⥤ D
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Cone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (G.preimage t.hom ≫ Y✝.π.app j) = G.map (X✝.π.app j)

Tactic:
simpa using t.w j

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

Goal state before:
pp: 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
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)

Tactic:
constructor <;> intro <;> constructor

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

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.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J' C

Tactic:
constructor
  intro F
  apply hasLimit_of_equivalence_comp e

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J' C

Tactic:
by
  constructor
  intro F
  apply hasLimit_of_equivalence_comp e

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

Goal state before:
pp: J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ arrows j ≫ ι arrows j ≫ g = head arrows ≫ g

Tactic:
← Category.assoc

Goal state after:
J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map inl = s.π.app WalkingCospan.left ≫ (cospan f g).map inl

Tactic:
← Category.assoc

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (cospan f g)
j : WalkingCospan
⊢ (lift s ≫ t.π.app WalkingCospan.left) ≫ (cospan f g).map inl = s.π.app WalkingCospan.left ≫ (cospan f g).map inl