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

Goal state before:
pp: case calc_4
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
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤
    c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))

pp: case calc_5
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
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ c K * A * supOfBasis K

pp: case calc_6
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
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * supOfBasis K ≤ c₂ K * A

Tactic:
· rw [mul_assoc, mul_assoc]
      gcongr _ * (?_ * _)
      · apply house_nonneg
      · exact habs kr.1 lu.1

Goal state after:
case calc_5
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
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ c K * A * supOfBasis K

case calc_6
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
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * supOfBasis K ≤ c₂ K * A
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ↑(Fintype.card (K →+* ℂ)) * ((↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) * supOfBasis K) ≤
    ↑h * c₂ K * (↑q * c₁ K * A) ^ (↑p / (↑q - ↑p))

Tactic:
Embeddings.card,

Goal state after:
case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ↑(finrank ℚ K) * ((↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) * supOfBasis K) ≤
    ↑h * c₂ K * (↑q * c₁ K * A) ^ (↑p / (↑q - ↑p))
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)
⊢ ↑p ^ (-↑(↑((p ^ t).choose (i + 1))).valuation) ≤ ↑↑p ^ (-1)

Tactic:
NNReal.coe_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)
⊢ ↑p ^ (-↑(↑((p ^ t).choose (i + 1))).valuation) ≤ ↑p ^ (-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 : ℕ
⊢ ‖Δ_[1]^[n + s * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
by
  -- We show the following more general statement by induction on `k`:
  suffices ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] f 0‖ ≤ ‖f‖ / p ^ k from this le_rfl
  intro k hk
  induction k generalizing n with
  | zero => -- base case just says that `‖Δ^[·] (⇑f) 0‖` is bounded by `‖f‖`
    simpa only [zero_mul, pow_zero, add_zero, div_one] using norm_fwdDiff_iter_apply_le 1 f 0 n
  | succ k IH => -- induction is the "step 2" lemma above
    rw [add_mul, one_mul, ← add_assoc]
    refine (bojanic_mahler_step2 hst (n + k * p ^ t)).trans (max_le ?_ ?_)
    · rw [← coe_nnnorm, ← NNReal.coe_natCast, ← NNReal.coe_pow, ← NNReal.coe_div, NNReal.coe_le_coe]
      refine Finset.sup_le fun j _ ↦ ?_
      rw [pow_succ, ← div_div, div_le_div_iff_of_pos_right (mod_cast hp.out.pos), add_right_comm]
      exact_mod_cast IH (n + (j + 1)) (by lia)
    · exact div_le_div_of_nonneg_left (norm_nonneg _)
        (mod_cast pow_pos hp.out.pos _) (mod_cast pow_le_pow_right₀ hp.out.one_le hk)

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : ‖↑x‖ ≤ 1
⊢ ¬p ∣ x.den

Tactic:
simpa [Nat.Prime.coprime_iff_not_dvd Fact.out] using isUnit_iff.1 <| isUnit_den _ h

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ⇑(f.prodMap f) ⁻¹' S ∈ 𝓝ˢ (diagonal X)

Tactic:
mem_nhdsSet_iff_forall

Goal state after:
X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : ∀ x ∈ diagonal V, S ∈ 𝓝 x
⊢ ∀ x ∈ diagonal X, ⇑(f.prodMap f) ⁻¹' S ∈ 𝓝 x
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ 0 - 1
⊢ False

Tactic:
zero_sub

Goal state after:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ -1
⊢ False
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) = ⊤
⊢ p • ⊤ = ⊤

Tactic:
calc
      p • ⊤ = Submodule.map M.mkQ (p • ⊤) := by
        rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]
      _ = ⊤ := by rw [Ideal.smul_top_eq_map, (Submodule.map_mkQ_eq_top M _).mpr hb']

Goal state after:
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
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ |a₁.x| ≤ |a.x|

Tactic:
abs_of_pos (zero_lt_one.trans h.1),

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ≤ |a.x|
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
⊢ 0 < (a * a₁⁻¹).x

Tactic:
simp only [x_mul, x_inv, y_inv, mul_neg, lt_add_neg_iff_add_lt, zero_add]

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a.y * a₁.y) < a.x * a₁.x
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
⊢ ∃ ia,
    True ∧
      ∀ x ∈ {x | (ValuativeRel.valuation (WithVal (valuation K v))) x < ↑ia},
        (algebraMap (WithVal (valuation K v)) (WithVal (valuation L w))) x ∈
          {x | (ValuativeRel.valuation (WithVal (valuation L w))) x < ↑γL}

Tactic:
let m : ℤᵐ⁰ := σw (σL (σwV γL))

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
m : WithZero (Multiplicative ℤ) := σw (σL (σwV ↑γL))
⊢ ∃ ia,
    True ∧
      ∀ x ∈ {x | (ValuativeRel.valuation (WithVal (valuation K v))) x < ↑ia},
        (algebraMap (WithVal (valuation K v)) (WithVal (valuation L w))) x ∈
          {x | (ValuativeRel.valuation (WithVal (valuation L w))) x < ↑γL}
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case hg
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
⊢ v ↑πᵥ < 1

Tactic:
exact valuation_uniformizingPolynomial_lt_one hle

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * 2 ≠ 0

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
⊢ ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0

Tactic:
decide

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

Goal state before:
pp: x y : ℤ
⊢ toComplex { re := x, im := y } = ↑x + ↑y * I

Tactic:
by simp [toComplex_def]

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

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

Tactic:
by simp [toComplex_def]

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

Goal state before:
pp: x : ℤ[i]
⊢ ↑x.im = (toComplex x).im

Tactic:
by simp [toComplex_def]

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

Goal state before:
pp: x y : ℤ
⊢ (toComplex { re := x, im := y }).re = ↑x

Tactic:
by simp [toComplex_def]

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

Goal state before:
pp: x y : ℤ
⊢ (toComplex { re := x, im := y }).im = ↑y

Tactic:
by simp [toComplex_def]

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

Goal state before:
pp: x : ℤ[i]
⊢ (norm x).natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs

Tactic:
zify
  rw [abs_norm (by simp)]
  simp [Zsqrtd.norm]

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
decide

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
hx0 : x = 0
⊢ -1 ≠ 0

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : -1 = y * y
⊢ p % 4 ≠ 3

Tactic:
rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h

Goal state after:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
⊢ p % 4 ≠ 3
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3

Tactic:
decide

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
hx0 : x = 0
⊢ 1 ≠ 0

Tactic:
decide

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 ≠ ↑3

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: 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
this✝ : Fact (Prime q)
this : n ≠ 0 → b.primeFactors ⊆ n.primeFactors
⊢ b.factorization q = 1

Tactic:
grind [Squarefree.natFactorization_le_one,
      Prime.dvd_iff_one_le_factorization, prime_of_mem_primeFactors, dvd_of_mem_primeFactors]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: case refine_2
r : ℚ
⊢ ↑r ∈ {x | ∀ (i : ℕ), ∃ i_1 i_2, ∃ (_ : 1 < i_2), x ∈ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i)}

Tactic:
refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩

Goal state after:
case refine_2.refine_1
r : ℚ
n : ℕ
⊢ 1 < ↑r.den * 2

case refine_2.refine_2
r : ℚ
n : ℕ
⊢ ↑r ∈ ball (↑(r.num * 2) / ↑(↑r.den * 2)) (1 / ↑(↑r.den * 2) ^ n)
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x ∈ Ico 1 (p - 1).succ, ↑x = ∏ x, ↑x

Tactic:
symm

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x, ↑x = ∏ x ∈ Ico 1 (p - 1).succ, ↑x
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: n : ℕ
h : n ≠ 1
h1 : Prime n
this : Fact (Prime n)
⊢ ↑(n - 1)! = -1

Tactic:
exact ZMod.wilsons_lemma n

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ ↑(sSup S) = ⨆ N ∈ S, ↑N

Tactic:
coe_sSup,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ sSup {x | ∃ s ∈ S, ↑s = x} = ⨆ N ∈ S, ↑N
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.left, b ≤ x✝) ↔ x✝ ∈ upperBounds A.left

Tactic:
mem_upperBounds

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.left, b ≤ x✝) ↔ ∀ x ∈ A.left, x ≤ x✝
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
s : Set α
f : α → β
⊢ Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂

Tactic:
by
  simp only [Tendsto, PTendsto, pmap_res]

Goal state after:
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ a ⊓ bᶜᶜ = a ⊓ b

Tactic:
hb.eq

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ a ⊓ b = a ⊓ b
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ a ⇨ bᶜᶜ = a ⇨ b

Tactic:
hb.eq

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ a ⇨ b = a ⇨ b
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
hb : IsRegular b
⊢ a ≤ bᶜᶜ ↔ a ≤ b

Tactic:
hb.eq

Goal state after:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
hb : IsRegular b
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : Regular α
⊢ ↑((a ⊔ b) ⊓ (a ⊔ c)) ≤ ↑(a ⊔ b ⊓ c)

Tactic:
by
        dsimp
        rw [sup_inf_left, compl_compl_inf_distrib]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case neg.inr.inr
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
p : Nat.Primes
h✝ : ¬B ↑p =ᵐ[μ] ∅
h : B ↑p =ᵐ[μ] univ
⊢ A ↑p ∪ B ↑p ∪ C ↑p =ᵐ[volume] univ

Tactic:
simp only [μ, h, union_ae_eq_univ_of_ae_eq_univ_left,
        union_ae_eq_univ_of_ae_eq_univ_right]

Goal state after:
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Ioc a b).ncard = b - a

Tactic:
simpa [← Set.ncard_coe_finset] using Nat.card_Ioc a b

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ

Tactic:
by
    obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this
    refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
    · simpa only [tsub_le_iff_right] using j.property.2.trans le_self_add
    · rw [sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm]
      exact (dist_triangle ((j : ℕ) • ξ) x ((i : ℕ) • ξ)).trans (by
        linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2])

Goal state after:
Module: Mathlib.Order.Interval.Set.SurjOn

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : b ≤ a
⊢ SurjOn f (Ico a b) (Ico (f a) (f b))

Tactic:
· rw [Ico_eq_empty (h_mono hab).not_gt]
    exact surjOn_empty f _

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n ((x ⇨ y) ⊓ x) = n (y ⊓ x)

Tactic:
himp_inf_self

Goal state after:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ n (y ⊓ x) = n (y ⊓ x)
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case left.a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨆ y ∈ Y, f a y

Tactic:
exact le_trans (iInf₂_le a ha) (le_rfl)

Goal state after:
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
h₁ : ∀ (a : α), ScottContinuous fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuous fun a ↦ f (a, b)
⊢ ScottContinuous f

Tactic:
simp_rw [← scottContinuousOn_univ] at ⊢

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
h₁ : ∀ (a : α), ScottContinuous fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuous fun a ↦ f (a, b)
⊢ ScottContinuousOn univ f
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
⊢ t.subtrees.PairwiseDisjoint SetLike.coe

Tactic:
intro t₁ ht₁ t₂ ht₂ h

Goal state after:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ Function.onFun Disjoint SetLike.coe t₁ t₂
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o₁ o₂ o₃ : OrderType.{u}
α : Type u
x✝² : LinearOrder α
β : Type u
x✝¹ : LinearOrder β
γ : Type u
x✝ : LinearOrder γ
⊢ type α * type β * type γ = type α * (type β * type γ)

Tactic:
simp only [← type_lex_prod]

Goal state after:
o₁ o₂ o₃ : OrderType.{u}
α : Type u
x✝² : LinearOrder α
β : Type u
x✝¹ : LinearOrder β
γ : Type u
x✝ : LinearOrder γ
⊢ type (Lex (γ × Lex (β × α))) = type (Lex (Lex (γ × β) × α))
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ (fun n ↦ (OrderDual.ofDual n).toSublocale) ((fun s ↦ OrderDual.toDual s.toNucleus) S) = S

Tactic:
ext x; simpa using ⟨by simp +contextual [eq_comm], fun hx ↦ ⟨x, by simp [hx]⟩⟩

Goal state after: