mathlib-initiative/mathlib-tactics huggingface dataset:
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.oadd (m' + 1).succPNat b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m'.succPNat ((f (i + 1)).oadd 1 zero) ∧
          a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd (m' + 1).succPNat b ∧
            ((a.oadd (m' + 1).succPNat b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd (m' + 1).succPNat b).repr, ∃ i, a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).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.oadd (m' + 1).succPNat b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m'.succPNat ((f (i + 1)).oadd 1 zero) ∧
          a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd (m' + 1).succPNat b ∧
            ((a.oadd (m' + 1).succPNat b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd (m' + 1).succPNat b).repr, ∃ i, a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
f✝ : ℝ → ℝ
⊢ Multiseries.nil = Multiseries.nil

Tactic:
]

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
hd : α
u v : Stream'.Seq α
ih : dist u v ≤ 2⁻¹ ^ n
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ 2⁻¹ * 2⁻¹ ^ n ≤ 2⁻¹ * 2⁻¹ ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.DeriveCountable

Goal state before:
pp: p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ a = a' → b = b' → p

Tactic:
]

Goal state after:
p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ a = a' → b = b' → p
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : (Nat.unpair n).1 = 0
⊢ n = n

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ n = n

pp: n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ 1 ≤ (Nat.unpair n).1

pp: case a
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).2 < n

pp: case a
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).1 - 1 < n

Tactic:
]

Goal state after:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ 1 ≤ (Nat.unpair n).1

case a
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).2 < n

case a
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).1 - 1 < n
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).1 ≠ 0

Tactic:
]

Goal state after:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).1 ≠ 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case nil
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'
f g : ℝ → ℝ
h_eq : g =ᶠ[atTop] f
h_approx : g =ᶠ[atTop] 0
⊢ 0 =ᶠ[atTop] 0

Tactic:
]

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

Goal state before:
pp: case oadd.inl.none.inl.some.zero
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')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * ↑(i + 1) < ω ^ a'.repr * ω

Tactic:
]

Goal state after:
case oadd.inl.none.inl.some.zero
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')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * ↑(i + 1) < ω ^ a'.repr * ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
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'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : g =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ f - basis_hd ^ exp * coef.toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun

Tactic:
]

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

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_1
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'.repr * ↑(i + 1) < ω ^ a'.repr * ω

Tactic:
]

Goal state after:
case oadd.inl.none.inl.some.succ.refine_1
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'.repr * ↑(i + 1) < ω ^ a'.repr * ω
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 : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * ↑↑i.succPNat + repr 0 < ω ^ a.repr

Tactic:
repr_zero,

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 : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * ↑↑i.succPNat + 0 < ω ^ a.repr
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 : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * ↑↑i.succPNat < ω ^ a'.repr * ω

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 : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * ↑↑i.succPNat < ω ^ a'.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
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ (f i).repr * ↑↑1 + repr 0 < ω ^ a.repr

Tactic:
repr_zero,

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
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ (f i).repr * ↑↑1 + 0 < ω ^ a.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
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ (f i).repr < a.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
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ (f i).repr < a.repr
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:
get_elem_tactic

Goal state after:
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.repr * ↑↑m + b'.repr + 1 = ω ^ a.repr * ↑↑m + b'.repr + 1

Tactic:
]

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

Goal state before:
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
this : succ b'.repr < ω ^ a.repr
⊢ b'.repr < ω ^ a.repr

Tactic:
]

Goal state after:
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
this : succ b'.repr < ω ^ a.repr
⊢ b'.repr < ω ^ a.repr
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
]

Goal state after:
x✝ : ONote
o : ONote := x✝
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
⊢ a.repr < succ a.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
⊢ (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), h =>
      have this := ⋯;
      fun i ↦ a.fastGrowing^[i] i
    | Sum.inr f, h => fun i ↦
      have this := ⋯;
      (f i).fastGrowing i) =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      ⋯ 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:
]

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

Goal state before:
pp: o : ONote
h : o.fundamentalSequence = Sum.inl none
⊢ (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inl none, ⋯ 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) =
    Nat.succ

Tactic:
]

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

Goal state before:
pp: o a : ONote
h : o.fundamentalSequence = Sum.inl (some a)
⊢ (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inl (some a), ⋯ 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) =
    fun i ↦ a.fastGrowing^[i] i

Tactic:
]

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

Goal state before:
pp: o : ONote
f : ℕ → ONote
h : o.fundamentalSequence = Sum.inr f
⊢ (match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) Sum.inr f, ⋯ 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) =
    fun i ↦ (f i).fastGrowing i

Tactic:
]

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

Goal state before:
pp: ⊢ (fun i ↦ (fastGrowing 0)^[i] i) = fun n ↦ 2 * n

Tactic:
]

Goal state after:
⊢ (fun i ↦ (fastGrowing 0)^[i] i) = fun n ↦ 2 * n
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: i : ℕ
⊢ Nat.succ^[i] i = i + i

Tactic:
]

Goal state after:
i : ℕ
⊢ Nat.succ^[i] i = i + i
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ (fun i ↦ (fastGrowing 1)^[i] i) = fun n ↦ 2 ^ n * n

Tactic:
]

Goal state after:
⊢ (fun i ↦ (fastGrowing 1)^[i] i) = fun n ↦ 2 ^ n * n
Module: Mathlib.Tactic.LinearCombinationPrime

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

Tactic:
]

Goal state after:
α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0
Module: Mathlib.Tactic.LinearCombinationPrime

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

Tactic:
]

Goal state after:
α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' = 0
⊢ a' - b' = 0
Module: Mathlib.Tactic.LinearCombinationPrime

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

Tactic:
]

Goal state after:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n - (a - b) = 0
⊢ a' - b' = 0
Module: Mathlib.Tactic.LinearCombinationPrime

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

Tactic:
]

Goal state after:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n = 0
⊢ (a' - b') ^ n = 0
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 < ↑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 < ↑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 % ↑n = a % ↑n

Tactic:
]

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

Tactic:
]

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
⊢ ¬d = 1

Tactic:
]

Goal state after:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬d = 1
Module: Mathlib.Tactic.NormNum.NatLog

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

Tactic:
]

Goal state after:
b n : ℕ
hl : n < b
⊢ Nat.log b n = 0
Module: Mathlib.Tactic.NormNum.NatLog

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

Tactic:
]

Goal state after:
b m n : ℕ
hb : 1 < b
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
Module: Mathlib.Tactic.NormNum.NatLog

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

Tactic:
]

Goal state after:
b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
Module: Mathlib.Tactic.NormNum.NatLog

Goal state before:
pp: b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : Nat.clog b n ≤ m + 1
⊢ Nat.clog b n = m + 1

Tactic:
]

Goal state after:
b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : Nat.clog b n ≤ m + 1
⊢ Nat.clog b n = m + 1
Module: Mathlib.Tactic.NormNum.NatSqrt

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

Tactic:
]

Goal state after:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ (y ^ 2 + r).sqrt = y
Module: Mathlib.Tactic.NormNum.NatSqrt

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

Tactic:
]

Goal state after:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (y + y) = true
⊢ (y ^ 2 + r).sqrt = y
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)
⊢ ↑q ^ a = ↑q ^ ↑a

Tactic:
]

Goal state after:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : ↑x = ↑q ^ (↑a / ↑b)
⊢ ↑q ^ a = ↑q ^ ↑a
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
⊢ n.factorization = q • f

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 ≤ n.factorization

Tactic:
]

Goal state after:
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
⊢ n.factorization = q • f

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 ≤ n.factorization
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case inr
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 : ℕ
⊢ n.factorization z = n.factorization z

pp: case inr
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 : ℕ
⊢ q ∣ n.factorization z

Tactic:
]

Goal state after:
case inr
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 : ℕ
⊢ q ∣ n.factorization z
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: m b : ℕ
hk₁ : (m + 1) ^ 2 ≤ b ^ 2
hk₂ : b ^ 2 ≤ m ^ 2 + 2 * m
⊢ False

Tactic:
]

Goal state after:
m b : ℕ
hk₁ : (m + 1) ^ 2 ≤ b ^ 2
hk₂ : b ^ 2 ≤ m ^ 2 + 2 * m
⊢ False
Module: Mathlib.Tactic.NormNum.Irrational

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

Tactic:
]

Goal state after:
n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
⊢ False
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
⊢ n = 0

Tactic:
]

Goal state after:
a : ℤ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℤ
hb : -↑n = b * b
⊢ n = 0
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
⊢ x * a = x * a

Tactic:
]

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
⊢ n = 0

Tactic:
]

Goal state after:
a : ℚ
n : ℕ
h : IsInt a (Int.negOfNat n)
x✝ : IsSquare a
b : ℚ
hb : -↑n = b * b
⊢ n = 0
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
h : ↑a / ↑b = (↑q.num / ↑q.den) ^ d
⊢ 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
h : ↑a / ↑b = (↑q.num / ↑q.den) ^ d
⊢ False
Module: Mathlib.Tactic.NormNum.LegendreSymbol

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

Tactic:
]

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

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

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

Tactic:
]

Goal state after:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < b
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
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
h : ↑a / ↑b = (↑x' / ↑y) ^ d
⊢ 0 ≤ q

Tactic:
]

Goal state after:
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
h : ↑a / ↑b = (↑x' / ↑y) ^ d
⊢ 0 ≤ q
Module: Mathlib.Tactic.NormNum.LegendreSymbol

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

Tactic:
]

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 (jacobiSym a p) r

Tactic:
]

Goal state after:
p : ℕ
pp : Fact (Nat.Prime p)
a r : ℤ
hr : IsInt (jacobiSym a p) r
⊢ IsInt (jacobiSym a p) r
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)

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

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.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 (↑ab') b = jacobiSym (↑ab') b

Tactic:
]

Goal state after: