mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ span R (p * q) ≤ Subalgebra.toSubmodule (adjoin R (s ∪ t))

Tactic:
rw [span_le, Set.mul_subset_iff]

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ ∀ x ∈ p, ∀ y ∈ q, x * y ∈ ↑(Subalgebra.toSubmodule (adjoin R (s ∪ t)))
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := ⋯
l' : ι → ↥S' := ⋯
e' : ∑ i ∈ ι', l' i * s' i = 1
⊢ ∀ c ∈ ι', l' c * s' c ∈ Ideal.span (s' '' ↑ι')

Tactic:
intro i hi

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
i : ι
hi : i ∈ ι'
⊢ l' i * s' i ∈ Ideal.span (s' '' ↑ι')
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S * toSubmodule S ≤ toSubmodule S

Tactic:
refine (mul_toSubmodule_le _ _).trans_eq ?_
    rw [sup_idem]

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

Goal state before:
pp: a b n : ℕ
⊢ ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]

Tactic:
unfold ModEq Nat.ModEq

Goal state after:
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : y ∈ ker f
hy : (Quotient.mk I) y = x
⊢ ∃ x ∈ ker f, (Quotient.mk I) x = (Quotient.mk I) y

Tactic:
exact ⟨y, hx, rfl⟩

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst✝ : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False

Tactic:
exact false_of_nontrivial_of_char_one (R := R)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Finite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

Tactic:
Nat.card_sum,

Goal state after:
case inl
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Finite { a // a ≠ 0 }
⊢ Nat.card { a // a = 0 } + Nat.card { a // ¬a = 0 } - 1 = Nat.card { a // a ≠ 0 }
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b : R
⊢ a + b = 0 ↔ a = b

Tactic:
rw [← CharTwo.sub_eq_add, sub_eq_iff_eq_add, zero_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
n : ℤ
⊢ ↑n = if Even n then 0 else 1

Tactic:
by
  obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg <;> simpa using natCast_eq_ite n

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

Goal state before:
pp: case mk
R : Type u
S : Type v
F : Type w
inst✝⁷ : Ring R
inst✝⁶ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
I : Ideal A
inst✝ : I.IsTwoSided
r : R₁
x✝ : A ⧸ I
x : A
⊢ ((mk I).comp (algebraMap R₁ A)) r * Quot.mk (⇑(Submodule.quotientRel I)) x =
    Quot.mk (⇑(Submodule.quotientRel I)) x * ((mk I).comp (algebraMap R₁ A)) r

Tactic:
exact congr_arg (⟦·⟧) (Algebra.commutes r x)

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
⊢ Multiset.Pairwise (Function.onFun _root_.Disjoint fun s ↦ s.val.lists) univSubsets

Tactic:
unfold Multiset.Pairwise

Goal state after:
case refine_1
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
⊢ ∃ l, univSubsets = ↑l ∧ List.Pairwise (Function.onFun _root_.Disjoint fun s ↦ s.val.lists) l
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ≤ J
⊢ comap (Quotient.mk I) (map (Quotient.mk I) J) = J

Tactic:
simpa

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

Goal state before:
pp: case hk
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
p : Ideal R
inst✝ : p.IsPrime
hIP : I ≤ p
⊢ ker (Quotient.mk I) ≤ p

Tactic:
simpa

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x

Tactic:
add_comm

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case e'_2
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n + n] x

Tactic:
Nat.sub_add_cancel this,

Goal state after:
case e'_2
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r] x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case e'_3
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n + n] x

Tactic:
Nat.sub_add_cancel this,

Goal state after:
case e'_3
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r] x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f x

Tactic:
rw [← iterate_one f]
    refine Function.IsPeriodicPt.isFixedPt ?_
    rw [← h]
    exact isPeriodicPt_minimalPeriod f x

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

Goal state before:
pp: case inl.nil
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ is' x, l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts

Tactic:
exact Or.inl ⟨l₁, by simpa using p⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ (y :: l ++ [x]).nextOr x ((y :: l ++ [x]).get ⟨0, ⋯⟩) = y

Tactic:
nextOr_concat

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ (y :: l ++ [x]).get ⟨0, ⋯⟩ = y

case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ x ∉ y :: l
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
⊢ ((y :: l).dropLast ++ [(y :: l).getLast ⋯]).nextOr ((y :: l).getLast ⋯) y = y

Tactic:
nextOr_concat

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
⊢ y = y

case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
⊢ (y :: l).getLast ⋯ ∉ (y :: l).dropLast
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
n : ℕ
hn : n < (permutations'Aux x s).length
⊢ (permutations'Aux x s).get ⟨n, hn⟩ = s.insertIdx n x

Tactic:
simp [getElem_permutations'Aux]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
⊢ l.next a ha = l[(idxOf a l + 1) % l.length]

Tactic:
by_cases ha' : a ∈ l.dropLast

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
ha' : a ∈ l.dropLast
⊢ l.next a ha = l[(idxOf a l + 1) % l.length]

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
ha' : a ∉ l.dropLast
⊢ l.next a ha = l[(idxOf a l + 1) % l.length]
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : m < n
this : x ∈ as
⊢ False

Tactic:
exact h x (ha.subset this) rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.length - 1 - k < (pmap l.reverse.prev l.reverse ⋯).length

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.Subsingleton

Tactic:
by
  rw [length_subsingleton_iff]
  induction s using Quotient.inductionOn'
  simp only [mk''_eq_coe, nodup_coe_iff] at h
  simp [h, Nat.succ_le_iff]

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

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList

Tactic:
by
  simp only [primeFactors, List.mem_toFinset]

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
rcases a.eq_zero_or_pos with (rfl | ha)

Goal state after:
case inl
b : ℕ
hab : Coprime 0 b
⊢ (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList

case inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime 1

Tactic:
rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_primeFactorsList hqa)
    (dvd_of_mem_primeFactorsList hqb)]

Goal state after:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime q
Module: Mathlib.Data.Nat.Factors

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

Tactic:
rcases a.eq_zero_or_pos with (rfl | ha)

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

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
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔ ∀ (b : G), Xor ((Equiv.inv G) a * b ∈ H) (b ∈ H)

Tactic:
refine fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ Xor (b * a ∈ H) (b ∈ H) ↔ Xor ((Equiv.inv G) a * (Equiv.inv G) b ∈ H) ((Equiv.inv G) b ∈ H)
Module: Mathlib.GroupTheory.Index

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

Tactic:
rw [Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), b * a ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * 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).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 ⊓ K ⊓ L).relIndex L ≤ H.relIndex L * K.relIndex L
Module: Mathlib.GroupTheory.Index

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

Tactic:
by
    rintro ⟨a, ha⟩
    by_cases ha' : a ∈ H
    · suffices ∀ b, b ∈ H by simp [(eq_top_iff' _).mpr this]
      exact fun b ↦ (ha b).elim (fun h ↦ by simpa using mul_mem h (inv_mem ha')) id
    · refine dvd_of_eq (index_eq_two_iff.mpr
        ⟨a, fun b ↦ (xor_iff_or_and_not_and _ _).mpr ⟨ha b, fun h ↦ ha' ?_⟩⟩)
      simpa using mul_mem (inv_mem h.2) h.1

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (a : G), (∀ (b : G), b * a ∈ H ∨ b ∈ H) ↔ ∀ (b : G), (Equiv.inv G) a * b ∈ H ∨ b ∈ H

Tactic:
refine fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ b * a ∈ H ∨ b ∈ H ↔ (Equiv.inv G) a * (Equiv.inv G) b ∈ H ∨ (Equiv.inv G) b ∈ H
Module: Mathlib.GroupTheory.Index

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

Tactic:
add_comm

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
⊢ n ≠ 0

Tactic:
by
      intro hn
      rw [hn] at h
      exact (Fintype.card_eq_zero_iff.mp h).elim' 0

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
⊢ 1 ≤ ↑k

Tactic:
← Ne,

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ↑k ≠ 0
⊢ 1 ≤ ↑k
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
← this

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n + ∑ x ∈ n.properDivisors, x = ∑ i ∈ n.properDivisors, i + n

Tactic:
add_comm

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ x ∈ n.properDivisors, x + n = ∑ i ∈ n.properDivisors, i + n
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
or_iff_not_imp_left,

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
Module: Mathlib.NumberTheory.Divisors

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

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

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
hmn : m ∣ n
⊢ {p ∈ {p ∈ n.divisors | Prime p} | p ∣ m} = {p ∈ m.divisors | Prime p}

Tactic:
filter_comm,

Goal state after:
m n : ℕ
hn : n ≠ 0
hmn : m ∣ n
⊢ {p ∈ {p ∈ n.divisors | p ∣ m} | Prime p} = {p ∈ m.divisors | Prime p}
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / (b - 1) + a = a + a / (b - 1)

Tactic:
add_comm

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + a / (b - 1) = a + a / (b - 1)
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ 0 < n.descFactorial k

Tactic:
simpa

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

Goal state before:
pp: n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ 1 < k !

Tactic:
simpa

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

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

Tactic:
rcases k with - | k
      · rw [choose_zero_right]
        exact Nat.one_le_two_pow
      · rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

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

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : NeZero n
x y : G
⊢ IsPeriodicPt (fun x_1 ↦ x + x_1) n y

Tactic:
by
    simpa [char_nsmul_eq_zero, IsPeriodicPt] using! isFixedPt_id _

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

Goal state before:
pp: b : ℕ
h : 1 < b
L : List ℕ
w₁ : ∀ l ∈ L, l < b
w₂ : ∀ (h : L ≠ []), L.getLast h ≠ 0
⊢ b.digits (ofDigits b L) = L

Tactic:
by
  induction L with
  | nil => simp
  | cons d L ih =>
    dsimp [ofDigits]
    replace w₂ := w₂ (by simp)
    rw [digits_add b h]
    · rw [ih]
      · intro l m
        apply w₁
        exact List.mem_cons_of_mem _ m
      · intro h
        rw [List.getLast_cons h] at w₂
        convert! w₂
    · exact w₁ d List.mem_cons_self
    · by_cases h' : L = []
      · rcases h' with rfl
        left
        simpa using w₂
      · right
        contrapose w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'

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

Goal state before:
pp: case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * ofDigits b (hd :: tl) = ofDigits b (List.map (fun x ↦ n * x) (hd :: tl))

Tactic:
List.map_cons,

Goal state after:
case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * ofDigits b (hd :: tl) = ofDigits b (n * hd :: List.map (fun x ↦ n * x) tl)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
convert! Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1

Goal state after:
case e'_3
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0
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 + 1) digits) = ofDigits p (List.drop (i + 1) digits)

Tactic:
add_comm

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 (1 + i) digits) = ofDigits p (List.drop (1 + i) digits)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits % p ^ 0 = ofDigits p (List.take 0 digits)

Tactic:
simp [mod_one]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ emultiplicity a b = ↑k

Tactic:
have : FiniteMultiplicity a b := ⟨k, hsucc⟩
  simp only [emultiplicity, this, ↓reduceDIte, Nat.cast_inj, find_eq_iff, hsucc, not_false_eq_true,
    Decidable.not_not, true_and]
  exact fun n hn ↦ (pow_dvd_pow _ hn).trans hk

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

Goal state before:
pp: case a
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
this : count p (replicate (count p n.primeFactorsList + 1) p) ≤ count p n.primeFactorsList
⊢ False

Tactic:
simp at this

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

Goal state before:
pp: case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ n.factorization + k • n.factorization = k • n.factorization + n.factorization

Tactic:
add_comm

Goal state after:
case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ k • n.factorization + n.factorization = k • n.factorization + n.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
if pp : p.Prime then
    exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)
  else
    simpa [Nat.factorization_eq_zero_of_not_prime n pp] using hn.bot_lt

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

Goal state before:
pp: case succ
p : ℕ
hp : Prime p
n : ℕ
ih : (p * n)!.factorization p = n !.factorization p + n
⊢ (p * (n + 1))!.factorization p = (n + 1)!.factorization p + (n + 1)

Tactic:
simp [factorization_factorial_mul_succ hp, ih, factorial_succ,
      factorization_mul (zero_ne_add_one n).symm (factorial_ne_zero n)]
    ring

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

Goal state before:
pp: x p : ℕ
hp : Prime p
hx : p ∣ x
⊢ p ^ 1 ∣ x

Tactic:
simpa

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

Goal state before:
pp: case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i

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