mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ (closure L).toFun ↑∅ = ⊥

Tactic:
Finset.coe_empty,

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ (closure L).toFun ∅ = ⊥
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
⊢ IsSemilinearSet {x | a + g (x ∘ Sum.inr) = f (x ∘ Sum.inl)}

Tactic:
convert!
    isSemilinearSet_setOfPred_eq a 0 (g.comp (LinearMap.funLeft ℕ ℕ Sum.inr).toAddMonoidHom)
      ((f : (ι → ℕ) →+ M).comp (LinearMap.funLeft ℕ ℕ Sum.inl).toAddMonoidHom)

Goal state after:
case e'_3
M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
x✝ : ι ⊕ Fin n → ℕ
⊢ f (x✝ ∘ Sum.inl) = 0 + ((↑f).comp (LinearMap.funLeft ℕ ℕ Sum.inl).toAddMonoidHom) x✝
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
x : β
hx : x ∈ Slt
y : β
hy : y ∈ Sgt
⊢ x < y

Tactic:
simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_attach, true_and, Subtype.exists,
      exists_and_left, Slt, Sgt] at hx hy

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
x y : β
hx : ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), f ⟨a_1, ⋯⟩ = x
hy : ∃ a_1, a < a_1 ∧ ∃ (x : a_1 ∈ S), f ⟨a_1, ⋯⟩ = y
⊢ x < y
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
n : ℕ
⊢ (F n).out ∈ K

Tactic:
obtain ⟨P, hP1, hP2⟩ := (hF (F n).out).2 ⟨n, Setoid.refl _⟩

Goal state after:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
n : ℕ
P : Bundled L.Structure
hP1 : P ∈ K
hP2 : (Quotient.mk' P).out ≈ (F n).out
⊢ (F n).out ∈ K
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsExtensionPair M M → L.IsUltrahomogeneous M

Tactic:
intro h S S_FG f

Goal state after:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
⊢ ∃ g, f = g.toEmbedding.comp S.subtype
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
iff_not_comm,

Goal state after:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ¬{p | S ⊆ ↑p} = ∅
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«1»
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ Finset.Ico 3 6
⊢ Admissible {2, 3, r}

Tactic:
conv at hr6 => change r ∈ ({3, 4, 5} : Multiset ℕ+)

Goal state after:
case «1».«1»
r : ℕ+
H : 1 < sumInv {2, 3, r}
hr6 : r ∈ {3, 4, 5}
⊢ Admissible {2, 3, r}
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ p ≠ 1 ∧ p ≠ 0 ∧ p ∈ Finset.range (p + 1)

Tactic:
rw [← and_assoc, and_comm (a := ¬ _), ← Nat.two_le_iff]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ 2 ≤ p ∧ p ∈ Finset.range (p + 1)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ (u * x) ^ 1 * ↑(p.choose 1) = ↑p * u * x

Tactic:
rw [Nat.choose_one_right]

Goal state after:
case h.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ (u * x) ^ 1 * ↑p = ↑p * u * x
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ False

Tactic:
exact hn (by simpa using mn)

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this✝ : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this : NeZero n
⊢ Odd (φ n)

Tactic:
simpa [show φ 4 = 2 from rfl] using h

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
n : σ →₀ ℕ
⊢ (if n = 0 then ↑(n i) + 1 else 0) = if n = 0 then 1 else 0

Tactic:
split_ifs <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
⊢ f = exp A

Tactic:
ext n
  induction n with
  | zero =>
    rw [coeff_zero_eq_constantCoeff, hc, constantCoeff_exp]
  | succ n ih =>
    have eq1 : coeff n (d⁄dX A f) = coeff n f := congrArg (coeff n) hd
    rw [coeff_derivative] at eq1
    have eq2 : coeff n (d⁄dX A (exp A)) = coeff n (exp A) := congrArg (coeff n) (derivative_exp A)
    rw [coeff_derivative] at eq2
    rw [ih] at eq1
    have h : coeff (n + 1) f * (n + 1) = coeff (n + 1) (exp A) * (n + 1) := by
      rw [eq1, eq2]
    rw [← Nat.cast_succ, mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul] at h
    exact (smul_right_inj (Nat.succ_ne_zero n)).mp h

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (n + 1) • bernoulli n = (n + 1) • X ^ n - ∑ k ∈ range n, (n + 1).choose k • bernoulli k

Tactic:
by
  simp_rw [← cast_smul_eq_nsmul (R := ℚ), smul_X_eq_monomial,
    Nat.cast_succ, ← sum_bernoulli n, sum_range_succ_sub_sum, choose_succ_self_right,
    Nat.cast_succ]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ ↑1 * (1 - ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k) +
      ∑ x ∈ range n, ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x =
    1

Tactic:
cast_one,

Goal state after:
n : ℕ
⊢ 1 * (1 - ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k) +
      ∑ x ∈ range n, ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x =
    1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    t ^ n * (algebraMap ℚ A) (↑(n + 1)! * (1 / ↑n !))

Tactic:
change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    t ^ n * (algebraMap ℚ A) (↑((n + 1) * n !) * (1 / ↑n !))
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n ↦ (algebraMap ℚ ℚ) (bernoulli n / ↑n !)) * (exp ℚ - 1) *
      PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
mul_right_comm

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n ↦ (algebraMap ℚ ℚ) (bernoulli n / ↑n !)) *
        PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)) *
      (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
p : ℕ
x✝ : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
⊢ p ^ 0 = 1

Tactic:
_root_.pow_zero

Goal state after:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
p : ℕ
x✝ : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
⊢ 1 = 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ↑p ^ (2 * k - 2 * m - 1)
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
hcmp : pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))
H : ∀ (x : ℚ), ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)
⊢ pIntegral p
    ((bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1))

Tactic:
apply (Rat.padicValuation p).map_sub_le

Goal state after:
case hx
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ⋯
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
hcmp : pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))
H : ∀ (x : ℚ), ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)
⊢ (Rat.padicValuation p)
      ((bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1)) ≤
    1

case hy
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ⋯
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
hcmp : pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))
H : ∀ (x : ℚ), ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)
⊢ (Rat.padicValuation p) (vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)) ≤ 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2.inr
n p : ℕ
hp : Prime p
this : 1 < p
h : n < p
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p

Tactic:
simp [log_of_lt h]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ψ ↑n ≤ ↑(π n) * log ↑n

Tactic:
psi_eq_sum_mul_log_prime,

Goal state after:
n : ℕ
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ↑(π n) * log ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ↑1 * log 2 ≤ log x

Tactic:
cast_one,

Goal state after:
x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 1 * log 2 ≤ log x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃! n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := exists_mem_range x

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hn₁ : n < p
hn₂ : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ∃! n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
h : 1 ≤ x
n : ℕ
hn : 2 ≤ n
⊢ ψ (x ^ (1 / ↑n)) ≤ (log 4 + 4) * √x

Tactic:
grw [psi_le_const_mul_self (by positivity), sqrt_eq_rpow x]

Goal state after:
x : ℝ
h : 1 ≤ x
n : ℕ
hn : 2 ≤ n
⊢ (log 4 + 4) * x ^ (1 / ↑n) ≤ (log 4 + 4) * x ^ (1 / 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ↑p ∣ x
⊢ x.zmodRepr = 0

Tactic:
by
  apply zmodRepr_unique _ _ (Nat.Prime.pos Fact.out)
  simp [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, hx]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x * y - ↑(f x * f y) ∈ Ideal.span {↑v}

Tactic:
let I : Ideal ℤ_[p] := Ideal.span {↑v}
      convert! I.add_mem (I.mul_mem_left x (f_spec y)) (I.mul_mem_right ↑(f y) (f_spec x)) using 1
      rw [cast_mul]
      ring

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ⋯
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ?m.295 ≠ 0

pp: R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ⋯
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ Ideal S

pp: R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ⋯
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ?m.295 * ↑⟨J, ⋯⟩ ∣ ?m.295 * Ideal.span {(algebraMap R S) M}

Tactic:
· exact mt Ideal.span_singleton_eq_bot.mp b_ne_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ⋯
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ Ideal.span {b} * ↑⟨J, ⋯⟩ ∣ Ideal.span {b} * Ideal.span {(algebraMap R S) M}
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝¹ : DecidableEq L := Classical.decEq L
this✝ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
⊢ Fintype (ClassGroup S)

Tactic:
choose s b hb_int using FiniteDimensional.exists_is_basis_integral R K L

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝¹ : DecidableEq L := Classical.decEq L
this✝ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b x)
⊢ Fintype (ClassGroup S)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ (toZModPow n) x = 0

Tactic:
dsimp [toZModPow, toZModHom]

Goal state after:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑(x.appr n) = 0
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 < Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
have := Fact.mk h

Goal state after:
case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this✝ : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 < Nat.card ↥(rootsOfUnity n L)
this : Fact (1 < Nat.card ↥(rootsOfUnity n L))
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 = Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
have := Finite.card_le_one_iff_subsingleton.mp h.ge
    obtain rfl : t = 1 := Subsingleton.elim t 1
    simp

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

Goal state before:
pp: case re
d x y : ℤ
⊢ ({ re := x, im := y } * star { re := x, im := y }).re = (↑x * ↑x - ↑d * ↑y * ↑y).re

Tactic:
simp [sub_eq_add_neg, mul_comm]

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

Goal state before:
pp: case im
d x y : ℤ
⊢ ({ re := x, im := y } * star { re := x, im := y }).im = (↑x * ↑x - ↑d * ↑y * ↑y).im

Tactic:
simp [sub_eq_add_neg, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Tactic:
by
  let t := pellZd_add a1 n (m - n)
  rw [add_tsub_cancel_of_le h] at t
  rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
⊢ (↑n * a).Nonneg

Tactic:
by
  rw [← Int.cast_natCast n]
  exact
    match a, nonneg_cases ha, ha with
    | _, ⟨x, y, Or.inl rfl⟩, _ => by rw [smul_val]; trivial
    | _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ha => by
      rw [smul_val]; simpa using! nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)
    | _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ha => by
      rw [smul_val]; simpa using! nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)

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

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg

Tactic:
exact
        nonnegg_neg_pos.2 (sqLe_mul.right.right.left (nonnegg_pos_neg.1 ha) (nonnegg_neg_pos.1 hb))

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
Nat.mod_eq_of_lt (strictMono_x _ (Nat.lt_of_succ_lt jn)),

Goal state after:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1) % xn a1 n
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ d * (a.im * a.im) ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)

Goal state after: