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

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : β₁ → α₁
m₂ : β₂ → α₂
⊢ comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p ↦ (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)

Tactic:
simp only [prod_eq_inf, comap_comap, comap_inf, Function.comp_def]

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : g.NeBot
s : Set α
⊢ s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f

Tactic:
simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def,
    exists_mem_subset_iff]

Goal state after:
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∈ I
⊢ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i ∈ map (f i) (l i)

Tactic:
simpa [hi] using image_mem_map (hs i hi)

Goal state after:
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
s : Set α
⊢ Coheyting.boundary (𝓟 s) = ⊥

Tactic:
simp [← Coheyting.inf_hnot_self]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : derivative P = 0
⊢ P ∣ derivative P

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map (⇑normalizeHom) (factors a)).prod = normalizeHom (Multiset.map (⇑normalizeHom) (factors a)).prod

Tactic:
← map_multiset_prod,

Goal state after:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalizeHom (factors a).prod = normalizeHom (normalizeHom (factors a).prod)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
⊢ p.IsRoot = ⊥

Tactic:
ext a

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
a : R
⊢ p.IsRoot a ↔ ⊥ a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
a : R
⊢ ?m.50 ∉ p.roots

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a x : R
⊢ p ≠ C a ∧ eval x (p - C a) = 0 ↔ p ≠ C a ∧ eval x p = a

Tactic:
eval_sub,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a x : R
⊢ p ≠ C a ∧ eval x p - eval x (C a) = 0 ↔ p ≠ C a ∧ eval x p = a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y

Tactic:
← Multiset.map_id' (normalizedFactors (x * y)),

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (fun x ↦ x) (normalizedFactors (x * y)) = normalizedFactors x + normalizedFactors y
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
u : R[X]ˣ
⊢ p.roots = (p * ↑u).roots

Tactic:
eq_C_of_degree_eq_zero <| degree_coe_units u,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
u : R[X]ˣ
⊢ p.roots = (p * C ((↑u).coeff 0)).roots
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
ha : a ≠ 0
n : ℕ
⊢ ((monomial n) a).roots = n • {0}

Tactic:
rw [← C_mul_X_pow_eq_monomial, roots_C_mul_X_pow ha]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hn : 0 < n
a x : R
⊢ eval x (X ^ n - C a) = 0 ↔ x ^ n = a

Tactic:
eval_sub,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hn : 0 < n
a x : R
⊢ eval x (X ^ n) - eval x (C a) = 0 ↔ x ^ n = a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < normalizedFactors x ↔ ¬IsUnit x

Tactic:
constructor
  · intro h hx
    obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'
    exact
      (prime_of_normalized_factor _ hp).not_isUnit
        (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx)
  · intro h
    obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h
    exact
      bot_lt_iff_ne_bot.mpr
        (mt Multiset.eq_zero_iff_forall_notMem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
h : ⇑Associates.mkMonoidHom ∘ Classical.choose ⋯ = id
⊢ Associates.mk (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) = x

Tactic:
rw [if_neg hx, ← mkMonoidHom_apply, MonoidHom.map_multiset_prod, map_map, h, map_id, ←
        associated_iff_eq]

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
h : ⇑Associates.mkMonoidHom ∘ Classical.choose ⋯ = id
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
⊢ eval x (p - q) = 0

Tactic:
eval_sub,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
⊢ eval x p - eval x q = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support

Tactic:
ext a

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ a ∈ (X * p).support ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ C a
⊢ (fun x ↦ eval x p) ⁻¹' {a} = (p - C a).rootSet R

Tactic:
ext; simp [mem_rootSet_of_ne (sub_ne_zero.mpr hp), sub_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ m.choose b • (m.descFactorial (m - b) • eval t (X - C t) ^ b * eval t ((⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0

Tactic:
eval_sub,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ m.choose b •
      (m.descFactorial (m - b) • (eval t X - eval t (C t)) ^ b * eval t ((⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) =
    0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : (C 0).degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False

Tactic:
simp only [map_zero] at h

Goal state after:
R : Type u
inst✝ : Field R
p : R[X]
this : p.degree ≤ 0
hc : p.coeff 0 = 0
h : degree 0 = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
⊢ q * p.div q + p.mod q = p

Tactic:
conv =>
      rhs
      rw [← modByMonic_add_div p (q * C q.leadingCoeff⁻¹)]
    rw [div, mod, add_comm, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x y : R[X]
x✝ : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)

Tactic:
gcd_val,

Goal state after:
R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x y : R[X]
x✝ : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ EuclideanDomain.gcd (map f y % map f x) (map f x) = map f (EuclideanDomain.gcd x y)
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial (↥s) D
ha : (rename Subtype.val) a' ≠ 0
h : a' = 0
⊢ (rename Subtype.val) a' = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0
f : R[X]
⊢ #↑(g ⁻¹' {f}) ≤ ℵ₀

Tactic:
le_aleph0_iff_set_countable

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0
f : R[X]
⊢ (g ⁻¹' {f}).Countable
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]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ R⁰
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
h : p.comp f = 0
⊢ (p.comp f).coeff (p.natDegree * f.natDegree) = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
⊢ (piLTLim hi).symm f l = ↑f k ⟨↑l, hl⟩

Tactic:
conv_rhs => rw [← (piLTLim hi).right_inv f]

Goal state after:
ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
⊢ (piLTLim hi).symm f l = ↑((piLTLim hi).toFun ((piLTLim hi).invFun f)) k ⟨↑l, hl⟩
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : ExpChar R p
⊢ ExpChar (MvPolynomial σ R) p

Tactic:
by
  cases ‹ExpChar R p›; exacts [ExpChar.zero, ExpChar.prime ‹_›]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ 0 = x

Tactic:
exact (f.map_eq_zero_iff hf).trans eq_comm

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 : α
g : α → β
⊢ (∏ x ∈ range k, g (F.intervalGapsWithin h a b ↑x.succ).1 / g (F.intervalGapsWithin h a b ↑x).1) *
      (g (F.intervalGapsWithin h a b ↑k).2 / g (F.intervalGapsWithin h a b ↑k).1) =
    g b / g a

Tactic:
prod_range_div (fun i ↦ g (F.intervalGapsWithin h a b i).1)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ g (F.intervalGapsWithin h a b ↑k).1 / g (F.intervalGapsWithin h a b ↑0).1 *
      (g (F.intervalGapsWithin h a b ↑k).2 / g (F.intervalGapsWithin h a b ↑k).1) =
    g b / g a
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:
n

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
⊢ g₁ n = g₂ n → g₁ (s • n) = g₂ (s • n)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (List.sym (n + 1) (x :: xs)).Nodup

Tactic:
rw [List.sym]

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs).Nodup
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ f ≍ f'

Tactic:
rw [e]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
hr : Std.Symm r
⊢ Disjoint diagSet (fromRel hr) ↔ Std.Irrefl r

Tactic:
by
  simp [Set.disjoint_left, Sym2.forall, irrefl_def]

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

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
G : Prefunctor V W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = G

Tactic:
obtain ⟨Gobj, Gmap⟩ := G

Goal state after:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
Gobj : V → W
Gmap : {X Y : V} → (X ⟶ Y) → (Gobj X ⟶ Gobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Gobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Gobj, map := Gmap }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = { obj := Gobj, map := Gmap }
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ uncurry Sym2.mk '' (fun p ↦ (f p.1, f p.2)) '' s ×ˢ s = Sym2.map f '' uncurry Sym2.mk '' s ×ˢ s

Tactic:
image_image,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (fun x ↦ uncurry Sym2.mk (f x.1, f x.2)) '' s ×ˢ s = (fun x ↦ Sym2.map f (uncurry Sym2.mk x)) '' s ×ˢ s
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
G : C ⥤ D
e : F ≅ G
X✝ Y✝ : C
f : G.obj X✝ ⟶ G.obj Y✝
⊢ G.map (hF.preimage (e.hom.app X✝ ≫ f ≫ e.inv.app Y✝)) = f

Tactic:
by simp [← NatIso.naturality_1 e]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Faithful
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ F.map a₁✝ = F.map a₂✝

Tactic:
rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]

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

Goal state before:
pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))

Tactic:
· rintro X Y f
    cases f
    · rfl
    · exact hΦinv (Sum.inl _)

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : g = eqToHom ⋯ ≫ f
⊢ eqToHom p ≫ g = f

Tactic:
by simp [h]

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

Tactic:
← H.map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f ≫ τ.app Y) = H.map (τ.app X) ≫ H.map (Y✝.map f)
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
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f ≫ τ.app Y) = H.map (τ.app X) ≫ H.map (Y✝.map f)

Tactic:
← H.map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f ≫ τ.app Y) = H.map (τ.app X ≫ Y✝.map f)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (Cᵒᵖ ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ (unop Y).rightOpLeftOpIso.op.hom =
      (unop X).rightOpLeftOpIso.op.hom ≫
        ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯,
                map_comp := ⋯ }).map
          f

Tactic:
intro F G η

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
⊢ (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map η ≫ (unop G).rightOpLeftOpIso.op.hom =
    (unop F).rightOpLeftOpIso.op.hom ≫
      ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯, map_comp := ⋯ }).map
        η
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mpr
X Y : Type u
f : X → Y
H : Function.Injective f
Z✝ : Type u
g g' : Z✝ ⟶ X
h : g ≫ ↾f = g' ≫ ↾f
x y : Z✝
⊢ (fun x ↦ f ∘ x) (⇑(ConcreteCategory.hom g)) y = (fun x ↦ f ∘ x) (⇑(ConcreteCategory.hom g')) y

Tactic:
exact ConcreteCategory.congr_hom h y

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

Goal state before:
pp: case mpr
X Y : Type u
f : X → Y
H : Function.Surjective f
Z✝ : Type u
g g' : Y ⟶ Z✝
h : ↾f ≫ g = ↾f ≫ g'
x : Y
y : X
⊢ (fun g ↦ g ∘ f) (⇑(ConcreteCategory.hom g)) y = (fun g ↦ g ∘ f) (⇑(ConcreteCategory.hom g')) y

Tactic:
exact ConcreteCategory.congr_hom h y

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.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)

Tactic:
simp only [isomorphisms.iff]

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ IsIso f → IsIso (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.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)

Tactic:
simp only [isomorphisms.iff]

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

Goal state before:
pp: R S : GrpCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ (ConcreteCategory.hom i) r = 1

Tactic:
by simp [h]

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

Goal state before:
pp: R S : CommGrpCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ (ConcreteCategory.hom i) r = 1

Tactic:
by simp [h]

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

Goal state before:
pp: X Y : CommGrpCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGrpCat).map f)
i : (forget CommGrpCat).obj X ≅ (forget CommGrpCat).obj Y := asIso ((forget CommGrpCat).map f)
e : ↑X ≃* ↑Y :=
  let __src := i.toEquiv;
  { toEquiv := __src, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toCommGrpIso.isIso_hom

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

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 adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ 𝟙 (G.obj X) = adj'.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)

Tactic:
Adjunction.right_triangle_components

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ 𝟙 (G.obj X) = 𝟙 (G.obj X)
Module: Mathlib.CategoryTheory.Adjunction.Basic

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' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k
⊢ F.map f ≫ g = h ≫ k

Tactic:
by simpa only [Equiv.symm_apply_apply]
      using homEquiv_naturality_right_square adj _ _ _ _ w

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
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ f = f'

Tactic:
rw [h.hom_lift f, h.hom_lift f']

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ h.lift { pt := W, π := { app := fun b ↦ f ≫ t.π.app b, naturality := ⋯ } } =
    h.lift { pt := W, π := { app := fun b ↦ f' ≫ t.π.app b, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Adjunction.Basic

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
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : f = F.map g ≫ adj.counit.app B
⊢ adj.unit.app A ≫ G.map f = g

Tactic:
by simp [h]

Goal state after: