mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : (a ^ n₁)⁻¹ * a ^ n₂ ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
← zpow_natCast,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : (a ^ ↑n₁)⁻¹ * a ^ n₂ ∈ H
⊢ a ^ (n₂ - n₁) ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : (a ^ ↑n₁)⁻¹ * a ^ n₂ ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
← zpow_natCast,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : (a ^ ↑n₁)⁻¹ * a ^ ↑n₂ ∈ H
⊢ a ^ (n₂ - n₁) ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val = ↑a

Tactic:
ZMod.natCast_val,

Goal state after:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ (↑a).cast = ↑a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ℤ
c : ℕ
⊢ ↑a = ↑b ↔ ↑c ∣ b - a

Tactic:
rw [ZMod.intCast_eq_intCast_iff, Int.modEq_iff_dvd]

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

Goal state before:
pp: a b : ℕ
⊢ ↑a = 0 ↔ b ∣ a

Tactic:
← Nat.cast_zero,

Goal state after:
a b : ℕ
⊢ ↑a = ↑0 ↔ b ∣ a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.relIndex K ≠ 0 ↔ (H.subgroupOf K).FiniteIndex

Tactic:
finiteIndex_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.relIndex K ≠ 0 ↔ (H.subgroupOf K).index ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex

Tactic:
finiteIndex_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.IsFiniteRelIndex ⊤ ↔ H.index ≠ 0
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: case succ
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
n : ℕ
inst✝ : Module (ZMod (n + 1)) R
r : ℕ
⊢ ↑r • 1 * x = ↑r • x ∧ x * ↑r • 1 = ↑r • x

Tactic:
simp [Nat.cast_smul_eq_nsmul, Nat.cast_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
n a b : ℕ
⊢ a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b

Tactic:
rintro ⟨rfl, hab⟩
    rw [mul_ne_zero_iff] at hab
    simpa [hab.1, hab.2] using Nat.le_mul_of_pos_right _ hab.2.bot_lt

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
by
  obtain rfl | hn := eq_or_ne n 0
  · simp
  refine (List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ ?_
  simp only [Option.ite_none_right_eq_some, Option.some.injEq, gt_iff_lt,
    and_imp, Prod.forall, Prod.mk.injEq]
  rintro a b hab _ _ ha rfl rfl _ _ hb rfl rfl
  rwa [Nat.div_lt_div_left hn ⟨_, hb.symm⟩ ⟨_, ha.symm⟩]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1

Tactic:
by
  refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
  · rw [geom_sum_two]
    exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩
  clear hn
  intro n _ ihn
  rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]
  exact
    ⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
      mul_neg_of_neg_of_pos hx ihn.1⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : 0 < x + 1
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
· have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
    split_ifs at this
    · exact this.ne
    · exact (zero_lt_one.trans this).ne'

Goal state after:
case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : 0 < x + 1
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : ∑ x ∈ n.properDivisors, x ∣ n
⊢ ∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n

Tactic:
by
  rcases n with - | n
  · simp
  · rcases n with - | n
    · simp at h
    · rw [or_iff_not_imp_right]
      intro ne_n
      have hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ :=
        lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n
      symm
      rw [← mem_singleton, eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
        (mem_properDivisors.2 ⟨h, hlt⟩)) (sum_singleton _ _), mem_properDivisors]
      exact ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range k)

Tactic:
simp [mem_properDivisors_prime_pow pp, eq_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
hn1 : 0 < n1 ∧ n1 ≤ N
hn2 : 0 < n2 ∧ n2 ≤ N
hn3 : n1 * n2 = n
⊢ n1 * n2 = n ∧ ¬n = 0

Tactic:
exact ⟨hn3, n_ne_zero⟩

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

Goal state before:
pp: n : ℕ
⊢ Nontrivial (ZMod n) ↔ n ≠ 1

Tactic:
rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1 + 1).choose (k + 1) ≤ 2 ^ (n + 1)

Tactic:
· rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

Goal state after:
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ (2 * n + 2).choose (n + 1) * (n + 1) = (2 * n + 1).choose n * (2 * n + 2)

Tactic:
choose_succ_right_eq,

