mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
a b : α
l : List α
⊢ flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)

Tactic:
induction l with
  | nil => exact Perm.swap [a, b] [b, a] []
  | cons c l ih => ?_

Goal state after:
case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ flatMap (permutations'Aux b) (permutations'Aux a (c :: l)) ~
    flatMap (permutations'Aux a) (permutations'Aux b (c :: l))
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
obtain rfl | h := eq_or_ne n 1

Goal state after:
case inl
⊢ (∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ ∃ p, p ≤ 1 ∧ 1 = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ 1 = Nat.minFac 1 ^ k

case inr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
⊢ Chain r₂ s

Tactic:
by
  induction s
  · trivial
  · rw [chain_coe_cons] at p ⊢
    exact p.imp H

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

Goal state before:
pp: k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h : (k + 2) / m = 0
⊢ False

Tactic:
by
        have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
        rw [zero_mul] at this; exact (show k + 2 ≠ 0 by simp) this

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

Goal state before:
pp: n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ∀ (p : ℕ), Prime p → p ∣ (k + 2) / (k + 2).minFac → (k + 2).minFac ≤ p

Tactic:
exact fun p pp d => minFac_le_of_dvd pp.two_le (d.trans <| div_dvd_of_dvd <| minFac_dvd _)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
apply le_antisymm

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore ≤ (MulAction.toPermHom G (G ⧸ H)).ker

case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0

Tactic:
exact dvd_zero _

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ q ∈ a.primeFactorsList → q ∈ b.primeFactorsList → False

Tactic:
hqa

Goal state after:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
⊢ q ∈ b.primeFactorsList → False
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ ∉ H

Tactic:
inv_mem_iff (x := b)

Goal state after:
case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b ∉ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = (ringEquivCongr ⋯) x

Tactic:
by
  rw [← ringEquivCongr_trans hab hbc]
  rfl

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

Goal state before:
pp: a b c : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD c]

Tactic:
simpa [Int.natCast_modEq_iff] using ZMod.intCast_eq_intCast_iff a b c

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

Goal state before:
pp: a b c : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD c]

Tactic:
by
  simpa [Int.natCast_modEq_iff] using ZMod.intCast_eq_intCast_iff a b c

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

Goal state before:
pp: a b : ℕ
⊢ a ≡ 0 [MOD b] ↔ b ∣ a

Tactic:
Nat.modEq_zero_iff_dvd

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Group M
inst✝¹ : Finite G
inst✝ : Finite M
f : G →* M
h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M
⊢ Function.Surjective ⇑f

Tactic:
by
  refine range_eq_top.1 <| SetLike.ext' <| Set.eq_of_subset_of_ncard_le (Set.subset_univ _) ?_
  rw [Subgroup.coe_top, Set.ncard_univ, ← Nat.card_coe_set_eq, SetLike.coe_sort_coe,
    ← Nat.card_congr (QuotientGroup.quotientKerEquivRange f).toEquiv]
  exact Nat.le_of_mul_le_mul_left (f.ker.card_mul_index ▸ Nat.mul_le_of_le_div _ _ _ h) Nat.card_pos

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

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
by
  rw [val_mul]
  apply Nat.mod_eq_of_lt h

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

Goal state before:
pp: a : ℤ
⊢ a * a.sign = ↑a.natAbs

Tactic:
by rw [Int.mul_sign_self]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
n n✝ : ℕ
h : n✝ + 1 ∈ n.divisors
⊢ 0 < n✝ + 1

Tactic:
apply Nat.succ_pos

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

Goal state before:
pp: n : ℕ
⊢ 1⁻¹ = 1

Tactic:
by
  obtain rfl | hn := eq_or_ne n 1
  · exact Subsingleton.elim _ _
  · simpa [ZMod.val_one'' hn] using mul_inv_eq_gcd (1 : ZMod n)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

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

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ Prod.swap '' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal

Tactic:
Set.image_swap_eq_preimage_swap

Goal state after:
n : ℕ
⊢ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
· exact geom_sum_pos' hx' hn

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

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
by
  have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)
  rw [← mul_inv_eq_gcd, Nat.cast_one] at this
  exact (Units.inv_eq_of_mul_eq_one_right this).symm

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

Goal state before:
pp: n k : ℕ
p : 0 < n
⊢ n.choose k < 2 ^ n

Tactic:
refine lt_of_le_of_lt ?_ (Nat.two_pow_pred_lt_two_pow p)

Goal state after:
n k : ℕ
p : 0 < n
⊢ n.choose k ≤ 2 ^ (n - 1)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.w
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n✝ + 1)

Tactic:
apply Nat.succ_pos

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

Goal state before:
pp: case succ
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
m : ℕ
ih : (a ^ m).val ≤ a.val ^ m
⊢ (a ^ m).val * a.val ≤ a.val ^ m * a.val

Tactic:
apply Nat.mul_le_mul_right _ ih

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ ↑f = ↑g

Tactic:
apply RingHom.ext_zmod _ _

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

Goal state before:
pp: case pos
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

pp: case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
· rcases h' with rfl
        left
        simpa using w₂

Goal state after:
case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : p ≠ 0
n k : ℕ
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
by
  obtain rfl | hp1 : p = 1 ∨ 1 < p := by grind
  · simp
  · rcases eq_or_ne n 0 with rfl | hn <;> simp [divMaxPow, *]

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

Goal state before:
pp: case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p (List.drop i digits) / p = ofDigits p (List.drop (i + 1) digits)

Tactic:
ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx,

Goal state after:
case succ
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p (List.drop i digits).tail = ofDigits p (List.drop (i + 1) digits)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
nth_rw 2 [← one_mul <| ofDigits p tl]

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case bit
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b ↦ bif b then 1 else 0) (bit b n).bits

Tactic:
rw [bits_append_bit _ _ fun hn => absurd hn h]
    cases b
    · rw [digits_def' one_lt_two]
      · simpa [Nat.bit]
      · simpa [Nat.bit, pos_iff_ne_zero]
    · simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]

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

Goal state before:
pp: case cons
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ↑d + b * ofDigits b L ≡ ↑d + b' * ofDigits b' L [ZMOD ↑k]

Tactic:
dsimp [Int.ModEq] at *

Goal state after:
case cons
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
⊢ (↑d + b * ofDigits b L) % ↑k = (↑d + b' * ofDigits b' L) % ↑k
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ (if h : ∃ n, ¬↑a ^ (n + 1) ∣ ↑b then ↑(Nat.find h) else ⊤) = if h : ∃ n, ¬a ^ (n + 1) ∣ b then ↑(Nat.find h) else ⊤

Tactic:
congr!

Goal state after:
case h₂
a b : ℕ
h_congr_thm✝ :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
h✝ : ∃ n, ¬a ^ (n + 1) ∣ b
x✝ : ℕ
⊢ ↑a ^ (x✝ + 1) ∣ ↑b ↔ a ^ (x✝ + 1) ∣ b

case h₁
a b x✝ : ℕ
⊢ ↑a ^ (x✝ + 1) ∣ ↑b ↔ a ^ (x✝ + 1) ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
⊢ emultiplicity a b < ↑k ↔ ¬↑k ≤ emultiplicity a b

Tactic:
not_le

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
⊢ emultiplicity a b < ↑k ↔ emultiplicity a b < ↑k
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hf : FiniteMultiplicity a b
⊢ multiplicity a b < k ↔ ¬k ≤ multiplicity a b

Tactic:
not_le

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hf : FiniteMultiplicity a b
⊢ multiplicity a b < k ↔ multiplicity a b < k
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.succ
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1

Tactic:
specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])

Goal state after:
case succ.succ.succ
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case neg
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1

Tactic:
simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ¬∃ n, 0 < n ∧ x ^ n = 1

Tactic:
not_exists,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ∀ (x_1 : ℕ), ¬(0 < x_1 ∧ x ^ x_1 = 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Subsingleton G
x : G
⊢ orderOf x = 1

Tactic:
simp [orderOf, nontriviality]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ (¬∃ n, 0 < n ∧ x ^ n = 1) ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Tactic:
not_exists,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ (∀ (x_1 : ℕ), ¬(0 < x_1 ∧ x ^ x_1 = 1)) ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : IsOfFinOrder x
h : orderOf y ∣ orderOf x
⊢ IsOfFinOrder y

Tactic:
rw [← orderOf_pos_iff] at hx ⊢

Goal state after:
G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ (x ^ n) ^ 1 = x

Tactic:
by rw [h, pow_one, pow_one]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p ∣ a.gcd b
⊢ False

Tactic:
rw [Coprime.gcd_eq_one hab, Nat.dvd_one] at this

Goal state after:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p = 1
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: x p : ℕ
hp : Prime p
hx : p ∣ x
⊢ x / p / p ^ (x / p).factorization p = x / p ^ x.factorization p

Tactic:
simpa [pow_one] using ordCompl_div_pow_of_dvd 1 hp (show p ^ 1 ∣ x by simpa)

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

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

Tactic:
apply le_antisymm

Goal state after:
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

case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
⊢ (n.choose k).factorization p = 0

Tactic:
by
  rcases em' p.Prime with hp | hp
  · exact factorization_eq_zero_of_not_prime (choose n k) hp
  rcases lt_or_ge n k with hnk | hkn
  · simp [choose_eq_zero_of_lt hnk]
  simp only [factorization_choose hp hkn (Nat.lt_add_one _), card_eq_zero, filter_eq_empty_iff,
    mem_Ico, not_le, and_imp]
  intro i hi₁ hi
  rcases eq_or_lt_of_le hi₁ with (rfl | hi)
  · rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]
    exact
      lt_of_le_of_lt
        (add_le_add
          (add_le_add_left (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk)) (k % p))
          (add_le_add_left (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk'))
            ((n - k) % p)))
        (by rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn])
  · replace hn : n < p ^ i := by
      have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
      calc
        n < 3 * p := hn
        _ ≤ p * p := by gcongr
        _ = p ^ 2 := (sq p).symm
        _ ≤ p ^ i := pow_right_mono₀ hp.one_lt.le hi
    rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn),
      add_tsub_cancel_of_le hkn]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1

Tactic:
have hp' := hp.prime

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
subst hn
    simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) = 1

Tactic:
simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]

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

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p

Tactic:
simp [factorization_eq_zero_of_not_prime, pp]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x

Tactic:
by
  ext g'
  dsimp only [coeff_add, of'_apply, Finsupp.add_apply]
  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
  · rw [coeff_modOf_self_add, add_zero, coeff_single_mul_add, one_mul, coeff_divOf]
  · rw [coeff_modOf_of_not_exists_add x _ _ h, coeff_single_mul_of_forall_add_ne, zero_add]
    simpa [eq_comm] using h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ ∃ i ≤ n, c = p ^ i

Tactic:
rwa [Nat.dvd_prime_pow hp.1] at hcpn

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ CharP R (p ^ n)

Tactic:
obtain ⟨i, hi, rfl⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn

Goal state after:
R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
i : ℕ
hi : i ≤ n
hc : CharP R (p ^ i)
hcpn : p ^ i ∣ p ^ n
⊢ CharP R (p ^ n)
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
hp : (f * g).degree = 1
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f

Tactic:
degree_mul,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
hp : f.degree + g.degree = 1
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f
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 : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

Tactic:
simp_rw [subset_iff, mem_image, mem_antidiagonal]

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

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

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ (derivative p).degree ≤ ↑(p.natDegree - 1)

case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ ↑(p.natDegree - 1) ≤ (derivative p).degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p.coeff p.natDegree ≠ 0

Tactic:
coeff_natDegree,

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p.leadingCoeff ≠ 0
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h.right
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
apply le_antisymm

Goal state after:
case h.right.a
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) ≤ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

case a
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ ⨅ i, 𝓟 (s i)
Module: Mathlib.Order.Filter.CountablyGenerated

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

Tactic:
rcases B.eq_empty_or_nonempty with hB | Bnonempty
  · rw [hB, iInf_emptyset]
    use fun _ => i₀
    simp [h]
  · exact countable_biInf_eq_iInf_seq Bcbl Bnonempty f

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
hgu : IsUnit g
⊢ ((X - C x) * g).degree = 1

Tactic:
degree_mul,

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
hgu : IsUnit g
⊢ (X - C x).degree + g.degree = 1
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inl.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a

Tactic:
exact Or.inl ha

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

Goal state before:
pp: case inl.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a

Tactic:
exact Or.inl ha

Goal state after: