mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case pos
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B

pp: case neg
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : ¬e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
·

Goal state after:
case pos
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
he : e = 0
⊢ P ^ (e - 1) ∣ differentIdeal A B
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : ζ ∈ torsion K
h : x = ζ * ∏ i, fundSystem K i ^ f i
⊢ Additive.ofMul ↑x = ∑ i, f i • (basisModTorsion K) i

Tactic:
calc
    Additive.ofMul ↑x
    _ = ∑ i, (f i) • Additive.ofMul ↑(fundSystem K i) := by
          rw [h, QuotientGroup.mk_mul, (QuotientGroup.eq_one_iff _).mpr hζ, one_mul,
            QuotientGroup.mk_prod, ofMul_prod]; rfl
    _ = ∑ i, (f i) • (basisModTorsion K i) := by
          simp_rw [fundSystem, QuotientGroup.out_eq', ofMul_toMul]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case pos
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : p = ⊥
⊢ ¬P ∣ differentIdeal A B

pp: case neg
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
⊢ ¬P ∣ differentIdeal A B

Tactic:
·

Goal state after:
case pos
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : p = ⊥
⊢ ¬P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))

pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x - 1
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x - 1
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))

Tactic:
·

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x - 1
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case pos.inl
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ ⊥
⊢ ¬⊥ ∣ differentIdeal A B

pp: case pos.inr
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
x : B
hx : (intTrace A B) x ∉ ⊥
hxQ : x ∈ ⊥
⊢ ¬P ∣ differentIdeal A B

Tactic:
·

Goal state after:
case pos.inl
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
Q : Ideal B
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ ⊥
⊢ ¬⊥ ∣ differentIdeal A B
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))

Tactic:
·

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case pos.inr
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
x : B
hx : (intTrace A B) x ∉ ⊥
hxQ : x ∈ ⊥
⊢ ¬P ∣ differentIdeal A B

Tactic:
·

Goal state after:
case pos.inr
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
x : B
hx : (intTrace A B) x ∉ ⊥
hxQ : x ∈ ⊥
⊢ ¬P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
h_tors : ζ ∈ torsion K
⊢ (fun ζe ↦ x = ↑ζe.1 * ∏ i, fundSystem K i ^ ζe.2 i) (⟨ζ, h_tors⟩, ⇑((basisModTorsion K).repr (Additive.ofMul ↑x)))

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
h_tors : ζ ∈ torsion K
⊢ ∀ (y : ↥(torsion K) × (Fin (rank K) → ℤ)),
    (fun ζe ↦ x = ↑ζe.1 * ∏ i, fundSystem K i ^ ζe.2 i) y →
      y = (⟨ζ, h_tors⟩, ⇑((basisModTorsion K).repr (Additive.ofMul ↑x)))

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
h_tors : ζ ∈ torsion K
⊢ (fun ζe ↦ x = ↑ζe.1 * ∏ i, fundSystem K i ^ ζe.2 i) (⟨ζ, h_tors⟩, ⇑((basisModTorsion K).repr (Additive.ofMul ↑x)))
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
h_tors : ζ ∈ torsion K
⊢ ∀ (y : ↥(torsion K) × (Fin (rank K) → ℤ)),
    (fun ζe ↦ x = ↑ζe.1 * ∏ i, fundSystem K i ^ ζe.2 i) y →
      y = (⟨ζ, h_tors⟩, ⇑((basisModTorsion K).repr (Additive.ofMul ↑x)))

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i, fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹
h_tors : ζ ∈ torsion K
⊢ ∀ (y : ↥(torsion K) × (Fin (rank K) → ℤ)),
    (fun ζe ↦ x = ↑ζe.1 * ∏ i, fundSystem K i ^ ζe.2 i) y →
      y = (⟨ζ, h_tors⟩, ⇑((basisModTorsion K).repr (Additive.ofMul ↑x)))
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case inl
n : ℕ
h : Prime n
⊢ (n ^ 0).Deficient

pp: case inr
n m : ℕ
h : Prime n
h✝ : m > 0
⊢ (n ^ m).Deficient

Tactic:
·

Goal state after:
case inl
n : ℕ
h : Prime n
⊢ (n ^ 0).Deficient
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case inr
n m : ℕ
h : Prime n
h✝ : m > 0
⊢ (n ^ m).Deficient

Tactic:
·

Goal state after:
case inr
n m : ℕ
h : Prime n
h✝ : m > 0
⊢ (n ^ m).Deficient
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case h.left
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient}

pp: case h.right
n : ℕ
⊢ n < 2 ^ (n + 1)

Tactic:
·

Goal state after:
case h.left
n : ℕ
⊢ 2 ^ (n + 1) ∈ {n | Even n ∧ n.Deficient}
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case h.right
n : ℕ
⊢ n < 2 ^ (n + 1)

Tactic:
·

Goal state after:
case h.right
n : ℕ
⊢ n < 2 ^ (n + 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case pos
n : ℕ
h : n = 0
⊢ n.Abundant ↔ 2 < n.abundancyIndex

pp: case neg
n : ℕ
h : ¬n = 0
⊢ n.Abundant ↔ 2 < n.abundancyIndex

Tactic:
·

Goal state after:
case pos
n : ℕ
h : n = 0
⊢ n.Abundant ↔ 2 < n.abundancyIndex
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case neg
n : ℕ
h : ¬n = 0
⊢ n.Abundant ↔ 2 < n.abundancyIndex

Tactic:
·

Goal state after:
case neg
n : ℕ
h : ¬n = 0
⊢ n.Abundant ↔ 2 < n.abundancyIndex
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
·

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case pos
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ False

pp: case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ False

Tactic:
·

Goal state after:
case pos
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
·

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ False

Tactic:
·

Goal state after:
case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg.refine_1
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
⊢ ∀ i ∈ FractionalIdeal.dual A K 1, ∀ j ∈ ↑(Ideal.map (algebraMap A B) p), (Algebra.trace K L) (i * j) ∈ ↑p

pp: case neg.refine_2
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
⊢ ∀ (x y : L), (Algebra.trace K L) x ∈ ↑p → (Algebra.trace K L) y ∈ ↑p → (Algebra.trace K L) (x + y) ∈ ↑p

Tactic:
·

Goal state after:
case neg.refine_1
A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x : B
hxQ : x ∈ Q
hx : (intTrace A B) x ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
⊢ ∀ i ∈ FractionalIdeal.dual A K 1, ∀ j ∈ ↑(Ideal.map (algebraMap A B) p), (Algebra.trace K L) (i * j) ∈ ↑p
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
·

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
·

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) → IsSquare a

pp: case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a

Tactic:
·

Goal state after:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ y, ↑y * ↑y = a) → IsSquare a
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a

Tactic:
·

Goal state after:
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a → ∃ y, ↑y * ↑y = a
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

Tactic:
·

Goal state after:
case inl
inst✝ : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
·

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl.«0»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨0, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨0, ⋯⟩ ^ (2 / 2) = -1

pp: case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = -1

Tactic:
·

Goal state after:
case inl.«0»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨0, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨0, ⋯⟩ ^ (2 / 2) = -1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = -1

Tactic:
·

Goal state after:
case inl.«1»
inst✝ : Fact (Nat.Prime 2)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0 → (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ ^ (2 / 2) = -1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
·

Goal state after:
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
·

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)