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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
w : InfinitePlace K
⊢ w ≠ W₀ ↔ (equivInfinitePlace K) w ≠ w₀

Tactic:
by rw [not_iff_not, Equiv.eq_symm_apply]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inr.inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
| inl hl =>

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝ : Field K
θ : 𝓞 K
⊢ exponent θ = 1 ↔ ℤ[θ] = ⊤

Tactic:
rw [exponent, absNorm_eq_one_iff, comap_eq_top_iff, conductor_eq_top_iff_adjoin_eq_top]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (fun x ↦ Real.exp 1) ^ x w₀ * ↑expMap (∑ i, x ↑i • (completeBasis K) ↑i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
Pi.pow_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (fun i ↦ Real.exp 1 ^ x w₀) * ↑expMap (∑ i, x ↑i • (completeBasis K) ↑i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ ↑(frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) ^ orderOf (unitOfCoprime (p ^ f) ⋯)) pB.gen = ↑1 pB.gen

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ ↑(unitOfCoprime (p ^ f) ⋯ ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P))) = ↑1

Tactic:
· simp only [AlgEquiv.coe_toAlgHom, AlgEquiv.coe_pow, AlgEquiv.one_apply,
      coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, hK]
    nth_rewrite 2 [← pow_one pB.gen]
    rw [powerBasis_gen hPirr.ne_zero, hζ'.pow_eq_pow_iff_modEq, ← hζ.eq_orderOf,
      ← natCast_eq_natCast_iff]
    simpa only [Nat.cast_pow, Nat.cast_one, coe_unitOfCoprime, Units.val_one,
      Units.val_pow_eq_pow_val] using! Units.val_inj.mpr <| pow_orderOf_eq_one
      (unitOfCoprime _ (hn.pow_left f))

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ ↑(unitOfCoprime (p ^ f) ⋯ ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P))) = ↑1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ p.totient) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))

Tactic:
← hζ.toInteger_isPrimitiveRoot.card_primitiveRoots,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (primitiveRoots p (𝓞 K)).card) (∏ x ∈ primitiveRoots p (𝓞 K), (1 - x))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card ↥((intermediateFieldEquivSubgroupChar n K R) F) = Module.finrank ℚ ↥F

Tactic:
unfold intermediateFieldEquivSubgroupChar
  rw [OrderIso.trans_apply, OrderIso.trans_apply, OrderIso.dualDual_symm_apply,
    IsGalois.intermediateFieldEquivSubgroup_apply, OrderIso.dual_apply, OrderDual.ofDual_toDual,
    OrderDual.ofDual_toDual, card_subgroupGalEquivSubgroupChar, finrank_eq_fixingSubgroup_index,
    ← Subgroup.index_eq_card]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ∃ y ∈ ↑↑↑J, (mixedEmbedding K) y = ↑↑(toMixed K) x) ∧
        (↑(toMixed K)).toEquiv x = x✝) →
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s

Tactic:
rintro ⟨_, ⟨⟨hx₁, hx₂⟩, _, ⟨x, hx₃, rfl⟩, h⟩, rfl⟩

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
w✝ : euclidean.mixedSpace K
hx₁ : (toMixed K) w✝ ∈ fundamentalCone K
hx₂ : mixedEmbedding.norm ((toMixed K) w✝) ≤ s
x : 𝓞 K
hx₃ : x ∈ ↑↑J
h : (mixedEmbedding K) ((Algebra.linearMap (𝓞 K) K) x) = ↑↑(toMixed K) w✝
⊢ ((↑(toMixed K)).toEquiv w✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = (↑(toMixed K)).toEquiv w✝) ∧
    mixedEmbedding.norm ((↑(toMixed K)).toEquiv w✝) ≤ s
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := ⋯
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⋯
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < ↑k

Tactic:
hk

Goal state after:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < ↑(⌈logb M (1 / 2)⌉₊ + 1)
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑B + 1) ^ (↑n - ↑m) * (↑B + 1) ^ m = (↑B + 1) ^ n

Tactic:
by
        rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
⊢ ∀ (t : Finset α), Disjoint t (Set.Finite.toFinset ⋯) → ∏ b ∈ t, f b ∈ U

Tactic:
intro t

Goal state after:
case h
α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
U : Set G
hU : U ∈ 𝓝 1
V : OpenSubgroup G
hV : ↑V ⊆ U
t : Finset α
⊢ Disjoint t (Set.Finite.toFinset ⋯) → ∏ b ∈ t, f b ∈ U
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ 0 ≤ x i

Tactic:
exact hxT.1 i

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case hr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ 0 ≤ c₂ K * A

Tactic:
exact mul_nonneg (c₂_nonneg _) Apos

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case hbc
f : AbsoluteValue ℚ ℝ
m✝ n✝ : ℕ
hm✝ : 1 < m✝
hn✝ : 1 < n✝
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
hfm : 1 < f ↑m
⊢ ↑d ≤ logb ↑m ↑n

Tactic:
exact natLog_le_logb n m

Goal state after:
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 ^ logb ↑m ↑n) ^ s ≤ ↑n ^ s

Tactic:
rpow_logb (mod_cast zero_lt_of_lt hm) (mod_cast hm.ne') (mod_cast zero_lt_of_lt hn)

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
⊢ ↑n ^ s ≤ ↑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
⊢ 0 < p * h

Tactic:
rw [mul_pos_iff]

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
⊢ 0 < p ∧ 0 < h ∨ p < 0 ∧ h < 0
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:
Padic.valuation_natCast,

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 ≤ ↑(padicValNat p ((p ^ t).choose (i + 1)))
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
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n k : ℕ
⊢ k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k

Tactic:
hk

Goal state after:
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 k : ℕ
hk : k ≤ s
⊢ ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
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 : (Rat.padicValuation p) (x' - y') < exp (-↑n)
⊢ ↑(↑(p ^ n)).num ≠ 0

Tactic:
· simp [Nat.Prime.ne_zero Fact.out]

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

Goal state before:
pp: case h
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)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs))⁻¹
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
⊢ ↑(↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs)).num ≠ 0

Tactic:
· simp [Nat.Prime.ne_zero Fact.out]

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

Goal state before:
pp: case ih
p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ : WithVal (Rat.padicValuation p)
⊢ ⋯.extend coe' ((extensionHom ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯) ↑a✝) = ↑a✝

Tactic:
rw [extensionHom_coe]
      apply IsDenseInducing.extend_eq
      exact continuous_coe _

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
a : Solution₁ d
⊢ ∃ b, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}

Tactic:
by
  refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩) <;>
      simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true] <;>
    assumption

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
hm₀ : ↑m ≠ 0
⊢ (↑q₁.num * ↑q₂.den - ↑q₂.num * ↑q₁.den) / ↑m ≠ 0

Tactic:
refine div_ne_zero_iff.mpr ⟨?_, hm₀⟩

Goal state after:
case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
hm₀ : ↑m ≠ 0
⊢ ↑q₁.num * ↑q₂.den - ↑q₂.num * ↑q₁.den ≠ 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ a.x ^ 2 - 1 = d * b.y ^ 2

Tactic:
b.prop_y,

Goal state after:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ a.x ^ 2 - 1 = b.x ^ 2 - 1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * a₁.y ≤ a.y * a₁.x

Tactic:
rw [← abs_of_pos <| zero_lt_one.trans hax, ← abs_of_pos hay, ← abs_of_pos h.x_pos, ←
    abs_of_pos h.2.1, ← abs_mul, ← abs_mul, ← sq_le_sq, mul_pow, mul_pow, a.prop_x, a₁.prop_x, ←
    sub_nonneg]

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ a.y ^ 2 * (1 + d * a₁.y ^ 2) - (1 + d * a.y ^ 2) * a₁.y ^ 2
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inl
hp : Fact (Nat.Prime 2)
⊢ ∃ a b k, 0 < k ∧ k < 2 ∧ a ^ 2 + b ^ 2 + 1 = k * 2

Tactic:
use 1, 0, 1

Goal state after:
case h
hp : Fact (Nat.Prime 2)
⊢ 0 < 1 ∧ 1 < 2 ∧ 1 ^ 2 + 0 ^ 2 + 1 = 1 * 2
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: weights : ℕ → ℝ
hw : weights 1 = 1
⊢ IsUpperMoebius (lambdaSquared weights)

Tactic:
by
  dsimp only [IsUpperMoebius, lambdaSquared]
  intro n
  split_ifs
  · simp_all
  grw [sq_nonneg (∑ d ∈ n.divisors, weights d), sum_divisors_lambda_sq_larger_sum _ n, sum_comm]
  apply le_of_eq
  simp_rw [sq, mul_sum, sum_mul]
  congr! 1 with d1 hd1
  rw [sum_comm]
  congr! 1 with d2 hd2
  rw [sum_ite_eq_of_mem', mul_comm]
  -- Deal with the side goal from `sum_ite_eq_of_mem'`
  rw [mem_divisors, Nat.lcm_dvd_iff]
  exact ⟨⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩, (mem_divisors.mp hd1).2⟩

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℤ
hk : ↑a ^ 2 + ↑b ^ 2 - -1 = ↑p * k
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
rw [sub_neg_eq_add, mul_comm] at hk

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℤ
hk : ↑a ^ 2 + ↑b ^ 2 + 1 = k * ↑p
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ k < p

Tactic:
refine lt_of_sum_four_squares_eq_mul hk ?_ ?_ ?_ ?_

Goal state after:
case inr.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * a < p

case inr.refine_2
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * b < p

case inr.refine_3
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 1 < p

case inr.refine_4
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 0 < p
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hlt : 1 < v X
hv : v.IsEquiv (inftyValuation K)
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))

Tactic:
refine .inl ⟨hv, ?_⟩

Goal state after:
case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hlt : 1 < v X
hv : v.IsEquiv (inftyValuation K)
⊢ ¬∃! u, v.IsEquiv (valuation K⟮X⟯ u)
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
⊢ (∑ x ∈ s.prodPrimes.divisors, if x = d1.lcm d2 then w d1 * w d2 * s.nu x else 0) =
    s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

Tactic:
have h : d1.lcm d2 ∣ s.prodPrimes :=
      Nat.lcm_dvd_iff.mpr ⟨dvd_of_mem_divisors hd1, dvd_of_mem_divisors hd2⟩

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ (∑ x ∈ s.prodPrimes.divisors, if x = d1.lcm d2 then w d1 * w d2 * s.nu x else 0) =
    s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case inr.refine_2
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
refine ⟨a, b, hab.symm, ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hb
      |>.mpr fun q hq hq4 ↦ ?_⟩

Goal state after:
case inr.refine_2
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
⊢ False
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)
⊢ False

Tactic:
have qR0 : (0 : ℝ) < q := Int.cast_pos.mpr (zero_lt_one.trans q1)

Goal state after:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)
qR0 : 0 < ↑q
⊢ False
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m ↦ (↑n)⁻¹ * ↑m)
B : x ∉ range fun m ↦ (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m ↦ (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (↑m / ↑n) x < δ
⊢ False

Tactic:
refine hε (ball_subset_ball hδ hlt) ⟨m, ?_⟩

Goal state after:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m ↦ (↑n)⁻¹ * ↑m)
B : x ∉ range fun m ↦ (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m ↦ (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (↑m / ↑n) x < δ
⊢ (fun m ↦ (↑n)⁻¹ * ↑m) m = ↑m / ↑n
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (↑a).val ∧ (↑a).val < (p - 1).succ

Tactic:
← Nat.succ_sub hp,

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (↑a).val ∧ (↑a).val < p.succ - succ 0
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b | ¬r b a}) ↔ Bounded r s

Tactic:
refine ⟨?_, Bounded.mono inter_subset_left⟩
  rintro ⟨b, hb⟩
  obtain ⟨m, hm⟩ := H a b
  exact ⟨m, fun c hc => hm c (or_iff_not_imp_left.2 fun hca => hb c ⟨hc, hca⟩)⟩

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' y x
hx : x ∈ c'.extent
⊢ y ∈ c'.extent

Tactic:
by
  rw [← lowerPolar_intent]
  exact fun z hz ↦ _root_.trans hy (rel_extent_intent hx hz)

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
⊢ a < b ↔ ∃ c, a < principal c ∧ principal c ≤ b

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨c, hca, hcb⟩ ↦ hca.trans_le hcb⟩
  rw [← extent_ssubset_extent_iff, Set.ssubset_iff_exists] at h
  simpa [← not_le, principal_le_iff, and_comm] using h.2

Goal state after: