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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
⊢ 0 = ∑ r, ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u

Tactic:
conv at this => enter [2, 2, u]; rw [sum_mul]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, ∑ i, (∑ l, ↑(a' K a k l i u) * ↑(x (l, i))) * (newBasis K) u
⊢ 0 = ∑ r, ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ (↑m ^ s) ^ logb ↑m ↑n ≤ ↑n ^ s

Tactic:
← rpow_mul (Nat.cast_nonneg m),

Goal state after:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ ↑m ^ (s * logb ↑m ↑n) ≤ ↑n ^ s
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
⊢ Fintype.card β * Fintype.card (K →+* ℂ) = q * h

Tactic:
cardβ,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
⊢ q * Fintype.card (K →+* ℂ) = q * h
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ 1 ≤ ↑(↑((p ^ t).choose (i + 1))).valuation

Tactic:
← PadicInt.valuation_coe,

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ 1 ≤ (↑↑((p ^ t).choose (i + 1))).valuation
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x ↦ Δ_[1]^[x] (⇑f) 0)
n : ℕ
⊢ (⇑f ∘ Nat.cast) n = (⇑(mahlerSeries fun x ↦ Δ_[1]^[x] (⇑f) 0) ∘ Nat.cast) n

Tactic:
simpa [mahlerSeries_apply_nat (fwdDiff_tendsto_zero f) le_rfl]
    using shift_eq_sum_fwdDiff_iter 1 f n 0

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : ¬x' - y' = 0
⊢ exp (-padicValRat p (x' - y')) < embedding ↑γ

Tactic:
rw [← lt_log_iff_exp_lt (embedding_unit_ne_zero _)]

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : ¬x' - y' = 0
⊢ -padicValRat p (x' - y') < (embedding ↑γ).log
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
⊢ ∃ n W, (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(W j) ∧ Pairwise (Disjoint on W)

Tactic:
obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
  obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
  simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun
  let t : Finset (Fin n) := {j | W j ≠ ⊥}
  refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
  · exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2
  · exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
  · obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
    have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
    exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩
  · exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective

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

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
⊢ T_gen p F a < 1

Tactic:
have h := (div_lt_one (deriv_sq_norm_pos hnorm)).2 hnorm
  rw [T_def]; exact h

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

Goal state before:
pp: case hab
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖(Polynomial.aeval z) F‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n

Tactic:
apply hz.2

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

Goal state before:
pp: case hab
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖(Polynomial.aeval z) F‖ ≤ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n

Tactic:
apply hz.2

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

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ¬‖(Polynomial.aeval a) (Polynomial.derivative F)‖ = 0

Tactic:
apply deriv_norm_ne_zero

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤

Tactic:
let A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1

Goal state after:
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
⊢ ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval (newton_seq n)) (Polynomial.derivative F)‖ =
    ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
by rw [newton_seq_deriv_norm]

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

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ≠ 0

Tactic:
apply deriv_norm_ne_zero

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case refine_2
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : v ↑πᵥ < 1 ∧ πᵥ ≠ 0
a b : K[X]
hab : πᵥ = a * b
H : ¬IsUnit a ∧ ¬IsUnit b
⊢ False

Tactic:
simp only [hab, ne_eq, mul_eq_zero, not_or] at hπᵥ

Goal state after:
case refine_2
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
a b : K[X]
hab : πᵥ = a * b
H : ¬IsUnit a ∧ ¬IsUnit b
hπᵥ : v ↑(a * b) < 1 ∧ ¬a = 0 ∧ ¬b = 0
⊢ False
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
⊢ (toComplex (x / y)).re = ↑(round (toComplex x / toComplex y).re)

Tactic:
rw [div_def, ← @Rat.round_cast ℝ _ _]

Goal state after:
x y : ℤ[i]
⊢ (toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round (↑(x * star y).im / ↑(norm y)) }).re =
    ↑(round (toComplex x / toComplex y).re)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ IsSquare (-1)

Tactic:
induction n using induction_on_primes with
  | zero => exact False.elim (hn.ne_zero rfl)
  | one => exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩
  | prime_mul p n hpp ih =>
    have : Fact p.Prime := ⟨hpp⟩
    have hcp : p.Coprime n := by
      by_contra hc
      exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
    have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr <| H _ <|
      Nat.mem_primeFactors.mpr ⟨hpp, Nat.dvd_mul_right .., Squarefree.ne_zero hn⟩
    exact ZMod.isSquare_neg_one_mul hcp hp₁ <| ih hn.of_mul_right fun q hqp => H q <|
        Nat.mem_primeFactors.mpr ⟨Nat.prime_of_mem_primeFactors hqp,
          dvd_mul_of_dvd_right (Nat.dvd_of_mem_primeFactors hqp) _, Squarefree.ne_zero hn⟩

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p

Tactic:
rw [← ZMod.natCast_mod p 4, hp3]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑3
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℂ[X]
s : ℂ
⊢ P f s = cexp s * (s * ∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) f)

Tactic:
integral_exp_mul_eval,

Goal state after:
f : ℂ[X]
s : ℂ
⊢ P f s = cexp s * (-(cexp (-s) * eval s (sumIDeriv f)) + eval 0 (sumIDeriv f))
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
⊢ ∃ a_1,
    (p.quotientToQuotientRangePowQuotSucc P a_mem) a_1 =
      Quot.mk ⇑(p.powQuotSuccInclusion P i).range.quotientRel ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x, hx⟩

Tactic:
have Pe_le_Pi : P ^ e ≤ P ^ i := Ideal.pow_le_pow_right hi.le

Goal state after:
case mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
Pe_le_Pi : P ^ e ≤ P ^ i
⊢ ∃ a_1,
    (p.quotientToQuotientRangePowQuotSucc P a_mem) a_1 =
      Quot.mk ⇑(p.powQuotSuccInclusion P i).range.quotientRel ⟨Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x, hx⟩
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, ‖x‖ ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
simp_rw [Real.norm_eq_abs] at h

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, |x| ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case neg.inr
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : ↑m ∣ w
hx : ↑m ∣ x
hy : ↑m ∣ y
hz : ↑m ∣ z
h : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
⊢ False

pp: p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
⊢ ∃ w x y z, ↑m ∣ w ∧ ↑m ∣ x ∧ ↑m ∣ y ∧ ↑m ∣ z ∧ w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)

Tactic:
· have : (w / m) ^ 2 + (x / m) ^ 2 + (y / m) ^ 2 + (z / m) ^ 2 = ↑(r * p) := by
        refine mul_left_cancel₀ (pow_ne_zero 2 (Nat.cast_ne_zero.2 hm₀.ne')) ?_
        conv_rhs => rw [← Nat.cast_pow, ← Nat.cast_mul, sq m, mul_mul_mul_comm, Nat.cast_mul, ← h]
        simp only [mul_add, ← mul_pow, Int.mul_ediv_cancel', *]
      rw [← natAbs_iff] at this
      exact hmin r hrm ⟨hrm.trans hmp, hr₀, _, _, _, _, this⟩

Goal state after:
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
⊢ ∃ w x y z, ↑m ∣ w ∧ ↑m ∣ x ∧ ↑m ∣ y ∧ ↑m ∣ z ∧ w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
⊢ b ^ m ∈ {y | orderOf y = n}

Tactic:
rw [mem_ofPred_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.intent ⊆ d.intent ∧ ¬d.intent ⊆ c.intent ↔ d ≤ c ∧ ¬c ≤ d

Tactic:
intent_subset_intent_iff,

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ d ≤ c ∧ ¬d.intent ⊆ c.intent ↔ d ≤ c ∧ ¬c ≤ d
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: α : Type u
l : Filter α
x✝ : CardinalInterFilter l (ℵ_ 1)
⊢ CountableInterFilter l

Tactic:
refine ⟨fun S h a ↦ CardinalInterFilter.cardinal_sInter_mem (c := ℵ₁) S ?_ a⟩

Goal state after:
α : Type u
l : Filter α
x✝ : CardinalInterFilter l (ℵ_ 1)
S : Set (Set α)
h : S.Countable
a : ∀ s ∈ S, s ∈ l
⊢ #↑S < ℵ_ 1
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
⊢ ∀ ⦃J : Ideal P⦄, I < J → ∀ (x : P), x ∈ ↑J

Tactic:
intro J

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
J : Ideal P
⊢ I < J → ∀ (x : P), x ∈ ↑J
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s x : α
inst✝ : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
x✝ : (fun y ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
⊢ ¬Disjoint z y

Tactic:
have := P.ne_bot_of_mem hx

Goal state after:
α : Type u_1
s x : α
inst✝ : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
x✝ : (fun y ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
this : x ≠ ⊥
⊢ ¬Disjoint z y
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this : MeasurableSpace (ι × Ω) := 𝓕.predictable
⊢ StronglyMeasurable fun p ↦ u (↑p.1) p.2

Tactic:
let : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (𝓕 i)

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
⊢ StronglyMeasurable fun p ↦ u (↑p.1) p.2
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f j ω ∂μ

Tactic:
by
  rw [← setIntegral_condExp (ℱ.le i) (hf.integrable j) hs]
  refine setIntegral_congr_ae (ℱ.le i s hs) ?_
  filter_upwards [hf.2 i j hij] with _ heq _ using heq.symm

Goal state after: