mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ (a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF

Tactic:
·

Goal state after:
case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
⊢ (a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat 0)).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (ω ^ a.repr) ∧
    (∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)) ∧
      ∀ a_1 < ω ^ a.repr, ∃ i, a_1 < ω ^ (f i).repr

pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ a.repr) ∧
    (∀ (i : ℕ),
        (f i).repr < (f (i + 1)).repr ∧
          (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ a.repr, ∃ i, a_1 < ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ (f i).repr

Tactic:
·

Goal state after:
case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (ω ^ a.repr) ∧
    (∀ (i : ℕ), (f i).repr < (f (i + 1)).repr ∧ (f i).repr < a.repr ∧ ((a.oadd 1 0).NF → ((f i).oadd 1 0).NF)) ∧
      ∀ a_1 < ω ^ a.repr, ∃ i, a_1 < ω ^ (f i).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ a.repr) ∧
    (∀ (i : ℕ),
        (f i).repr < (f (i + 1)).repr ∧
          (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ a.repr, ∃ i, a_1 < ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ (f i).repr

Tactic:
·

Goal state after:
case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ a.repr) ∧
    (∀ (i : ℕ),
        (f i).repr < (f (i + 1)).repr ∧
          (f i).repr < a.repr ∧ ((a.oadd (m' + 1).succPNat 0).NF → (a.oadd m'.succPNat ((f i).oadd 1 0)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ a.repr, ∃ i, a_1 < ω ^ a.repr * ↑m' + ω ^ a.repr + ω ^ (f i).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.some
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)

pp: case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
ihb :
  IsSuccLimit b.repr ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ i, a < (f i).repr
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m (f i)).repr

Tactic:
·

Goal state after:
case oadd.inl.some
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.some.refine_1
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr

pp: case oadd.inl.some.refine_2
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
H : (a.oadd m b).NF
⊢ b'.repr < ω ^ a.repr

Tactic:
·

Goal state after:
case oadd.inl.some.refine_1
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
b' : ONote
ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)
e : b.fundamentalSequence = Sum.inl (some b')
⊢ (a.oadd m b).repr = succ (a.oadd m b').repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
ihb :
  IsSuccLimit b.repr ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ i, a < (f i).repr
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m (f i)).repr

Tactic:
·

Goal state after:
case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
ihb :
  IsSuccLimit b.repr ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ i, a < (f i).repr
e : b.fundamentalSequence = Sum.inr f
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m (f i)).repr
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_1
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ (a % ↑n).toNat < n

pp: case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]

Tactic:
·

Goal state after:
case refine_1
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ (a % ↑n).toNat < n
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]

Tactic:
·

Goal state after:
case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a ≡ ↑(a % ↑n).toNat [ZMOD ↑n]
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_1
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a % n < n

pp: case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]

Tactic:
·

Goal state after:
case refine_1
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a % n < n
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]

Tactic:
·

Goal state after:
case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]
Module: Mathlib.Tactic.NormNum.NatLog

Goal state before:
pp: eb en : Q(ℕ)
b : ℕ := Expr.natLit! eb
n : ℕ := Expr.natLit! en
x✝¹ : ¬b ≤ 1
x✝ : ¬n ≤ 1
h : Nat.clog b n = 0
⊢ 1 < b

Tactic:
by lia

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

Goal state before:
pp: eb en : Q(ℕ)
b : ℕ := Expr.natLit! eb
n : ℕ := Expr.natLit! en
x✝¹ : ¬b ≤ 1
x✝ : ¬n ≤ 1
h : Nat.clog b n = 0
⊢ 1 < n

Tactic:
by lia

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

Goal state before:
pp: case inl
p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
h : ∀ (m : ℕ), 0 ≠ m ^ q
⊢ 0 ^ p ≠ m ^ q

pp: case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
hn : n ≠ 0
⊢ n ^ p ≠ m ^ q

Tactic:
·

Goal state after:
case inl
p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
h : ∀ (m : ℕ), 0 ≠ m ^ q
⊢ 0 ^ p ≠ m ^ q
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
hf0 : f 0 = 0
⊢ q ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case inl
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
hb : -↑n = 0 * 0
⊢ n = 0

pp: case inr
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℤ
hb : -↑n = b * b
hb₀ : b ≠ 0
⊢ n = 0

Tactic:
·

Goal state after:
case inl
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
hb : -↑n = 0 * 0
⊢ n = 0
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case a
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ a ∣ y

pp: case a
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ y ∣ a

Tactic:
·

Goal state after:
case a
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ a ∣ y
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: case inr
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℤ
hb : -↑n = b * b
hb₀ : b ≠ 0
⊢ n = 0

Tactic:
·

Goal state after:
case inr
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℤ
hb : -↑n = b * b
hb₀ : b ≠ 0
⊢ n = 0
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case a
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ y ∣ a

Tactic:
·

Goal state after:
case a
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ y ∣ a
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: case inl
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
hb : -↑n = 0 * 0
⊢ n = 0

pp: case inr
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℚ
hb : -↑n = b * b
hb₀ : b ≠ 0
⊢ n = 0

Tactic:
·

Goal state after:
case inl
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
hb : -↑n = 0 * 0
⊢ n = 0
Module: Mathlib.Tactic.NormNum.Irrational

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

pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
·

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

Goal state before:
pp: case inr
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℚ
hb : -↑n = b * b
hb₀ : b ≠ 0
⊢ n = 0

Tactic:
·

Goal state after:
case inr
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℚ
hb : -↑n = b * b
hb₀ : b ≠ 0
⊢ n = 0
Module: Mathlib.Tactic.NormNum.IsSquare

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

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

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

Tactic:
·

Goal state after:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare ↑n ∧ IsSquare (↑↑n / ↑↑d).den)
Module: Mathlib.Tactic.NormNum.IsSquare

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

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

Tactic:
·

Goal state after:
case hb0
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d
Module: Mathlib.Tactic.NormNum.IsSquare

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

Tactic:
·

Goal state after:
case h
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (↑n).natAbs.Coprime (↑d).natAbs
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)
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
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:
case hb0
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
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:
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.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 b = r

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
⊢ jacobiSymNat a b = r

Tactic:
·

Goal state after:
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 b = r
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
⊢ jacobiSymNat a b = 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
⊢ jacobiSymNat a b = r
Module: Mathlib.Tactic.NormNum.Irrational

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

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

Tactic:
·

Goal state after:
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
Module: Mathlib.Tactic.NormNum.Irrational

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

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

Tactic:
·

Goal state after:
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.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
⊢ jacobiSymNat a b = r

Tactic:
rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]

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

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

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

Tactic:
·

Goal state after:
case pos
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
⊢ ↑a / ↑b ≠ q ^ d
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
⊢ ↑a / ↑b ≠ q ^ d

pp: case neg.inr
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_odd : Odd 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
⊢ ↑a / ↑b ≠ q ^ d
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 : ℚ
hq : ¬0 ≤ q
h_odd : Odd d
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
·

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

Goal state before:
pp: case refine_1
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)
⊢ ∀ (p : ℚ), (↑x_num / ↑x_den) ^ y_num ≠ p ^ y_den

pp: case refine_2
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)
⊢ 0 ≤ ↑x_num / ↑x_den

Tactic:
·

Goal state after:
case refine_1
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)
⊢ ∀ (p : ℚ), (↑x_num / ↑x_den) ^ y_num ≠ p ^ y_den
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case refine_1.h_coprime
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)
⊢ (x_num ^ y_num).Coprime (x_den ^ y_num)

pp: case refine_1.ha
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)
⊢ ∀ (x : ℕ), x_num ^ y_num ≠ x ^ y_den

Tactic:
·

Goal state after:
case refine_1.h_coprime
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)
⊢ (x_num ^ y_num).Coprime (x_den ^ y_num)
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case refine_1.ha
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)
⊢ ∀ (x : ℕ), x_num ^ y_num ≠ x ^ y_den

Tactic:
·

Goal state after:
case refine_1.ha
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)
⊢ ∀ (x : ℕ), x_num ^ y_num ≠ x ^ y_den
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case refine_2
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)
⊢ 0 ≤ ↑x_num / ↑x_den

Tactic:
·

Goal state after:
case refine_2
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)
⊢ 0 ≤ ↑x_num / ↑x_den
Module: Mathlib.Tactic.NormNum.RealSqrt

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

pp: case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ sqrt (↑n * ⅟↑d) = ↑sn * ⅟↑sd

Tactic:
·

Goal state after:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ Invertible ↑sd