mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p + k.factorization p ≤ n

Tactic:
have hdisj : Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
        {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
      simp +contextual [Finset.disjoint_right, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
    rw [factorization_choose hp hkn (lt_succ_self _), factorization_eq_card_pow_dvd_of_lt hp
      hk0.bot_lt (lt_of_le_of_lt hkn <| Nat.pow_lt_pow_succ hp.one_lt), log_pow hp.one_lt,
      ← card_union_of_disjoint hdisj, filter_union_right]
    have filter_le_Ico := (Ico 1 n.succ).card_filter_le
      fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
    rwa [card_Ico 1 n.succ] at filter_le_Ico

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a ∣ b

Tactic:
prime_dvd_prime_iff_eq pa pb

Goal state after:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a = b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
n : ℕ
hn : n ≠ 0
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n

Tactic:
simp only [zero_dvd_iff, hn, false_iff, not_forall]

Goal state after:
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ ∃ x x_1, ∃ (_ : Prime x) (_ : x ^ x_1 ∣ 0), ¬x ^ x_1 ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).factorization = (a.gcd b).factorization + a.factorization ⊔ b.factorization

Tactic:
factorization_gcd ha hb,

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
coprime : m'.Coprime n'
pow_eq : a ^ m' = b ^ n'
⊢ ∃ c, a = c ^ (n / g) ∧ b = c ^ (m / g)

Tactic:
exact exists_eq_pow_of_exponent_coprime_of_pow_eq_pow coprime pow_eq

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = (p ^ (q.natDegree + 1) * r).natDegree
⊢ False

Tactic:
natDegree_mul' hpnr0,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = (p ^ (q.natDegree + 1)).natDegree + r.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f g : R[X]
⊢ derivative (f * g) = derivative f * g + f * derivative g

Tactic:
induction f using Polynomial.induction_on' with

Goal state after:
case monomial
R : Type u
inst✝ : Semiring R
g : R[X]
m : ℕ
a : R
⊢ derivative ((monomial m) a * g) = derivative ((monomial m) a) * g + (monomial m) a * derivative g
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f y %ₘ map f x = 0 ↔ y %ₘ x = 0

Tactic:
←
    map_modByMonic f hx

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ C (1 + 1) * p ^ 1 * derivative p = C 2 * p * derivative p

Tactic:
one_add_one_eq_two,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ C 2 * p ^ 1 * derivative p = C 2 * p * derivative p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
⊢ (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q

Tactic:
by
  simp [sub_eq_add_neg, add_modByMonic, neg_modByMonic]

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

Goal state before:
pp: case right
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ b, ↑b
w✝ : Set ↑(range f)
left✝² : w✝.Finite
V : ↑(range f) → Set α
hVs : ∀ (i : ↑(range f)), V i ∈ ↑i
left✝¹ : ∀ i ∉ w✝, V i = univ
left✝ : s = ⋂ i ∈ w✝, V i
hVU' : s = ⋂ i, V i
⊢ s = ⋂ i, (V ∘ rangeFactorization f) i

Tactic:
rw [hVU', ← rangeFactorization_surjective.iInter_comp, comp_def]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
this : update g i x ∈ I'.pi t
⊢ x ∈ s i

Tactic:
simpa using hts this i hi

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x

Tactic:
rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

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

Goal state before:
pp: α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Tactic:
rw [← not_iff_not]
  simp [hI]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔
    ∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)

Tactic:
simpa only [Set.prod_subset_iff] using! @mem_prod_iff α β p f g

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : f.NeBot
⊢ map Prod.snd (f ×ˢ g) = g

Tactic:
by
  rw [prod_comm, map_map]; apply map_fst_prod

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
⊢ (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g

Tactic:
by
  rw [prod_inf_prod, inf_idem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂

Tactic:
by
  rw [prod_inf_prod, inf_idem]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset (Associates M)
⊢ ∀ (a : Associates M) (s : Multiset (Associates M)),
    (s.prod = 1 ↔ ∀ a ∈ s, a = 1) → ((a ::ₘ s).prod = 1 ↔ ∀ a_2 ∈ a ::ₘ s, a_2 = 1)

Tactic:
by simp +contextual [mul_eq_one, or_imp, forall_and]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ normalizedFactors 1 = 0

Tactic:
· rw [← Multiset.rel_zero_right]
    apply factors_unique irreducible_of_normalized_factor
    · intro x hx
      exfalso
      apply Multiset.notMem_zero x hx
    · apply prod_normalizedFactors one_ne_zero

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
    gcd (p.coeff p.natDegree) (p.eraseLead.support.gcd p.eraseLead.coeff)

Tactic:
eraseLead_support

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
⊢ gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
    gcd (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i ↦ (X - C ((algebraMap R (FractionRing R)) i)) ^ rootMultiplicity i p) a b

Tactic:
exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b ~ᵤ 0

Tactic:
← ha

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b ~ᵤ a
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✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
rw [le_rootMultiplicity_iff hmap, ← Multiset.prod_replicate, ←
    Multiset.map_replicate fun a => X - C a]

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a ↦ X - C a) (replicate (count b (Multiset.map (⇑f) p.roots)) b)).prod ∣ map f p
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ p.primPart.eraseLead.degree < p.primPart.degree

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ q.primPart.degree ≠ ⊥

Tactic:
· apply degree_erase_lt p.primPart_ne_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ q.primPart.degree ≠ ⊥
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ (X ^ n).rootSet S = {0}

Tactic:
by
  rw [← one_mul (X ^ n : R[X]), ← C_1, rootSet_C_mul_X_pow hn]
  exact one_ne_zero

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y : Associates D[X] := Associates.mk f
hy : y ≠ 0
H : Type (max 0 u) := { x // x ∣ y }
hfin : Fintype H := fintypeSubtypeDvd y hy
i : G → H := fun x ↦ ⟨Associates.mk ↑x, ⋯⟩
⊢ Fintype G

Tactic:
refine Fintype.ofInjective i fun x y heq ↦ ?_

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y✝ : Associates D[X] := Associates.mk f
hy : y✝ ≠ 0
H : Type (max 0 u) := { x // x ∣ y✝ }
hfin : Fintype H := fintypeSubtypeDvd y✝ hy
i : G → H := fun x ↦ ⟨Associates.mk ↑x, ⋯⟩
x y : G
heq : i x = i y
⊢ x = y
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
inst✝ : Countable R
⊢ lift.{?u.26, v} #↑{x | IsAlgebraic R x} ≤ ℵ₀

Tactic:
apply (cardinalMk_lift_le_max R A).trans

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
inst✝ : Countable R
⊢ max (lift.{v, u} #R) ℵ₀ ≤ ℵ₀
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : DirectLimit F₁ f₁
w : DirectLimit F₂ f₂
x✝⁵ : (i : ι) × F₁ i
x✝⁴ : (i : ι) × F₂ i
x✝³ : (i : ι) × F₁ i
x✝² : (i : ι) × F₂ i
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
j : ι
hx : x✝⁵.fst ≤ j
hyj : x✝³.fst ≤ j
jeq : (f₁ x✝⁵.fst j hx) x✝⁵.snd = (f₁ x✝³.fst j hyj) x✝³.snd
k : ι
hyk : x✝⁴.fst ≤ k
hz : x✝².fst ≤ k
keq : (f₂ x✝⁴.fst k hyk) x✝⁴.snd = (f₂ x✝².fst k hz) x✝².snd
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ↑(lift₂Aux f₁ f₂ ih compat x✝⁵ x✝⁴) = ↑(lift₂Aux f₁ f₂ ih compat x✝³ x✝²)

Tactic:
simp_rw [(lift₂Aux ..).2 _ (hx.trans hji) (hyk.trans hki),
        (lift₂Aux ..).2 _ (hyj.trans hji) (hz.trans hki),
        ← map_map' _ hx hji, jeq, ← map_map' _ hz hki, ← keq, map_map']

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

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ 0 ⊆ (fun x ↦ (monomial x) 1) ⁻¹' ↑1

Tactic:
simp only [monomial, AddMonoidAlgebra.lsingle_apply, zero_subset, mem_preimage,
      ← AddMonoidAlgebra.one_def, SetLike.mem_coe, Submodule.mem_one, algebraMap_eq]

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ ∃ y, C y = 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✝³ : (i : ι) → Mul (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarMul (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧) = star ⟦⟨i, x✝⟩⟧ * star ⟦⟨i, x✝¹⟩⟧

Tactic:
simp_rw [mul_def, star_def, star_mul, mul_def]

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

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding a)) (range (b + 1 - a).toNat) ↔ a ≤ x ∧ x ≤ b

Tactic:
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + ↑a_1 = x) ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding a)) (range (b - a).toNat) ↔ a ≤ x ∧ x < b

Tactic:
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + ↑a_1 = x) ↔ a ≤ x ∧ x < b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (range (b - a).toNat) ↔ a < x ∧ x ≤ b

Tactic:
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + 1 + ↑a_1 = x) ↔ a < x ∧ x ≤ b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (range (b - a - 1).toNat) ↔ a < x ∧ x < b

Tactic:
simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply,
      addLeftEmbedding_apply]

Goal state after:
a b x : ℤ
⊢ (∃ a_1 < (b - a - 1).toNat, a + 1 + ↑a_1 = x) ↔ a < x ∧ x < b
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ico (-(↑m + 1)) (↑n + 1) = Ico (-↑m) ↑n ∪ {-(↑m + 1), ↑n}

Tactic:
ext
  simp only [mem_Ico, union_insert, union_singleton, mem_insert]
  omega

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

Goal state before:
pp: case cons
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ x :: xs
hb : b ∈ x :: xs
⊢ s(a, b) ∈ (x :: xs).sym2

Tactic:
rw [mem_sym2_cons_iff]
    grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.sym2 = image (Function.uncurry Sym2.mk) (s ×ˢ s)

Tactic:
ext ⟨a, b⟩

Goal state after:
case mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : Sym2 α
a b : α
⊢ Quot.mk (Sym2.Rel α) (a, b) ∈ s.sym2 ↔ Quot.mk (Sym2.Rel α) (a, b) ∈ image (Function.uncurry Sym2.mk) (s ×ˢ s)
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Sym2 α
⊢ s.inf = t.inf ∧ s.sup = t.sup ↔ s = t

Tactic:
induction s with | _ a b

Goal state after:
case h
α : Type u_1
inst✝ : LinearOrder α
t : Sym2 α
a b : α
⊢ s(a, b).inf = t.inf ∧ s(a, b).sup = t.sup ↔ s(a, b) = t
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ Set.range diag = diagSet

Tactic:
ext ⟨a, b⟩

Goal state after:
case mk
α : Type u_1
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ Set.range diag ↔ Quot.mk (Rel α) (a, b) ∈ diagSet
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ diagSet = fromRel ⋯

Tactic:
ext ⟨a, b⟩

Goal state after:
case mk
α : Type u_1
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ diagSet ↔ Quot.mk (Rel α) (a, b) ∈ fromRel ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ diagSetᶜ = fromRel ⋯

Tactic:
ext ⟨a, b⟩

Goal state after:
case mk
α : Type u_1
x✝ : Sym2 α
a b : α
⊢ Quot.mk (Rel α) (a, b) ∈ diagSetᶜ ↔ Quot.mk (Rel α) (a, b) ∈ fromRel ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Std.Symm r
f : α → β
⊢ fromRel ⋯ = map f '' fromRel hr

Tactic:
ext ⟨a, b⟩

Goal state after:
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
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y a✝ : α
⊢ a✝ ∈ s(x, y).toFinset ↔ a✝ ∈ {x, y}

Tactic:
simp [← Sym2.mem_toFinset, ← Sym2.mem_iff]

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

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ y✝ : α
⊢ [(x✝, y✝).2].Perm [(x✝, y✝).2]

Tactic:
apply List.Perm.refl

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

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := G_obj, map := map✝ }.map f))
⊢ F_obj = G_obj

Tactic:
by
    ext X
    apply h_obj

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f ≫ h = f ↔ h = 𝟙 Y

Tactic:
by
  convert! cancel_epi f
  simp

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ (↑f • ↑g) x✝¹ x✝ = (↑f • ↑g) x✝ x✝¹

Tactic:
Pi.smul_apply',

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ (↑f x✝¹ • ↑g x✝¹) x✝ = (↑f • ↑g) x✝ x✝¹
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ (↑f x✝¹ • ↑g x✝¹) x✝ = (↑f • ↑g) x✝ x✝¹

Tactic:
Pi.smul_apply',

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ ↑f x✝¹ x✝ • ↑g x✝¹ x✝ = (↑f • ↑g) x✝ x✝¹
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ ↑f x✝¹ x✝ • ↑g x✝¹ x✝ = (↑f • ↑g) x✝ x✝¹

Tactic:
Pi.smul_apply',

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ ↑f x✝¹ x✝ • ↑g x✝¹ x✝ = (↑f x✝ • ↑g x✝) x✝¹
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ ↑f x✝¹ x✝ • ↑g x✝¹ x✝ = (↑f x✝ • ↑g x✝) x✝¹

Tactic:
Pi.smul_apply',

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.43
R : Type ?u.14
N : Type ?u.13
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ ↑f x✝¹ x✝ • ↑g x✝¹ x✝ = ↑f x✝ x✝¹ • ↑g x✝ x✝¹
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
s : Set α
z : Sym2 α
⊢ z ∈ s.sym2 ↔ ↑z ⊆ s

Tactic:
induction z using Sym2.inductionOn
  simp [pair_subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (f '' s).sym2 = Sym2.map f '' s.sym2

Tactic:
simp_rw [sym2_eq_mk_image, prod_image_image_eq, image_image, uncurry, Sym2.map_mk]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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

Tactic:
by
  rw [p]
  exact 𝟙 _

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ F.map e.inv = eqToHom ⋯ ≫ G.map e.inv ≫ eqToHom ⋯

Tactic:
simp only [← IsIso.Iso.inv_hom e, Functor.map_inv, h₂, IsIso.inv_comp, inv_eqToHom,
    Category.assoc]

Goal state after: