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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule S * toSubmodule T = toSubmodule (S ⊔ T)

Tactic:
refine le_antisymm (mul_toSubmodule_le _ _) ?_

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule (S ⊔ T) ≤ toSubmodule S * toSubmodule T
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ x✝ ∈ RingHom.ker (map f) ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f

Tactic:
RingHom.mem_ker,

Goal state after:
R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ (map f) x✝ = 0 ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ OrzechProperty R

Tactic:
refine ⟨fun {M} _ _ _ {N} f hf ↦ ?_⟩
  let := addCommMonoidToAddCommGroup R (M := M)
  let := addCommMonoidToAddCommGroup R (M := N)
  let i := N.subtype
  let hi : Function.Injective i := N.injective_subtype
  refine LinearMap.ker_eq_bot.1 <| LinearMap.ker_eq_bot'.2 fun n hn ↦ ?_
  obtain ⟨k, mj, hmj⟩ := exists_fin (R := R) (M := M)
  rw [← surjective_piEquiv_apply_iff] at hmj
  obtain ⟨b, hb⟩ := hmj (i n)
  choose nj hnj using fun j ↦ hf (mj j)
  choose c hc using fun j ↦ hmj (i (nj j))
  let A := Subring.closure (Set.range b ∪ Set.range c.uncurry)
  let N' := span A ({n} ∪ Set.range nj)
  let M' := span A (Set.range mj)
  have : IsNoetherianRing A := is_noetherian_subring_closure _
    (.union (Set.finite_range _) (Set.finite_range _))
  have : Module.Finite A M' := span_of_finite A (Set.finite_range _)
  refine congr($((LinearMap.ker_eq_bot'.1 <| LinearMap.ker_eq_bot.2 <|
    IsNoetherian.injective_of_surjective_of_injective
      ((i.restrictScalars A).restrict fun x hx ↦ ?_ : N' →ₗ[A] M')
      ((f.restrictScalars A).restrict fun x hx ↦ ?_ : N' →ₗ[A] M')
      (fun _ _ h ↦ injective_subtype _ (hi congr(($h).1)))
      fun ⟨x, hx⟩ ↦ ?_) ⟨n, (subset_span (by simp))⟩ (Subtype.val_injective hn)).1)
  · induction hx using span_induction with
    | mem x hx =>
      change i x ∈ M'
      simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx
      rcases hx with hx | ⟨j, rfl⟩
      · rw [hx, ← hb, piEquiv_apply_apply]
        refine Submodule.sum_mem _ fun j _ ↦ ?_
        let b' : A := ⟨b j, Subring.subset_closure (by simp)⟩
        rw [show b j • mj j = b' • mj j from rfl]
        exact smul_mem _ _ (subset_span (by simp))
      · rw [← hc, piEquiv_apply_apply]
        refine Submodule.sum_mem _ fun j' _ ↦ ?_
        let c' : A := ⟨c j j', Subring.subset_closure
          (by simp [show ∃ a b, c a b = c j j' from ⟨j, j', rfl⟩])⟩
        rw [show c j j' • mj j' = c' • mj j' from rfl]
        exact smul_mem _ _ (subset_span (by simp))
    | zero => simp
    | add x _ y _ hx hy => rw [map_add]; exact add_mem hx hy
    | smul a x _ hx => rw [map_smul]; exact smul_mem _ _ hx
  · induction hx using span_induction with
    | mem x hx =>
      change f x ∈ M'
      simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx
      rcases hx with hx | ⟨j, rfl⟩
      · rw [hx, hn]; exact zero_mem _
      · exact subset_span (by simp [hnj])
    | zero => simp
    | add x _ y _ hx hy => rw [map_add]; exact add_mem hx hy
    | smul a x _ hx => rw [map_smul]; exact smul_mem _ _ hx
  suffices x ∈ LinearMap.range ((f.restrictScalars A).domRestrict N') by
    obtain ⟨a, ha⟩ := this
    exact ⟨a, Subtype.val_injective ha⟩
  induction hx using span_induction with
  | mem x hx =>
    obtain ⟨j, rfl⟩ := hx
    exact ⟨⟨nj j, subset_span (by simp)⟩, hnj j⟩
  | zero => exact zero_mem _
  | add x y _ _ hx hy => exact add_mem hx hy
  | smul a x _ hx => exact smul_mem _ a hx

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ b * c [ZMOD n * c]

Tactic:
mul_comm b,

Goal state after:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD n * c]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a + n ≡ b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by
  simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b + n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by
  simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ n + b [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by
  simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a + b * n ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by
  simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b + c * n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by
  simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a + n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by
  simp [ModEq]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b + n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by
  simp [ModEq]

Goal state after:
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
b : ℤ
hb₀ : 0 ≤ b
hb : b < ↑p
a : ℕ
ha : ↑a < ↑p
hab : ↑↑a = ↑b
⊢ ↑a = b

Tactic:
lift b to ℕ using hb₀

Goal state after:
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a : ℕ
ha : ↑a < ↑p
b : ℕ
hb : ↑b < ↑p
hab : ↑↑a = ↑↑b
⊢ ↑a = ↑b
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J) = RingHom.id (R ⧸ I ⊔ J)

Tactic:
repeat apply Ideal.Quotient.ringHom_ext
      rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J) = RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)

Tactic:
repeat apply Ideal.Quotient.ringHom_ext
      rfl

Goal state after:
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
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
S : StarSubalgebra R A
s : Set A
hs : s = ↑S
a : A
ha : a ∈ (S.copy s hs).carrier
⊢ a ∈ S.carrier

Tactic:
simpa [hs] using ha

Goal state after:
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
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
S : StarSubalgebra R A
a : A
hs : ↑S = ↑S
__Subalgebra✝ : Subalgebra R A := S.copy (↑S) hs
ha : a ∈ (S.copy (↑S) hs).carrier
⊢ a ∈ S.carrier

Tactic:
simpa [hs] using ha

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.next (l.getLast h) ⋯ = l.head h

Tactic:
have h1 : l.length - 1 + 1 = l.length := by grind [length_pos_iff]
  simp [getLast_eq_getElem h, head_eq_getElem h, next_getElem l hn (l.length - 1) (by grind), h1]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
⊢ (∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b) → Chain r ↑(a :: l)

Tactic:
| cons a l =>

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
⊢ (∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b) → Chain r ↑(a :: l)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
⊢ Chain r ↑(a :: l) → ∀ a_2 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_2 b

Tactic:
| cons a l =>

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
⊢ Chain r ↑(a :: l) → ∀ a_2 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_2 b
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
⊢ ∀ b_1 ∈ ↑(a :: l), r b b_1

Tactic:
c

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
c : α
⊢ c ∈ ↑(a :: l) → r b c
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc))

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
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
⊢ (Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = q

Tactic:
induction q using Quotient.inductionOn'

Goal state after:
case h
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
a✝ : ↑(orbitRel.Quotient.orbit ω)
⊢ ((Quotient.mk'' a✝).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = Quotient.mk'' a✝
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
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
⊢ Quotient.liftOn' (q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = q

Tactic:
induction q using Quotient.inductionOn'

Goal state after:
case h
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
a✝ : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
⊢ Quotient.liftOn' ((Quotient.mk'' a✝).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = Quotient.mk'' a✝
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n a : ℕ
h' : n * a ≠ 0
⊢ n.primeFactorsList <+ (n * a).primeFactorsList

Tactic:
exact primeFactorsList_sublist_right (right_ne_zero_of_mul h')

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : Finite (MulAction.orbitRel.Quotient G X)
hi : H.index ≠ 0
this : Fintype (G ⧸ H)
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
exact MulAction.finite_quotient_of_finite_quotient_of_finite_quotient

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑n = ↑n + 1 - 1

Tactic:
add_sub_cancel_right

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.zero
R : Type u_1
inst✝ : Ring R
k : ZMod 0
hk : ¬k = 0
⊢ ↑(k - 1) = ↑k - 1

Tactic:
rw [Int.cast_sub, Int.cast_one]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image Prod.snd n.divisorsAntidiagonal = n.divisors

Tactic:
rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]
  exact image_fst_divisorsAntidiagonal

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image Prod.snd n.divisorsAntidiagonal = n.divisors

Tactic:
by
  rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]
  exact image_fst_divisorsAntidiagonal

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

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)

Tactic:
clear this

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ 0 < ∑ i ∈ range n, x ^ i ↔ Odd n ∨ 0 < x + 1

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Odd n ∨ 0 < x + 1

case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
⊢ a * b ∈ {1, 2, 3} ↔
    (a, b) ∈ {(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}

Tactic:
simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]

Goal state after:
a b : ℤ
⊢ (a, b) ∈ divisorsAntidiag 1 ∨ (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ↔
    (a, b) = (1, 1) ∨
      (a, b) = (-1, -1) ∨
        (a, b) = (1, 2) ∨
          (a, b) = (2, 1) ∨
            (a, b) = (-1, -2) ∨
              (a, b) = (-2, -1) ∨ (a, b) = (1, 3) ∨ (a, b) = (3, 1) ∨ (a, b) = (-1, -3) ∨ (a, b) = (-3, -1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b ∈ {0, 1, 2, 3, 4} ↔
    (a, b) ∈
      {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
        (-4, -1), (-1, -4), (2, 2), (-2, -2)}

Tactic:
simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]

Goal state after:
a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b = 0 ∨
      (a, b) ∈ divisorsAntidiag 1 ∨
        (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ∨ (a, b) ∈ divisorsAntidiag 4 ↔
    (a, b) = (0, 0) ∨
      (a, b) = (1, 1) ∨
        (a, b) = (-1, -1) ∨
          (a, b) = (1, 2) ∨
            (a, b) = (2, 1) ∨
              (a, b) = (-1, -2) ∨
                (a, b) = (-2, -1) ∨
                  (a, b) = (1, 3) ∨
                    (a, b) = (3, 1) ∨
                      (a, b) = (-1, -3) ∨
                        (a, b) = (-3, -1) ∨
                          (a, b) = (4, 1) ∨
                            (a, b) = (1, 4) ∨
                              (a, b) = (-4, -1) ∨ (a, b) = (-1, -4) ∨ (a, b) = (2, 2) ∨ (a, b) = (-2, -2)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ -a = a ↔ a = 0 ∨ 2 * a.val = n

Tactic:
rw [neg_eq_iff_add_eq_zero, ← two_mul]
  cases n
  · simp
  conv_lhs =>
    rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_eq_zero_iff]
  constructor
  · rintro ⟨m, he⟩
    rcases m with - | m
    · rw [mul_zero, mul_eq_zero] at he
      rcases he with (⟨⟨⟩⟩ | he)
      exact Or.inl (a.val_eq_zero.1 he)
    cases m
    · right
      rwa [show 0 + 1 = 1 from rfl, mul_one] at he
    refine (a.val_lt.not_ge <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim
    rw [he, mul_comm]
    apply Nat.mul_le_mul_left
    simp
  · rintro (rfl | h)
    · rw [val_zero, mul_zero]
      apply dvd_zero
    · rw [h]

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

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

Tactic:
rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc,
      choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]

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

Goal state before:
pp: case snd
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).2 = p.2

Tactic:
· simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
        (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]

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

Goal state before:
pp: 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
hx : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length

Tactic:
specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)

Goal state after:
b f n : ℕ
l1 l2 : List Char
ih :
  ((n % b).digitChar :: l1).length = ((n % b).digitChar :: l2).length →
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
      (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
hlen : l1.length = l2.length
hx : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
⊢ ∀ (c : Char) (tl : List Char), (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1

Tactic:
c

Goal state after:
case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
⊢ ∀ (tl : List Char), (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b n : ℕ
⊢ ∀ (c : Char) (tl : List Char), (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Tactic:
c

Goal state after:
case zero
b n : ℕ
c : Char
⊢ ∀ (tl : List Char), (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]
      simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ ¬a ≠ 1 ∨ ¬0 < b

Tactic:
not_ne_iff,

Goal state after:
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ ¬0 < 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 (b + a) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
emultiplicity_add_of_gt hab,

Goal state after:
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 = min (emultiplicity p a) (emultiplicity p b)
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:
emultiplicity_add_of_gt hab,

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 = min (emultiplicity p a) (emultiplicity p b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ (x ^ n) ^ m = x

Tactic:
rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
exact left_ne_zero_of_mul hx

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
a : ↥(zpowers x)
⊢ x ^ ↑((finEquivZPowers hx).symm a) = ↑a

Tactic:
simpa only [finEquivZPowers_apply] using
    congr_arg Subtype.val ((finEquivZPowers hx).apply_symm_apply a)

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + (↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p) + y ^ p - y ^ p)

Tactic:
add_sub_cancel_right

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers y ↔ x = y ∨ x⁻¹ = y

Tactic:
by
  refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩
  have hx_mem : x ∈ zpowers y := by simp [← h]
  have hy_mem : y ∈ zpowers x := by simp [h]
  obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp hy_mem
  obtain ⟨l, hl⟩ := mem_zpowers_iff.mp hx_mem
  rw [← zpow_mul] at hl
  nth_rewrite 2 [← zpow_one x] at hl
  have h1 := (injective_zpow_iff_not_isOfFinOrder.mpr hx) hl
  rcases (Int.mul_eq_one_iff_eq_one_or_neg_one).mp h1 with (h | h) <;> simp [h.1]

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

Tactic:
constructor
  · rintro rfl
    simp
  · intro h
    refine eq_of_factorization_eq ha hb fun p => ?_
    by_cases pp : p.Prime
    · simp [factorization_def, pp, h p pp]
    · simp [factorization_eq_zero_of_not_prime, pp]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (X * p.divX + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
by rintro ⟨_ | _⟩ <;> simp [coeff_C]

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

Goal state before:
pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
c

Goal state after:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
⊢ c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x : G
inst✝ : DecidableEq G
⊢ Finset.image (fun i ↦ x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x)).toFinset

Tactic:
by
  let : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred
  ext x
  rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]

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

Goal state before:
pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
set c := factors.prod (· ^ ·) with hc

Goal state after:
case neg
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
⊢ ∃ c, a = c ^ n ∧ b = c ^ m