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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsIntegrallyClosed A
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegralClosure B A L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : Nontrivial B
inst✝ : NoZeroDivisors B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (b x)
⊢ IsFractional B⁰ (↑I)ᵛ

Tactic:
obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsIntegrallyClosed A
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegralClosure B A L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : Nontrivial B
inst✝ : NoZeroDivisors B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (b x)
x : B
hx : x ≠ 0
hx' : (algebraMap B L) x ∈ I
⊢ IsFractional B⁰ (↑I)ᵛ
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsIntegrallyClosed A
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegralClosure B A L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : Nontrivial B
inst✝ : NoZeroDivisors B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (b x)
x : B
hx : x ≠ 0
hx' : (algebraMap B L) x ∈ I
y : B
hy : (algebraMap B L) y = (algebraMap K L) (discr K ⇑b)
⊢ y ≠ 0

pp: case refine_2
A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsIntegrallyClosed A
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegralClosure B A L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : Nontrivial B
inst✝ : NoZeroDivisors B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (b x)
x : B
hx : x ≠ 0
hx' : (algebraMap B L) x ∈ I
y : B
hy : (algebraMap B L) y = (algebraMap K L) (discr K ⇑b)
z : L
hz : z ∈ (↑I)ᵛ
⊢ IsInteger B ((y * x) • z)

Tactic:
· rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, map_zero,
        ← (algebraMap K L).map_zero, (algebraMap K L).injective.ne_iff]
      exact discr_not_zero_of_basis K b

Goal state after:
case refine_2
A : Type u_1
K : Type u_2
L : Type u
B : Type ?u.10
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsIntegrallyClosed A
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : IsIntegralClosure B A L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsDomain A
inst✝² : IsFractionRing B L
inst✝¹ : Nontrivial B
inst✝ : NoZeroDivisors B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
s : Finset L
b : Basis (↥s) K L
hb : ∀ (x : ↥s), IsIntegral A (b x)
x : B
hx : x ≠ 0
hx' : (algebraMap B L) x ∈ I
y : B
hy : (algebraMap B L) y = (algebraMap K L) (discr K ⇑b)
z : L
hz : z ∈ (↑I)ᵛ
⊢ IsInteger B ((y * x) • z)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case inr
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {2} ℚ ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp : ↑p ∣ (-1) ^ Module.finrank (↥ℚ⟮ζ⟯) K * 2 ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 = n
⊢ ↑p ∣ ↑2 ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
IsUnit.dvd_mul_left
        ((isUnit_pow_iff Module.finrank_pos.ne').mpr isUnit_neg_one)

Goal state after:
case inr
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {2} ℚ ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp : ↑p ∣ 2 ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 = n
⊢ ↑p ∣ ↑2 ^ Module.finrank (↥ℚ⟮ζ⟯) K
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp : ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤ ∑ x_1, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
refine (le_trans ?_ hyp).trans ?_

Goal state after:
case pos.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp : ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤ ∑ x_1, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))|

case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp : ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤ ∑ x_1, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ ∑ x_1, |(logEmbedding K) (Additive.ofMul x) x_1| ≤ ↑(Fintype.card (InfinitePlace K)) * r
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
refine (le_trans ?_ hyp).trans ?_

Goal state after:
case neg.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤
    ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))|

case neg.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ r ≤ ↑(Fintype.card (InfinitePlace K)) * r
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : ∏ w, g w ^ w.mult = ↑B
⊢ minkowskiBound K 1 < MeasureTheory.volume (convexBodyLT K g)

Tactic:
rw [convexBodyLT_volume]; convert! hB; exact congr_arg ((↑) : NNReal → ENNReal) h_gprod

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
⊢ 3 ≠ 0

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ 2 < 3

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
⊢ Odd 3

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ 0 < 3

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ ∑ x ∈ univ.erase w, |v w x| < |v w w|

Tactic:
rw [← sub_pos, sum_congr rfl (fun x hx ↦ abs_of_neg ?_), sum_neg_distrib, sub_neg_eq_add,
    sum_erase_eq_sub (mem_univ _), ← add_comm_sub]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < |v w w| - v w w + ∑ x, v w x

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ v w x < 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑⋯.unit - ↑n
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ Nat.Coprime 2 3

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ Nat.Coprime 2 3

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < ∑ x, v w x

Tactic:
· rw [sum_logEmbedding_component (exists_unit K w).choose]
      refine mul_pos_of_neg_of_neg ?_ ((exists_unit K w).choose_spec _ w.prop.symm)
      rw [mult]; split_ifs <;> norm_num

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ Nat.Coprime 2 3

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ 1 < 3

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ Finset.univ
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : ↥(unitLattice K)
a : logSpace K
b : Additive (𝓞 K)ˣ
left✝ : b ∈ ↑⊤
ha : (logEmbedding K).toIntLinearMap b = a
⊢ ((logEmbeddingQuot K).codRestrict (unitLattice K) ⋯).toIntLinearMap ⟦b⟧ = ⟨a, ⋯⟩

Tactic:
by simpa using! ha

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ quadraticCharFun F a = 0 ↔ a = 0

Tactic:
simp only [quadraticCharFun]

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ (if a = 0 then 0 else if IsSquare a then 1 else -1) = 0 ↔ a = 0
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ 4 ∣ 8

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ 3 ≠ 0

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : λ ∣ ↑a
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : (Algebra.norm ℤ) λ ∣ a
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : λ ∣ ↑b
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
hdvd : (Algebra.norm ℤ) λ ∣ b
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ 3 ≠ 2

Tactic:
by decide

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

Goal state before:
pp: case 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
inst✝³ : p.IsMaximal
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
y : B
hy : (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) y = e.symm (x, 0)
⊢ y ∈ Q

Tactic:
have := congr((e $hy).2)

Goal state after:
case 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
inst✝³ : p.IsMaximal
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝² : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝¹ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this✝ : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
y : B
hy : (Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) y = e.symm (x, 0)
this : (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) y)).2 = (e (e.symm (x, 0))).2
⊢ y ∈ Q
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ 3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (3 ^ 1)
⊢ 3 ≠ 2

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime (a ^ (2 ^ k * m) + 1)
⊢ ∃ m_1, 2 ^ k * m = 2 ^ m_1

Tactic:
rw [pow_mul] at hP

Goal state after:
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
⊢ ∃ m_1, 2 ^ k * m = 2 ^ m_1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case pos
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ n.Coprime b

Tactic:
apply Nat.coprime_of_dvd

Goal state after:
case pos
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ ∀ (k : ℕ), Prime k → k ∣ n → ¬k ∣ b
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case pos
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ n.Coprime b

pp: case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n.Coprime b

Tactic:
· -- To prove that `n` is coprime with `b`, we need to show that for all prime factors of `n`,
    -- we can derive a contradiction if `n` divides `b`.
    apply Nat.coprime_of_dvd
    -- If `k` is a prime number that divides both `n` and `b`, then we know that `n = m * k` and
    -- `b = j * k` for some natural numbers `m` and `j`. We substitute these into the hypothesis.
    rintro k hk ⟨m, rfl⟩ ⟨j, rfl⟩
    -- Because prime numbers do not divide 1, it suffices to show that `k ∣ 1` to prove a
    -- contradiction
    apply Nat.Prime.not_dvd_one hk
    -- Since `n` divides `b ^ (n - 1) - 1`, `k` also divides `b ^ (n - 1) - 1`
    replace h := dvd_of_mul_right_dvd h
    -- Because `k` divides `b ^ (n - 1) - 1`, if we can show that `k` also divides `b ^ (n - 1)`,
    -- then we know `k` divides 1.
    rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]
    -- Since `k` divides `b`, `k` also divides any power of `b` except `b ^ 0`. Therefore, it
    -- suffices to show that `n - 1` isn't zero. However, we know that `n - 1` isn't zero because we
    -- assumed `2 ≤ n` when doing `by_cases`.
    refine dvd_of_mul_right_dvd (dvd_pow_self (k * j) ?_)
    lia

Goal state after:
case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n.Coprime b
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
⊢ ↑a ≠ 0

Tactic:
intro h

Goal state after:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
h : ↑a = 0
⊢ False
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: n b : ℕ
h : n.FermatPsp b
h₁ : 1 ≤ b
⊢ n.Coprime b

Tactic:
by
  rcases h with ⟨hp, _, hn₂⟩
  exact coprime_of_probablePrime hp (by lia) h₁

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 1 < a ^ 1

Tactic:
by simpa using! ha

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ 2 ≠ 0

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ S.X
⊢ 3 ≠ 0

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ S.Y
⊢ 3 ≠ 0

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ S.Z
⊢ 3 ≠ 0

Tactic:
by decide

Goal state after: