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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap (mixedSpaceOfRealSpace (↑expMapBasis x))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
expMapBasis_apply'',

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap (mixedSpaceOfRealSpace (Real.exp (x w₀) • ↑expMapBasis fun i ↦ if i = w₀ then 0 else x i))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((Subgroup.toAddSubgroup (Subgroup.closure (Set.range u) ⊔ torsion K)).relIndex
        (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v) ⊔ torsion K))) =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
← Subgroup.relIndex_toAddSubgroup

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((Subgroup.toAddSubgroup (Subgroup.closure (Set.range u) ⊔ torsion K)).relIndex
        (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v) ⊔ torsion K))) =
    ↑((Subgroup.toAddSubgroup (Subgroup.closure (Set.range u) ⊔ torsion K)).relIndex
        (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v) ⊔ torsion K)))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this : Measurable ↑expMapBasis
⊢ Measurable fun x ↦
    ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
      f (↑expMapBasis x)

Tactic:
fun_prop

Goal state after:
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
σ : Gal(K/ℚ)
x : K
hx : x ^ n = 1
⊢ σ x = x ^ (↑((galEquivZMod n K) σ)).val

Tactic:
obtain ⟨a, -, rfl⟩ := (zeta_spec n ℚ K).eq_pow_of_pow_eq_one hx
  rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ Measurable fun x ↦ ENNReal.ofReal (Real.exp (x w₀ * ↑n))

Tactic:
fun_prop

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
hx : x ∈ compactSet K
w : InfinitePlace K
⊢ 0 ≤ x w

Tactic:
obtain ⟨c, hc, ⟨_, ⟨⟨a, ha, rfl⟩, _, rfl⟩⟩⟩ := hx
  exact mul_nonneg hc.1 (expMapBasis_pos _ _).le

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
⊢ (↑expMapBasis fun w ↦ if w = w₀ then Real.log c else y w) = (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y)

Tactic:
expMapBasis_apply'',

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
⊢ (Real.exp (if w₀ = w₀ then Real.log c else y w₀) •
      ↑expMapBasis fun i ↦ if i = w₀ then 0 else if i = w₀ then Real.log c else y i) =
    (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (normLeOne K) ⊆ normAtAllPlaces ⁻¹' compactSet K

Tactic:
rw [normLeOne_eq_preimage]
  refine ((continuous_normAtAllPlaces K).closure_preimage_subset _).trans (Set.preimage_mono ?_)
  refine (isCompact_compactSet K).isClosed.closure_subset_iff.mpr ?_
  exact (Set.image_mono subset_closure).trans (expMapBasis_closure_subset_compactSet _)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable fun x ↦ ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
fun_prop

Goal state after:
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.Coprime m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ : P.inertiaDeg ℤ = (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).natDegree
this : P.IsMaximal
⊢ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ) ∣ cyclotomic m (ZMod p)

Tactic:
rw [← map_cyclotomic_int, cyclotomic_eq_minpoly (zeta_spec m ℚ K) (NeZero.pos _),
      ← (zeta_spec m ℚ K).coe_toInteger, ← RingOfIntegers.minpoly_coe ζ]

Goal state after:
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.Coprime m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ : P.inertiaDeg ℤ = (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).natDegree
this : P.IsMaximal
⊢ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ↑ζ) ∣
    Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ↑⋯.toInteger)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K)
h₂ : MeasurableSet (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
⊢ Measurable fun x ↦ ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:

Tactic:
f m ≤ (L.mapIdx fun i _ ↦ n₀ * f n₀ ^ i).sum := apply_le_sum_digits m hn₀
    _ ≤ (L.mapIdx fun _ _ ↦ (n₀ : ℝ)).sum := by
      simp only [List.mapIdx_eq_zipIdx_map]
      refine List.sum_le_sum fun ⟨i, a⟩ _ ↦ ?_
      exact mul_le_of_le_one_right (by positivity) (pow_le_one₀ (by positivity) h)
    _ = n₀ * (Nat.log n₀ m + 1) := by
      rw [List.mapIdx_eq_zipIdx_map, List.eq_replicate_of_mem (a := (n₀ : ℝ)) (l := L.zipIdx.map _),
        List.sum_replicate, List.length_map, List.length_zipIdx, nsmul_eq_mul, mul_comm,
        Nat.length_digits n₀ m hn₀ (ne_zero_of_lt hm), Nat.cast_add_one]
      simp +contextual
    _ ≤ n₀ * (logb n₀ m + 1) := by
      gcongr
      exact natLog_le_logb ..

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
⊢ ∀ (x : X), dist (f x) (h x) ≤ max (dist f g) (dist g h)

Tactic:
refine fun x ↦ (dist_triangle_max (f x) (g x) (h x)).trans (max_le_max ?_ ?_)

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist (f x) (g x) ≤ dist f g

case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist (g x) (h x) ≤ dist g h
Module: Mathlib.NumberTheory.Padics.AddChar

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑κ
hκ' : κ 1 = 1 + r
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑(addChar_of_value_at_one r hr)

Tactic:
fun_prop

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Valued.v ((algebraMap (PadicAlgCl p) ℂ_[p]) ↑p) = 1 / ↑p

Tactic:
← coe_eq,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Valued.v ↑↑p = 1 / ↑p
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x ↦ ⟨↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) / ↑k.factorial, ⋯⟩

Tactic:
fun_prop

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x ↦ Ring.multichoose (x - ↑k + 1) k

Tactic:
fun_prop

Goal state after:
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 ^ t).choose (i + 1))‖₊ ≤ ↑(↑p ^ (-1))

Tactic:
coe_nnnorm,

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 ^ t).choose (i + 1))‖ ≤ ↑(↑p ^ (-1))
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
⊢ ((prodMk' μ) ν) (f.comp fst * g.comp snd) = μ f * ν g

Tactic:
simp only [prodMk'_apply, mul_comm (μ f) (ν g), ← smul_eq_mul, ← map_smul]

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
⊢ μ ((contractSnd ν) (f.comp fst • g.comp snd)) = μ (ν g • f)
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝⁵ : CompactSpace X
inst✝⁴ : CompactSpace Y
inst✝³ : T2Space X
inst✝² : T2Space Y
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T0Space R
⊢ Continuous ⇑((prodMk μ) ν)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝⁵ : CompactSpace X
inst✝⁴ : CompactSpace Y
inst✝³ : T2Space X
inst✝² : T2Space Y
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T0Space R
⊢ Continuous ⇑((prodMk' μ) ν)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
⊢ False

Tactic:
have H := x_zpow_pos h.x_pos n

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : 0 < (a ^ n).x
⊢ False
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: case inr
A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : x ≠ 0
⊢ (exp (v.asIdeal.ramificationIdx' w.asIdeal • ↑(multiplicity v.asIdeal (Ideal.span {x}))))⁻¹ =
    (exp ↑(multiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x}))))⁻¹

Tactic:
Int.nsmul_eq_mul,

Goal state after:
case inr
A : Type u_1
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
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
x : A
hx : x ≠ 0
⊢ (exp (↑(v.asIdeal.ramificationIdx' w.asIdeal) * ↑(multiplicity v.asIdeal (Ideal.span {x}))))⁻¹ =
    (exp ↑(multiplicity w.asIdeal (Ideal.map (algebraMap A B) (Ideal.span {x}))))⁻¹
Module: Mathlib.NumberTheory.SumFourSquares

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

Tactic:
Int.mul_ediv_cancel' _,

Goal state after:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ (x - y) ^ 2 + (x + y) ^ 2 = (x - y) ^ 2 + (2 * ((x + y) / 2)) ^ 2

m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 ∣ x - y
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
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m

Tactic:
set f : Fin 4 → ℤ := ![a, b, c, d]

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]
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
Module: Mathlib.NumberTheory.SelbergSieve

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

Tactic:
intro d1 hd1

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

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

Tactic:
abs_norm (by simp)

Goal state after:
x : ℤ[i]
⊢ norm x = |x.re| * |x.re| + |x.im| * |x.im|
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
⊢ ¬(norm ↑p).natAbs = 1

Tactic:
rw [norm_natCast, Int.natAbs_mul, mul_eq_one]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
⊢ ¬((↑p).natAbs = 1 ∧ (↑p).natAbs = 1)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: p : ℂ[X]
s : ℂ
⊢ ContinuousOn (fun x ↦ s * (cexp (-(x • s)) * eval (x • s) p)) (Set.uIcc 0 1)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

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

Tactic:
obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩, ⟨c, rfl⟩, ⟨d, rfl⟩⟩ : m ∣ a ∧ m ∣ b ∧ m ∣ c ∧ m ∣ d := by
        simp only [← ZMod.natCast_eq_zero_iff, ← hf_mod, hr, Int.cast_zero, and_self]

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

Goal state before:
pp: f : ℤ[X]
s : ℂ
h :
  (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1 ⊆
    (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Icc 0 1
⊢ Continuous fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖

Tactic:
fun_prop

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

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
⊢ LiouvilleWith p (-x)

Tactic:
by
  rcases h with ⟨C, hC⟩
  refine ⟨C, hC.mono ?_⟩
  rintro n ⟨m, hne, hlt⟩
  refine ⟨-m, by simp [neg_div, hne], ?_⟩
  convert! hlt using 1
  rw [abs_sub_comm]
  congr! 1; push_cast; ring

Goal state after:
Module: Mathlib.Order.Category.OmegaCompletePartialOrder

Goal state before:
pp: X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m✝ : s.pt ⟶ (equalizer f g).pt
hm : m✝ ≫ (equalizer f g).ι = s.ι
⊢ m✝ = { toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, monotone' := ⋯, map_ωSup' := ⋯ }

Tactic:
ext x : 2; apply Subtype.ext ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
      apply ContinuousHom.congr_fun hm

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ orderOf (a * b⁻¹) = n

Tactic:
apply han

Goal state after:
case refine_1
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := ⋯
b : A
hb : b ∈ {b | orderOf b = n}
⊢ orderOf b⁻¹ = n
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case refine_2
ι α β : 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 t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : tᶜ ⊆ sᶜ
⊢ tᶜ ∈ l

Tactic:
exact hmono sᶜ ht tᶜ hsub

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

Goal state before:
pp: case hUnion
α : Type u
c : Cardinal.{u}
hreg✝ hreg : c.IsRegular
⊢ ∀ (S : Set (Set α)), #↑S < c → (∀ s ∈ S, s ∈ {s | #↑s < c}) → ⋃₀ S ∈ {s | #↑s < c}

Tactic:
refine fun s hS hSc ↦ lt_of_le_of_lt (mk_sUnion_le _) <| mul_lt_of_lt hreg.aleph0_le hS ?_
    apply iSup_lt_of_lt_cof_ord _ fun i ↦ hSc i.1 i.2
    rwa [hreg.cof_ord]

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r = 0
⊢ s = ∅

Tactic:
simp only [chainHeight, iSup_eq_zero, encard_eq_zero, Subtype.forall, and_imp] at h

Goal state after:
case refine_1
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ a ⊆ s, IsChain r a → a = ∅
⊢ s = ∅
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b : α
h : ∀ (a : α), IsRegular (a ⊔ aᶜ)
a : α
⊢ a ⊔ aᶜ = ⊤

Tactic:
by rw [← (h a), compl_sup, inf_compl_eq_bot, compl_bot]

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub

Tactic:
hcNe

Goal state after:
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : 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
⊢ ScottContinuous (Prod.map f g)

Tactic:
refine .fromProd (fun a d hd₁ hd₂ c hdc ↦ ?_) (fun b d hd₁ hd₂ c hdc ↦ ?_)

Goal state after:
case refine_1
α : 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
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
⊢ IsLUB ((fun b ↦ Prod.map f g (a, b)) '' d) ((fun b ↦ Prod.map f g (a, b)) c)

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
⊢ IsLUB ((fun a ↦ Prod.map f g (a, b)) '' d) ((fun a ↦ Prod.map f g (a, b)) c)
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x y : α
u t✝ : Set α
P : Partition u
ht : t✝ ∈ P
t : Set α
ht' : t ∈ P
hx : x ∈ t
hy : y ∈ t
h : y ∈ t✝
⊢ x ∈ t✝

Tactic:
rwa [P.eq_of_mem_of_mem ht ht' h hy]

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

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

Tactic:
exact h.1 rfl

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

Goal state before:
pp: t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
hb : ⊥ ∈ ↑t₂
ha : t₁.root = ⊥
⊢ False

Tactic:
exact t₁.root_ne_bot_of_mem_subtrees ht₁ ha

Goal state after: