mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)

Tactic:
rename_i h

Goal state after:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
rw [hB, iInf_emptyset]
    use fun _ => i₀
    simp [h]

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

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
⊢ ∃ x, f = ⨅ i, 𝓟 (x i)

Tactic:
by
    rcases h with ⟨s, hsc, rfl⟩
    rw [generate_eq_biInf]
    exact countable_biInf_principal_eq_seq_iInf hsc

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n k : ℕ
c : R
⊢ (⇑derivative)^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k)

Tactic:
rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
⊢ ∀ (x_1 : α →₀ ℕ), mapDomain f x_1 = x → ∃ x_2, degree x_2 ≤ degree x ∧ embDomain e x_2 = x_1

Tactic:
refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ degree (comapDomain (⇑e) y ⋯) ≤ degree x

case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ ↑y.support ⊆ range ⇑e
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : p ∣ s.prod → ∃ a ∈ s, p ∣ a
h : p ∣ (a ::ₘ s).prod
⊢ p ∣ a * s.prod

Tactic:
simpa using h

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
⊢ ∀ {g : Multiset α},
    (∀ x ∈ p ::ₘ f, Prime x) → (∀ x ∈ g, Prime x) → (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g

Tactic:
intro g hf hg hfg

Goal state after:
case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ Multiset.Rel Associated (p ::ₘ f) g
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
s✝ : Multiset (Associates M₀)
p : Associates M₀
hp : Prime p
a : Associates M₀
s : Multiset (Associates M₀)
ih : p ≤ s.prod → ∃ a ∈ s, p ≤ a
h : p ≤ (a ::ₘ s).prod
⊢ p ≤ a * s.prod

Tactic:
simpa using h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : q ≠ 0
⊢ p ∣ q → p.roots ≤ q.roots

Tactic:
rintro ⟨k, rfl⟩
  exact Multiset.le_iff_exists_add.mpr ⟨k.roots, roots_mul h⟩

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

Goal state before:
pp: case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hs : ∀ a ∈ 0, Irreducible a
⊢ normalizedFactors 1 = Multiset.map normalize 0

Tactic:
normalizedFactors_one,

Goal state after:
case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hs : ∀ a ∈ 0, Irreducible a
⊢ 0 = Multiset.map normalize 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Tactic:
· rw [dif_neg h, Nat.cast_lt]
      have cne0 : c ≠ 0 := by
        refine mt (fun con => ?_) h
        rw [b_eq, con, mul_zero]
      calc
        Multiset.card (Classical.choose (pf a ane0)) <
            _ + Multiset.card (Classical.choose (pf c cne0)) :=
          lt_add_of_pos_right _
            (Multiset.card_pos.mpr fun con => hc (associated_one_iff_isUnit.mp ?_))
        _ = Multiset.card (Classical.choose (pf a ane0) + Classical.choose (pf c cne0)) :=
          (Multiset.card_add _ _).symm
        _ = Multiset.card (Classical.choose (pf b h)) :=
          Multiset.card_eq_card_of_rel
          (prime_factors_unique ?_ (Classical.choose_spec (pf _ h)).1 ?_)
      · convert! (Classical.choose_spec (pf c cne0)).2.symm
        rw [con, Multiset.prod_zero]
      · intro x hadd
        rw [Multiset.mem_add] at hadd
        rcases hadd with h | h <;> apply (Classical.choose_spec (pf _ _)).1 _ h <;> assumption
      · rw [Multiset.prod_add]
        trans a * c
        · apply Associated.mul_mul <;> apply (Classical.choose_spec (pf _ _)).2 <;> assumption
        · rw [← b_eq]
          apply (Classical.choose_spec (pf _ _)).2.symm; assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
exact
    ⟨w.map e, fun b hb =>
        let ⟨c, hc, he⟩ := Multiset.mem_map.1 hb
        he ▸ (prime_iff e).2 (hp c hc),
        Units.map e.toMonoidHom u,
      by
        rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
s : Multiset { a // Irreducible a }
⊢ p.count ↑s = Multiset.count ⟨p, hp⟩ s

Tactic:
simp only [count, dif_pos hp, bcount]

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

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ ↑u * C ↑(w⁻¹ * normUnit a✝.leadingCoeff) = C ↑(normUnit a✝.leadingCoeff)

Tactic:
Units.val_mul,

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ ↑u * C (↑w⁻¹ * ↑(normUnit a✝.leadingCoeff)) = C ↑(normUnit a✝.leadingCoeff)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ C ↑(normUnit a✝.leadingCoeff * normUnit b✝.leadingCoeff) =
    C ↑(normUnit a✝.leadingCoeff) * C ↑(normUnit b✝.leadingCoeff)

Tactic:
Units.val_mul,

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ C (↑(normUnit a✝.leadingCoeff) * ↑(normUnit b✝.leadingCoeff)) =
    C ↑(normUnit a✝.leadingCoeff) * C ↑(normUnit b✝.leadingCoeff)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain A
inst✝¹ : IsDomain B
f : A →+* B
inst✝ : DecidablePred fun x ↦ x ∈ f.range
hf : Function.Injective ⇑f
p : A[X]
⊢ Multiset.filter (fun x ↦ x ∈ f.range) (map f p).roots = Multiset.map (⇑f) p.roots

Tactic:
ext b
  rw [Multiset.count_filter]
  split_ifs with h
  · obtain ⟨a, rfl⟩ := h
    simp [hf, Multiset.count_map_eq_count', eq_rootMultiplicity_map hf]
  · refine (Multiset.count_eq_zero.mpr fun h' ↦ h ?_).symm
    exact Exists.imp (fun _ ↦ And.right) <| Multiset.mem_map.mp h'

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 ↔
    (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ r ∣ s.primPart

Tactic:
← hr s.primPart

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 ↔
    (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ p.primPart ∣ s.primPart ∧ q.primPart ∣ s.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
⊢ k ∣ p.count a.factors

Tactic:
by_cases ha : a = 0
  · simpa [*] using habk
  rcases count_of_coprime ha hb hab hp with hz | h
  · rw [hz]
    exact dvd_zero k
  · rw [count_mul ha hb hp, h] at habk
    exact habk

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
⊢ (aeval x) (C ↑m * X - C r) = 0

Tactic:
by simpa [sub_eq_zero, mul_comm x] using h

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

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
halg : IsAlgebraic R a
hf : Function.Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ IsAlgebraic S (g a)

Tactic:
obtain ⟨p, h1, h2⟩ := halg
  refine ⟨p.map f, (Polynomial.map_ne_zero_iff hf).2 h1, ?_⟩
  change aeval ((g : A →+* B) a) _ = 0
  rw [← map_aeval_eq_aeval_map h, h2, map_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
A : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : NoZeroDivisors S
inst✝⁵ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul R A
⊢ FaithfulSMul S A

Tactic:
faithfulSMul_iff_algebraMap_injective

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
A : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : NoZeroDivisors S
inst✝⁵ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Function.Injective ⇑(algebraMap R A)
⊢ Function.Injective ⇑(algebraMap S A)
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
P Q : { P // Small.{u, u_2} ↥P }
⊢ Q ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
rw [← Subtype.coe_le_coe]; exact le_sup_right

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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R N
⊢ Injective ⇑(baseChangeHom R S M N)

Tactic:
intro f g h
  ext m
  simpa using Flat.tensorProduct_mk_injective R N S <| LinearMap.congr_fun h (1 ⊗ₜ[R] m)

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

Goal state before:
pp: case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(cons i s hi)).PairwiseDisjoint t
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f = fun a ↦ ∏ i ∈ cons i s hi, (t i).mulIndicator f a

Tactic:
ext j
    rw [coe_cons, Set.pairwiseDisjoint_insert_of_notMem (Finset.mem_coe.not.2 hi)] at hs
    classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ ∀ i ∈ {i ∈ t | q i}, f i = g i

Tactic:
simpa using h

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 ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a < b
⊢ ↑(#(Ioo a b)) = b - a - 1

Tactic:
rw [card_Ioo, sub_sub, toNat_sub_of_le h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

Tactic:
by
  rw [powerset_insert, prod_union, prod_image]
  · exact insert_erase_invOn.2.injOn.mono fun t ht ↦ notMem_mono (mem_powerset.1 ht) ha
  · aesop (add simp [disjoint_left, insert_subset_iff])

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Std.Symm r
f : α → β
x✝ : Sym2 β
a b : β
⊢ Quot.mk (Rel β) (a, b) ∈ fromRel ⋯ ↔ Quot.mk (Rel β) (a, b) ∈ map f '' fromRel hr

Tactic:
simp only [fromRel_prop, Relation.Map, Set.mem_image, Sym2.exists, map_mk, Sym2.eq,
    rel_iff', Prod.mk.injEq, Prod.swap_prod_mk, and_or_left, exists_or, iff_self_or,
    forall_exists_index, and_imp]

Goal state after:
case mk
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Std.Symm r
f : α → β
x✝ : Sym2 β
a b : β
⊢ ∀ (x x_1 : α), r x x_1 → f x = b → f x_1 = a → ∃ a_4 b_1, r a_4 b_1 ∧ f a_4 = a ∧ f b_1 = b
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α✝
f : α✝ → β
α : Type u_4
z : Sym2 α
⊢ { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }

Tactic:
use (Multiset.ofList [·, ·])

Goal state after:
case property
α✝ : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α✝
f : α✝ → β
α : Type u_4
z : Sym2 α
⊢ ∀ (a₁ a₂ : α), (fun x1 x2 ↦ ↑[x1, x2]) a₁ a₂ = (fun x1 x2 ↦ ↑[x1, x2]) a₂ a₁
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ reverse f = reverse (reverse g) ↔ reverse f = g

Tactic:
reverse_reverse

Goal state after:
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ reverse f = g ↔ reverse f = g
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
⊢ ({ obj := fun G ↦ X✝ ⋙ G, map := fun {X Y} α ↦ X✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.obj H).map f ≫
      H.map (τ.app Y) =
    H.map (τ.app X) ≫
      ({ obj := fun G ↦ Y✝ ⋙ G, map := fun {X Y} α ↦ Y✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.obj H).map f

Tactic:
dsimp; rw [← H.map_comp, ← H.map_comp, ← τ.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ IsIso f.unop ↔ IsIso f

Tactic:
by
  rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]

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

Goal state before:
pp: C : Type u_1
⊢ ∀ {X Y : Discrete C} (f : X ⟶ Y), X = Y

Tactic:
rintro ⟨_⟩ ⟨_⟩ ⟨⟨rfl⟩⟩

Goal state after:
C : Type u_1
as✝ : C
⊢ { as := as✝ } = { as := { as := as✝ }.as }
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
F : C ⥤ E
X : C
⊢ (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)

Tactic:
by
  dsimp [funInvIdAssoc]
  simp

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

Tactic:
← homEquiv_naturality_left_symm,

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

Goal state before:
pp: case e_8.mk
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
t : Cone F
X : C
h : F.cones.RepresentableBy X
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
m : { pt := pt✝, π := π✝ }.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = { pt := pt✝, π := π✝ }.π.app j
⊢ { pt := { pt := pt✝, π := π✝ }.pt, π := (const J).map m ≫ (limitCone h).π } = { pt := pt✝, π := π✝ }

Tactic:
congr with j

Goal state after:
case e_8.mk
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
t : Cone F
X : C
h : F.cones.RepresentableBy X
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
m : { pt := pt✝, π := π✝ }.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = { pt := pt✝, π := π✝ }.π.app j
j : J
⊢ ((const J).map m ≫ (limitCone h).π).app j = π✝.app j
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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
j : J
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h s = s.ι.app j

Tactic:
by
    have h := cocone_fac h s
    cases s
    injection h with h₁ h₂
    simp only at h₂
    conv_rhs => rw [← h₂]
    rfl

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

Goal state before:
pp: case e_8.mk
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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
m : (colimitCocone h).pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ { pt := { pt := pt✝, ι := ι✝ }.pt, ι := (colimitCocone h).ι ≫ (const J).map m } = { pt := pt✝, ι := ι✝ }

Tactic:
congr with j

Goal state after:
case e_8.mk
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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
m : (colimitCocone h).pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt✝, ι := ι✝ }.ι.app j
j : J
⊢ ((colimitCocone h).ι ≫ (const J).map m).app j = ι✝.app j
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
F : Cᵒᵖ ⥤ Type v₁
g : ((yoneda.op ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((yoneda.op ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation Cᵒᵖ (Type v₁) ⋙
                      (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                  f).app
            F)).toFun
      g

Tactic:
simpa [← ULift.down_inj] using! (yonedaEquiv_naturality _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f' } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f' }
⊢ f = f'

Tactic:
simpa using h

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : s.π.app one = s.π.app left ≫ F.map inl
h₂ : t.π.app one = t.π.app left ≫ F.map inl
⊢ s.π.app none = i.hom ≫ t.π.app none

Tactic:
simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X : CostructuredArrow S T
⊢ (eqToHom ⋯).left = eqToHom ⋯

Tactic:
simp only [eqToHom_refl, id_left]

Goal state after: