mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case refine_1
α : 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})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
⊢ (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩

Tactic:
if hxS : x ∈ S
    then if hyS : y ∈ S
      then simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]
      else
        obtain rfl := Finset.eq_of_mem_insert_of_notMem hy hyS
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
    else
      obtain rfl := Finset.eq_of_mem_insert_of_notMem hx hxS
      if hyS : y ∈ S
      then
        simp only [hxS, hyS, ↓reduceDIte]
        exact hb' _ (Finset.mem_image_of_mem _ (Finset.mem_filter.2 ⟨Finset.mem_attach _ _, hxy⟩))
      else simp only [Finset.eq_of_mem_insert_of_notMem hy hyS, lt_self_iff_false] at hxy

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ Finset.image (⇑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ Finset.image (⇑(Equiv.prodComm α β)) f
⊢ (Equiv.prodComm α β).symm q ∈ f

Tactic:
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_symm] at hq
          rwa [← Finset.mem_coe]

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
⊢ ∃ y ∈ {f | ∃ b, (a, b) ∈ ↑f}, f ≤ y

Tactic:
refine
      ⟨⟨insert (a, b) f.val, fun p hp q hq ↦ ?_⟩, ⟨b, Finset.mem_insert_self _ _⟩,
        Finset.subset_insert _ _⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
p : α × β
hp : p ∈ insert (a, b) ↑f
q : α × β
hq : q ∈ insert (a, b) ↑f
⊢ cmp p.1 q.1 = cmp p.2 q.2
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.noBotOrderSentence ↔ NoBotOrder M

Tactic:
by
  simp only [noBotOrderSentence, Sentence.Realize, Formula.Realize, BoundedFormula.realize_all,
    BoundedFormula.realize_ex, BoundedFormula.realize_not, Term.realize_le]
  refine ⟨fun h => ⟨fun a => h a⟩, ?_⟩
  intro h a
  exact exists_not_ge a

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
⊢ Language.order.IsExtensionPair M N

Tactic:
isExtensionPair_iff_exists_embedding_closure_singleton_sup

Goal state after:
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
⊢ ∀ (S : Language.order.Substructure M),
    S.FG → ∀ (f : ↥S ↪[Language.order] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
⊢ Nonempty (M ≃[L] N)

Tactic:
let S : L.Substructure M := ⊥

Goal state after:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
⊢ Nonempty (M ≃[L] N)
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
⊢ ¬Set.univ = ∅ ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable

Tactic:
not_iff_comm,

Goal state after:
L : Language
T : L.Theory
α : Type w
⊢ ¬((L.lhomWithConstants α).onTheory T).IsSatisfiable ↔ Set.univ = ∅
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
hG : IsGδ s
this✝ : LocallyCompactSpace ↑(closure s)
this : BaireSpace ↑(closure s)
⊢ BaireSpace ↑s

Tactic:
have : BaireSpace ((↑) ⁻¹' s : Set (closure s)) :=
    (hG.preimage continuous_subtype_val).baireSpace_of_dense
    (by simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure])

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
hG : IsGδ s
this✝¹ : LocallyCompactSpace ↑(closure s)
this✝ : BaireSpace ↑(closure s)
this : BaireSpace ↑(Subtype.val ⁻¹' s)
⊢ BaireSpace ↑s
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ IsMaximal {φ | T.typesWith φ ∈ F}

Tactic:
rw [Theory.IsMaximal, Theory.isSatisfiable_iff_isFinitelySatisfiable]
    refine ⟨?_, ?_⟩
    · rw[Theory.IsFinitelySatisfiable]
      intro x hx
      have : ∀ φ ∈ x, T.typesWith φ ∈ F.toFilter := by intro φ hφ; exact hx hφ
      rw [← Filter.biInter_finset_mem x] at this
      obtain ⟨T, T_inter⟩ := F.neBot.nonempty_of_mem this
      have subset : (x : Set _) ⊆ T.toTheory := by rwa [Set.mem_iInter₂] at T_inter
      exact T.isMaximal.1.mono subset
    · intro φ
      simp only [mem_ofPred_eq, typesWith_not]
      exact Ultrafilter.mem_or_compl_mem F (T.typesWith φ)

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

Goal state before:
pp: case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1

Tactic:
rintro ⟨p, m, -, odd, -, eq⟩
      have := eq ▸ odd.pow
      simp [← Nat.not_even_iff_odd] at this

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ π' n = 0 ↔ n ≤ 2

Tactic:
rw [primeCounting', Nat.count_eq_zero ⟨_, Nat.prime_two⟩, Nat.nth_prime_zero_eq_two]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
⊢ ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x =
    ∏ x ∈ {p ∈ Ico 0 (m + 1) | Nat.Prime p} ∪ {p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p}, x

pp: m n : ℕ
⊢ Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})

Tactic:
← filter_union,

Goal state after:
m n : ℕ
⊢ ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x = ∏ x ∈ Ico 0 (m + 1) ∪ Ico (m + 1) (m + n + 1) with Nat.Prime x, x

m n : ℕ
⊢ Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
⊢ x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x

Tactic:
have hf' : ∀ x, 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3) := fun x h =>
    div_pos (mul_pos h (rpow_pos_of_pos (mul_pos two_pos h) _)) (rpow_pos_of_pos four_pos _)

Goal state after:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
⊢ x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n / 3) ≤ 2 * ↑n / 3

Tactic:
· exact cast_div_le.trans (by norm_cast)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ k ∈ range n, ↑k ^ p.succ + ↑n ^ p.succ = ∑ i ∈ range p.succ.succ, f i + ↑n ^ p.succ

Tactic:
simp [f, sum_range_pow]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (n + 1)), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
obtain ⟨k₀, k₁, hk, h⟩ := ih hε hb fun x ↦ Fin.tail (A (s x))

Goal state after:
case succ
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h✝.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h✝.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h✝.card ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
k₀ k₁ : Fin (h✝.card ε ^ n).succ
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < abv b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (n + 1)), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
h₀ : θ x = 0
contra : 2 ∈ Ioc 0 ⌊x⌋₊
h₁ : log ↑2 ≤ θ x
⊢ False

Tactic:
have := Real.log_pos one_lt_two

Goal state after:
x : ℝ
h₀ : θ x = 0
contra : 2 ∈ Ioc 0 ⌊x⌋₊
h₁ : log ↑2 ≤ θ x
this : 0 < log 2
⊢ False
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
by
    rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero.inr
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
hp2 : p ≠ 2
⊢ (Rat.padicValuation p) (-(↑p ^ (2 * k - 1) / 2)) ≤ 1

Tactic:
rw [Valuation.map_neg]

Goal state after:
case succ.zero.inr
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
hp2 : p ≠ 2
⊢ (Rat.padicValuation p) (↑p ^ (2 * k - 1) / 2) ≤ 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ IsUnit ↑↑r.den

Tactic:
exact isUnit_den r h

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ maximalIdeal ℤ_[p] → x - ↑b ∈ maximalIdeal ℤ_[p] → ↑a = ↑b

Tactic:
exact zmod_congr_of_sub_mem_max_ideal

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ p ^ n < p ^ (n + 1)

Tactic:
apply Nat.pow_lt_pow_right hp_prime.1.one_lt n.lt_add_one

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
x✝ : x ∈ Set.Icc a b
left✝ : a ≤ x
right✝ : x ≤ b
⊢ 1 / log x ^ 2 ≤ 1 / log a ^ 2

Tactic:
gcongr <;> bound

Goal state after:
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
s : Finset L
b✝ : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b✝ x)
this : LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b✝)
n : ℕ
b : Basis (Fin n) R ↥(↑R (Algebra.linearMap S L)).range
⊢ (S ⧸ (↑R (Algebra.linearMap S L)).ker) ≃ₗ[R] S

Tactic:
by
    rw [LinearMap.ker_eq_bot.mpr]
    · exact Submodule.quotEquivOfEqBot _ rfl
    · exact IsIntegralClosure.algebraMap_injective _ R _

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]), x - ↑(x.appr n) ∈ Ideal.span {↑(p ^ n)}

Tactic:
intros
      rw [Nat.cast_pow]
      exact appr_spec n _

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hh
x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ |θ t / (t * log t ^ 2)| ≤ log 4 * (1 / log t ^ 2)

Tactic:
case hh =>
    calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field

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

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : ↑(x.appr n) = 0
⊢ x.appr n = 0

Tactic:
rw [ZMod.natCast_eq_zero_iff] at h

Goal state after:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : p ^ n ∣ x.appr n
⊢ x.appr n = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℝ) in atTop, ↑(π ⌊x⌋₊) ≤ (log 4 + ε) * x / log x

Tactic:
have := integral_theta_div_log_sq_isLittleO.bound εpos
  filter_upwards [eventually_ge_atTop 2, this] with x hx hx2
  rw [primeCounting_eq_theta_div_log_add_integral hx, add_mul, add_div]
  have : 0 ≤ log x := by bound
  rw [norm_of_nonneg (show 0 ≤ x / log x by bound), ← mul_div_assoc] at hx2
  grw [theta_le_log4_mul_x (by linarith), ← hx2]
  grind [le_norm_self]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ↑(↑((f j) (r * s)).val - ↑((f j) r).val * ↑((f j) s).val) = 0

Tactic:
simp only [ZMod.natCast_val, map_mul, Int.cast_sub, ZMod.intCast_cast, Int.cast_mul]

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ((f j) r * (f j) s).cast - ((f j) r).cast * ((f j) s).cast = 0
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hfg : (autToPow K hμ) f = (autToPow K hμ) g
this : ↑f = ↑g
⊢ f = g

Tactic:
exact AlgEquiv.coe_toAlgHom_injective this

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

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'
x : R
n : ℕ
⊢ ((toZModPow n).comp g) x = ((toZModPow n).comp g') x

Tactic:
hg n

Goal state after:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'
x : R
n : ℕ
⊢ ((toZModPow n).comp g') x = ((toZModPow n).comp g') x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g') ↔ g = g'

Tactic:
constructor
  · intro hg
    ext x : 1
    apply ext_of_toZModPow.mp
    intro n
    change (toZModPow n).comp g x = (toZModPow n).comp g' x
    rw [hg n]
  · rintro rfl _
    rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this✝¹ : n * n + 1 = a * a
na : n < a
this✝ : (n + 1) * (n + 1) ≤ n * n + 1
this : n + n ≤ 0
⊢ d a1 = 0

Tactic:
Nat.eq_zero_of_le_zero ((Nat.le_add_left _ _).trans this)

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = 0 * 0
this✝¹ : n * n + 1 = a * a
na : n < a
this✝ : (n + 1) * (n + 1) ≤ n * n + 1
this : n + n ≤ 0
⊢ d a1 = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
⊢ xn a1 (m + n) = xn a1 m * xn a1 n + d a1 * yn a1 m * yn a1 n

Tactic:
injection pellZd_add a1 m n with h _
  zify
  rw [h]
  simp [pellZd]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
s : α ⊕ β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) s = (v ⊗ t) s

Tactic:
rcases s with a | b <;> dsimp [(· ∘ ·)]; try rw [inv]; rfl

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

Goal state before:
pp: case mpr
d : ℤ
hd : d < 0
⊢ norm 0 = 0

Tactic:
exact norm_zero

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n k : ℕ
⊢ xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧
    yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
let ⟨hx, hy⟩ := xy_modEq_yn n k
    have L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡
        xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2] := by
      gcongr
      rw [modEq_zero_iff_dvd, sq]
      gcongr
      apply dvd_mul_of_dvd_right
      rw [← modEq_zero_iff_dvd]
      refine (hy.of_dvd <| dvd_pow_self _ <| by decide).trans ?_
      simp [modEq_zero_iff_dvd]
    have R : xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡
        xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3] := by
      gcongr ?_ + ?_
      · rw [_root_.pow_succ]
        exact hx.mul_right' _
      · have : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n := by
          rcases k with - | k <;> simp [_root_.pow_succ]; ring_nf
        rw [← this]
        gcongr
    rw [add_tsub_cancel_right, Nat.mul_succ, xn_add, yn_add, pow_succ (xn _ n), Nat.succ_mul,
      add_comm (k * xn _ n ^ k) (xn _ n ^ k), right_distrib]
    exact ⟨L, R⟩

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

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

Tactic:
simp only [sub_self]; trivial

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

Goal state before:
pp: case zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑0 }
⊢ { re := ↑x + ↑d * ↑0 - ↑x, im := 0 - ↑0 }.Nonneg

pp: case succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑(y + 1) }
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg

Tactic:
· simp only [Nat.cast_zero, mul_zero, add_zero, sub_self]
    trivial

Goal state after:
case succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑(y + 1) }
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Tactic:
let t := le_antisymm yx xy
    rw [one_mul] at t
    exact absurd t (not_divides_sq _ _)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 0 % xn a1 n

Tactic:
rw [Nat.mod_eq_of_lt (strictMono_x a1 (Nat.pos_of_ne_zero npos))]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 0
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
h : -1 < ↑u * (2 * ↑v - 1) - ξ * ↑v * (2 * ↑v - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)

Tactic:
← sub_mul

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
h : -1 < (↑u - ξ * ↑v) * (2 * ↑v - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
| ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε

Tactic:
N

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ N : ℕ
| N ≥ N₀ → ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε