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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
⊢ star a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))

Tactic:
rw [← mem_star_iff _ a, star_adjoin_comm, sup_comm]

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
⊢ a ∈ Algebra.adjoin R (star (↑(star S) ⊔ ↑S))
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f

Tactic:
rcases hx with ⟨m, hm, hx⟩

Goal state after:
α : Type u_1
f : α → α
x : α
n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ f^[n] x ∈ periodicPts f
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n] x) (f^[n] (f x))

Tactic:
← iterate_mod_minimalPeriod_eq,

Goal state after:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[n] (f x))
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ n • b = b ↔ ↑(minimalPeriod (fun x ↦ a • x) b) ∣ n

Tactic:
rw [← period_eq_minimalPeriod, zpow_smul_eq_iff_period_dvd]

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

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
dsimp only

Goal state after:
case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Algebra.IsPrimePow

Goal state before:

Tactic:
k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mpr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
· rintro ⟨k, hkle, hk_pos, heq⟩
    refine ⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩
    · grind [Nat.minFac_prime_iff, nonpos_iff_eq_zero, Nat.log_zero_right, lt_self_iff_false]
    · grind [Nat.minFac_prime_iff]

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

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
H : Subgroup G
inst✝¹ : Finite (orbitRel.Quotient G X)
inst✝ : Finite (G ⧸ H)
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
by
  rw [(equivSubgroupOrbits X H).finite_iff]
  infer_instance

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

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₁ y₂ : X
h : y₁ ∈ orbit (↥H) y₂
⊢ (fun x y ↦ x⁻¹ * y ∈ H) ⋯.choose ⋯.choose

Tactic:
dsimp only

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₁ y₂ : X
h : y₁ ∈ orbit (↥H) y₂
⊢ ⋯.choose⁻¹ * ⋯.choose ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₂ : X
g : ↥H
⊢ ⋯.choose⁻¹ * ⋯.choose ∈ H

Tactic:
dsimp only

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₂ : X
g : ↥H
⊢ ⋯.choose⁻¹ * ⋯.choose ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case e'_5
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
a✝ : X
⊢ ⋯.choose⁻¹ • x = a✝

Tactic:
rw [inv_smul_eq_iff, (exists_smul_eq G _ x).choose_spec]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: 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)

pp: 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)

Tactic:
· simp only [hb, iff_true, mul_mem_cancel_right hb]

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

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
inf_relIndex_right,

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ H.relIndex (K ⊓ L) * (K ⊓ L).relIndex L ≤ H.relIndex L * K.relIndex L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x : ZMod n
⊢ (-x).cast = -x.cast % ↑n

Tactic:
rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]

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

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1

Tactic:
· dsimp [ZMod, ZMod.cast, ZMod.val]
      rw [Fin.coe_sub_one, if_neg]
      · rw [Nat.cast_sub, Nat.cast_one]
        rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
      · exact hk

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

Goal state before:
pp: p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z ↔ ∃ k, n = z.val + p * k

Tactic:
constructor
  · rintro rfl
    refine ⟨n / p, ?_⟩
    rw [val_natCast, Nat.mod_add_div]
  · rintro ⟨k, rfl⟩
    rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]

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

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val % 0

pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)

Tactic:
· rw [Nat.mod_zero]
    apply Int.natAbs_mul

Goal state after:
case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case ofNat.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, ofNat a✝) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (ofNat a✝¹, ofNat a✝).1 * (ofNat a✝¹, ofNat a✝).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

pp: case ofNat.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (ofNat a✝¹, -[a✝+1]).1 * (ofNat a✝¹, -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

pp: case ofNat.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], ofNat a✝) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], ofNat a✝).1 * (-[a✝¹+1], ofNat a✝).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

pp: case ofNat.negSucc.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

pp: case negSucc.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, ofNat a✝) ∈ -[a✝²+1].divisorsAntidiag ↔
    (ofNat a✝¹, ofNat a✝).1 * (ofNat a✝¹, ofNat a✝).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

pp: case negSucc.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, -[a✝+1]) ∈ -[a✝²+1].divisorsAntidiag ↔
    (ofNat a✝¹, -[a✝+1]).1 * (ofNat a✝¹, -[a✝+1]).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

pp: case negSucc.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], ofNat a✝) ∈ -[a✝²+1].divisorsAntidiag ↔
    (-[a✝¹+1], ofNat a✝).1 * (-[a✝¹+1], ofNat a✝).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

pp: case negSucc.negSucc.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ -[a✝²+1].divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

Tactic:
case ofNat.negSucc.negSucc =>
    simp [divisorsAntidiag]
    grind [Nat.cast_inj]

Goal state after:
case ofNat.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, ofNat a✝) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (ofNat a✝¹, ofNat a✝).1 * (ofNat a✝¹, ofNat a✝).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

case ofNat.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (ofNat a✝¹, -[a✝+1]).1 * (ofNat a✝¹, -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

case ofNat.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], ofNat a✝) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], ofNat a✝).1 * (-[a✝¹+1], ofNat a✝).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

case negSucc.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, ofNat a✝) ∈ -[a✝²+1].divisorsAntidiag ↔
    (ofNat a✝¹, ofNat a✝).1 * (ofNat a✝¹, ofNat a✝).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

case negSucc.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, -[a✝+1]) ∈ -[a✝²+1].divisorsAntidiag ↔
    (ofNat a✝¹, -[a✝+1]).1 * (ofNat a✝¹, -[a✝+1]).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

case negSucc.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], ofNat a✝) ∈ -[a✝²+1].divisorsAntidiag ↔
    (-[a✝¹+1], ofNat a✝).1 * (-[a✝¹+1], ofNat a✝).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

case negSucc.negSucc.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ -[a✝²+1].divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
hn : ¬2 ∣ n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
← Nat.prime_two.coprime_iff_not_dvd

Goal state after:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a + a = 0 ↔ a = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ image Prod.snd z.divisorsAntidiag = z.divisors

Tactic:
by
  ext
  simp [Eq.comm, mul_comm, dvd_def]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x y z : ℤ
hz : z ≠ 0
⊢ (x, y) ∈ z.divisorsAntidiag ↔ x * y = z

Tactic:
simp [hz]

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

Goal state before:
pp: case inr
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ 2 ^ n

Tactic:
exact (Nat.choose_lt_two_pow _ _ hn).le

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

Goal state before:
pp: b n : ℕ
⊢ ofDigits b [n] = n

Tactic:
simp [ofDigits]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
h : ℕ
L : List ℕ
⊢ ofDigits 1 (h :: L) = ↑h + ofDigits 1 L

Tactic:
simp [ofDigits]

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

Goal state before:
pp: case nil
b : ℕ
l2 : List ℕ
⊢ ofDigits b ([] ++ l2) = ofDigits b [] + b ^ [].length * ofDigits b l2

Tactic:
simp [ofDigits]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Semiring α
b : ℕ
⊢ ↑(ofDigits b []) = ofDigits ↑b []

Tactic:
simp [ofDigits]

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

Goal state before:
pp: case case2
p✝ p e q : ℕ
hqp : ¬q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e, q).snd

Tactic:
simp_all [Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.mul_pow, Nat.pow_add]

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

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

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

Goal state before:
pp: p n : ℕ
hp : 1 < p
hn : n ≠ 0
⊢ p.maxPowDvdDiv (p * n) = (padicValNat p n + 1, n.divMaxPow p)

Tactic:
by
  simpa using maxPowDvdDiv_base_pow_mul hp hn 1

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

Goal state before:
pp: case inl.nil
p : ℕ
h : 1 < p
h_nonempty : [] ≠ []
h_ne_zero : [].getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ [], l < p
⊢ (p - 1) * ∑ i ∈ range [].length, ofDigits p [] / p ^ i.succ = ofDigits p [] - [].sum

Tactic:
simp [ofDigits]

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

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

Tactic:
simp [ofDigits]

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

Goal state before:
pp: case nil
b : ℕ
hl : ∀ x ∈ [], x < b + 2
⊢ ofDigits (b + 2) [] < (b + 2) ^ [].length

Tactic:
simp [ofDigits]

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

Goal state before:
pp: case nil
p : ℕ
hpos : 0 < p
w₁ : ∀ l ∈ [], l < p
⊢ ofDigits p [] / p = ofDigits p [].tail

Tactic:
simp [ofDigits]

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

Goal state before:
pp: case inr.inr.cons
p : ℕ
h : p < 1
head✝ : ℕ
tail✝ : List ℕ
h_nonempty : head✝ :: tail✝ ≠ []
h_ne_zero : (head✝ :: tail✝).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ head✝ :: tail✝, l < p
⊢ 0 = ofDigits 0 (head✝ :: tail✝) - (head✝ :: tail✝).sum

Tactic:
simp [ofDigits]

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

Goal state before:
pp: case inr.inr.zero
p : ℕ
h : p < 1
⊢ 0 = 0 - (digits 0 0).sum

pp: case inr.inr.succ
p : ℕ
h : p < 1
n✝ : ℕ
⊢ 0 = n✝ + 1 - (digits 0 (n✝ + 1)).sum

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ multiplicity a b = 1

Tactic:
multiplicity,

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ WithTop.untopD 1 (emultiplicity a b) = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ↑(Nat.find h✝) < ↑m
⊢ False

pp: case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False

