mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n = 0 ↔ n = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n ≤ 1 ↔ n ≤ 1

Tactic:
]

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

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ (match 0, fun m x ↦
      Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
        (fun n ih s t r' s' t' ↦
          match n, ih with
          | 0, ih => (r', s', t')
          | k.succ, ih =>
            have q := r' / k.succ;
            ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
        m with
    | 0, ih => (r', s', t')
    | k.succ, ih =>
      have q := r' / k.succ;
      ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t) =
    (r', s', t')

Tactic:
]

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

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ (match r.succ, fun m x ↦
      Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
        (fun n ih s t r' s' t' ↦
          match n, ih with
          | 0, ih => (r', s', t')
          | k.succ, ih =>
            have q := r' / k.succ;
            ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
        m with
    | 0, ih => (r', s', t')
    | k.succ, ih =>
      have q := r' / k.succ;
      ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t) =
    (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t

Tactic:
]

Goal state after:
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ (match r.succ, fun m x ↦
      Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
        (fun n ih s t r' s' t' ↦
          match n, ih with
          | 0, ih => (r', s', t')
          | k.succ, ih =>
            have q := r' / k.succ;
            ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
        m with
    | 0, ih => (r', s', t')
    | k.succ, ih =>
      have q := r' / k.succ;
      ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t) =
    (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
⊢ (match 0, fun m x ↦
          Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
            (fun n ih s t r' s' t' ↦
              match n, ih with
              | 0, ih => (r', s', t')
              | k.succ, ih =>
                have q := r' / k.succ;
                ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
            m with
        | 0, ih => (s, 0, 1)
        | k.succ, ih =>
          have q := s / k.succ;
          ih (s % k.succ) ⋯ (0 - ↑q * 1) (1 - ↑q * 0) k.succ 1 0).2.1 =
    0

Tactic:
]

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

Goal state before:
pp: s : ℕ
⊢ (match 0, fun m x ↦
          Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
            (fun n ih s t r' s' t' ↦
              match n, ih with
              | 0, ih => (r', s', t')
              | k.succ, ih =>
                have q := r' / k.succ;
                ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
            m with
        | 0, ih => (s, 0, 1)
        | k.succ, ih =>
          have q := s / k.succ;
          ih (s % k.succ) ⋯ (0 - ↑q * 1) (1 - ↑q * 0) k.succ 1 0).2.2 =
    1

Tactic:
]

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

Goal state before:
pp: x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x
s t s' t' : ℤ
⊢ x.gcd y = x.gcd y

Tactic:
]

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

Goal state before:
pp: x y : ℕ
⊢ x.xgcdAux 1 0 y 0 1 = ((x.xgcdAux 1 0 y 0 1).1, (x.xgcdAux 1 0 y 0 1).2)

Tactic:
]

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y ((b % a).xgcdAux (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)

Tactic:
]

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y ((b % a).xgcdAux (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
⊢ ↑b - ↑a * (↑b / ↑a) = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)

Tactic:
]

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
⊢ ↑b - ↑a * (↑b / ↑a) = ↑x * (s' - ↑b / ↑a * s) + ↑y * (t' - ↑b / ↑a * t)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑x * s' + ↑y * t' - (↑y * t * k + ↑x * s * k) = ↑x * s' + ↑y * t' - (↑y * t * k + ↑x * s * k)

Tactic:
]

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

Goal state before:
pp: x y : ℕ
this : x.P y (x.gcd y, x.gcdA y, x.gcdB y)
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y

Tactic:
]

Goal state after:
x y : ℕ
this : x.P y (x.gcd y, x.gcdA y, x.gcdB y)
⊢ ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑n.natAbs = ↑n.natAbs

Tactic:
]

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

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
]

Goal state after:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ n.gcdA k % ↑k < ↑k

Tactic:
]

Goal state after:
case refine_1
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ n.gcdA k % ↑k < ↑k
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n

Tactic:
]

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case refine_2
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : n.gcd k = (↑n * n.gcdA k % ↑k).toNat
⊢ ↑n * n.gcdA k % ↑k = ↑n * n.gcdA k % ↑k

Tactic:
]

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

Goal state before:
pp: case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ n * m % k * (r % k) % k = r % k

Tactic:
hm,

Goal state after:
case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ 1 * (r % k) % k = r % k
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ r % k = r % k

Tactic:
]

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

Goal state before:
pp: m n : ℕ
⊢ ↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + (↑n + 1) * (↑m).natAbs.gcdB n.succ

Tactic:
]

Goal state after:
m n : ℕ
⊢ ↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + (↑n + 1) * (↑m).natAbs.gcdB n.succ
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: m n : ℕ
⊢ ↑(-[m+1].gcd ↑n) = (↑m + 1) * m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n

Tactic:
]

Goal state after:
m n : ℕ
⊢ ↑(-[m+1].gcd ↑n) = (↑m + 1) * m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: m n : ℕ
⊢ ↑(-[m+1].gcd -[n+1]) = (↑m + 1) * m.succ.gcdA -[n+1].natAbs + (↑n + 1) * -[m+1].natAbs.gcdB n.succ

Tactic:
]

Goal state after:
m n : ℕ
⊢ ↑(-[m+1].gcd -[n+1]) = (↑m + 1) * m.succ.gcdA -[n+1].natAbs + (↑n + 1) * -[m+1].natAbs.gcdB n.succ
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
⊢ ↑p.succ * a_n + ↑q.succ * b_n = ↑(p + 1) * a_n + ↑(q + 1) * b_n

Tactic:
]

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

Goal state before:
pp: x y : ℤ
hc : x = 0 ∧ y = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c

Tactic:
]

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ (∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, a * (a.gcdA b * ↑(n / a.gcd b)) + b * (a.gcdB b * ↑(n / a.gcd b)) = a * x + b * y

Tactic:
]

Goal state after:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, a * (a.gcdA b * ↑(n / a.gcd b)) + b * (a.gcdB b * ↑(n / a.gcd b)) = a * x + b * y
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ b = a * c → (a ≠ b ↔ 1 < c)

Tactic:
]

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
c : α
⊢ b = a * c → (a ≠ b ↔ 1 < c)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → c ≠ 1

Tactic:
]

Goal state after:
case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → c ≠ 1
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mp
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
⊢ a = a

Tactic:
]

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

Goal state before:
pp: case mpr
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ ↑(a.gcd b) ∣ a * x + b * y

Tactic:
]

Goal state after:
case mpr
a b : ℤ
n : ℕ
x y : ℤ
h : ↑n = a * x + b * y
⊢ ↑(a.gcd b) ∣ a * x + b * y
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a < a * c

Tactic:
]

Goal state after:
case mpr
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a : α
inst✝ : MulLeftStrictMono α
c : α
⊢ 1 < c → a < a * c
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ ∃ c_1, (fun x1 x2 ↦ x1 * x2) a (b * c) = (fun x1 x2 ↦ x1 * x2) a b * c_1

Tactic:
]

Goal state after:
α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ ∃ c_1, (fun x1 x2 ↦ x1 * x2) a (b * c) = (fun x1 x2 ↦ x1 * x2) a b * c_1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b * a * a.gcdA c + b * c * a.gcdB c

Tactic:
]

Goal state after:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b * a * a.gcdA c + b * c * a.gcdB c
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b c : ℤ
habc : a ∣ c * b
hab : a.gcd b = 1
⊢ a ∣ c

Tactic:
]

Goal state after:
a b c : ℤ
habc : a ∣ c * b
hab : a.gcd b = 1
⊢ a ∣ c
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑n = ↑n

pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ 0 ≤ b

Tactic:
]

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ 0 ≤ b
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case left
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case right
M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hmn : a ^ m.gcd n = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ ↑((m + 1).gcd n) = 1

Tactic:
]

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ y ^ ↑((m + 1).gcd n) = 1
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n < ↑n

Tactic:
]

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n < ↑n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ (y ^ ↑(m + 1)) ^ (m + 1).gcdA n * 1 ^ (m + 1).gcdB n = 1

Tactic:
hm,

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ 1 ^ (m + 1).gcdA n * 1 ^ (m + 1).gcdB n = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
m n : ℕ
hmn : m.Coprime n
c : α
hab : Commute (c ^ n) (c ^ m)
⊢ c ^ (n * m) = c ^ (n * m)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ p * q ≤ n

Tactic:
]

Goal state after:
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ p * q ≤ n
Module: Mathlib.Algebra.GroupWithZero.Equiv

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : EquivLike F α β
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
f : F
⊢ f 0 = f 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * 0 = b * 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ 0 * b = 0 * b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝ + a✝¹

Tactic:
]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝ + a✝¹
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝¹ + a✝

Tactic:
]

Goal state after:
case coe.coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ a✝ ≤ a✝¹ + a✝
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsLeftRegular (a * b)
⊢ Function.Injective fun x ↦ a * b * x

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsLeftRegular (a * b)
⊢ Function.Injective fun x ↦ a * b * x
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x ↦ x * b) x = (fun x ↦ x * b) y
⊢ x * b * a = y * b * a

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x ↦ x * b) x = (fun x ↦ x * b) y
⊢ x * b * a = y * b * a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemigroup R
a b : R
ab : IsRegular (a * b)
⊢ IsRegular (a * b)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemigroup R
a b : R
ab : IsRegular (a * b)
⊢ IsRegular (a * b)
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective (fun x ↦ x * a)^[n]

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective (fun x ↦ x * a)^[n]
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : a * b = a
⊢ a * b = a

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : a * b = a
⊢ a * b = a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : b = 1
⊢ a = a

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b * a = a

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b * a = a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
h : ⊤ = 0
a : α
ha : 0 + a ≠ 0
⊢ False

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
h : ⊤ = 0
a : α
ha : 0 + a ≠ 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
n : ℕ
⊢ 0 ^ (n + 1) = 0 ^ n * 0

Tactic:
by simp only [mul_zero]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤

Tactic:
]

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a ≠ ⊤ ↔ a ≠ ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : M
⊢ x = 0 ↔ x = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
ha : a ≠ ⊤
⊢ b = a ↔ b = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀ˣ
hx : ↑x ≠ 0
H : f ↑x = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case inr
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
h : a ≤ a + c
⊢ a + c ≤ a + c

Tactic:
]

Goal state after: