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

Goal state before:
pp: case inl
b p : ℕ
hab : Coprime 0 b
⊢ p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList

pp: case inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
· simp [(coprime_zero_left _).mp hab]

Goal state after:
case inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ (comap f H).relIndex K = H.relIndex (map f K)

Tactic:
relIndex,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ ((comap f H).subgroupOf K).index = H.relIndex (map f K)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ K.index * H.relIndex K = H.index

Tactic:
relIndex,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ K.index * (H.subgroupOf K).index = H.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).relIndex K = H.relIndex K

Tactic:
relIndex,

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ((H ⊓ K).subgroupOf K).index = H.relIndex K

Tactic:
relIndex,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ((H ⊓ K).subgroupOf K).index = (H.subgroupOf K).index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H

Tactic:
simp only [index_eq_two_iff', xor_iff_or_and_not_and]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ a, ∀ (b : G), (a * b ∈ H ∨ b ∈ H) ∧ ¬(a * b ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), a * b ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H = Nat.card ↥H

Tactic:
relIndex,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (⊥.subgroupOf H).index = Nat.card ↥H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊥ = 1

Tactic:
relIndex,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (H.subgroupOf ⊥).index = 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex H = 1

Tactic:
relIndex,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (H.subgroupOf H).index = 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ Nat.card ((ι → G) ⧸ pi Set.univ H) = Nat.card ((a : ι) → G ⧸ H a)

Tactic:
refine Nat.card_congr
    ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.piQuotientEquiv _).symm)

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
x y : ι → G
⊢ (QuotientGroup.leftRel (pi Set.univ H)) x y ↔ piSetoid x y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ZMod 0
⊢ a * a⁻¹ = ↑(a.val.gcd 0)

pp: case succ
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = ↑(a.val.gcd (n + 1))

Tactic:
· dsimp [ZMod] at a ⊢
    calc
      _ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]

Goal state after:
case succ
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = ↑(a.val.gcd (n + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
⊢ m % n ≡ m [MOD n]

Tactic:
by simp [Nat.ModEq]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
n : ℕ
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ↔ Prime (n + 1)

Tactic:
cases n
    · simp [Nat.not_prime_one]
    · rw [← properDivisors_eq_singleton_one_iff_prime]
      refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
      rw [@eq_comm (Finset ℕ) _ _]
      apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2
            (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
| n.divisors

Tactic:
rw [← image_fst_divisorsAntidiagonal, ← map_div_left_divisors, map_eq_image, image_image]

Goal state after:
n : ℕ
| image (Prod.fst ∘ ⇑{ toFun := fun d ↦ (n / d, d), inj' := ⋯ }) n.divisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n

Tactic:
exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h

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

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

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

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

Goal state before:
pp: b k : ℕ
hb : 1 < b
n : ℕ
⊢ k < (b.digits n).length ↔ b ^ k ≤ n

Tactic:
by
  contrapose!
  exact digits_length_le_iff hb n

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : DivisionMonoid G
x : G
⊢ IsOfFinOrder x ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1

Tactic:
rw [isOfFinOrder_iff_pow_eq_one]

Goal state after:
G : Type u_6
inst✝ : DivisionMonoid G
x : G
⊢ (∃ n, 0 < n ∧ x ^ n = 1) ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d

Tactic:
· intro h
    unfold emultiplicity
    -- aesop? says
    split
    next h_1 =>
      obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]
    next h_1 =>
      simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.natCast_ne_top, imp_false, not_false_eq_true, implies_true]

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

Goal state before:
pp: case inr
n b : ℕ
hb : 1 < b
l : ℕ
left✝ : l - (b.digits n).length ≠ 0
⊢ 0 < b

Tactic:
· linarith

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
⊢ ¬IsOfFinOrder a

Tactic:
rw [isOfFinOrder_iff_pow_eq_one]

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
⊢ ¬∃ n, 0 < n ∧ a ^ n = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → f a ^ n ∣ f b

Tactic:
rw [← map_pow]; exact map_dvd f

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: M₀ : Type u_6
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
⊢ orderOf 0 = 0

Tactic:
by
  rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one]
  simp +contextual [ne_of_gt]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x

Tactic:
rw [isOfFinOrder_iff_pow_eq_one]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ ∃ n, 0 < n ∧ x ^ n = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬p ∣ n / p ^ n.factorization p

Tactic:
by
  rw [Nat.Prime.dvd_iff_one_le_factorization hp (ordCompl_pos p hn).ne']
  rw [Nat.factorization_div (Nat.ordProj_dvd n p)]
  simp [hp.factorization]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ x ^ ↑i = 1

Tactic:
zpow_natCast,

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ x ^ i = 1
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
zpow_natCast,

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
h' : y ∈ zpowers x
⊢ IsOfFinOrder y

Tactic:
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h'

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
h : IsOfFinOrder x
k : ℤ
h' : x ^ k ∈ zpowers x
⊢ IsOfFinOrder (x ^ k)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G₀ : Type u_6
inst✝¹ : GroupWithZero G₀
inst✝ : Finite G₀
a : G₀
⊢ orderOf a = 0 ↔ a = 0

Tactic:
have : Finite G₀ˣ := .of_injective _ Units.val_injective

Goal state after:
G₀ : Type u_6
inst✝¹ : GroupWithZero G₀
inst✝ : Finite G₀
a : G₀
this : Finite G₀ˣ
⊢ orderOf a = 0 ↔ a = 0
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * x).coeff g' = 0

Tactic:
coeff_single_mul_of_forall_add_ne

Goal state after:
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ 0 = 0

case inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ ∀ (d : G), g + d ≠ g'
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
⊢ _root_.Pairwise (Function.onFun Coprime fun p ↦ ↑p ^ n.factorization ↑p)

Tactic:
by
  intro p1 p2 hp
  refine Nat.Coprime.pow (n.factorization p1) (n.factorization p2) ?_
  refine (Nat.coprime_primes ?_ ?_).mpr <| Subtype.coe_ne_coe.mpr hp
  · exact Nat.prime_of_mem_primeFactors p1.2
  · exact Nat.prime_of_mem_primeFactors p2.2

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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ ↑((Nat.card G).gcd n) = (g ^ ↑(Nat.card G)) ^ (Nat.card G).gcdA n * (g ^ ↑n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
zpow_natCast,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ ↑(Nat.card G)) ^ (Nat.card G).gcdA n * (g ^ ↑n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g
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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ ↑(Nat.card G)) ^ (Nat.card G).gcdA n * (g ^ ↑n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
zpow_natCast,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ ↑n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g
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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ ↑n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
zpow_natCast,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
⊢ #({x ∈ Ioc 0 n | p ∣ x}) = n / p

Tactic:
induction n <;> simp [Nat.succ_div, add_ite, ← insert_Ioc_right_eq_Ioc_add_one, filter_insert,
    apply_ite card, *]

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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ ↑((Nat.card G).gcd n) = (g ^ ↑(Nat.card G)) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ ↑n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
zpow_natCast,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ ↑(Nat.card G)) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ ↑n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ ↑(Nat.card G)) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ ↑n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
zpow_natCast,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ ↑n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ ↑n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
zpow_natCast,

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ (Nat.card G).gcd n = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (contract p (f + g)).coeff n✝ = (contract p f).coeff n✝ + (contract p g).coeff n✝

Tactic:
coeff_contract hp,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (f + g).coeff (n✝ * p) = f.coeff (n✝ * p) + g.coeff (n✝ * p)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ (contract p (f * (expand R p) g)).coeff n = (contract p f * g).coeff n

Tactic:
coeff_contract hp,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ (f * (expand R p) g).coeff (n * p) = (contract p f * g).coeff n
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
d : ℕ
hd : ((⇑derivative)^[d] p).natDegree ≤ p.natDegree - d
⊢ (derivative ((⇑derivative)^[d] p)).natDegree ≤ p.natDegree - d - 1

Tactic:
exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
x✝ : ℕ
h : p.natDegree = x✝
⊢ (⇑derivative)^[x] p = 0

Tactic:
induction h : p.natDegree using Nat.strong_induction_on generalizing p x with

Goal state after:
case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
ih : ∀ m < n✝, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
p : R[X]
x : ℕ
hx : p.natDegree < x
h : p.natDegree = n✝
⊢ (⇑derivative)^[x] p = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ derivative (map f p) = map f (derivative p)

Tactic:
let n := max p.natDegree (map f p).natDegree
  rw [derivative_apply, derivative_apply]
  rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]
  on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
  · simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map,
      map_natCast, Polynomial.map_natCast, Polynomial.map_pow, map_X]
  all_goals intro n; rw [zero_mul, C_0, zero_mul]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * (p * X ^ (q.natDegree - p.natDegree + p.natDegree - p.natDegree)))).coeff
      (q.natDegree - p.natDegree + p.natDegree) =
    0

Tactic:
add_comm _ p.natDegree

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ (C p.leadingCoeff * q +
          -(C q.leadingCoeff * (p * X ^ (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree)))).coeff
      (p.natDegree + (q.natDegree - p.natDegree)) =
    0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p : R[X]
i : ℕ
⊢ (⇑derivative)^[i] p ≠ 0 → i ∈ range (p.natDegree + 1)

Tactic:
contrapose

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p : R[X]
i : ℕ
⊢ i ∉ range (p.natDegree + 1) → (⇑derivative)^[i] p = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1

Tactic:
simp [natDegree, degree_derivative hp]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ C (↑n + 1) * p ^ n * derivative p * p + p ^ n.succ * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p

Tactic:
mul_right_comm,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ C (↑n + 1) * p ^ n * p * derivative p + p ^ n.succ * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
x : ℕ → Set α
hx : f.HasAntitoneBasis x
⊢ ∀ {s : Set α}, s ∈ f ↔ ∃ i, x i ⊆ s

Tactic:
simp [hx.1.mem_iff]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - m).pred ∣ (⇑derivative)^[m + 1] p

Tactic:
Function.iterate_succ'

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - m).pred ∣ (⇑derivative ∘ (⇑derivative)^[m]) p
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩

Goal state after:
α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
this : Finite ↑t
s : ↑t → Set α
hsl : ∀ (i : ↑t), s i ∈ l ↑i
hsd : Pairwise (Disjoint on s)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s

Tactic:
exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩

Goal state after:
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
d : σ →₀ R
⊢ degree d = 0 ↔ d = 0

Tactic:
simp only [degree_apply, Finset.sum_eq_zero_iff, mem_support_iff, ne_eq, _root_.not_imp_self,
    DFunLike.ext_iff, coe_zero, Pi.zero_apply]

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

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Goal state after:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ihn : (0 ^ n).roots = n • roots 0
⊢ (0 ^ (n + 1)).roots = (n + 1) • roots 0

case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ ¬∃ a ∈ s, X - C a = 0

Tactic:
rintro ⟨a, -, h⟩

Goal state after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
a : R
h : X - C a = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
a : R
h : X - C a = 0
⊢ False

Tactic:
exact X_sub_C_ne_zero a h

Goal state after: