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

Goal state before:
pp: case cons.nil
x e : ℝ
es : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (∀ f ∈ basis, 0 < f x) → 0 < toFun es basis x ∧ (log ∘ toFun es basis) x = toLogFun es basis x
h_basis : WellFormedBasis []
hx : ∀ f ∈ [], 0 < f x
⊢ 0 < toFun (e :: es) [] x ∧ (log ∘ toFun (e :: es) []) x = toLogFun (e :: es) [] x

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: x e : ℝ
es : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (∀ f ∈ basis, 0 < f x) → 0 < toFun es basis x ∧ (log ∘ toFun es basis) x = toLogFun es basis x
b : ℝ → ℝ
bs : List (ℝ → ℝ)
h_basis : WellFormedBasis (b :: bs)
hx : ∀ f ∈ b :: bs, 0 < f x
hpos : 0 < toFun es bs x
heq : (log ∘ toFun es bs) x = toLogFun es bs x
⊢ b ∈ b :: bs

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
hx : ∀ f ∈ basis, 0 < f x
⊢ 0 < m.toFun basis x ∧ (log ∘ m.toFun basis) x = m.toLogFun basis x

Tactic:
induction m generalizing basis with
  | nil => simp
  | cons e es ih =>
    cases basis with
    | nil => simp
    | cons b bs =>
      simp only [toFun_cons, Pi.mul_apply, Pi.pow_apply, Function.comp_apply, toLogFun_cons,
        Pi.add_apply, Pi.smul_apply, smul_eq_mul]
      obtain ⟨hpos, heq⟩ := ih h_basis.tail (hx · <| by simp [·])
      refine ⟨mul_pos (Real.rpow_pos_of_pos (hx b (by simp)) _) hpos, ?_⟩
      rw [Real.log_mul (Real.rpow_pos_of_pos (hx b (by simp)) _).ne' hpos.ne',
            Real.log_rpow (hx b (by simp)), ← heq]
      rfl

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ nil.leadingExp = ⊥ ↔ nil = nil

Tactic:
simp

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

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
⊢ (cons exp✝ coef✝ tl✝).leadingExp = ⊥ ↔ cons exp✝ coef✝ tl✝ = nil

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
e : ℝ
es : List ℝ
ih :
  ∀ {basis_tl : Basis},
    (∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)) → toLogFun es basis_tl =o[atTop] (log ∘ basis_hd)
b : ℝ → ℝ
bs : List (ℝ → ℝ)
hlo : ∀ b_1 ∈ b :: bs, (log ∘ b_1) =o[atTop] (log ∘ basis_hd)
⊢ b ∈ b :: bs

Tactic:
simp

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

Goal state before:
pp: case h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ x ∈ (mk Multiseries.nil 0).seq, x.2.Sorted

Tactic:
simp

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

Goal state before:
pp: case h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk Multiseries.nil 0).seq

Tactic:
simp

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Multiseries.nil.Sorted

Tactic:
constructor <;> simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
⊢ basis_hd ∈ basis_hd :: basis_tl

Tactic:
simp

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

Goal state before:
pp: case h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (cons exp coef Multiseries.nil) 0).seq

Tactic:
simp

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

Goal state before:
pp: case seq.h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk tl 0).seq
⊢ ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted

Tactic:
simp at h_tl_coef ⊢

Goal state after:
case seq.h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk tl 0).seq
h_tl_coef : ∀ (a : ℝ) (b : MultiseriesExpansion basis_tl), (a, b) ∈ tl → b.Sorted
⊢ coef.Sorted ∧ ∀ (a : ℝ) (b : MultiseriesExpansion basis_tl), (a, b) ∈ tl → b.Sorted
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd < 0
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
⊢ basis_hd ∈ basis_hd :: basis_tl

Tactic:
simp

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq
⊢ (exp, coef) ∈ (mk (Multiseries.cons exp coef tl) 0).seq

Tactic:
simp

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

Goal state before:
pp: case seq.right.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef Multiseries.nil) 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef Multiseries.nil) 0).seq
⊢ Multiseries.nil.leadingExp < ↑exp ∧ Multiseries.nil.Sorted

Tactic:
simp

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
h : Multiseries.nil.Sorted
⊢ Multiseries.nil.tail.Sorted

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case e'_5
coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_exps : exps.FirstNonzeroIsNeg
t : Monomial := { coef := coef, unit := exps }
⊢ 0 = t.coef * 0

Tactic:
simp

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
f : ℝ → ℝ
⊢ (mk Multiseries.nil f).Sorted

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case h₁
basis : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis basis
h1 : List.length t1.unit = List.length basis
h2 : List.length t2.unit = List.length basis
h_coef2 : ¬t2.coef = 0
h_lt : t1.unit < t2.unit
⊢ (fun x ↦ t1.coef) =O[atTop] fun x ↦ t2.coef

Tactic:
simp

Goal state after:
case h₁
basis : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis basis
h1 : List.length t1.unit = List.length basis
h2 : List.length t2.unit = List.length basis
h_coef2 : ¬t2.coef = 0
h_lt : t1.unit < t2.unit
⊢ t2.coef = 0 → t1.coef = 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case a
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
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'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ 0 ≤ dist s t

Tactic:
simp

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

Goal state before:
pp: case zero
α : 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'
s t : Stream'.Seq α
base : motive s t
⊢ dist s t ≤ 2⁻¹ ^ 0

Tactic:
simp

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ ¬(mk (Multiseries.cons exp coef tl) f).IsZero

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case nat
n : ℕ
⊢ (let p := Nat.unpair (Nat.pair 0 n);
    if h : p.1 = 0 then S.nat p.2
    else
      have this := ⋯;
      have this := ⋯;
      have this := ⋯;
      (S.decode (p.1 - 1)).cons (S.decode p.2)) =
    S.nat n

Tactic:
simp

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

Goal state before:
pp: case hyp.inr.inr
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ((mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)).Approximates ∨
      ∃ (h : basis_hd = basis_hd ∧ basis_tl = basis_tl), motive (⋯ ▸ mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))) ∧
    (basis_hd = basis_hd ∧ basis_tl = basis_tl) ∧ ms ≍ mk (Multiseries.cons exp coef tl) ms.toFun

Tactic:
simp

Goal state after:
case hyp.inr.inr
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ((mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)).Approximates ∨
      motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))) ∧
    ms.seq = Multiseries.cons exp coef tl
Module: Mathlib.Tactic.DeriveEncodable

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

Tactic:
simp

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

Goal state before:
pp: case oadd.inl.none.inl.none.zero.left
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ 1 = succ 0

Tactic:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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

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:
simp

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:
simp

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

Goal state before:
pp: case h
d : ℕ
q : ℚ
hq : 0 ≤ q
ha : ↑1 / ↑0 = q ^ d
⊢ 1 = 1 ^ d

Tactic:
simp

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:
simp

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
⊢ jacobiSym (↑a) b = jacobiSym (↑a / 2) b

Tactic:
← jacobiSym.even_odd (mod_cast ha),

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (↑a / 2) b else jacobiSym (↑a / 2) b) = jacobiSym (↑a / 2) b

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: a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
by_cases hq : 0 ≤ q

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

case neg
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.LegendreSymbol

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

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
⊢ jacobiSym (↑a) b = jacobiSym (↑a / 2) b

Tactic:
← jacobiSym.even_odd (mod_cast ha),

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (↑a / 2) b else jacobiSym (↑a / 2) b) = jacobiSym (↑a / 2) b

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: 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:
simp

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
⊢ jacobiSym (↑a) b = -jacobiSym (↑a / 2) b

Tactic:
← jacobiSym.even_odd (mod_cast ha),

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (↑a / 2) b else jacobiSym (↑a / 2) b) = -jacobiSym (↑a / 2) b

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.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:
simp

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
⊢ ↑y_num * (↑y_den)⁻¹ = ↑y_num / ↑y_den
Module: Mathlib.Tactic.NormNum.LegendreSymbol

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

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
⊢ jacobiSym (↑a) b = -jacobiSym (↑a / 2) b

Tactic:
← jacobiSym.even_odd (mod_cast ha),

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (↑a / 2) b else jacobiSym (↑a / 2) b) = -jacobiSym (↑a / 2) b

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.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:
simp

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)
⊢ ↑x_num * (↑x_den)⁻¹ = ↑x_num / ↑x_den
Module: Mathlib.Tactic.NormNum.LegendreSymbol

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

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: x : ℝ
n k : ℕ
hx_isNat : IsNat x n
hn1 : k ^ 2 < n
hn2 : n < (k + 1) ^ 2
⊢ n.Coprime 1

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: m n : ℕ+
⊢ m = n ↔ ↑m = ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: m n : ℕ+
⊢ m ≤ n ↔ ↑m ≤ ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: m n : ℕ+
⊢ m < n ↔ ↑m < ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Tactic.Polynomial.Basic

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
r : R
⊢ Polynomial.map (algebraMap R A) ((algebraMap R (Polynomial R)) r) = (algebraMap A (Polynomial A)) ((algebraMap R A) r)

Tactic:
simp

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:
simp

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

Goal state after:
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case cons.nil
p a : Prop
as : List Prop
⊢ ∀ (n n' : ℕ), n' = [].length + n → ∀ (bs : List Prop), mk ([].reverseAux bs) n' ↔ mk bs n

Tactic:
simp

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

Goal state before:
pp: m : ℕ
⊢ Ico m 0 = ∅

Tactic:
simp

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

Goal state before:
pp: ⊢ Iio 0 = ∅

Tactic:
simp

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

Goal state before:
pp: case e_opt.nil
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) []) = List.dlookup x []

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
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)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y

Tactic:
simp

Goal state after: