mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite] {f | ∀ (i : ι), ↑f i ∈ A i}

Tactic:
simp_rw +instances [topologicalSpace_eq_iSup cofinite, isOpen_iSup_iff, isOpen_coinduced]
  exact fun S hS ↦ isOpen_forall_mem_of_principal hAopen hS

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) (c • 1)) - Real.log (mixedEmbedding.norm (c • 1)) * (↑(finrank ℚ K))⁻¹) =
    0 x✝

Tactic:
normAtPlace_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult * (Real.log (|c| * (normAtPlace ↑x✝) 1) - Real.log (mixedEmbedding.norm (c • 1)) * (↑(finrank ℚ K))⁻¹) =
    0 x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f
          (fun w ↦ ((homeoRealMixedSpacePolarSpace K) x).1 ↑w,
            Pi.map (fun i ↦ ↑Complex.polarCoord.symm) fun w ↦
              (((homeoRealMixedSpacePolarSpace K) x).1 ↑w, ((homeoRealMixedSpacePolarSpace K) x).2 w)) ∂volume =
    ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, (x.2 w).1) • f (x.1, Pi.map (fun i ↦ ↑Complex.polarCoord.symm) x.2)

Tactic:
homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f
          (fun w ↦ x.1 w,
            Pi.map (fun i ↦ ↑Complex.polarCoord.symm) fun w ↦
              (((homeoRealMixedSpacePolarSpace K) x).1 ↑w, ((homeoRealMixedSpacePolarSpace K) x).2 w)) ∂volume =
    ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, (x.2 w).1) • f (x.1, Pi.map (fun i ↦ ↑Complex.polarCoord.symm) x.2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f
          (fun w ↦ ((homeoRealMixedSpacePolarSpace K) a).1 ↑w,
            Pi.map (fun i ↦ ↑Complex.polarCoord.symm) fun w ↦
              (((homeoRealMixedSpacePolarSpace K) a).1 ↑w, ((homeoRealMixedSpacePolarSpace K) a).2 w)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (x.1, Pi.map (fun i ↦ ↑Complex.polarCoord.symm) x.2)

Tactic:
homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f
          (fun w ↦ a.1 w,
            Pi.map (fun i ↦ ↑Complex.polarCoord.symm) fun w ↦
              (((homeoRealMixedSpacePolarSpace K) a).1 ↑w, ((homeoRealMixedSpacePolarSpace K) a).2 w)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (x.1, Pi.map (fun i ↦ ↑Complex.polarCoord.symm) x.2)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (unitsComplexConj K) u = u ↔ u ∈ realUnits K

Tactic:
by
  simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) K]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ normAtAllPlaces x ∈ normAtAllPlaces '' A

Tactic:
← normAtAllPlaces_eq_of_normAtComplexPlaces_eq ha₂

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A
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
⊢ Subgroup.map (unitsMulComplexConjInv K) (torsion K) = (powMonoidHom 2).range

Tactic:
rw [← MonoidHom.domRestrict_range]
  exact congr_arg (MonoidHom.range ·) (MonoidHom.ext fun ζ ↦ by simp)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

Tactic:
by
  simp_rw [fundamentalCone, Set.mem_sdiff, Set.mem_preimage, logMap_normAtAllPlaces,
    Set.mem_ofPred_eq, norm_normAtAllPlaces]

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

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ ↑p ∈ span {hζ.toInteger - 1}

Tactic:
convert! absNorm_mem _
  exact (absNorm_span_zeta_sub_one ..).symm

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
⊢ δ ≤ 1

Tactic:
refine le_of_tendsto h (Eventually.of_forall fun s ↦ ?_)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
s : ℝ
⊢ primeIdealZetaSum S s / primeIdealZetaSum univ s ≤ 1
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j ≤ ↑B

Tactic:
apply hv.2

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ False

Tactic:
apply hA

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ A = 0
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
hs : 0 ≤ s
this : Fintype { I // ↑(absNorm ↑I) ≤ s }
e : (C : ClassGroup (𝓞 K)) → { x // ClassGroup.mk0 ↑x = C } ≃ { x // ↑(absNorm ↑x) ≤ s ∧ ClassGroup.mk0 x = C } :=
  fun C ↦ Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ ↑(absNorm ↑I) ≤ s) fun I ↦ ClassGroup.mk0 I = C
⊢ ∑ x, ↑(Fintype.card { x_1 // ClassGroup.mk0 ↑x_1 = x }) / s = ↑(Fintype.card { I // ↑(absNorm ↑I) ≤ s }) / s

Tactic:
Fintype.subtype_card

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
hs : 0 ≤ s
this : Fintype { I // ↑(absNorm ↑I) ≤ s }
e : (C : ClassGroup (𝓞 K)) → { x // ClassGroup.mk0 ↑x = C } ≃ { x // ↑(absNorm ↑x) ≤ s ∧ ClassGroup.mk0 x = C } :=
  fun C ↦ Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ ↑(absNorm ↑I) ≤ s) fun I ↦ ClassGroup.mk0 I = C
⊢ ∑ x, ↑{x_1 | ClassGroup.mk0 ↑x_1 = x}.card / s = ↑(Fintype.card { I // ↑(absNorm ↑I) ≤ s }) / s
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case hd
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
⊢ Real.log (max (f ↑p) (f ↑m)) < 0

Tactic:
exact log_neg (lt_sup_iff.mpr <| .inl hp0) (sup_lt_iff.mpr ⟨hp1, hm⟩)

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
n₀ : ℕ
hn₀ : 1 < n₀
⊢ 1 < f ↑n₀

Tactic:
contrapose! notbdd with h

Goal state after:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
⊢ ∀ (n : ℕ), f ↑n ≤ 1
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ‖↑(Polynomial.eval x (ascPochhammer ℤ_[p] k))‖ / ‖↑k.factorial‖ ≤ 1

Tactic:
div_le_one (by simpa using k.factorial_ne_zero)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ‖↑(Polynomial.eval x (ascPochhammer ℤ_[p] k))‖ ≤ ‖↑k.factorial‖
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁ - 1) = 1
⊢ a₁ ^ n₂ = a₁

Tactic:
rcases Int.isUnit_iff.mp
          (.of_mul_eq_one _ <|
            sub_eq_zero.mp <| (ha₁.zpow_eq_one_iff (n₂ * n₁ - 1)).mp hn₁) with
        (rfl | rfl)

Goal state after:
case inl.inl.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (a₁ ^ 1).x
Hy : 0 < (a₁ ^ 1).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ 1) ^ n ∨ a = -(a₁ ^ 1) ^ n
hn₁ : a₁ ^ (1 * n₁ - 1) = 1
⊢ a₁ ^ 1 = a₁

case inl.inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (a₁ ^ (-1)).x
Hy : 0 < (a₁ ^ (-1)).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ (-1)) ^ n ∨ a = -(a₁ ^ (-1)) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ a₁ ^ (-1) = a₁
Module: Mathlib.NumberTheory.Pell

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

Tactic:
have hd := d_nonsquare_of_one_lt_x h.1

Goal state after:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
⊢ IsFundamental a
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✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
⊢ 𝓟D.ramificationIdxIn B = p.ramificationIdxIn B ∧ 𝓟D.inertiaDegIn B = p.inertiaDegIn B

Tactic:
obtain ⟨_, _, _, _, _, h𝓟⟩ := instances A K L P D 𝓞D 𝓟D hp
  refine eq_and_eq_of_pos_of_le_of_mul_le_mul ?_ ?_ ?_ ?_ ?_
  · exact Nat.pos_of_ne_zero <| ramificationIdxIn_ne_zero (stabilizer Gal(L/K) P)
  · exact Nat.pos_of_ne_zero <| inertiaDegIn_ne_zero (stabilizer Gal(L/K) P)
  · rw [ramificationIdxIn_eq_ramificationIdx p P Gal(L/K),
      ramificationIdxIn_eq_ramificationIdx _ P (stabilizer Gal(L/K) P)]
    exact 𝓟D.ramificationIdx_above_le P
  · rw [inertiaDegIn_eq_inertiaDeg p P Gal(L/K),
      inertiaDegIn_eq_inertiaDeg _ P (stabilizer Gal(L/K) P)]
    exact inertiaDeg_above_le 𝓟D P
  · have := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 𝓟D B (stabilizer Gal(L/K) P)
    rw [primesOver_eq_singleton K L P D 𝓞D, Set.ncard_singleton, one_mul] at this
    rw [this, IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L,
      IsDecompositionField.rank_left A K L P D hp]

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case refine_1
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
⊢ ¬IsUnit πᵥ

Tactic:
simp only [Polynomial.isUnit_iff, isUnit_iff_ne_zero]

Goal state after:
case refine_1
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
⊢ ¬∃ r, r ≠ 0 ∧ Polynomial.C r = πᵥ
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case e_f.e_s
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
n : ℕ
⊢ (s.prodPrimes.gcd n).divisors = {a ∈ s.prodPrimes.divisors | a ∣ n}

Tactic:
rw [← divisors_filter_dvd_of_dvd prodPrimes_ne_zero (Nat.gcd_dvd_left _ _)]

Goal state after:
case e_f.e_s
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
n : ℕ
⊢ {d ∈ s.prodPrimes.divisors | d ∣ s.prodPrimes.gcd n} = {a ∈ s.prodPrimes.divisors | a ∣ n}
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]
⊢ ↑(f 0) ^ 2 + ↑(f 1) ^ 2 + ↑(f 2) ^ 2 + ↑(f 3) ^ 2 = 0

Tactic:
← @zero_mul (ZMod 2) _ m,

Goal state after:
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]
⊢ ↑(f 0) ^ 2 + ↑(f 1) ^ 2 + ↑(f 2) ^ 2 + ↑(f 3) ^ 2 = 0 * ↑m
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
P : Ideal S
i : ℕ
⊢ Function.Injective ⇑(p.powQuotSuccInclusion P i)

Tactic:
by
  rintro ⟨_, _⟩ ⟨_, _⟩ h
  rwa [Subtype.ext_iff] at h ⊢

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

Goal state before:
pp: case refine_1
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
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ Q j

Tactic:
dsimp only [Q]
    rw [rank_pow_quot_aux p P _ lt_e, ih, ← succ_nsmul', Nat.sub_succ, ← Nat.succ_eq_add_one,
      Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt lt_e)]
    assumption

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

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑m / ↑n + ↑r ∧ |x - ↑m / ↑n| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p

Tactic:
refine ⟨by simpa, hlt.trans_le (le_of_eq ?_)⟩

Goal state after:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ C / ↑n ^ p = ↑r.den ^ p * C / ↑(r.den • id n) ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
n : ℕ
⊢ LiouvilleWith p (x + ↑n) ↔ LiouvilleWith p x

Tactic:
by
  rw [← Rat.cast_natCast n, add_rat_iff]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedGroup A
n : ℕ
δ : ℝ
a : A
⊢ a ∈ approxOrderOf A n δ ↔ ∃ b, orderOf b = n ∧ a ∈ ball b δ

Tactic:
simp only [approxOrderOf, thickening_eq_biUnion_ball, mem_iUnion₂, mem_ofPred_eq, exists_prop]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case mpr
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ) → ∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ

Tactic:
· rintro ⟨m, hm₁, hm₂, hx⟩; exact ⟨↑((m : ℝ) / n), ⟨m, hm₁, hm₂, rfl⟩, hx⟩

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:
by
  rw [coe_sSup, ← Set.image, sSup_image]

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
⊢ SupClosed (countableInfClosure s)

Tactic:
rintro a ha b hb

Goal state after:
α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
a : α
ha : a ∈ countableInfClosure s
b : α
hb : b ∈ countableInfClosure s
⊢ a ⊔ b ∈ countableInfClosure s
Module: Mathlib.Order.Height

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : ↑n ≤ s.chainHeight r
h' : ¬n = 0
⊢ ∃ t ⊆ s, t.encard = ↑n ∧ IsChain r t

Tactic:
· obtain ⟨t, ht₁, ht₂, ht₃⟩ : ∃ t ⊆ s, IsChain r t ∧ n ≤ t.encard := by
      contrapose! h
      refine iSup_lt_iff.mpr ⟨n - 1, ?_, fun m ↦ ENat.le_sub_one_of_lt <| h m.1 m.2.1 m.2.2⟩
      exact_mod_cast Nat.sub_one_lt h'
    obtain ⟨u, hu₁, hu₂⟩ := exists_subset_encard_eq ht₃
    exact ⟨u, hu₁.trans ht₁, hu₂, ht₂.mono hu₁⟩

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)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ

Tactic:
suffices ¬ Pairwise (Disjoint on B) 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:
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)
⊢ ¬Pairwise (Disjoint on B)
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
i j k : ι
⊢ MonovaryOrder f g i j → MonovaryOrder f g j k → MonovaryOrder f g i k

Tactic:
by rw [MonovaryOrder]; exact _root_.trans

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
n : Nucleus X
a b : X
⊢ rangeFactorization (⇑n) (a ⊓ b) = rangeFactorization (⇑n) a ⊓ rangeFactorization (⇑n) b

Tactic:
ext; exact map_inf

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
⊢ ∀ ⦃y : α⦄, y ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} → a ≠ y → Function.onFun Disjoint id a y

Tactic:
a'

Goal state after:
α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
a' : α
⊢ a' ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} → a ≠ a' → Function.onFun Disjoint id a a'
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun a ↦ (f a, g b)) '' d = (f '' d) ×ˢ {g b}
⊢ IsLUB ((fun a ↦ Prod.map f g (a, b)) '' d) ((fun a ↦ Prod.map f g (a, b)) c)

Tactic:
simp_rw [Prod.map_apply, e2]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun a ↦ (f a, g b)) '' d = (f '' d) ×ˢ {g b}
⊢ IsLUB ((f '' d) ×ˢ {g b}) (f c, g b)
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_2.inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h : a ≠ b → P.Rel a b
hne : a ≠ b
⊢ f a = f b

Tactic:
exact hf.apply_eq_apply (h hne)

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ InfClosed ↑S

Tactic:
rintro a ha b hb

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ ↑S
b : X
hb : b ∈ ↑S
⊢ a ⊓ b ∈ ↑S