Goal state after:
n : ℕ
⊢ (2 * n + 2).choose n * (2 * n + 2 - n) = (2 * n + 1).choose n * (2 * n + 2)
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
  rcases lt_trichotomy n 4 with (hn | rfl | hn)
  · clear IH; exact False.elim ((not_lt.2 n_big) hn)
  · norm_num [centralBinom, choose]
  obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.ne_zero_of_lt hn)
  calc
    4 ^ (n + 1)
    _ = 4 * 4 ^ n := by rw [pow_succ']
    _ < 4 * (n * centralBinom n) := by gcongr; exact IH n n.lt_succ_self (Nat.le_of_lt_succ hn)
    _ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
    _ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm

Goal state after:
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
have hk : k = (p.maxPowDvdDiv n).1 := by
      · apply Nat.le_antisymm
        · rw [← padicValNat, ← pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn,
            pow_dvd_iff_le_of_spec hp hn h hl]
          apply Nat.le_refl
        · rw [← pow_dvd_iff_le_of_spec hp hn h hl, pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn]
          apply Nat.le_refl
    rw [← pow_padicValNat_mul_divMaxPow p n, hk, padicValNat, Nat.mul_left_cancel_iff] at h
    · exact Prod.ext hk.symm h.symm
    · exact Nat.pow_pos <| Nat.zero_lt_of_lt hp

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

Goal state before:
pp: case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
len : L.length = l.length
eqd : D = d
h : ofDigits b L = ofDigits b l
this : L = l
⊢ D :: L = d :: l

Tactic:
eqd,

Goal state after:
case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
len : L.length = l.length
eqd : D = d
h : ofDigits b L = ofDigits b l
this : L = l
⊢ d :: L = d :: l
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
nh : ∀ (n : ℕ), a ^ (n + 1) ∣ b
⊢ False

Tactic:
simp [nh] at h

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
ha

Goal state after:
a b : ℕ
h : ∀ (n : ℕ), 0 ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Tactic:
exact hm.or_of_add

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

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digitsAppend l (ofDigits b L)).length = l

Tactic:
length_digitsAppend hb _ (mapsTo_ofDigits hb _ hL)

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ l = l
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) ↑(fixedLengthDigits hb l) ↑(Finset.range (b ^ l))

Tactic:
rw [fixedLengthDigits, Set.coe_toFinset]
  convert! bijOn_ofDigits hb l
  ext; simp

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

Goal state before:
pp: b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ (a✝.length = 1 ∧ ∀ x ∈ a✝, x < b) ↔ a✝ ∈ Finset.image (fun x ↦ [x]) (Finset.range b)

Tactic:
List.length_eq_one_iff

Goal state after:
b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ ((∃ a, a✝ = [a]) ∧ ∀ x ∈ a✝, x < b) ↔ a✝ ∈ Finset.image (fun x ↦ [x]) (Finset.range b)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p a ≤ emultiplicity p b

Tactic:
exact le_of_lt hab

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
rw [emultiplicity_add_of_gt hab, min_eq_right]

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b ≤ emultiplicity p a
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b ≤ emultiplicity p a

Tactic:
exact le_of_lt hab

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a ≤ multiplicity p b

Tactic:
exact le_of_lt hab

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p b ≤ multiplicity p a

Tactic:
exact le_of_lt hab

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

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

pp: n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ≠ 0

Tactic:
factorization_prod_pow_eq_self_of_le_factorization hf

Goal state after:
case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ f ≤ n.factorization

n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ≠ 0
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_not_prime h

Goal state after:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
hp : Prime p
⊢ (n.choose k).factorization p ≤ log p n
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) = ↑p * (x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p))

Tactic:
rw [Nat.cast_comm, mul_assoc (_ * _)]

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) = x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) * ↑p)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
← zpow_natCast,

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ ↑(orderOf x) = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 ↦ x ^ x_1) i = y
⊢ x ^ (i % ↑(orderOf x)).natAbs = y

Tactic:
← zpow_natCast,

Goal state after:
G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 ↦ x ^ x_1) i = y
⊢ x ^ ↑(i % ↑(orderOf x)).natAbs = y
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ ∑ m ∈ n.divisors, #{x | orderOf x = m} = #{x | x ^ n = 1}

Tactic:
refine (Finset.card_biUnion ?_).symm.trans ?_
  · simp +contextual [Set.PairwiseDisjoint, Set.Pairwise, disjoint_iff, Finset.ext_iff]
  · congr; ext; simp [hn, orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ x ^ (orderOf x - 1 + 1) = 1

Tactic:
tsub_add_cancel_of_le,

Goal state after:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ x ^ orderOf x = 1

G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x✝ y : G
n : ℕ
x : G
⊢ 1 ≤ orderOf x
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
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
rw [degree_add_eq_left_of_degree_lt this]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this✝ : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
this : (C (p.coeff 0)).degree < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X).degree
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'
⊢ ∃ c, a = c ^ (n / g) ∧ b = c ^ (m / g)

Tactic:
have pow_eq : a ^ m' = b ^ n' := by
    conv_lhs at h => rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]
    conv_rhs at h => rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]
    rw [pow_mul, pow_mul] at h
    have : g ≠ 0 := by
      rcases hmn with hm | hn
      · exact gcd_ne_zero_left hm
      · exact gcd_ne_zero_right hn
    exact Nat.pow_left_injective this h

Goal state after:
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)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ ⦃x : ℕ × ℕ⦄, x ∈ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → x ∈ antidiagonal (n * p)

Tactic:
mem_image,

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

Goal state before:
pp: case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Tactic:
mem_image,

Goal state after:
case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    (¬∃ a ∈ antidiagonal n, (a.1 * p, a.2 * p) = x) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
hp : (aeval s) p = 0
hq : (aeval s) q = 0
⊢ False

Tactic:
rcases h with ⟨_, _, h⟩

Goal state after:
S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
s : S
hp : (aeval s) p = 0
hq : (aeval s) q = 0
w✝¹ w✝ : R[X]
h : w✝¹ * p + w✝ * q = 1
⊢ False
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case prime
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hprime : Nat.Prime p
hchar : CharP R p
⊢ (expand R p) (contract p f) = f

Tactic:
have := Fact.mk hchar; exact expand_contract p hf hprime.ne_zero

Goal state after:
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 x ∣ map f y ↔ x ∣ y

Tactic:
rw [← modByMonic_eq_zero_iff_dvd hx, ← modByMonic_eq_zero_iff_dvd (hx.map f), ←
    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.Div

Goal state before:
pp: case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
rw [coeff_divByMonic_X_sub_C_rec, ih, eq_comm, Icc_eq_cons_Ioc (Nat.succ_le_iff.mpr hn),
          sum_cons, Nat.sub_self, pow_zero, one_mul, mul_sum]
      congr 1; refine sum_congr ?_ fun i hi ↦ ?_
      · ext; simp
      rw [← mul_assoc, ← pow_succ', eq_comm, i.sub_succ', Nat.sub_add_cancel]
      apply Nat.le_sub_of_add_le
      rw [add_comm]; exact (mem_Icc.mp hi).1

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ p.degree < (X - C a).degree

Tactic:
apply degree_lt_degree

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ p.natDegree < (X - C a).natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : q ∣ p₁ - p₂
a✝ : Nontrivial R
⊢ p₁ %ₘ q = p₂ %ₘ q

Tactic:
obtain ⟨f, sub_eq⟩ := h

Goal state after:
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
a✝ : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₁ %ₘ q = p₂ %ₘ q
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
⊢ a ∈ {x | s x = univ}ᶜ.pi s → a ∈ univ.pi s

Tactic:
ha

Goal state after:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
⊢ a ∈ univ.pi s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 (Prod.fst ⁻¹' s) ⊔ 𝓟 (Prod.snd ⁻¹' t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Tactic:
sup_principal,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case zero
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
⊢ normalizedFactors (x ^ 0) = 0 • normalizedFactors x

Tactic:
simp [zero_nsmul]

Goal state after:
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
h : normalizedFactors x < normalizedFactors y
⊢ DvdNotUnit x y

Tactic:
exact
      dvdNotUnit_of_dvd_of_not_dvd
        ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
        (mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_ge)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : ¬n = 0
⊢ (nthRoots n a).card ≤ n

Tactic:
by
    rw [← Nat.cast_le (α := WithBot ℕ)]
    rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
    exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ nthRoots 2 1 = {-1, 1}

Tactic:
by
  have h₁ : (X ^ 2 - C 1 : R[X]) = (X + C 1) * (X - C 1) := by simp [← sq_sub_sq]
  have h₂ : (X ^ 2 - C 1 : R[X]) ≠ 0 := fun h ↦ by simpa using congrArg (coeff · 0) h
  rw [nthRoots, h₁, roots_mul (h₁ ▸ h₂), roots_X_add_C, roots_X_sub_C]; rfl

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

Goal state before:
pp: case neg.calc_2.inl
α : 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
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ Prime x

Tactic:
apply (Classical.choose_spec (pf _ _)).1 _ h

Goal state after:
α : 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
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ a ≠ 0