mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
this : ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range f = 0
⊢ f = 0

Tactic:
simpa [ModularForm.norm_eq_zero_iff]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
this : ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range f = 0
⊢ f = 0

Tactic:
by simpa [ModularForm.norm_eq_zero_iff]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ ∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (∏ x_1, ENNReal.ofReal (x ↑x_1)) *
          (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        volume (Set.univ.pi fun x ↦ Set.Ioo (-π) π) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
volume_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (∏ x_1, ENNReal.ofReal (x ↑x_1)) *
          (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        (Measure.pi fun x ↦ volume) (Set.univ.pi fun x ↦ Set.Ioo (-π) π) ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
⊢ regOfFamily u = |(of fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))).det|

Tactic:
· rw [regOfFamily_eq_zero hu, det_eq_zero_of_not_linearIndependent_rows, abs_zero]
    rwa [IsMaxRank, ← linearIndependent_equiv (equivFinRank K).symm] at hu

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
⊢ u • x ∈ fundamentalCone K ↔ u ∈ torsion K

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩
  rw [← logEmbedding_eq_zero_iff]
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
  · rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
    exact ⟨u, trivial, rfl⟩
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]
    exact h.1
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
    exact hx.1

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
⊢ v.inertiaDeg w = Module.finrank v.Completion w.Completion

Tactic:
by
  rw [inertiaDeg_of_liesOver, Ideal.inertiaDeg_eq_of_isMaximal ⊥]
  exact Algebra.finrank_eq_of_equiv_equiv (RingEquiv.quotientBot v.Completion)
    (RingEquiv.quotientBot w.Completion) (by ext; simp [RingHom.algebraMap_toAlgebra])

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
hgs : ∑ i ∈ range n, ζ ^ i = 0
⊢ ↑n = ∑ i ∈ range n, (1 - ζ ^ i)

Tactic:
rw [Finset.sum_sub_distrib, hgs, sub_zero, Finset.sum_const, card_range, nsmul_eq_mul, mul_one]

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
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * ↑n)) = (↑n)⁻¹

Tactic:
volume_pi,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ (∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * ↑n)) ∂Measure.pi fun x ↦ volume) = (↑n)⁻¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsBounded (normLeOne K)

Tactic:
classical
  rw [normLeOne_eq_preimage]
  suffices IsBounded (expMapBasis '' paramSet K) by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w
  refine IsBounded.subset ?_ (Set.image_mono subset_closure)
  exact (isCompact_compactSet K).isBounded.subset (expMapBasis_closure_subset_compactSet K)

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 ζ
⊢ P.inertiaDeg ℤ = orderOf ↑p

Tactic:
have h₂ := (primesOverSpanEquivMonicFactorsMod h₁ ⟨P, ⟨inferInstance, inferInstance⟩⟩).2

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₂ : ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∈ monicFactorsMod ζ p
⊢ P.inertiaDeg ℤ = orderOf ↑p
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
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
⊢ P.ramificationIdx ℤ = 1

Tactic:
have h₂ := (primesOverSpanEquivMonicFactorsMod h₁ ⟨P, ⟨inferInstance, inferInstance⟩⟩).2

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 ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ : ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∈ monicFactorsMod ζ p
⊢ P.ramificationIdx ℤ = 1
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
⊢ Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C } =
    Nat.card { I // J ∣ I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }

Tactic:
refine Nat.card_congr ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
⊢ { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C } ≃
    { I // J ∣ I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s * ↑(absNorm ↑J) }
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
k' : α
hs : ∀ (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a k' l.1 * (newBasis K) l.2)) b) = 0 (k', b)
l : β
b : K →+* ℂ
⊢ (newBasis K).repr (a k' l * (newBasis K) b) = 0

Tactic:
ext b'
    specialize hs b'
    rw [funext_iff] at hs
    simp only [Prod.forall] at hs
    apply hs

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

Goal state before:
pp: case e_f.e_f
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 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r✝ : K →+* ℂ
r : β
⊢ ∑ x_1, ↑(a' K a k r r✝ x_1) * ↑(x (r, r✝)) * (newBasis K) x_1 =
    ↑(x (r, r✝)) * ∑ u, ↑(a' K a k r r✝ u) * (newBasis K) u

Tactic:
mul_sum

Goal state after:
case e_f.e_f
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 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r✝ : K →+* ℂ
r : β
⊢ ∑ x_1, ↑(a' K a k r r✝ x_1) * ↑(x (r, r✝)) * (newBasis K) x_1 =
    ∑ i, ↑(x (r, r✝)) * (↑(a' K a k r r✝ i) * (newBasis K) i)
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case e_f
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 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l : β
⊢ ∑ x_1, ↑(x (l, x_1)) * ∑ u, ↑(a' K a k l x_1 u) * (newBasis K) u =
    (fun j ↦ a k j) l * ∑ r, ↑(x (l, r)) * (newBasis K) r

Tactic:
mul_sum

Goal state after:
case e_f
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 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l : β
⊢ ∑ x_1, ↑(x (l, x_1)) * ∑ u, ↑(a' K a k l x_1 u) * (newBasis K) u =
    ∑ i, (fun j ↦ a k j) l * (↑(x (l, i)) * (newBasis K) i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion

Goal state before:
pp: G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
⊢ C ∈ 𝓝 (toCompl 0)

Tactic:
rwa [map_zero]

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : AddCommMonoid M
inst✝¹ : SeminormedAddCommGroup G
inst✝ : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖((-1) ^ (n - i) * ↑(n.choose i)) • f (m + i • h)‖ ≤ ‖f‖

Tactic:
exact (norm_zsmul_le _ _).trans (f.norm_coe_le_norm _)

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

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (Rat.padicValuation p) (x' - y') < exp (-↑n)
⊢ padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y)) ≤ (↑(p ^ n))⁻¹

Tactic:
rw [map_sub, ← hx, ← hy]

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (Rat.padicValuation p) (x' - y') < exp (-↑n)
⊢ padicNorm p (x' - y') ≤ (↑(p ^ n))⁻¹
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
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ Tendsto (fun n ↦ mahlerTerm (a n) n) cofinite (𝓝 0)

Tactic:
tendsto_zero_iff_norm_tendsto_zero

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto (fun x ↦ ‖a x‖) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ ‖mahlerTerm (a x) x‖) cofinite (𝓝 0)
Module: Mathlib.NumberTheory.Padics.WithVal

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

Tactic:
by
    induction y using isClosed_property (Padic.denseRange_ratCast p)
    · refine isClosed_eq ?_ continuous_id
      refine continuous_extension.comp ?_
      exact (uniformContinuous_uniformly_extend Padic.isUniformInducing_cast_withVal
        Padic.isDenseInducing_cast_withVal.dense (uniformContinuous_coe _)).continuous
    · 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: case e'_4
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
⊢ ∑ x_1, { toFun := (↑(U x_1)).indicator fun x ↦ 1, continuous_toFun := ⋯ } x • (v x_1) y =
    ∑ i, ((↑(U i)).indicator (fun x ↦ v i) x) y

Tactic:
congr 1 with i

Goal state after:
case e'_4.e_f
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
i : Fin n
⊢ { toFun := (↑(U i)).indicator fun x ↦ 1, continuous_toFun := ⋯ } x • (v i) y = ((↑(U i)).indicator (fun x ↦ v i) x) y
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
inst✝² : IsGalois K L
inst✝¹ : Algebra K E
inst✝ : IsScalarTower K E L
hp : p ≠ ⊥
⊢ Module.finrank K E = (p.primesOver B).ncard * p.inertiaDegIn B

Tactic:
by
  have : p.IsMaximal := over_def P p ▸ Ideal.IsMaximal.under A P
  have : FiniteDimensional E L := FiniteDimensional.right K E L
  refine mul_left_injective₀ (b := Module.finrank E L) Module.finrank_pos.ne' ?_
  dsimp only
  rw [Module.finrank_mul_finrank, rank_left A K L P E hp, mul_assoc, mul_comm (p.inertiaDegIn B),
    ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn p B Gal(L/K),
    IsGaloisGroup.card_eq_finrank Gal(L/K) K L]

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

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
⊢ Tendsto
    (fun n ↦
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ *
        (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n))
    atTop (𝓝 (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * 0))

Tactic:
apply Tendsto.mul

Goal state after:
case hf
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
⊢ Tendsto (fun x ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖) atTop
    (𝓝 ‖(Polynomial.aeval a) (Polynomial.derivative F)‖)

case hg
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
⊢ Tendsto (fun x ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ x) atTop (𝓝 0)
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
⊢ False

Tactic:
have h₃ := add_lt_add_of_lt_of_le h₁₁ h₂₁

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 / r + ↑j / s
⊢ False
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ siftedSum ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d

Tactic:
siftedSum_eq_sum_support_mul_ite

Goal state after:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0) ≤
    ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: 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
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π) + (algebraMap K[X] K⟮X⟯) (π * (q / π))) = 1

Tactic:
suffices v (algebraMap K[X] (RatFunc K) (q % π)) = 1 ∧
      v (algebraMap K[X] (RatFunc K) (π * (q / π))) < 1 by
    obtain ⟨h₁, h₂⟩ := this
    rw [← h₁] at h₂ ⊢
    exact Valuation.map_add_eq_of_lt_left _ h₂

Goal state after:
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
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1 ∧ v ((algebraMap K[X] K⟮X⟯) (π * (q / π))) < 1
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inr.f
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
inst✝ : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer ↑pi
⊢ v ((algebraMap K[X] K⟮X⟯) p) / v ((algebraMap K[X] K⟮X⟯) q) ≤ 1 ↔
    (exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors))⁻¹ *
        exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {q})).factors) ≤
      1

Tactic:
valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hp0,

Goal state after:
case inr.f
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
inst✝ : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer ↑pi
⊢ v (↑πᵥ ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors) / v ((algebraMap K[X] K⟮X⟯) q) ≤
      1 ↔
    (exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors))⁻¹ *
        exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {q})).factors) ≤
      1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ ∑ a ∈ s.prodPrimes.divisors with a ∣ d, selbergTerms (d / a) =
    selbergTerms d * ∑ a ∈ s.prodPrimes.divisors with a ∣ d, (selbergTerms a)⁻¹

Tactic:
mul_sum

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ ∑ a ∈ s.prodPrimes.divisors with a ∣ d, selbergTerms (d / a) =
    ∑ i ∈ s.prodPrimes.divisors with i ∣ d, selbergTerms d * (selbergTerms i)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * ∑ a ∈ s.prodPrimes.divisors with a ∣ d1.gcd d2, (selbergTerms a)⁻¹ =
    ∑ a ∈ s.prodPrimes.divisors with a ∣ d1.gcd d2, (selbergTerms a)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2)

Tactic:
mul_sum

Goal state after:
case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ ∑ i ∈ s.prodPrimes.divisors with i ∣ d1.gcd d2, s.nu d1 * w d1 * s.nu d2 * w d2 * (selbergTerms i)⁻¹ =
    ∑ a ∈ s.prodPrimes.divisors with a ∣ d1.gcd d2, (selbergTerms a)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2)
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
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 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ { re := ↑k, im := 1 } * { re := ↑k, im := -1 } = ↑p * ↑y

Tactic:
by rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h₂
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (f p)‖ ≤ |c| ^ p

Tactic:
· rw [← abs_pow]
    exact (hc p x hx).trans (le_abs_self _)

Goal state after: