mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd : ℝ → ℝ
basis_tl : Basis
h : (mk Multiseries.nil f).Approximates
⊢ f =ᶠ[atTop] 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (mk (Multiseries.cons exp coef tl) f).Approximates
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
⊢ ms.replaceFun f = ms.replaceFun f ∧ ms.Approximates ∧ ms.toFun =ᶠ[atTop] f

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
⊢ (ms.replaceFun f).Approximates

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_neg : ms.leadingExp < 0
h_approx : ms.Approximates
⊢ Tendsto ms.toFun atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
f : ℝ → ℝ
h : (mk Multiseries.nil f).Approximates
⊢ (mk Multiseries.nil f).leadingExp < 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd✝ : ℝ → ℝ
basis_tl✝ : Basis
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ (x : MultiseriesExpansion (basis_hd :: basis_tl)), x.seq = x.seq ∧ x.toFun =ᶠ[atTop] x.toFun

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd✝ : ℝ → ℝ
basis_tl✝ : Basis
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ {x y : MultiseriesExpansion (basis_hd :: basis_tl)},
    x.seq = y.seq ∧ x.toFun =ᶠ[atTop] y.toFun → y.seq = x.seq ∧ y.toFun =ᶠ[atTop] x.toFun

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd✝ : ℝ → ℝ
basis_tl✝ : Basis
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ {x y z : MultiseriesExpansion (basis_hd :: basis_tl)},
    x.seq = y.seq ∧ x.toFun =ᶠ[atTop] y.toFun →
      y.seq = z.seq ∧ y.toFun =ᶠ[atTop] z.toFun → x.seq = z.seq ∧ x.toFun =ᶠ[atTop] z.toFun

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
x y : MultiseriesExpansion (basis_hd :: basis_tl)
⊢ x ≈ y ↔ x.seq = y.seq ∧ x.toFun =ᶠ[atTop] y.toFun

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DuplicateDecls

Goal state before:
pp: e✝² : Expr
fvars✝ : Array Expr
e✝¹ : Expr
n : Nat := fvars✝.size
fvars : Vector Expr n := fvars✝.toVector
remainingTypes✝ : Vector (Option Expr) n
e✝ : Expr := eraseUnivs e✝¹
sortedTypes✝ : Array Expr := #[]
x✝ : Nat
remainingTypes : Vector (Option Expr) n := __s✝².fst
__s✝¹ : Expr × Array Expr := __s✝².snd
e : Expr := __s✝¹.fst
sortedTypes : Array Expr := __s✝¹.snd
minType?✝ : Option (Fin n × Expr) := none
i : Nat
h : i ∈ 0...n
minType? : Option (Fin n × Expr) := __s✝
type : Expr
__r✝ : Unit
⊢ i < n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
⊢ o.FundamentalSequenceProp o.fundamentalSequence

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: x✝ : ONote
o : ONote := x✝
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
⊢ a < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
x : Option ONote ⊕ (ℕ → ONote)
e : o.fundamentalSequence = x
⊢ o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) x, ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i ↦ a.fastGrowing^[i] i
    | Sum.inr f, x => fun i ↦ (f i).fastGrowing i

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
h : o.fundamentalSequence = Sum.inl none
⊢ o.fastGrowing = Nat.succ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o a : ONote
h : o.fundamentalSequence = Sum.inl (some a)
⊢ o.fastGrowing = fun i ↦ a.fastGrowing^[i] i

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
f : ℕ → ONote
h : o.fundamentalSequence = Sum.inr f
⊢ o.fastGrowing = fun i ↦ (f i).fastGrowing i

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ fastGrowing 1 = fun n ↦ 2 * n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ fastGrowing 2 = fun n ↦ 2 ^ n * n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ fastGrowingε₀ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ fastGrowingε₀ 1 = 2

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ fastGrowingε₀ 2 = 2048

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (cmp ⟨a, ha⟩ ⟨b, hb⟩).Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: C : NONote → Sort u_1
o : NONote
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
⊢ C o

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a = b
H : a' - b' - (a - b) = 0
⊢ a' = b'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
⊢ a' = b'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: p q : AndKind
⊢ Ordering

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: p q : IProp
⊢ Ordering

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ModCases

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

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ModCases

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

Tactic:
by

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

Goal state before:
pp: x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬IsCoprime x y

Tactic:
by

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

Goal state before:
pp: b n : ℕ
hl : n.blt b = true
⊢ Nat.log b n = 0

Tactic:
by

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

Goal state before:
pp: b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1

Tactic:
by

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 < b

Tactic:
by

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

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

Goal state before:
pp: x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ x.sqrt = y

Tactic:
by

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

Goal state before:
pp: q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : ↑x = ↑q ^ (↑a / ↑b)
⊢ 0 ≤ ↑q

Tactic:
by

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

Goal state before:
pp: q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : ↑x = ↑q ^ (↑a / ↑b)
⊢ ↑b ≠ 0

Tactic:
by

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

Goal state before:
pp: q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
⊢ Irrational ((↑q).rpow ↑(↑a / ↑b))

Tactic:
by

Goal state after:
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
⊢ 0 / q = 0

Tactic:
by

Goal state after:
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
⊢ f 0 = 0

Tactic:
by

Goal state after:
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
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ^ q ∈ {x | x ≠ 0}

Tactic:
by

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

Goal state after:
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
⊢ ∃ m, n = m ^ q

Tactic:
by

Goal state after:
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
z : ℕ
⊢ p * n.factorization z = q * ?m.185

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a n : ℕ
h : IsNat a n
m k : ℕ
hm : m * m = k
hk₁ : k.blt n = true
hk₂ : n.ble (k + 2 * m) = true
⊢ ¬IsSquare a

Tactic:
by

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

Goal state before:
pp: a : ℤ
n : ℕ
h : IsNat a n
⊢ IsSquare n ↔ IsSquare a

Tactic:
by

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

Goal state before:
pp: a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
h' : n = 0
⊢ IsSquare a

Tactic:
by

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

Goal state before:
pp: n k d : ℕ
h_left : k ^ d < n
h_right : n < (k + 1) ^ d
m : ℕ
⊢ n ≠ m ^ d

Tactic:
by

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

Goal state before:
pp: n k p q : ℕ
hq : 0 < q
h_coprime : p.Coprime q
h_left : k ^ q < n
h_right : n < (k + 1) ^ q
m : ℕ
⊢ n ^ p ≠ m ^ q

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a

Tactic:
by

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

Goal state before:
pp: a : ℚ
n : ℕ
h : IsNat a n
⊢ IsSquare n ↔ IsSquare a

Tactic:
by

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

Goal state before:
pp: a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
h' : n = 0
⊢ IsSquare a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ℕ
⊢ jacobiSymNat a 0 = 1

Tactic:
by

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

Goal state before:
pp: a : ℕ
⊢ jacobiSymNat a 1 = 1

Tactic:
by

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

Goal state before:
pp: a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
⊢ n = 0 ↔ IsSquare a

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < 2 * 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSymNat 0 b = 0

Tactic:
by

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

Goal state before:
pp: a : ℚ
n d : ℕ
hn : IsSquare n
hd : IsSquare d
ha : IsNNRat a n d
⊢ IsSquare a

Tactic:
by

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

Goal state before:
pp: b : ℕ
⊢ jacobiSymNat 1 b = 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
pp : Fact (Nat.Prime p)
a r : ℤ
hr : IsInt (jacobiSym a p) r
⊢ IsInt (legendreSym p a) r

Tactic:
by

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

Goal state before:
pp: a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym a b = r

Tactic:
by

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

Goal state before:
pp: a : ℚ
n d : ℕ
hn : ¬IsSquare n
ha : IsNNRat a n d
hnd : ↑d ≤ 0
⊢ n ≠ 1

Tactic:
by

Goal state after:
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 a

Tactic:
by

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

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

Tactic:
by

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 a

Tactic:
by

Goal state after:
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
⊢ -(↑n / ↑d) < 0

Tactic:
by

Goal state after:
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 a

Tactic:
by

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

Goal state before:
pp: 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
⊢ a * y ^ d = x ^ d * b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ ¬(b % 8 = 3 ∨ b % 8 = 5)

Tactic:
by

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

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

Tactic:
by

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

Tactic:
by

Goal state after:
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
⊢ ¬(b % 8 = 3 ∨ b % 8 = 5)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
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
⊢ 0 < y_den

Tactic:
by

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

Tactic:
by

Goal state after:
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
⊢ b % 8 = 3 ∨ b % 8 = 5

Tactic:
by

Goal state after:
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
⊢ ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)

Tactic:
by

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

Tactic:
by

Goal state after:
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
⊢ b % 8 = 3 ∨ b % 8 = 5

Tactic:
by

Goal state after:
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)
⊢ ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: a b m c : ℕ
h1 : (a.pow b).mod m = c
⊢ (a.pow (2 * b)).mod m = (c.mul c).mod m

Tactic:
by

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

Goal state before:
pp: a : ℕ
⊢ (a.pow 0).mod 0 = 1

Tactic:
by

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

Goal state before:
pp: a : ℕ
⊢ (a.pow 0).mod 1 = 0

Tactic:
by

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

Goal state before:
pp: a m : ℕ
⊢ (a.pow 0).mod m.succ.succ = 1

Tactic:
by

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

Goal state before:
pp: a m : ℕ
⊢ (a.pow 1).mod m = a.mod m

Tactic:
by

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

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
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
⊢ Irrational (x ^ y)

Tactic:
by

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
⊢ 0 ≤ x

Tactic:
by

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

Goal state before:
pp: a b m c : ℕ
⊢ (a.pow b).mod m = c → (a.pow (2 * b + 1)).mod m = (c.mul ((c.mul a).mod m)).mod m

Tactic:
by

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
⊢ x⁻¹ = ↑x_den * ⅟↑x_num

Tactic:
by

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

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hx_isNNRat : IsNNRat x x_num x_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
⊢ Irrational (x ^ y)

Tactic:
by

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

Goal state before:
pp: x y : ℝ
x_num y_num y_den k : ℕ
hx_isNat : IsNat x x_num
hy_isNNRat : IsNNRat y y_num y_den
hy_coprime : y_num.Coprime y_den
hn1 : k ^ y_den < x_num
hn2 : x_num < (k + 1) ^ y_den
⊢ x_num.Coprime 1

Tactic:
by

Goal state after:
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
⊢ Nat.Coprime 1 2

Tactic:
by

Goal state after:
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
⊢ 1 / 2 * ↑2 = 1

Tactic:
by

Goal state after:
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
⊢ ↑2 * (1 / 2) = 1

Tactic:
by

Goal state after:
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
⊢ 1 / 2 = ↑1 * ⅟↑2

Tactic:
by

Goal state after: