mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: 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), ((mk I).comp (algebraMap R₁ A)) r * x = x * ((mk I).comp (algebraMap R₁ A)) r

Tactic:
by rintro r ⟨x⟩; exact congr_arg (⟦·⟧) (Algebra.commutes r x)

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

Goal state before:
pp: n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2

Tactic:
have ha : a ≠ 1 := Nat.succ_succ_ne_one n

Goal state after:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = s.insertIdx n x
n : ℕ
hn : n < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n] = (y :: s).insertIdx n x

Tactic:
cases n

Goal state after:
case cons.zero
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = s.insertIdx n x
hn : 0 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[0] = (y :: s).insertIdx 0 x

case cons.succ
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = s.insertIdx n x
n✝ : ℕ
hn : n✝ + 1 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n✝ + 1] = (y :: s).insertIdx (n✝ + 1) x
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✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : StarRing B
inst✝⁴ : StarModule R A
inst✝³ : FunLike F A B
inst✝² : AlgHomClass F R A B
inst✝¹ : StarHomClass F A B
f g : F
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
⊢ ∀ {a : B}, a ∈ (↑φ).range.carrier → star a ∈ (↑φ).range.carrier

Tactic:
rintro _ ⟨b, rfl⟩; exact ⟨star b, map_star φ b⟩

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

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
cases n

Goal state after:
case zero
p : ℕ
⊢ p ∈ primeFactorsList 0 ↔ Prime p ∧ p ∣ 0 ∧ 0 ≠ 0

case succ
p n✝ : ℕ
⊢ p ∈ (n✝ + 1).primeFactorsList ↔ Prime p ∧ p ∣ n✝ + 1 ∧ n✝ + 1 ≠ 0
Module: Mathlib.GroupTheory.Index

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

Tactic:
← comap_map_eq,

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

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

Tactic:
← comap_map_eq,

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
⊢ (map f H).index = (H ⊔ f.ker).index * f.range.index

Tactic:
← comap_map_eq,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
⊢ (map f H).index = (comap f (map f H)).index * f.range.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ a.val < n

Tactic:
cases n

Goal state after:
case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ a.val < 0

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.val < n✝ + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n a : ℕ
⊢ (↑a).val = a % n

Tactic:
cases n

Goal state after:
case zero
a : ℕ
⊢ (↑a).val = a % 0

case succ
a n✝ : ℕ
⊢ (↑a).val = a % (n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑0 = n / n.gcd 0

Tactic:
simp only [Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right,
      Nat.pos_of_ne_zero n0, Nat.div_self]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (J ⊓ L).relIndex (K ⊓ L) ≠ 0

Tactic:
rw [← range_subtype L, inf_comm, ← map_comap_eq, inf_comm, ← map_comap_eq, ← relIndex_comap,
    comap_map_eq_self_of_injective (subtype_injective L)]
  exact relIndex_comap_ne_zero _ hJK

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) n with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) 0 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero n
a : ZMod n
⊢ a.cast = ↑a.val

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
inst✝ : NeZero 0
a : ZMod 0
⊢ a.cast = ↑a.val

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ a.cast = ↑a.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ a.cast.1 = a.cast

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.1 = a.cast

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ a.cast.2 = a.cast

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.2 = a.cast

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = a

Tactic:
cases n

Goal state after:
case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ ↑a.val = a

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ ↑a.val = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ ↑a.cast = a

Tactic:
cases n

Goal state after:
case zero
a : ZMod 0
⊢ ↑a.cast = a

case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero n
⊢ Nat.cast ∘ val = cast

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : NeZero 0
⊢ Nat.cast ∘ val = cast

case succ
R : Type u_1
inst✝¹ : Ring R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Nat.cast ∘ val = cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast

case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ ↑(1 % (n + 1)) = 1

Tactic:
cases n

Goal state after:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0 + 1
⊢ ↑(1 % (0 + 1)) = 1

case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑(1 % (n✝ + 1 + 1)) = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
a b : ZMod n
⊢ (a + b).cast = a.cast + b.cast

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a + b).cast = a.cast + b.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
a b : ZMod n
⊢ (a * b).cast = a.cast * b.cast

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a * b).cast = a.cast * b.cast

case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a * b).cast = a.cast * b.cast
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₁ < n₂
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₂ < n₁
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
· exact ⟨n₁, n₂, hlt, hle₂, he⟩

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₂ < n₁
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ℤ
⊢ (↑a).cast = a % ↑n

Tactic:
cases n

Goal state after:
case zero
a : ℤ
⊢ (↑a).cast = a % ↑0

case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ ↑(-1) = n

Tactic:
cases n

Goal state after:
case zero
⊢ ↑(-1) = 0

case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index ≠ H.index

Tactic:
← relIndex_mul_index h.le,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index ≠ H.relIndex K * K.index
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
cases n

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

case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ (k - 1).cast = k.cast - 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Injective val

Tactic:
cases n

Goal state after:
case zero
inst✝ : NeZero 0
⊢ Injective val

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Injective val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a + b).val = (a.val + b.val) % n

Tactic:
cases n

Goal state after:
case zero
inst✝ : NeZero 0
a b : ZMod 0
⊢ (a + b).val = (a.val + b.val) % 0

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
⊢ (a + b).val = (a.val + b.val) % (n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a + b).val ≤ a.val + b.val

Tactic:
cases n

Goal state after:
case zero
a b : ZMod 0
⊢ (a + b).val ≤ a.val + b.val

case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
cases n

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

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: n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
hx : x ∈ m.divisors
⊢ x ∈ n.properDivisors

Tactic:
exact
    Nat.mem_properDivisors.2
      ⟨(Nat.mem_divisors.1 hx).1.trans h,
        lt_of_le_of_lt (divisor_le hx)
          (lt_of_le_of_ne (divisor_le (Nat.mem_divisors.2 ⟨h, hzero⟩)) hdiff)⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n ≤ n.divisors.sup id

Tactic:
rcases Decidable.eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
⊢ 0 ≤ (divisors 0).sup id

case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
grw [← hx.le]

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < x + 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

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 hn.geom_sum_pos

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

Goal state before:
pp: n : ℕ
s : Finset ℕ
hsub : s ⊆ n.properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ n.properDivisors, x → s = n.properDivisors

Tactic:
cases n

Goal state after:
case zero
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
cases n

Goal state after:
case succ.zero
⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ↔ Prime (0 + 1)

case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
rw [mem_properDivisors, Nat.dvd_prime_pow pp]
  constructor
  · rintro ⟨⟨j, hjk, rfl⟩, hlt⟩
    exact ⟨j, (Nat.pow_lt_pow_iff_right pp.one_lt).mp hlt, rfl⟩
  · rintro ⟨j, hjk, rfl⟩
    exact ⟨⟨j, le_of_lt hjk, rfl⟩, Nat.pow_lt_pow_of_lt pp.one_lt hjk⟩

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

Goal state before:
pp: case refine_1
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast.val ≡ x.val [MOD m]

pp: case refine_2
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast.val ≡ x.val [MOD n]

Tactic:
· rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]

Goal state after:
case refine_2
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast.val ≡ x.val [MOD n]
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
⊢ n.divisorsAntidiagonal = {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
ext ⟨n1, n2⟩
  rw [Nat.mem_divisorsAntidiagonal]
  simp only [ne_eq, Finset.mem_filter, Finset.mem_product, Finset.mem_Ioc]
  constructor
  · intro ⟨rfl, hn2⟩
    grw [← hn]
    simp (disch := lia) only [le_mul_iff_one_le_right, le_mul_iff_one_le_left, and_true]
    lia
  · intro ⟨⟨hn1, hn2⟩, hn3⟩
    exact ⟨hn3, n_ne_zero⟩

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

Goal state before:
pp: case refine_2
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast.val ≡ x.val [MOD n]

Tactic:
· rw [← ZMod.natCast_eq_natCast_iff, ZMod.natCast_zmod_val, ZMod.natCast_val]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ (-↑n).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) n.divisorsAntidiagonal).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) n.divisorsAntidiagonal) ⋯

Tactic:
cases n

Goal state after:
case zero
⊢ (-↑0).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) (Nat.divisorsAntidiagonal 0)).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) (Nat.divisorsAntidiagonal 0)) ⋯

case succ
n✝ : ℕ
⊢ (-↑(n✝ + 1)).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) (n✝ + 1).divisorsAntidiagonal).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) (n✝ + 1).divisorsAntidiagonal) ⋯
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
cases n

Goal state after:
case zero
a : ZMod 0
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0

case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 = 0 ∨ a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
rcases he with (⟨⟨⟩⟩ | he)

Goal state after:
case succ.mp.zero.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
he : a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 2 * val 0

Tactic:
val_zero,

Goal state after:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 2 * 0
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
Nat.add_sub_cancel_left

Goal state after:
n : ℕ
⊢ 2 * ((n + (n + 1)).choose n * (n + 1)) = 2 * ((n + (n + 1)).choose n * (n + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - val 0) % n = 0

Tactic:
val_zero,

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - 0) % n = 0
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ n + 1 ∣ (2 * n + 1) * n.centralBinom

Tactic:
apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two

Goal state after:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * n.centralBinom)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
⊢ b.digitsAux h n = n % b :: b.digitsAux h (n / b)

Tactic:
cases n

Goal state after:
case zero
b : ℕ
h : 2 ≤ b
w : 0 < 0
⊢ b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)

case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
h : 1 < b
x y : ℕ
hxb : x < b
hxy : x ≠ 0 ∨ y ≠ 0
⊢ b.digits (x + b * y) = x :: b.digits y

Tactic:
rcases Nat.exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩

Goal state after:
x y : ℕ
hxy : x ≠ 0 ∨ y ≠ 0
b : ℕ
h : 1 < b + 2
hxb : x < b + 2
⊢ (b + 2).digits (x + (b + 2) * y) = x :: (b + 2).digits y
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ↑hd + b * ofDigits b (tl ++ l2) = ↑hd + b * ofDigits b tl + b ^ (hd :: tl).length * ofDigits b l2

Tactic:
IH,

Goal state after:
case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b ^ (hd :: tl).length * ofDigits b l2
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ZMod n
k : ZMod n
⊢ f k.cast = k

Tactic:
cases n

Goal state after:
case zero
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ZMod 0
k : ZMod 0
⊢ f k.cast = k

case succ
R : Type u_1
inst✝ : NonAssocRing R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f k.cast = k
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.ind
b n : ℕ
h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
cases n

Goal state after:
case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0

case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n✝ + 1)) = n✝ + 1
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: n p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ n / (p * p) < n / p

Tactic:
rw [← Nat.dvd_iff_mod_eq_zero] at hmod
    rcases hmod with ⟨m, rfl⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]
    exact Nat.div_lt_self (by grind) hp.1

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
⊢ k ≤ (p.maxPowDvdDiv n).fst

Tactic:
rw [← padicValNat, ← pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn,
            pow_dvd_iff_le_of_spec hp hn h hl]

Goal state after:
case h₁
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ k
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.Digits.Lemmas

Goal state before:
pp: case inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
interval_cases b <;> simp +arith [digits_zero_succ', hn]

Goal state after: