mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := ⋯
ϖ : R := ⋯
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := ⋯
x : R
⊢ x ∈ I → x * ϖ ^ n ∈ I * I ^ n

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := ⋯
ϖ : R := ⋯
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := ⋯
x : R
⊢ x * ϖ ^ n ∈ I * I ^ n → x ∈ I

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := ⋯
ϖ : R := ⋯
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := ⋯
x : R
⊢ x ∈ I → x * ϖ ^ n ∈ I * I ^ n

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := ⋯
ϖ : R := ⋯
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := ⋯
x : R
⊢ x * ϖ ^ n ∈ I * I ^ n → x ∈ I
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ J(a | b) ^ 2 = 1

pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ J(a | b) ^ 2 = 1

Tactic:
<;>

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ J(a | b) ^ 2 = 1

case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ J(a | b) ^ 2 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ 1 ^ 2 = 1

pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ (-1) ^ 2 = 1

Tactic:
<;>

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ 1 ^ 2 = 1

case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ (-1) ^ 2 = 1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε

Tactic:
have h₀ : LocallyIntegrableOn (fun t ↦ S t - l * t) (Set.Ici 1) := by
    refine .sub ?_ <| ContinuousOn.locallyIntegrableOn (by fun_prop) measurableSet_Ici
    simpa using locallyIntegrableOn_mul_sum_Icc f zero_le_one (locallyIntegrableOn_const 1)

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n * y

pp: case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * x = y

Tactic:
<;>

Goal state after:
case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n * y

case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * x = y
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ha
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ Odd a

pp: case hb
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ Odd b

Tactic:
<;>

Goal state after:
case ha
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ Odd a

case hb
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ Odd b
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑a.natAbs
⊢ J(a | b) = J(a | b % (4 * a.natAbs))

pp: case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ J(a | b) = J(a | b % (4 * a.natAbs))

Tactic:
<;>

Goal state after:
case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑a.natAbs
⊢ J(a | b) = J(a | b % (4 * a.natAbs))

case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ J(a | b) = J(a | b % (4 * a.natAbs))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑a.natAbs
⊢ J(a | b) = J(↑a.natAbs | b % (4 * a.natAbs))

pp: case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ J(a | b) = J(-↑a.natAbs | b % (4 * a.natAbs))

Tactic:
<;>

Goal state after:
case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑a.natAbs
⊢ J(a | b) = J(↑a.natAbs | b % (4 * a.natAbs))

case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ J(a | b) = J(-↑a.natAbs | b % (4 * a.natAbs))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
h✝ : a % 4 = 0
⊢ fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

pp: case ind.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
h✝ : ¬a % 4 = 0
⊢ (if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
    else
      if ha1 : a = 1 then if flip = true then -1 else 1
      else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
<;>

Goal state after:
case ind.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
h✝ : a % 4 = 0
⊢ fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

case ind.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
h✝ : ¬a % 4 = 0
⊢ (if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
    else
      if ha1 : a = 1 then if flip = true then -1 else 1
      else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ Set.Icc x y = Set.Icc x y⁻¹⁻¹

pp: case inr.h₁
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ x ≤ 1

pp: case inr.h₂
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ 1 ≤ y⁻¹⁻¹

Tactic:
<;>

Goal state after:
case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ Set.Icc x y = Set.Icc x y⁻¹⁻¹

case inr.h₁
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ x ≤ 1

case inr.h₂
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ 1 ≤ y⁻¹⁻¹
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
h✝ : a % 2 = 0
⊢ fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

pp: case ind.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
h✝ : ¬a % 2 = 0
⊢ (if ha1 : a = 1 then if flip = true then -1 else 1
    else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
<;>

Goal state after:
case ind.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
h✝ : a % 2 = 0
⊢ fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

case ind.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
h✝ : ¬a % 2 = 0
⊢ (if ha1 : a = 1 then if flip = true then -1 else 1
    else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case pos
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(↑a / 2 | b) else J(↑a / 2 | b)) =
    if flip = true then -if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)

pp: case neg
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : ¬(b % 8 = 3 ∨ b % 8 = 5)
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(↑a / 2 | b) else J(↑a / 2 | b)) =
    if flip = true then -if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)

Tactic:
<;>

Goal state after:
case pos
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(↑a / 2 | b) else J(↑a / 2 | b)) =
    if flip = true then -if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)

case neg
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : ¬(b % 8 = 3 ∨ b % 8 = 5)
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(↑a / 2 | b) else J(↑a / 2 | b)) =
    if flip = true then -if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case pos.false
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if false = false then -J(↑a / 2 | b) else J(↑a / 2 | b)) = if false = true then J(↑a / 2 | b) else -J(↑a / 2 | b)

pp: case pos.true
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if true = false then -J(↑a / 2 | b) else J(↑a / 2 | b)) = if true = true then J(↑a / 2 | b) else -J(↑a / 2 | b)

Tactic:
<;>

Goal state after:
case pos.false
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if false = false then -J(↑a / 2 | b) else J(↑a / 2 | b)) = if false = true then J(↑a / 2 | b) else -J(↑a / 2 | b)

case pos.true
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if true = false then -J(↑a / 2 | b) else J(↑a / 2 | b)) = if true = true then J(↑a / 2 | b) else -J(↑a / 2 | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
h✝ : a = 1
⊢ (if flip = true then -1 else 1) = if flip = true then -J(↑a | b) else J(↑a | b)

pp: case ind.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
h✝ : ¬a = 1
⊢ (if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
<;>

Goal state after:
case ind.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
h✝ : a = 1
⊢ (if flip = true then -1 else 1) = if flip = true then -J(↑a | b) else J(↑a | b)

case ind.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
h✝ : ¬a = 1
⊢ (if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isFalse.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
h✝ : b % a = 0
⊢ 0 = if flip = true then -J(↑a | b) else J(↑a | b)

pp: case ind.isFalse.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
h✝ : ¬b % a = 0
⊢ fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
<;>

Goal state after:
case ind.isFalse.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
h✝ : b % a = 0
⊢ 0 = if flip = true then -J(↑a | b) else J(↑a | b)

case ind.isFalse.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
h✝ : ¬b % a = 0
⊢ fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case pos
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J(↑b | a) else J(↑b | a)) =
    if flip = true then -if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)
    else if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)

pp: case neg
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : ¬(a % 4 = 3 ∧ b % 4 = 3)
⊢ (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J(↑b | a) else J(↑b | a)) =
    if flip = true then -if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)
    else if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)

Tactic:
<;>

Goal state after:
case pos
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J(↑b | a) else J(↑b | a)) =
    if flip = true then -if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)
    else if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)

case neg
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : ¬(a % 4 = 3 ∧ b % 4 = 3)
⊢ (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J(↑b | a) else J(↑b | a)) =
    if flip = true then -if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)
    else if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case pos.false
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if false = false then -J(↑b | a) else J(↑b | a)) = if false = true then J(↑b | a) else -J(↑b | a)

pp: case pos.true
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if true = false then -J(↑b | a) else J(↑b | a)) = if true = true then J(↑b | a) else -J(↑b | a)

Tactic:
<;>

Goal state after:
case pos.false
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if false = false then -J(↑b | a) else J(↑b | a)) = if false = true then J(↑b | a) else -J(↑b | a)

case pos.true
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if true = false then -J(↑b | a) else J(↑b | a)) = if true = true then J(↑b | a) else -J(↑b | a)