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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
⊢ (algebraMap F K).fieldRange = maximalRealSubfield K

Tactic:
have := IsTotallyReal.ofRingEquiv (algebraMap F K).rangeRestrictFieldEquiv

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
⊢ (algebraMap F K).fieldRange = maximalRealSubfield K
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this✝ : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
this : IsTotallyReal ↥L
⊢ IsCMField K

Tactic:
have : IsQuadraticExtension L K := ⟨by
    rw [IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, hσ']⟩

Goal state after:
K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this✝¹ : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
this✝ : IsTotallyReal ↥L
this : IsQuadraticExtension (↥L) K
⊢ IsCMField K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMapBasis.source = Set.univ

Tactic:
by
  simp [expMapBasis, expMap_source]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ span {↑p} ⊔ span {(aeval θ) Q} = span {↑p, (aeval θ) Q}

Tactic:
← span_insert

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ span {↑p, (aeval θ) Q} = span {↑p, (aeval θ) Q}
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card =
    (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) / orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
mul_div_left _ (orderOf_pos _),

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card = (normalizedFactors (cyclotomic n K)).card
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case h_fin
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (normLeOne K) < ∞

Tactic:
rw [volume_normLeOne]

Goal state after:
case h_fin
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) < ∞
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
⊢ P.ramificationIdx ℤ = 1

Tactic:
let ζ := (zeta_spec m ℚ K).toInteger
  have h₁ : ¬ p ∣ exponent ζ := by
    rw [exponent_eq_one_iff.mpr <| adjoin_singleton_eq_top (zeta_spec m ℚ K)]
    exact hp.out.not_dvd_one
  have h₂ := (primesOverSpanEquivMonicFactorsMod h₁ ⟨P, ⟨inferInstance, inferInstance⟩⟩).2
  have h₃ := ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply' h₁ h₂
  simp only [Subtype.coe_eta, Equiv.symm_apply_apply] at h₃
  rw [Multiset.mem_toFinset, Polynomial.mem_normalizedFactors_iff
    (map_monic_ne_zero (minpoly.monic ζ.isIntegral))] at h₂
  rw [h₃]
  refine multiplicity_eq_of_emultiplicity_eq_some (le_antisymm ?_ ?_)
  · apply emultiplicity_le_one_of_separable
    · exact isUnit_iff_degree_eq_zero.not.mpr (Irreducible.degree_pos h₂.1).ne'
    · exact (zeta_spec m ℚ K).toInteger_isPrimitiveRoot.separable_minpoly_mod hm
  · rw [ENat.natCast_one]
    exact Order.one_le_iff_pos.mpr <| emultiplicity_pos_of_dvd h₂.2.2

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ¬∃ δ, HasDirichletDensity S δ
⊢ 0 ≤ 0

Tactic:
· exact le_rfl

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
⊢ Tendsto (fun s ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) / s) atTop
    (𝓝 (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|)))

Tactic:
have h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K := by ext; simp

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
⊢ Tendsto (fun s ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) / s) atTop
    (𝓝 (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|)))
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 : ∀ (x_1 : α × (K →+* ℂ)), (asiegel K a *ᵥ x) x_1 = 0 x_1
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
specialize hmulvec0 ⟨k, u⟩

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 β
k : α
u : K →+* ℂ
hmulvec0 : (asiegel K a *ᵥ x) (k, u) = 0 (k, u)
l : β
hξ : ¬ξ K x l = 0 l
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case refine_1.inr
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this✝ : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
w✝ m : ℕ
hpm : ¬p ∣ m
hn : p ^ w✝ * m ≠ 0
this : padicNorm p ↑m = 1
⊢ f ↑(p ^ w✝ * m) ^ t⁻¹ = (padic p) ↑(p ^ w✝ * m)

Tactic:
simp_all [← rpow_natCast, ← rpow_mul, mul_comm t, mul_inv_cancel_right₀ ht.ne',
        eq_one_of_not_dvd bdd hp0 hp1 hmin hpm]

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

Goal state before:
pp: case succ.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
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
j : ℕ
x✝ : j ∈ range (p ^ t - 1)
⊢ ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ ≤ ‖f‖₊ / ↑p ^ k

Tactic:
add_right_comm

Goal state after:
case succ.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
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
j : ℕ
x✝ : j ∈ range (p ^ t - 1)
⊢ ‖Δ_[1]^[n + (j + 1) + 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)
a✝ : ℚ
⊢ (extensionHom ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯) (⋯.extend coe' ↑a✝) = ↑a✝

Tactic:
· have : ∀ q : ℚ, Padic.isDenseInducing_cast_withVal.extend coe' q = coe'
        ((WithVal.equiv (Rat.padicValuation p)).symm q) := by
        intro q
        apply IsDenseInducing.extend_eq
        exact continuous_coe _
      rw [this, extensionHom_coe]
      simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
⊢ ∃ x, x ∈ U ∩ Set.range ⇑tensorHom

Tactic:
have := mem_nhds_uniformity_iff_right.mp (hUo.mem_nhds hUf)

Goal state after:
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝¹ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this✝ : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this : {p | p.1 = f → p.2 ∈ U} ∈ 𝓤 C(X × Y, R)
⊢ ∃ x, x ∈ U ∩ Set.range ⇑tensorHom
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: k : ℕ
hk0 : k ≠ 0
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ 1 [MOD k]

Tactic:
refine frequently_atTop.2 fun n => ?_
  obtain ⟨p, hp⟩ := exists_prime_gt_modEq_one n hk0
  exact ⟨p, ⟨hp.2.1.le, hp.1, hp.2.2⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : Field K
inst✝¹⁷ : Field L
inst✝¹⁶ : Algebra K L
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
p : Ideal A
P : Ideal B
inst✝¹² : P.LiesOver p
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : MulSemiringAction Gal(L/K) B
inst✝⁹ : IsGaloisGroup Gal(L/K) A B
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Ring.HasFiniteQuotients A
inst✝³ : P.IsMaximal
E : Type u_6
inst✝² : Field E
inst✝¹ : Algebra E L
inst✝ : IsInertiaField K L P E
hp : p ≠ ⊥
⊢ Module.finrank E L = p.ramificationIdxIn B

Tactic:
have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
  have : Finite (A ⧸ p) := Ring.HasFiniteQuotients.finiteQuotient hp
  rw [← IsGaloisGroup.card_eq_finrank (inertia Gal(L/K) P) E L, card_inertia_eq_ramificationIdxIn p]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, b⁻¹ = a₁ ^ n ∨ b⁻¹ = -a₁ ^ n

Tactic:
exact ⟨-n, Or.inl (by simp [hn])⟩

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a ∈ {-b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
Set.mem_singleton_iff

Goal state after:
case inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
⊢ ∃! a₁, 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
refine ⟨a₁, ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩, fun a (H : 1 < _ ∧ _) => ?_⟩

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
a : Solution₁ d
H : 1 < a.x ∧ 0 < a.y ∧ ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n
⊢ a = a₁
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : ↑k < ↑j / r
h₁₂ : (↑j + 1) / r ≤ ↑k + 1
h₂₁ : ↑m ≤ ↑j / s
h₂₂ : (↑j + 1) / s < ↑m + 1
h₃ : ↑k + ↑m < ↑j
h₄ : ↑j < ↑k + ↑1 + ↑m
⊢ False

Tactic:
add_right_comm

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k m : ℤ
h₁₁ : ↑k < ↑j / r
h₁₂ : (↑j + 1) / r ≤ ↑k + 1
h₂₁ : ↑m ≤ ↑j / s
h₂₂ : (↑j + 1) / s < ↑m + 1
h₃ : ↑k + ↑m < ↑j
h₄ : ↑j < ↑k + ↑m + ↑1
⊢ False
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

Tactic:
suffices ∀ d1 d2, (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2) by
    simp_rw [← Nat.divisors_filter_dvd_of_dvd hd.2 hd.1, sum_filter, ite_sum_zero, ← ite_and, this]

Goal state after:
case a
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (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
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
⊢ ↑(f (σ 0) ^ 2 + f (σ 1) ^ 2) = 0

Tactic:
simpa only [σ, Int.cast_pow, Int.cast_add, Equiv.swap_apply_right, ZMod.pow_card] using! hσ.1

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ 0 = 0 * 1

Tactic:
zero_mul

Goal state after:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case hbc
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ‖∫ (x : ℝ) in Set.Ioc 0 1, cexp (-(x • s)) * eval (x • s) (f p) ∂MeasureTheory.volume‖ ≤ Real.exp ‖s‖ * |c| ^ p * 1

Tactic:
convert! MeasureTheory.norm_setIntegral_le_of_norm_le_const _ _

Goal state after:
case e'_4.e'_6
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ 1 = MeasureTheory.volume.real (Set.Ioc 0 1)

case hbc.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ MeasureTheory.volume (Set.Ioc 0 1) < ⊤

case hbc.convert_11
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ∀ x ∈ Set.Ioc 0 1, ‖cexp (-(x • s)) * eval (x • s) (f p)‖ ≤ Real.exp ‖s‖ * |c| ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: ⊢ {x | Liouville x} = ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Tactic:
by
  ext x
  simp only [mem_iInter, mem_iUnion, Liouville, mem_ofPred_eq, exists_prop, Set.mem_sdiff,
    mem_singleton_iff, mem_ball, Real.dist_eq, and_comm]

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

Goal state before:
pp: x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x

Tactic:
refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩

Goal state after:
x : ℝ
hx : Liouville x
p : ℝ
⊢ ∀ (x_1 : ℕ),
    (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ ⌈p⌉₊) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < 1 / ↑x_1 ^ ↑⌈p⌉₊
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
⊢ IsGLB s (sInf s)

Tactic:
by
  refine ⟨fun e he ↦ ?_, fun e h ↦ ?_⟩
  · by_contra! hs
    obtain ⟨a, ha⟩ := hs
    exact ha.2.not_ge (sInf_apply_le he ha.1)
  · by_contra! hs
    obtain ⟨a, ha⟩ := hs
    refine ha.2.not_ge <| le_sInf_apply fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_
    simp_all

Goal state after:
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
x✝ : Set (Lex ((i : ι) → (fun i ↦ α i) i))
⊢ IsGLB x✝ (sInf x✝)

Tactic:
by exact isGLB_sInf

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊔ b = ⊤ ↔ ↑(a ⊔ b) = ⊤

Tactic:
← coe_top (L := L),

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ a ⊔ b = ⊤ ↔ ↑(a ⊔ b) = ↑⊤
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
⊢ Disjoint c'.extent c'.intent

Tactic:
rw [disjoint_iff_forall_ne]

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
⊢ ∀ ⦃a : α⦄, a ∈ c'.extent → ∀ ⦃b : α⦄, b ∈ c'.intent → a ≠ b
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
⊢ principal (sSup A.left) = A

Tactic:
by
  apply ext'
  ext
  rw [right_principal, mem_Ici, sSup_le_iff, ← upperBounds_left, mem_upperBounds]

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ countableSupClosure s
⊢ b ≤ a

Tactic:
mem_countableSupClosure_iff

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A b
⊢ b ≤ a
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case refine_1
ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hUnion : ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : #↑S < c
hSp : S ⊆ {s | sᶜ ∈ l}
t : Set α
ht : t ∈ S
⊢ tᶜ ∈ l

Tactic:
apply hSp ht

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mpr.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
S✝ : Set (Set α)
Sct : #↑S✝ < c
a✝ : ∀ s ∈ S✝, CardinalGenerateSets g s
ih : ∀ s ∈ S✝, s ∈ f
⊢ ⋂₀ S✝ ∈ f

Tactic:
exact (cardinal_sInter_mem Sct).mpr ih

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid (x ⊓ y) (x ⊔ y)
⊢ x ⊓ y ≈ y

Tactic:
simpa using c.inf h (c.refl y)

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid x y
⊢ x ⊓ y ≈ ?m.27 h

Tactic:
simpa using c.inf h (c.refl y)

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ AntivaryOn f g s ↔ ∃ x, MonotoneOn f s ∧ AntitoneOn g s

Tactic:
← monovaryOn_toDual_right,

Goal state after:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ ∃ x, MonotoneOn f s ∧ AntitoneOn g s
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
s : Set (Nucleus X)
x y : X
⊢ ⨅ f ∈ s, f (x ⊓ y) = (⨅ f ∈ s, f x) ⊓ ⨅ f ∈ s, f y

Tactic:
simp only [InfHomClass.map_inf, le_antisymm_iff, le_inf_iff, le_iInf_iff]
      refine ⟨⟨?_, ?_⟩, ?_⟩ <;> rintro f hf
      · exact iInf₂_le_of_le f hf inf_le_left
      · exact iInf₂_le_of_le f hf inf_le_right
      · exact ⟨inf_le_of_left_le <| iInf₂_le f hf, inf_le_of_right_le <| iInf₂_le f hf⟩

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
⊢ (∀ i ≥ y, l ⊓ m i ≤ n i) → l ≤ m k → l ≤ n k

Tactic:
hly

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
⊢ l ≤ m k → l ≤ n k
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x1 x2 ↦ x1 ≥ x2) (↑I)ᶜ

Tactic:
intro x hx y hy

Goal state after:
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
x : P
hx : x ∈ (↑I)ᶜ
y : P
hy : y ∈ (↑I)ᶜ
⊢ ∃ z ∈ (↑I)ᶜ, (fun x1 x2 ↦ x1 ≥ x2) x z ∧ (fun x1 x2 ↦ x1 ≥ x2) y z
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: 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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ f x b

Tactic:
← h'

Goal state after:
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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : IsAtom (findAtom r)
nh : r = ⊥
⊢ False

Tactic:
by simp only [nh, findAtom_bot] at h; exact h.1 rfl

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : t₁ ≠ t₂
⊢ Disjoint v₁ v₂

Tactic:
SubRootedTree.mem_iff

Goal state after:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : t₁ ≠ t₂
⊢ Disjoint v₁ v₂