Tactic:
· simp only [cast_lt, find_lt_iff] at hm
    obtain ⟨n, hn1, hn2⟩ := hm
    exact hn2 ((pow_dvd_pow _ hn1).trans nh)

Goal state after:
case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length

Tactic:
if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial

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

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

Tactic:
exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)

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

Goal state before:
pp: a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p

Tactic:
by
  simp [factorization_mul ha hb, pow_add]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
pos_iff_ne_zero,

Goal state after:
a b : ℤ
⊢ a.natAbs ≠ 1 ∧ b.natAbs ≠ 0 ↔ a.natAbs ≠ 1 ∧ b ≠ 0
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)

Tactic:
simpa using h.add_pow_prime_pow_eq' hp 1

Goal state after:
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
⊢ (fun x_1 ↦ x ^ x_1) (i % ↑(orderOf x)).natAbs = y

Tactic:
dsimp only

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.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g : G
⊢ x * of' k G g %ᵒᶠ g = 0

Tactic:
ext g'
  simp only [of'_apply, coeff_zero, Finsupp.zero_apply]
  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
  · rw [coeff_modOf_self_add]
  · rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_mul_single_of_forall_add_ne]
    simpa [eq_comm, add_comm] using h

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

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

Tactic:
induction n

Goal state after:
case zero
p : ℕ
⊢ #({x ∈ Ioc 0 0 | p ∣ x}) = 0 / p

case succ
p n✝ : ℕ
a✝ : #({x ∈ Ioc 0 n✝ | p ∣ x}) = n✝ / p
⊢ #({x ∈ Ioc 0 (n✝ + 1) | p ∣ x}) = (n✝ + 1) / p
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd✝ : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i ↦ s i (ind i))

Tactic:
choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)

Goal state after:
α : Type u_1
I : Type u_7
inst✝ : Finite I
l : I → Filter α
ι : I → Sort u_6
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
hd✝ : Pairwise (Disjoint on l)
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : Pairwise (Disjoint on t)
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Disjoint on fun i ↦ s i (ind i))
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i ↦ s i (ind i)

Tactic:
choose ind hp ht using fun i => (h i).mem_iff.1 (htl i)

Goal state after:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
ind : (i : I) → ι i
hp : ∀ (i : I), p i (ind i)
ht : ∀ (i : I), s i (ind i) ⊆ t i
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i ↦ s i (ind i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x

Tactic:
pos_iff_ne_zero,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ rootMultiplicity x p ≠ 0 ↔ p ≠ 0 ∧ p.IsRoot x
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i ∈ s i

Tactic:
dsimp only

Goal state after:
case refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (if hi : i ∈ I then V ⟨i, hi⟩ else univ) ∈ s i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ (⇑derivative)^[k] (X ^ n) = C ↑(n.descFactorial k) * X ^ (n - k)

Tactic:
by
  rw [iterate_derivative_X_pow_eq_natCast_mul n k, C_eq_natCast]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f ↔ ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s

Tactic:
by
  constructor
  · simp only [pi, mem_iInf', mem_comap, pi_def]
    rintro ⟨I, If, V, hVf, -, rfl, -⟩
    choose t htf htV using hVf
    exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩
  · rintro ⟨I, If, t, htf, hts⟩
    exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
      Nat.WithBot.one_le_iff_zero_lt] using hdegree

Goal state after:
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) = 𝓟 ((Prod.fst ⁻¹' s)ᶜᶜ ∪ (Prod.snd ⁻¹' t)ᶜᶜ)

Tactic:
compl_compl,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' s ∪ (Prod.snd ⁻¹' t)ᶜᶜ)
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ
σ : Type u_5
s : Set ℕ
n : ℕ
hn : n + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n + 1) • s) = (n + 1) • ⇑degree ⁻¹' s

Tactic:
induction n

Goal state after:
case succ.zero
σ : Type u_5
s : Set ℕ
hn : 0 + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((0 + 1) • s) = (0 + 1) • ⇑degree ⁻¹' s

case succ.succ
σ : Type u_5
s : Set ℕ
n✝ : ℕ
a✝ : n✝ + 1 ≠ 0 → ⇑degree ⁻¹' ((n✝ + 1) • s) = (n✝ + 1) • ⇑degree ⁻¹' s
hn : n✝ + 1 + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n✝ + 1 + 1) • s) = (n✝ + 1 + 1) • ⇑degree ⁻¹' s
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : 0 ∉ hd :: tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots

Tactic:
by
    rw [List.mem_cons, not_or] at H
    rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
      Multiset.cons_coe, Multiset.cons_bind, ih H.2]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ nthRoots n 0 = replicate n 0

Tactic:
rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (a • p).aroots S = p.aroots S

Tactic:
by
  rw [smul_eq_C_mul, aroots_C_mul _ ha]

Goal state after: