mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
h : ↑a / ↑b = (↑↑x / ↑y) ^ d
hx' : x' = ↑x
⊢ False

Tactic:
]

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
h : ↑a / ↑b = (↑↑x / ↑y) ^ d
hx' : x' = ↑x
⊢ False
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b

Tactic:
]

Goal state after:
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
⊢ False

Tactic:
have h : 2 ∣ a.gcd b := Nat.dvd_gcd (Nat.dvd_of_mod_eq_zero ha) (Nat.dvd_of_mod_eq_zero hb₁)

Goal state after:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : 2 ∣ a.gcd b
⊢ False
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : Even 1
⊢ False

Tactic:
]

Goal state after:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : (↑a).gcd ↑b = 1
h : Even 1
⊢ False
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑↑n / ↑↑d).num ∧ IsSquare ↑d)

pp: case hb0
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

pp: case h
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (↑n).natAbs.Coprime (↑d).natAbs

Tactic:
]

Goal state after:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (↑↑n / ↑↑d).num ∧ IsSquare ↑d)

case hb0
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

case h
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (↑n).natAbs.Coprime (↑d).natAbs
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a * ↑y ^ d = ↑x ^ d * ↑b
⊢ False

pp: case neg.hb
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ ↑b ≠ 0

pp: case neg.hd
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ ↑y ^ d ≠ 0

Tactic:
]

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a * ↑y ^ d = ↑x ^ d * ↑b
⊢ False

case neg.hb
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ ↑b ≠ 0

case neg.hd
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ ↑y ^ d ≠ 0
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
⊢ ¬IsSquare (-(↑n / ↑d))

Tactic:
]

Goal state after:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
⊢ ¬IsSquare (-(↑n / ↑d))
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑n / ↑d

Tactic:
]

Goal state after:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑n / ↑d
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: case inl
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
ha' : legendreSym 2 ↑a = 1
hc : b / 2 = 0
hr : jacobiSymNat a 0 = r
⊢ jacobiSymNat a 0 = jacobiSymNat a 0

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSym (↑a) c = r

Tactic:
]

Goal state after:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSym (↑a) c = r
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a / 2) b = jacobiSym (↑a / 2) b

pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
]

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg.inl
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
this : ↑a / ↑b ≠ q ^ d
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
]

Goal state after:
case neg.inl
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
this : ↑a / ↑b ≠ q ^ d
⊢ ↑a / ↑b ≠ q ^ d
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 1 % 2 = 1

pp: case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Tactic:
]

Goal state after:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg.inr
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
h_odd : Odd d
hq : ↑a / ↑b = q ^ d
⊢ 0 ≤ ↑a / ↑b

Tactic:
]

Goal state after:
case neg.inr
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
h_odd : Odd d
hq : ↑a / ↑b = q ^ d
⊢ 0 ≤ ↑a / ↑b
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a / 2) b = jacobiSym (↑a / 2) b

pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
]

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 7 % 2 = 1

pp: case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Tactic:
]

Goal state after:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
⊢ Irrational ((↑x_num * ⅟↑x_den) ^ (↑y_num * ⅟↑y_den))

Tactic:
]

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
⊢ Irrational ((↑x_num * ⅟↑x_den) ^ (↑y_num * ⅟↑y_den))
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ -jacobiSym (↑a / 2) b = -jacobiSym (↑a / 2) b

pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
]

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 3 % 2 = 1

pp: case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Tactic:
]

Goal state after:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ -jacobiSym (↑a / 2) b = -jacobiSym (↑a / 2) b

pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
]

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 5 % 2 = 1

pp: case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Tactic:
]

Goal state after:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSym (↑b) a = r

Tactic:
]

Goal state after:
a b : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSym (↑b) a = r
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSym (↑b) a = r

Tactic:
]

Goal state after:
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSym (↑b) a = r
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ Irrational (↑(↑x_num / ↑x_den) ^ ↑(↑y_num / ↑y_den))

Tactic:
]

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ Irrational (↑(↑x_num / ↑x_den) ^ ↑(↑y_num / ↑y_den))
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSym (↑b) a = r

Tactic:
]

Goal state after:
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSym (↑b) a = r
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a m : ℕ
⊢ a.mod m = a.mod m

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a b m : ℕ
⊢ a ^ b * (a ^ b * a) % m = a ^ b * (a ^ b * a) % m

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ Irrational (x⁻¹ ^ y)

Tactic:
]

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ Irrational (x⁻¹ ^ y)
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : num_k ^ 2 < num
hn2 : num < (num_k + 1) ^ 2
⊢ Irrational (x ^ (1 / 2))

Tactic:
]

Goal state after:
x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : num_k ^ 2 < num
hn2 : num < (num_k + 1) ^ 2
⊢ Irrational (x ^ (1 / 2))
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ Irrational (x ^ (1 / 2))

Tactic:
]

Goal state after:
x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ Irrational (x ^ (1 / 2))
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ ↑d ≠ 0

Tactic:
]

Goal state after:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ ↑d ≠ 0
Module: Mathlib.Tactic.Polynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
a : R
n : ℕ
⊢ Polynomial.C a * Polynomial.X ^ n = Polynomial.C a * Polynomial.X ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ ↑r = ↑r

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑(a ^ b % n) = ↑((a ^ b).mod n)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑(a ^ b % n) = ↑((a ^ b).mod n)
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ a✝ ^ ↑b = ↑((a.pow b).mod n)

Tactic:
rw [h, Nat.cast_id, Nat.pow_eq, ← Nat.cast_pow, CharP.natCast_eq_natCast_mod α n]
    rfl

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -1 * b = (↑n - 1) * b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -1 * b = (↑n - 1) * b
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -1 * (a * b) = (↑n - 1) * a * b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -1 * (a * b) = (↑n - 1) * a * b
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a ≤ b
h₃ : b.minFac = b
H : FactorsHelper m b l
pa : Nat.Prime a
pb : Nat.Prime b
f₁ : List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (b :: l)
f₂ : ∀ (a : ℕ), a ∈ l → Nat.Prime a
f₃ : l.prod = m
⊢ n = n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ Icc m n = Icc m n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc m n = s
⊢ Icc m n = Icc m n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) n = s
⊢ Ioc m n = Ioc m n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) (n - 1) = s
⊢ Icc (m + 1) (n - 1) = Icc (m + 1) (n - 1)

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ Icc m n = Icc m n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc m (n - 1) = s
⊢ Ico m n = Ico m n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) n = s
⊢ Ioc m n = Ioc m n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) (n - 1) = s
⊢ Icc (m + 1) (n - 1) = Icc (m + 1) (n - 1)

Tactic:
]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) = List.dlookup x m

pp: case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst

Tactic:
]

Goal state after:
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) = List.dlookup x m

case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true) ↔ ¬(List.dlookup a A).getD 0 = 0

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true) ↔ ¬(List.dlookup a A).getD 0 = 0
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ ¬(some od).getD 0 = 0

pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ List.dlookup a A = some od

Tactic:
]

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ ¬(some od).getD 0 = 0

α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ List.dlookup a A = some od
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
⊢ ⟨a, (List.dlookup a A.dedupKeys).getD 0⟩ ∈ A.dedupKeys ∧ (decide ¬(List.dlookup a A.dedupKeys).getD 0 = 0) = true

Tactic:
]

Goal state after:
case h
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
⊢ ⟨a, (List.dlookup a A.dedupKeys).getD 0⟩ ∈ A.dedupKeys ∧ (decide ¬(List.dlookup a A.dedupKeys).getD 0 = 0) = true
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId (xs.zip tail✝) x = y ↔ tail✝[n✝]? = some y

pp: case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x

Tactic:
]

Goal state after:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId (xs.zip tail✝) x = y ↔ tail✝[n✝]? = some y

case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case none
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = none
⊢ x ∈ ys ↔ x ∈ ys

Tactic:
]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : y = val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
]

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : y = val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs