mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
inst✝⁸ : CommRing A
B : Type u_2
inst✝⁷ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁶ : CommRing K
inst✝⁵ : Algebra A K
inst✝⁴ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝³ : CommRing L
inst✝² : Algebra B L
inst✝¹ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
inst✝ : IsDomain B
hf' : Function.Injective ⇑f
hN : 0 ∉ N
⊢ extended L hf I = 0 → I = 0

Tactic:
contrapose!

Goal state after:
A : Type u_1
inst✝⁸ : CommRing A
B : Type u_2
inst✝⁷ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁶ : CommRing K
inst✝⁵ : Algebra A K
inst✝⁴ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝³ : CommRing L
inst✝² : Algebra B L
inst✝¹ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
inst✝ : IsDomain B
hf' : Function.Injective ⇑f
hN : 0 ∉ N
⊢ I ≠ 0 → extended L hf I ≠ 0
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case neg
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : ¬w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}

Tactic:
apply Set.mem_union_right

Goal state after:
case neg
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
hK₁ : ⟨K, hK₀⟩ ∈ {K | |discr ↥↑K| ≤ ↑N}
this✝ : CharZero ↥K
this : NumberField ↥K
w₀ : InfinitePlace ↥K
hw₀ : ¬w₀.IsReal
⊢ ⟨K, hK₀⟩ ∈ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
⊢ Function.Injective fun I ↦ (extendedHom L B) I

Tactic:
intro I J h
  dsimp only at h
  by_cases hI : I = 0
  · rwa [hI, map_zero, eq_comm, extendedHom_eq_zero_iff L B, eq_comm, ← hI] at h
  by_cases hJ : J = 0
  · rwa [hJ, map_zero, extendedHom_eq_zero_iff L B, ← hJ] at h
  rwa [← mul_inv_eq_one₀ ((extendedHom_eq_zero_iff _ _).not.mpr hJ), ← map_inv₀, ← map_mul,
    extendedHom_eq_one_iff _ _ (mul_ne_zero hI (inv_ne_zero hJ)), mul_inv_eq_one₀ hJ] at h

Goal state after:
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case inr
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Infinite (S ⧸ I)
⊢ absNorm (under ℤ I) ∣ absNorm I

Tactic:
absNorm_apply I,

Goal state after:
case inr
S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Infinite (S ⧸ I)
⊢ absNorm (under ℤ I) ∣ Submodule.cardQuot I
Module: Mathlib.NumberTheory.NumberField.Discriminant.Different

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪), P.IsMaximal → P.LiesOver (Ideal.span {p}) → ¬P ∣ differentIdeal ℤ 𝒪

Tactic:
contrapose!

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
p : ℤ
hp : Prime p
this✝³ : IsDomain 𝒪
this✝² : IsDedekindDomain 𝒪
this✝¹ : IsFractionRing 𝒪 K
this✝ : Module.Finite ℤ 𝒪
this : CharZero 𝒪
⊢ p ∣ discr K ↔ ∃ P, P.IsMaximal ∧ P.LiesOver (Ideal.span {p}) ∧ P ∣ differentIdeal ℤ 𝒪
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg.refine_3
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q ∈ normalizedFactors I
hQ' : Q ≠ ⊥
⊢ absNorm ((relNorm R) Q) = absNorm Q

Tactic:
Ideal.mem_normalizedFactors_iff hI

Goal state after:
case neg.refine_3
R : Type u_1
inst✝¹⁴ : CommRing R
inst✝¹³ : IsDomain R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : IsIntegrallyClosed R
inst✝⁹ : IsIntegrallyClosed S
inst✝⁸ : Algebra R S
inst✝⁷ : Module.Finite R S
inst✝⁶ : IsTorsionFree R S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ R
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : PerfectField (FractionRing R)
I : Ideal S
this : Module.Finite ℤ R
hI : ¬I = ⊥
Q : Ideal S
hQ : Q.IsPrime ∧ I ≤ Q
hQ' : Q ≠ ⊥
⊢ absNorm ((relNorm R) Q) = absNorm Q
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: 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 {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
⊢ p ∣ n

Tactic:
rsuffices ⟨q, hq, t, s, ht₁, ht₂, hs⟩ :
      ∃ q, q.Prime ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ (p : ℤ) ∣ (q : ℤ) ^ s := by
    obtain hn | hn := lt_or_eq_of_le hn
    · by_cases! h : ∃ q, q.Prime ∧ ∃ t, q ^ t = n
      · obtain ⟨q, hq, t, hn'⟩ := h
        have : Fact (Nat.Prime q) := ⟨hq⟩
        cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp
      · rw [IsPrimitiveRoot.norm_toInteger_sub_one_eq_one hμ hn, one_pow,
          Int.natCast_dvd_ofNat, Nat.dvd_one] at hp
        · exact (Nat.Prime.ne_one hF.out hp).elim
        · exact fun {p} a k ↦ h p a k
    · rw [← hn] at hμ hC ⊢
      refine ⟨2, Nat.prime_two, 1, Module.finrank ℚ⟮ζ⟯ K, one_ne_zero, by rw [pow_one], ?_⟩
      rwa [hμ.norm_toInteger_sub_one_of_eq_two, neg_eq_neg_one_mul, mul_pow, IsUnit.dvd_mul_left
        ((isUnit_pow_iff Module.finrank_pos.ne').mpr isUnit_neg_one)] at hp

Goal state after:
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 {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : ↑p ∣ ↑q ^ s
⊢ p ∣ n
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 : FractionalIdeal B⁰ L
hI : I ≠ 0
b : B
hb : b ∈ B⁰
hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)
this : b = 0
e : dual A K I = 0
⊢ False

Tactic:
exact mem_nonZeroDivisors_iff_ne_zero.mp hb this

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((K[x].equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
y : L
this : (minpoly A x).natDegree = (minpoly K x).natDegree
⊢ y ∈ ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range (minpoly A x).natDegree)) ↔ y ∈ Set.range ⇑pb.basis

Tactic:
simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio, Set.mem_range,
      pb.basis_eq_pow, pbgen]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : K[x] = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((K[x].equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : (traceForm K L).Nondegenerate
hpb :
  ⇑((traceForm K L).dualBasis hnondeg pb.basis) = fun x ↦
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
y : L
this : (minpoly A x).natDegree = (minpoly K x).natDegree
⊢ (∃ x_1 < (minpoly A x).natDegree, x ^ x_1 = y) ↔ ∃ y_1, x ^ ↑y_1 = y
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
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 : ↑(differentIdeal A B) * ↑Q ≤ ↑(Ideal.map (algebraMap A B) p)
⊢ False

Tactic:
coeIdeal_differentIdeal A K

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
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 : (FractionalIdeal.dual A K 1)⁻¹ * ↑Q ≤ ↑(Ideal.map (algebraMap A B) p)
⊢ False
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: 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
⊢ ¬3 ∣ -b

Tactic:
simp [h3b]

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

Goal state before:
pp: case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : (3 ∣ a ∨ 3 ∣ b) ∨ 3 ∣ c
⊢ False

Tactic:
← sub_eq_zero,

Goal state after:
case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 - c ^ 3 = 0
h1 : (3 ∣ a ∨ 3 ∣ b) ∨ 3 ∣ c
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
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:
· simp only [map_add]
    exact fun _ _ h₁ h₂ ↦ Submodule.add_mem _ h₁ h₂

Goal state after:
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ p ≠ 0 ∧ p ≠ 1

Tactic:
constructor <;> rintro rfl

Goal state after:
case left
a : ZMod 0
ha : a ^ (0 - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ 0 - 1 → a ^ ((0 - 1) / q) ≠ 1
⊢ False

case right
a : ZMod 1
ha : a ^ (1 - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ 1 - 1 → a ^ ((1 - 1) / q) ≠ 1
⊢ False
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ 3 ^ (2 ^ 2 ^ n / p) ≠ 1

Tactic:
(Nat.prime_dvd_prime_iff_eq hp1 prime_two).mp (hp1.dvd_of_dvd_pow hp2),

Goal state after:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ 3 ^ (2 ^ 2 ^ n / 2) ≠ 1
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1

Tactic:
by
  have : Fact (2 < p) := Fact.mk (lt_of_le_of_ne hp.two_le hp2.symm)
  have : Fact p.Prime := Fact.mk hp
  have ha1 : (a : ZMod p) ^ (2 ^ n) = -1 := by
    rw [eq_neg_iff_add_eq_zero]
    exact_mod_cast (natCast_eq_zero_iff (a ^ (2 ^ n) + 1) p).mpr hpdvd
  have ha0 : (a : ZMod p) ≠ 0 := by
    intro h
    rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1
    exact one_ne_zero ha1
  have ha : orderOf (a : ZMod p) = 2 ^ (n + 1) := by
    apply orderOf_eq_prime_pow
    · rw [ha1]
      exact neg_one_ne_one
    · rw [pow_succ, pow_mul, ha1, neg_one_sq]
  simpa [ha, dvd_def, Nat.sub_eq_iff_eq_add hp.one_le, mul_comm] using orderOf_dvd_card_sub_one ha0

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Tactic:
suffices h : p ∣ a.val ^ (2 ^ (n + 1)) + 1 by
    exact pow_pow_add_primeFactors_one_lt hp hp2 h

Goal state after:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p) ^ 2 - b ^ 2 = (b ^ p + b) * (b ^ p - b)

Tactic:
rw [Nat.sq_sub_sq]

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: a b : ℕ
hab : a + b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
by
    have h : a = 1 ∨ b = 1 := by lia
    apply h.imp <;> simp +contextual

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

Goal state before:
pp: case inr.mp.left
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
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
H : ¬P ∣ differentIdeal A B
⊢ Algebra.IsSeparable (Ideal.under A P).ResidueField P.ResidueField

Tactic:
suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance

Goal state after:
case inr.mp.left
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
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : ¬P ∣ differentIdeal A B
⊢ Algebra.IsSeparable (A ⧸ Ideal.under A P) (B ⧸ P)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight ![x, y] = logHeight ![y, x]

Tactic:
by
  simp only [logHeight_eq_log_mulHeight, mulHeight_swap]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 0)

Tactic:
rw [show 𝓝 (0 : ℝ) = 𝓝 (0 ^ (s - 1)) by rw [zero_rpow]; linarith]

Goal state after:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 (0 ^ (s - 1)))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.card = ∑ i, 1

Tactic:
← Multiset.length_toList,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.toList.length = ∑ i, 1
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ∈ univ \ {0, 1}
⊢ (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1

Tactic:
rw [← map_mul, MulChar.trivial_apply, if_pos]

Goal state after:
case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ∈ univ \ {0, 1}
⊢ IsUnit (x * (1 - x))
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case refine_4
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬1 = -y
⊢ y / (1 + y) / (1 - y / (1 + y)) = y

Tactic:
← sub_eq_zero,

Goal state after:
case refine_4
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬1 - -y = 0
⊢ y / (1 + y) / (1 - y / (1 + y)) = y
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
x : 𝓞 K
hx : ∀ (v : InfinitePlace K), v ↑x ≤ B'
⊢ IsIntegral ℤ ↑x ∧ ∀ (φ : K →+* ℂ), ‖φ ↑x‖ ≤ B'

Tactic:
exact ⟨x.isIntegral_coe, fun φ ↦ hx <| .mk φ⟩

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : (fun x ↦ x - 1) =o[𝓝 1] fun x ↦ 1
⊢ (fun s ↦ (s - 1) ^ 2) =o[𝓝[≠] 1] fun x ↦ x - 1

Tactic:
simpa [pow_two] using (this.mul_isBigO <| isBigO_refl ..).mono nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
⊢ (h.algEquiv h') h.root = h'.root

Tactic:
simp [algEquiv_def]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
a✝ : S
⊢ (h.algEquiv h) a✝ = AlgEquiv.refl a✝

Tactic:
simp [algEquiv_def]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
f : R[X]
inst✝⁴ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝³ : Ring T
inst✝² : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
x : S
⊢ (h'.algEquiv h'') ((h.algEquiv h') x) = (h.algEquiv h'') x

Tactic:
simp [algEquiv_def]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : z = h.map w
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : z - h.map w = 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z) - eval₂ i x w = 0