mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)

Tactic:
let B := Pi.basisFun ℂ (K →+* ℂ)
    let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
      Fintype.equivOfCardEq ((Embeddings.card K ℂ).trans (finrank_eq_card_basis (integralBasis K)))
    let M := B.toMatrix (fun i => canonicalEmbedding K (integralBasis K (e i)))
    suffices M.det ≠ 0 by
      rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← Basis.is_basis_iff_det] at this
      exact (basisOfPiSpaceOfLinearIndependent this.1).reindex e
  -- In order to prove that the determinant is nonzero, we show that it is equal to the
  -- square of the discriminant of the integral basis and thus it is not zero
    let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i))
      (RingHom.equivRatAlgHom K ℂ)
    rw [show M = N.transpose by { ext : 2; rfl }]
    rw [Matrix.det_transpose, ← pow_ne_zero_iff two_ne_zero]
    convert!
      (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
        (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
    rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
    exact (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
      (fun i => integralBasis K (e i)) (RingHom.equivRatAlgHom K ℂ)).symm

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ Nontrivial (mixedSpace K)

Tactic:
have : Nonempty {w : InfinitePlace K // IsReal w} := ⟨⟨w, hw⟩⟩
    exact nontrivial_prod_left

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∏ _k, 2⁻¹ * I = (2⁻¹ * I) ^ Fintype.card { w // w.IsComplex }

Tactic:
rw [prod_const, Fintype.card]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) =
    ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * volume (fundamentalDomain (latticeBasis K))

Tactic:
by
  let e : (Module.Free.ChooseBasisIndex ℤ I) ≃ (Module.Free.ChooseBasisIndex ℤ (𝓞 K)) := by
    refine Fintype.equivOfCardEq ?_
    rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex,
      fractionalIdeal_rank]
  rw [← fundamentalDomain_reindex (fractionalIdealLatticeBasis K I) e,
    measure_fundamentalDomain ((fractionalIdealLatticeBasis K I).reindex e)]
  · rw [show (fractionalIdealLatticeBasis K I).reindex e = (mixedEmbedding K) ∘
        (basisOfFractionalIdeal K I) ∘ e.symm by
      ext1; simp only [Basis.coe_reindex, Function.comp_apply, fractionalIdealLatticeBasis_apply]]
    rw [mixedEmbedding.det_basisOfFractionalIdeal_eq_norm]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ |(latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)| = ↑(FractionalIdeal.absNorm ↑I)

Tactic:
suffices Basis.det (latticeBasis K) ((mixedEmbedding K ∘ (basisOfFractionalIdeal K I) ∘ e)) =
      (algebraMap ℚ ℝ) ((Basis.det (integralBasis K)) ((basisOfFractionalIdeal K I) ∘ e)) by
    rw [this, eq_ratCast, ← Rat.cast_abs, ← Equiv.symm_symm e, ← Basis.coe_reindex,
      det_basisOfFractionalIdeal_eq_absNorm K I e]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ (latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) =
    (algebraMap ℚ ℝ) ((integralBasis K).det (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I := Fintype.equivOfCardEq ⋯
⊢ Basis (ChooseBasisIndex ℤ ↥↑↑I) ℝ (mixedSpace K)

Tactic:
refine Basis.reindex ?_ e

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I := Fintype.equivOfCardEq ⋯
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_1.inl
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
s : Set { w // w.IsReal }
x : mixedSpace K
hx : x ∈ A
right✝ : x ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
⊢ (negAt s) x ∈ A

pp: case refine_1.inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}
⊢ x ∈ A

Tactic:
· simp_rw +singlePass [hA, negAt_apply_norm_isReal, negAt_apply_snd]
      rwa [← hA]

Goal state after:
case refine_1.inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A ∧ ∃ i, x ∈ {x | x.1 i = 0}
⊢ x ∈ A
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
h : ∃ P, P.IsPrime ∧ P.LiesOver p
⊢ p.ramificationIdxIn B = P.ramificationIdx A

Tactic:
obtain ⟨_, _⟩ := h.choose_spec

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.ramificationIdxIn B = P.ramificationIdx A
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
h : ∃ P, P.IsPrime ∧ P.LiesOver p
⊢ p.inertiaDegIn B = P.inertiaDeg A

Tactic:
obtain ⟨_, _⟩ := h.choose_spec

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
h : ∃ P, P.IsPrime ∧ P.LiesOver p
left✝ : h.choose.IsPrime
right✝ : h.choose.LiesOver p
⊢ p.inertiaDegIn B = P.inertiaDeg A
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
hI : 1 ∈ I
⊢ (IsLocalization.map L f hf) 1 = 1

Tactic:
rw [map_one]

Goal state after:
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
I J : FractionalIdeal A⁰ K
h : (fun I ↦ (extendedHom L B) I) I = (fun I ↦ (extendedHom L B) I) J
⊢ I = J

Tactic:
dsimp only at h

Goal state after:
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
I J : FractionalIdeal A⁰ K
h : (extendedHom L B) I = (extendedHom L B) J
⊢ I = J
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
⊢ ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P

Tactic:
have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
  have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
  have := CharZero.of_module (R := 𝒪) K
  rw [NumberField.not_dvd_discr_iff_forall_liesOver K 𝒪 hp]
  exact ⟨fun H P hP h ↦ H P (hP.isMaximal (by aesop))
    ((Ideal.liesOver_span_iff hP.ne_top hp).mpr h),
    fun H P _ h ↦ H P _ (h.1.le (Ideal.mem_span_singleton_self _))⟩

Goal state after:
Module: Mathlib.RingTheory.Prime

Goal state before:
pp: case insert.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = p i * d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ t_1 u_1 b c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b * c_1 ∧ p i * d * ∏ i ∈ t, p i = b * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i

pp: case insert.inr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = b * (p i * d)
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ t_1 u_1 b_1 c,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ p i * d * ∏ i ∈ u, p i = c * ∏ i ∈ u_1, p i

Tactic:
· rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc
      exact ⟨insert i t, u, d, c, by rw [insert_union, htus], disjoint_insert_left.2 ⟨hiu, htu⟩, by
          simp [hbc, prod_insert hit, mul_comm, mul_left_comm]⟩

Goal state after:
case insert.inr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = b * (p i * d)
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ t_1 u_1 b_1 c,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ p i * d * ∏ i ∈ u, p i = c * ∏ i ∈ u_1, p i
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
⊢ (↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
refine (Set.Finite.image (logEmbedding K) this).subset ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
⊢ ↑(unitLattice K) ∩ Metric.closedBall 0 r ⊆
    ⇑(logEmbedding K) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(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 < ↑(convexBodyLTFactor K) * ↑(∏ w, g w ^ w.mult)

Tactic:
convert! hB

Goal state after:
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
⊢ ↑(∏ w, g w ^ w.mult) = ↑B
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:
· rintro ⟨⟨ζ', h_tors'⟩, η⟩ hf
    simp only [ζ, ← fun_eq_repr K h_tors' hf, Prod.mk.injEq, Subtype.mk.injEq, and_true]
    nth_rewrite 1 [hf]
    rw [_root_.mul_inv_cancel_right]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
⊢ 2 ^ (n + 1) = 2 ^ n + 2 ^ n

Tactic:
by rw [pow_succ, mul_two]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

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

Tactic:
· calc
      n ≤ 2 ^ n := Nat.le_of_lt n.lt_two_pow_self
      _ < 2 ^ (n + 1) := (Nat.pow_lt_pow_iff_right (Nat.one_lt_two)).mpr (lt_add_one n)

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

Goal state before:
pp: 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
this : (Algebra.trace K L) ((algebraMap B L) x) ∈ ↑p
⊢ (intTrace A B) x ∈ p

Tactic:
by
    obtain ⟨y, hy, e⟩ := this
    rw [← Algebra.algebraMap_intTrace (A := A), Algebra.linearMap_apply,
      (IsLocalization.injective _ le_rfl).eq_iff] at e
    exact e ▸ hy

Goal state after:
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
hF : ringChar F ≠ 2
a : F
ha : a = 0
⊢ ↑((quadraticChar F) a) = a ^ (Fintype.card F / 2)

pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
⊢ ↑((quadraticChar F) a) = a ^ (Fintype.card F / 2)

Tactic:
· have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card two_pos
    simp only [ha, quadraticChar_apply, quadraticCharFun_zero, Int.cast_zero, zero_pow this.ne']

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : ¬a = 0
⊢ ↑((quadraticChar F) a) = a ^ (Fintype.card F / 2)
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
⊢ 2 * (n.fermatNumber - 1) ^ 2 ≤ (n + 1).fermatNumber ^ 2

Tactic:
simp only [fermatNumber, add_tsub_cancel_right]
  have : 0 ≤ 1 + 2 ^ (2 ^ n * 4) := le_add_left _ _
  ring_nf
  lia

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
⊢ Prime n.fermatNumber

Tactic:
have key : 2 ^ n = 2 ^ n - 1 + 1 := (Nat.sub_add_cancel Nat.one_le_two_pow).symm

Goal state after:
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ Prime n.fermatNumber
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 : 0 ^ 2 ^ n = -1
h : ↑a = 0
⊢ False

Tactic:
zero_pow (pow_ne_zero n two_ne_zero),

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 : 0 = -1
h : ↑a = 0
⊢ False
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)
⊢ b ^ 2 - 1 ∣ b ^ (2 * p) - 1

Tactic:
simpa only [one_pow, pow_mul] using Nat.sub_dvd_pow_sub_pow _ 1 p

Goal state after:
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)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) - (b ^ 2 - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
← one_mul (b ^ 2 - 1)

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)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) - 1 * (b ^ 2 - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: case h₂.calc_1
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ d ∈ Finset.Ico 2 (n + 1), (↑d)⁻¹ = ∑ x ∈ Finset.Ico 2 (n + 1), (↑x + 1 - 1)⁻¹

Tactic:
add_sub_cancel_right

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

Goal state before:
pp: n : ℕ
Hn : n ≠ 0
⊢ 0 < harmonic n

Tactic:
unfold harmonic

Goal state after:
n : ℕ
Hn : n ≠ 0
⊢ 0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹
Module: Mathlib.NumberTheory.Harmonic.Int

Goal state before:
pp: case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
⊢ padicValRat 2 (harmonic n + (↑(n + 1))⁻¹) = -↑(Nat.log 2 (n + 1))

Tactic:
padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
        (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key,

Goal state after:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
⊢ min (padicValRat 2 (harmonic n)) (padicValRat 2 (↑n.succ)⁻¹) = -↑(Nat.log 2 (n + 1))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ HasFiniteMulSupport fun v ↦ max (↑v x) 1

Tactic:
rcases eq_or_ne x 0 with rfl | hx
  · simp [HasFiniteMulSupport]
  fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ Sum.elim x 0 (Sum.inl i) ≠ 0 (Sum.inl i)

Tactic:
by simpa using hi

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

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -1 < -2 ∨ -2 ≠ -1 ∧ 0 ∉ uIcc (↑n) (↑n + 1)

Tactic:
refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
        all_goals positivity

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (fun I ↦ ∏ a, x a (I a)) ≠ 0

Tactic:
simp_rw [ne_iff, Pi.zero_def] at hx ⊢
    choose f hf using hx
    exact ⟨f, prod_ne_zero_iff.mpr fun a _ ↦ hf a⟩

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

Goal state before:
pp: K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b : NumberField.RingOfIntegers K
⊢ ∀ (c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ),
    c ≠ 0 →
      ¬hζ.toInteger - 1 ∣ a → ¬hζ.toInteger - 1 ∣ b → hζ.toInteger - 1 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ ↑u * c ^ 3

Tactic:
c

Goal state after:
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := IsCyclotomicExtension.zeta_spec 3 ℚ K
this : NumberField K
a b c : NumberField.RingOfIntegers K
⊢ ∀ (u : (NumberField.RingOfIntegers K)ˣ),
    c ≠ 0 →
      ¬hζ.toInteger - 1 ∣ a → ¬hζ.toInteger - 1 ∣ b → hζ.toInteger - 1 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ ↑u * c ^ 3
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_1.hx.hy
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∏ j ∈ range k, Z (j + 1) ∈ ℤ[μ]

Tactic:
· exact Subalgebra.prod_mem _ fun _ _ ↦ (Zdef _).1

Goal state after: