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

Goal state before:
pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴⁶ : CommRing A
inst✝⁴⁵ : Field K
inst✝⁴⁴ : Algebra A K
inst✝⁴³ : IsFractionRing A K
inst✝⁴² : CommRing B
inst✝⁴¹ : Field L
inst✝⁴⁰ : Algebra B L
inst✝³⁹ : Algebra A L
inst✝³⁸ : Algebra K L
inst✝³⁷ : FiniteDimensional K L
inst✝³⁶ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝³⁵ : CommRing R₁
inst✝³⁴ : CommRing R₂
inst✝³³ : IsDomain R₁
inst✝³² : Algebra A R₁
inst✝³¹ : Algebra A R₂
inst✝³⁰ : Algebra R₁ B
inst✝²⁹ : Algebra R₂ B
inst✝²⁸ : Algebra R₁ L
inst✝²⁷ : Algebra R₂ L
inst✝²⁶ : IsScalarTower A R₁ L
inst✝²⁵ : IsScalarTower R₁ B L
inst✝²⁴ : IsScalarTower R₂ B L
inst✝²³ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝²² : Algebra R₁ ↥F₁
inst✝²¹ : Algebra R₂ ↥F₂
inst✝²⁰ : IsTorsionFree R₁ ↥F₁
inst✝¹⁹ : IsScalarTower A (↥F₂) L
inst✝¹⁸ : IsScalarTower A R₂ ↥F₂
inst✝¹⁷ : IsScalarTower R₁ (↥F₁) L
inst✝¹⁶ : IsScalarTower R₂ (↥F₂) L
inst✝¹⁵ : Algebra.IsSeparable K ↥F₂
inst✝¹⁴ : Algebra.IsSeparable (↥F₁) L
inst✝¹³ : IsDomain A
inst✝¹² : IsDedekindDomain B
inst✝¹¹ : IsDedekindDomain R₁
inst✝¹⁰ : IsDedekindDomain R₂
inst✝⁹ : IsFractionRing B L
inst✝⁸ : IsFractionRing R₁ ↥F₁
inst✝⁷ : IsFractionRing R₂ ↥F₂
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsIntegralClosure B R₁ L
inst✝⁴ : IsTorsionFree R₁ B
inst✝³ : IsTorsionFree R₂ B
inst✝² : Algebra.IsIntegral R₂ B
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
this : Algebra.IsSeparable (FractionRing A) (FractionRing R₂)
⊢ (extendedHom L B) ↑(differentIdeal A R₂) ≠ 0

Tactic:
exact (_root_.map_ne_zero _).mpr <| coeIdeal_eq_zero.not.mpr differentIdeal_ne_bot

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

Goal state before:
pp: case e'_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)
z : L
hz : z ∈ (↑I)ᵛ
⊢ (y * x) • z = discr K ⇑b • (algebraMap B L) x * z

Tactic:
rw [Algebra.smul_def, map_mul, hy, ← Algebra.smul_def]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ ↑(dual A K 1) = 1ᵛ

Tactic:
← coe_one,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ ↑(dual A K 1) = (↑1)ᵛ

A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
⊢ Submonoid B
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
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✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
⊢ dual A K J / dual A K I = I / J

Tactic:
by
  rw [dual_eq_mul_inv A K J, dual_eq_mul_inv A K I, mul_div_mul_comm, div_self, one_mul]
  · exact inv_div_inv J I
  · simp only [ne_eq, dual_eq_zero_iff, one_ne_zero, not_false_eq_true]

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

Goal state before:
pp: A : Type u_1
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsDedekindDomain B
inst✝¹² : IsTorsionFree A B
C : Type u_3
inst✝¹¹ : IsDomain B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra B C
inst✝⁸ : Algebra A C
inst✝⁷ : IsDedekindDomain C
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.Finite A C
inst✝⁴ : Module.Finite B C
inst✝³ : IsTorsionFree A C
inst✝² : IsTorsionFree B C
inst✝¹ : IsScalarTower A B C
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing C)
this✝³ : Algebra.IsSeparable (FractionRing B) (FractionRing C)
this✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝¹ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing C)
this : FiniteDimensional (FractionRing B) (FractionRing C)
⊢ (dual A (FractionRing A) 1)⁻¹ =
    (dual B (FractionRing B) 1)⁻¹ * ((extendedHom (FractionRing C) C) (dual A (FractionRing A) 1))⁻¹

Tactic:
← mul_inv,

Goal state after:
A : Type u_1
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsDedekindDomain B
inst✝¹² : IsTorsionFree A B
C : Type u_3
inst✝¹¹ : IsDomain B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra B C
inst✝⁸ : Algebra A C
inst✝⁷ : IsDedekindDomain C
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.Finite A C
inst✝⁴ : Module.Finite B C
inst✝³ : IsTorsionFree A C
inst✝² : IsTorsionFree B C
inst✝¹ : IsScalarTower A B C
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing C)
this✝³ : Algebra.IsSeparable (FractionRing B) (FractionRing C)
this✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝¹ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing C)
this : FiniteDimensional (FractionRing B) (FractionRing C)
⊢ (dual A (FractionRing A) 1)⁻¹ =
    (dual B (FractionRing B) 1 * (extendedHom (FractionRing C) C) (dual A (FractionRing A) 1))⁻¹
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ (↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
convert! Set.finite_empty
    rw [Metric.closedBall_eq_empty.mpr hr]
    exact Set.inter_empty _

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

Goal state before:
pp: case inl
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
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = ζ ^ r
⊢ u = η ^ r ∨ u = -η ^ r

Tactic:
left

Goal state after:
case inl
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
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = ζ ^ r
⊢ u = η ^ r
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «0»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑1 - ↑n
⊢ 1 = 1 ∨ 1 = -1

Tactic:
left

Goal state after:
case «0»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑1 - ↑n
⊢ 1 = 1
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
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
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
left

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
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := ⋯
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := ⋯
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := ⋯
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x
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
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := ⋯
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := ⋯
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := ⋯
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
left

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
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := ⋯
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := ⋯
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := ⋯
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x - 1
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
x : 𝓞 K
h : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
replace h : λ ∣ -x - 1 := by
    convert! h.neg_right using 1
    exact (neg_add' x 1).symm
  convert! (lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ h).neg_right using 1
  ring

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

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

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

Tactic:
left

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
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 : F
ha : a = 0
⊢ (quadraticChar F) a = 0 ∨ (quadraticChar F) a = 1 ∨ (quadraticChar F) a = -1

Tactic:
left

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a = 0
⊢ (quadraticChar F) a = 0
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl
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 = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.hb with
    ⟨y, hy⟩ | ⟨y, hy⟩

Goal state after:
case inl.inl
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 = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

case inl.inr
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 = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr
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 = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S'.hb with
    ⟨y, hy⟩ | ⟨y, hy⟩

Goal state after:
case inr.inl
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 = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

case inr.inr
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 = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.inr
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 = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Tactic:
left

Goal state after:
case inl.inr
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 = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ legendreSym q ↑p = -legendreSym p ↑q

Tactic:
rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul] <;>
  rwa [← Prime.mod_two_eq_one_iff_ne_two Fact.out, odd_of_mod_four_eq_three]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
⊢ d = 1 ∨ d = n

Tactic:
let h := Nat.sub_dvd_pow_sub_pow (2 ^ d) 1 (n / d)

Goal state after:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ (2 ^ d) ^ (n / d) - 1 ^ (n / d) := Nat.sub_dvd_pow_sub_pow (2 ^ d) 1 (n / d)
⊢ d = 1 ∨ d = n
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ 2 ^ (d * (n / d)) - 1
⊢ d = 1 ∨ d = n

Tactic:
Nat.mul_div_cancel' hdn

Goal state after:
n : ℕ
hn1 : n ≠ 1
hn0 : n ≠ 0
hP : Prime (2 ^ n - 1)
han1 : 1 < 2 ^ n
ha1 : 1 < 2
ha0 : 0 < 2
d : ℕ
hdn : d ∣ n
hinj : ∀ (x y : ℕ), 2 ^ x - 1 = 2 ^ y - 1 → x = y
h : 2 ^ d - 1 ∣ 2 ^ n - 1
⊢ d = 1 ∨ d = n
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_2
⊢ 2 ≤ ringKrullDim ℕ

Tactic:
refine le_iSup_of_le ⟨2, ![⊥, ⟨_, (span_singleton_prime two_ne_zero).mpr <| Nat.prime_iff.mp
      Nat.prime_two⟩, ⟨_, (maximalIdeal.isMaximal ℕ).isPrime⟩], fun i ↦ ?_⟩ le_rfl
    fin_cases i
    · exact bot_lt_iff_ne_bot.mpr (Ideal.span_singleton_eq_bot.not.mpr two_ne_zero)
    · simp_rw [Nat.maximalIdeal_eq_span_two_three]
      exact SetLike.lt_iff_le_and_exists.mpr ⟨Ideal.span_mono (by simp),
        3, Ideal.subset_span (by simp), Ideal.mem_span_singleton.not.mpr <| by simp⟩

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

Goal state before:
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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
x : B
hx : x ∈ a
this✝ : Algebra (A ⧸ p) (B ⧸ a) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this : IsScalarTower A (A ⧸ p) (B ⧸ a)
⊢ (Algebra.trace (A ⧸ p) (B ⧸ Ideal.map (algebraMap A B) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x) = 0

Tactic:
have : Module.Finite (A ⧸ p) (B ⧸ a) := .of_restrictScalars_finite A _ _

Goal state after:
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
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
x : B
hx : x ∈ a
this✝¹ : Algebra (A ⧸ p) (B ⧸ a) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ a)
this : Module.Finite (A ⧸ p) (B ⧸ a)
⊢ (Algebra.trace (A ⧸ p) (B ⧸ Ideal.map (algebraMap A B) p)) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x) = 0
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
q₁ : p.Coprime (b ^ 2 - 1)
⊢ 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
have q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1 := Nat.Coprime.mul_dvd_of_dvd_of_dvd q₁ ha₃ ha₄

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
q₁ : p.Coprime (b ^ 2 - 1)
q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1
⊢ 2 * p * (b ^ 2 - 1) ∣ b * (b ^ (p - 1) - 1) * (b ^ p + b)
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: n : ℕ
⊢ Real.log ↑(n + 1) ≤ ↑(harmonic n)

Tactic:
calc _ = ∫ x in (1 : ℕ)..↑(n + 1), x⁻¹ := ?_
       _ ≤ ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ := ?_
       _ = harmonic n := ?_
  · rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by simp)]), div_one]
  · exact (inv_antitoneOn_Icc_right <| by simp).integral_le_sum_Ico (Nat.le_add_left 1 n)
  · simp only [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
⊢ log ((Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1) =
    (Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal).sum + ∑ᶠ (v : ↑nonarchAbsVal), log⁺ (↑v x)

Tactic:
have : ∀ a ∈ archAbsVal.map (fun v ↦ max (v x) 1), a ≠ 0 := by
    intro a ha
    contrapose ha
    rw [ha]
    exact Multiset.prod_eq_zero_iff.not.mp <| left_ne_zero_of_mul H

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
this : ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0
⊢ log ((Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1) =
    (Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal).sum + ∑ᶠ (v : ↑nonarchAbsVal), log⁺ (↑v x)