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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
⊢ ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
⊢ ∀ (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = n.primeFactorsList.prod

Tactic:
refine (prod_primeFactorsList ?_).symm

Goal state after:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
by_cases hb : b ∈ H

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n m : ℕ
h : m ∣ n
a : ZMod m
⊢ ∃ a_1, (castHom h (ZMod m)) a_1 = a

Tactic:
obtain ⟨a, rfl⟩ := intCast_surjective a; exact ⟨a, map_intCast ..⟩

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), (castHom ⋯ R) a = 0 → a = 0

Tactic:
intro x

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
x : ZMod n
⊢ (castHom ⋯ R) x = 0 → x = 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0

Tactic:
grw [← hx]

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ x + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ ∀ ⦃x : ℕ⦄, x ∈ m.divisors → x ∈ n.properDivisors

Tactic:
intro x

Goal state after:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
⊢ x ∈ m.divisors → x ∈ n.properDivisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal

Tactic:
by
  rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (↑H.unit).val.Coprime n
⊢ m.Coprime n

Tactic:
rw [IsUnit.unit_spec, val_natCast, Nat.coprime_iff_gcd_eq_one] at H'

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.Coprime n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun

Tactic:
intro x

Goal state after:
case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
x : ZMod (0 * 1)
⊢ inv_fun (to_fun x) = x
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun

Tactic:
intro x

Goal state after:
case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
x : ZMod (1 * 0)
⊢ inv_fun (to_fun x) = x
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ LeftInverse inv_fun to_fun

Tactic:
intro x

Goal state after:
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ inv_fun (to_fun x) = x
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors

Tactic:
intro x

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
⊢ x ∈ ↑n.divisors → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑n.divisors → n / x = n / x₂ → x = x₂
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors

Tactic:
intro x hx y hy h

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
y : ℕ
hy : y ∈ ↑n.divisors
h : n / x = n / y
⊢ x = y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
S : Type u_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : SetLike S G
inst✝¹ : AddSubgroupClass S G
K : S
inst✝ : Module (ZMod n) G
x : G
hx : x ∈ K
⊢ ∀ (a : ZMod n), a • x ∈ K

Tactic:
simpa [ZMod.forall, Int.cast_smul_eq_zsmul] using zsmul_mem hx

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = ↑n → multiplicity a b = n

pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ multiplicity a b = n → emultiplicity a b = ↑n

Tactic:
· exact multiplicity_eq_of_emultiplicity_eq_some

Goal state after:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ multiplicity a b = n → emultiplicity a b = ↑n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case ind.succ
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
i : ℕ
⊢ ((b + 2).digits n.succ)[i + 1]?.getD 0 = n.succ / (b + 2) ^ (i + 1) % (b + 2)

Tactic:
· simp [IH _ (le_of_lt_succ (div_lt_self' n b)), pow_succ', Nat.div_div_eq_div_mul]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n e : ℕ
⊢ 0 < e → n < 10 ^ e → n.repr.length ≤ e

Tactic:
simpa [Nat.repr] using toDigits_length _ _ _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ y ^ n = 1

Tactic:
rw [← isConj_one_right, ← eq']

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj (x ^ n) (y ^ n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ ∀ x ∈ d :: L, x < b

Tactic:
intro x

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
⊢ x ∈ d :: L → x < b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ ∀ (a : α) (s : Finset α),
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert a s).prod g).factorization = ∑ x ∈ insert a s, (g x).factorization

Tactic:
intro x

Goal state after:
case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
⊢ ∀ (s : Finset α),
    x ∈ S →
      s ⊆ S →
        x ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert x s).prod g).factorization = ∑ x ∈ insert x s, (g x).factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
by_cases h0 : orderOf x = 0

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by
  rw [← add_tsub_cancel_of_le hf, Finsupp.prod_add_index' (by simp) Nat.pow_add,
    prod_factorization_pow_eq_self hn]
  apply n.dvd_mul_right

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℤ
⊢ FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0

Tactic:
by
  rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
    pos_iff_ne_zero, Int.natAbs_ne_zero]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
by_cases h0 : orderOf x = 0

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i ∈ Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) =
    ∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, (n - k) / p ^ i + #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})

Tactic:
simp [sum_add_distrib, sum_boole]

Goal state after:
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
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ ((p ^ n).choose k).factorization p + k.factorization p ≤ n

Tactic:
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]

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
← add_right_inj (a.gcd b).factorization,

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.gcd b).factorization + (a.lcm b).factorization = (a.gcd b).factorization + a.factorization ⊔ b.factorization
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x

Tactic:
← divOf_add_modOf x g,

Goal state after:
case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
by
        have hXp0 : divX p ≠ 0 := by
          simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
        have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
        have : degree (C (p.coeff 0)) < degree (divX p * X) :=
          calc
            degree (C (p.coeff 0)) ≤ 0 := degree_C_le
            _ < 1 := by decide
            _ = degree (X : R[X]) := degree_X.symm
            _ ≤ degree (divX p * X) := by
              rw [← zero_add (degree X), degree_mul' this]
              exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl
        rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
r : R
⊢ (expand R p) ((expand R q) (C r)) = (expand R (p * q)) (C r)

Tactic:
expand_C

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
r : R
⊢ (expand R 1) (C r) = C r

Tactic:
expand_C

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
r : R
⊢ C r = C r
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
x✝ : X ∣ f
g : R[X]
hfg : f = X * g
⊢ (X * g).coeff 0 = 0

Tactic:
coeff_X_mul_zero

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
x✝ : X ∣ f
g : R[X]
hfg : f = X * g
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ f = C r ↔ f = (expand R p) (C r)

Tactic:
expand_C

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ f = C r ↔ f = C r
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p

Tactic:
exact pow_rootMultiplicity_not_dvd h a

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity x (X - C y) = 1

pp: case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (X - C y) = 0

Tactic:
· rw [hxy]
    exact rootMultiplicity_X_sub_C_self

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (X - C y) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ Set.InjOn (fun x ↦ (x.1 * p, x.2 * p)) ↑(antidiagonal n)

Tactic:
intro x

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ ↑(antidiagonal n) →
    ∀ ⦃x₂ : ℕ × ℕ⦄, x₂ ∈ ↑(antidiagonal n) → (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) x₂ → x = x₂
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree < ↑q.natDegree + ↑(p /ₘ q).natDegree

Tactic:
exact
        Nat.cast_lt.2
          (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
            by simpa [degree_eq_natDegree hq.ne_zero] using! h0q))

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t) → t ∈ ⨅ i, l i

Tactic:
· rintro ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
    grw [← hsub]
    cases hI.nonempty_fintype
    exact iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _

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

Goal state before:
pp: case mp.inter
α : Type u
s : Set (Set α)
U s✝ t✝ : Set α
a✝¹ : GenerateSets s s✝
a✝ : GenerateSets s t✝
t : Set (Set α)
hts : t ⊆ s
ht : t.Finite
htV : ⋂₀ t ⊆ s✝
u : Set (Set α)
hus : u ⊆ s
hu : u.Finite
huW : ⋂₀ u ⊆ t✝
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s✝ ∩ t✝

Tactic:
exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩

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

Goal state before:
pp: case mpr
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ f.IsCountablyGenerated

Tactic:
rw [h.1.eq_iInf]

Goal state after:
case mpr
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n + 1, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ (n + 1) ∣ p

Tactic:
· exact h n n.lt_succ_self

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢∂ a = ⊤

Tactic:
by rw [boundary, hnot_inf_distrib, sup_hnot_self]

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

Goal state before:
pp: case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
⊢ ∀ (x : α), x ∉ f.ker

Tactic:
intro x

Goal state after:
case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
x : α
⊢ x ∉ f.ker
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
by_cases h : s ∈ f.support

Goal state after:
case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), Prime x

Tactic:
intro x

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
x : α
⊢ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯) → Prime x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), normalize x = x

Tactic:
intro x

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
h : ¬a = 0
x : α
⊢ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯) → normalize x = x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.natDegree ≠ 0
⊢ ∀ (b : R), ((fun x ↦ eval x p) ⁻¹' {b}).Finite

Tactic:
intro x

Goal state after:
R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.natDegree ≠ 0
x : R
⊢ ((fun x ↦ eval x p) ⁻¹' {x}).Finite
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
mem_roots',

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

Goal state before:
pp: case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ ∀ x ∈ 0, Irreducible x

Tactic:
intro x

Goal state after:
case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
x : α
⊢ x ∈ 0 → Irreducible x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
⊢ f s ≤ degree f

Tactic:
by_cases h : s ∈ f.support

Goal state after:
case pos
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∈ f.support
⊢ f s ≤ degree f

case neg
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ f s ≤ degree f
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
⊢ ∀ (a_1 : R), count a_1 (Multiset.map f (p.comp (C a * X + C b)).roots) = count a_1 p.roots

Tactic:
intro x

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
x : R
⊢ count x (Multiset.map f (p.comp (C a * X + C b)).roots) = count x p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case hf
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ ∀ x_1 ∈ normalizedFactors x + normalizedFactors y, Irreducible x_1

Tactic:
intro x

Goal state after:
case hf
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
⊢ x ∈ normalizedFactors x✝ + normalizedFactors y → Irreducible x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ k • normalizedFactors p = Multiset.replicate k (normalize p)

Tactic:
normalizedFactors_irreducible hp,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ k • {normalize p} = Multiset.replicate k (normalize p)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod

Tactic:
apply Multiset.prod_dvd_prod_of_le

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
⊢ ∀ {a_1 : α}, a_1 ∈ normalizedFactors a → a_1 ∉ normalizedFactors b

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
⊢ x ∈ normalizedFactors a → x ∉ normalizedFactors b