mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝⁵ : Countable ↥Γ
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕)) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
this : AEStronglyMeasurable (fun x ↦ g ↑x) μ
⊢ Integrable (g ∘ π * f) μ

Tactic:
refine Integrable.essSup_smul f_ℒ_1 this ?_

Goal state after:
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝⁵ : Countable ↥Γ
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕)) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
this : AEStronglyMeasurable (fun x ↦ g ↑x) μ
⊢ essSup (fun x ↦ ‖g ↑x‖ₑ) μ ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
this : AEStronglyMeasurable (fun x ↦ g ↑x) μ'
⊢ Integrable (g ∘ π * f) μ'

Tactic:
refine Integrable.essSup_smul f_ℒ_1 this ?_

Goal state after:
G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
this : AEStronglyMeasurable (fun x ↦ g ↑x) μ'
⊢ essSup (fun x ↦ ‖g ↑x‖ₑ) μ' ≠ ∞
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ), (Ioi b).indicator f x ∂μ) (Ici a₀) a₀

Tactic:
apply tendsto_integral_filter_of_dominated_convergence ((Ioi a₀).indicator (norm ∘ f))

Goal state after:
case hF_meas
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, AEStronglyMeasurable ((Ioi n).indicator f) μ

case h_bound
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Ioi n).indicator f a‖ ≤ (Ioi a₀).indicator (norm ∘ f) a

case bound_integrable
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ Integrable ((Ioi a₀).indicator (norm ∘ f)) μ

case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun n ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: r x : ℝ
c : ℂ
⊢ circleMap c (-r) x = circleMap c r (x + π)

Tactic:
by
  simp [circleMap, add_mul, Complex.exp_add]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
⊢ MemLp (fun x ↦ f x.1) p (μ.prod ν)

Tactic:
have hf' : MemLp f p (ν .univ • μ) := hf.smul_measure (by simp)
  change MemLp (f ∘ Prod.fst) p (μ.prod ν)
  rw [← memLp_map_measure_iff ?_ (by fun_prop)]
  · simpa using hf'
  · simpa using hf'.1

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case e'_1
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔ Integrable (fun z ↦ f z.swap) (ν.prod μ)

Tactic:
funext fun _ => Function.comp_apply.symm,

Goal state after:
case e'_1
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : SFinite ν
inst✝ : SFinite μ
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔ Integrable (fun x ↦ (f ∘ Prod.swap) x) (ν.prod μ)
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)
hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
⊢ ∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
        ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)

Tactic:
have HJ_eq := fun k =>
    integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ (J k) f f' s hs (HcJ k) (HdJ k)
      (HiJ k)

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Box.Icc I)
Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc I) volume
J : ℕ →o Box (Fin (n + 1))
hJ_sub : ∀ (n_1 : ℕ), Box.Icc (J n_1) ⊆ Box.Ioo I
hJl : Tendsto (Box.lower ∘ ⇑J) atTop (𝓝 I.lower)
hJu : Tendsto (Box.upper ∘ ⇑J) atTop (𝓝 I.upper)
hJ_sub' : ∀ (k : ℕ), Box.Icc (J k) ⊆ Box.Icc I
hJ_le : ∀ (k : ℕ), J k ≤ I
HcJ : ∀ (k : ℕ), ContinuousOn f (Box.Icc (J k))
HdJ : ∀ (k : ℕ), ∀ x ∈ Box.Icc (J k) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x
HiJ : ∀ (k : ℕ), IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Box.Icc (J k)) volume
HJ_eq :
  ∀ (k : ℕ),
    ∫ (x : Fin (n + 1) → ℝ) in Box.Icc (J k), ∑ i, (f' x) (e i) i =
      ∑ i,
        ((∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).upper i) x) i) -
          ∫ (x : Fin n → ℝ) in Box.Icc ((J k).face i), f (i.insertNth ((J k).lower i) x) i)
⊢ ∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
        ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I ∩ s
ε : ℝ
ε0 : ε > 0
this : ContinuousWithinAt (fun δ ↦ (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖) (Set.Ioi 0) 0
⊢ (fun δ ↦ (2 * δ) ^ (n + 1) * ‖(f' x) (Pi.single i 1)‖) 0 < ε / 2

Tactic:
simpa using half_pos ε0

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case c0
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := ⋯
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := ⋯
F : Fin (n + 1) →ᵇᵃ[↑I] E := ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ 0 ≤ volume.toBoxAdditive J

pp: case h₂
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := ⋯
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := ⋯
F : Fin (n + 1) →ᵇᵃ[↑I] E := ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ volume.toBoxAdditive J ≤ (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
exacts [by dsimp; positivity, by simp]

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑π * I) • f w

Tactic:
set F : ℂ → E := dslope f w

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑π * I) • f w
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: case e_t
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (fun t ↦ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) = fun t ↦ {∑ i ∈ t, Finsupp.single i 1}

Tactic:
funext

Goal state after:
case e_t
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
x✝ : Finset σ
⊢ (Finsupp.single (∑ i ∈ x✝, Finsupp.single i 1) 1).support = {∑ i ∈ x✝, Finsupp.single i 1}
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (esymm σ R n).support = (powersetCard n univ).biUnion fun t ↦ {∑ i ∈ t, Finsupp.single i 1}

Tactic:
by
  rw [support_esymm'']
  congr
  funext
  exact Finsupp.support_single _ one_ne_zero

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val

Tactic:
funext

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
x✝ : Finset σ
⊢ (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) x✝ = x✝.val
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < p.degree
hf : f p.leadingCoeff ≠ 0
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop

Tactic:
revert hf; refine degree_pos_induction_on p hd ?_ ?_ ?_ <;> clear hd p
  · rintro _ - hc
    rw [leadingCoeff_mul_X, leadingCoeff_C] at hc
    simpa [abv_mul abv] using hz.const_mul_atTop ((abv_pos abv).2 hc)
  · intro _ _ ihp hf
    rw [leadingCoeff_mul_X] at hf
    simpa [abv_mul abv] using (ihp hf).atTop_mul_atTop₀ hz
  · intro _ a hd ihp hf
    rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf
    refine .atTop_of_add_const (abv (-f a)) ?_
    refine tendsto_atTop_mono (fun _ => abv_add abv _ _) ?_
    simpa using ihp hf

Goal state after:
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ 1 ^ ((map f p).natDegree - i) * ‖(map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)

Tactic:
one_pow,

Goal state after:
case inr.inr
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ (map f p).natDegree
⊢ 1 * ‖(map f p).roots.esymm ((map f p).natDegree - i)‖ ≤
    B ^ ((map f p).natDegree - i) * ↑((map f p).natDegree.choose i)
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case h
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
n : ℕ
hn : x ≤ n • 1
num : ℤ
den : ℕ
den_nz✝ : den ≠ 0
reduced✝ : num.natAbs.Coprime den
⊢ { num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ } ∈ {r | r.num • 1 < r.den • x} →
    { num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ } ≤ ↑n

Tactic:
Rat.le_iff

Goal state after:
case h
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : M
n : ℕ
hn : x ≤ n • 1
num : ℤ
den : ℕ
den_nz✝ : den ≠ 0
reduced✝ : num.natAbs.Coprime den
⊢ { num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ } ∈ {r | r.num • 1 < r.den • x} →
    { num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ }.num * ↑(↑n).den ≤
      (↑n).num * ↑{ num := num, den := den, den_nz := den_nz✝, reduced := reduced✝ }.den
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mp
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a

Tactic:
obtain ⟨k, hk⟩ := Archimedean.arch (1 + 1) <| sub_pos.mpr h

Goal state after:
case mp
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mpr
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
⊢ (∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a) → a ∈ ratLt (x + y)

Tactic:
intro ⟨u, hu, v, hv, huv⟩
    rw [← huv]
    rw [Set.mem_ofPred_eq] at hu hv ⊢
    exact num_smul_one_lt_den_smul_add hu hv

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case refine_2
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ofClass v.restrict).ValueGroup₀ˣ
h : (hom v.restrict) ↑x < γ
k : K
hk : (restrict₀ (ofClass v.restrict)) k = ↑x
⊢ (hom v) (v.restrict k) < γ

Tactic:
convert! h
    simp only [restrict_RankOne_hom_eq, coe_comp, Function.comp_apply, ← hk]
    congr 1
    exact (embedding_restrict₀ k).symm

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.RankOne

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
R : Type u_2
inst✝ : Ring R
v : Valuation R Γ
hv : v.IsRankOneDiscrete
k : ℤ
⊢ (valueGroup₀_equiv_withZeroMulInt v) (↑(generator' v) ^ k) = exp (-k)

Tactic:
simp [WithZero.exp, ← mulintEquivOfZPowersEqTop_symm_apply_zpow
    (Subgroup.zpowers_inv (g := hv.generator') ▸ hv.generator'_zpowers_eq_top)]

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ embedRealFun 0 = 0

Tactic:
apply le_antisymm
  · apply csSup_le (ratLt'_nonempty 0)
    intro x
    unfold ratLt' ratLt
    suffices ∀ (y : ℚ), y.num • (1 : M) < 0 → y = x → x ≤ 0 by simpa using this
    intro y hy hyx
    rw [← hyx, Rat.cast_nonpos, ← Rat.num_nonpos]
    exact (neg_of_smul_neg_right hy zero_le_one).le
  · rw [le_csSup_iff (ratLt'_bddAbove (0 : M)) (ratLt'_nonempty 0)]
    intro x
    rw [mem_upperBounds]
    suffices (∀ (y : ℚ), y.num • (1 : M) < 0 → y ≤ x) → 0 ≤ x by simpa using this
    intro h
    have h' (y : ℚ) (hy : y < 0) : y ≤ x := by
      exact h _ <| (smul_neg_iff_of_neg_left (by simpa using hy)).mpr zero_lt_one
    contrapose! h'
    obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'
    exact ⟨y, by simpa using hy, hxy⟩

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

Goal state before:
pp: case inr.inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball y r
hd : ball x r = ball y r
⊢ ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ

Tactic:
simp [h.not_ge] at hy

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) < φ.lexOrder
hφ : ¬φ = 0
⊢ (coeff d) φ = 0

Tactic:
rcases lexOrder_def_of_ne_zero hφ with ⟨ne, hφ'⟩

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) < φ.lexOrder
hφ : ¬φ = 0
ne : (⇑toLex '' Function.support φ).Nonempty
hφ' : φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
⊢ (coeff d) φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w (f * g) = weightedOrder w f + weightedOrder w g

Tactic:
by
  apply le_antisymm _ (le_weightedOrder_mul w)
  by_cases hf : f.weightedOrder w < ⊤
  · by_cases hg : g.weightedOrder w < ⊤
    · let p := (f.weightedOrder w).toNat
      have hp : p = f.weightedOrder w := by
        simpa only [p, ENat.natCast_toNat_eq_self, ← lt_top_iff_ne_top]
      let q := (g.weightedOrder w).toNat
      have hq : q = g.weightedOrder w := by
        simpa only [q, ENat.natCast_toNat_eq_self, ← lt_top_iff_ne_top]
      have : f.weightedHomogeneousComponent w p * g.weightedHomogeneousComponent w q ≠ 0 := by
        simp only [ne_eq, mul_eq_zero]
        intro H
        rcases H with H | H <;>
        · refine weightedHomogeneousComponent_of_weightedOrder ?_ H
          simp only [ENat.natCast_toNat_eq_self, ne_eq, weightedOrder_eq_top_iff, p, q]
          rw [← ne_eq, ne_zero_iff_weightedOrder_finite w]
          exact ENat.natCast_toNat (ne_top_of_lt (by simpa))
      rw [← weightedHomogeneousComponent_mul_of_le_weightedOrder
          (le_of_eq hp) (le_of_eq hq)] at this
      rw [← hp, ← hq, ← Nat.cast_add, ← not_lt]
      intro H
      apply this
      apply weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero H
    · rw [not_lt_top_iff] at hg
      simp [hg]
  · rw [not_lt_top_iff] at hf
    simp [hf]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
⊢ Unit_of_divided_by_X_pow_order 0 = 1

Tactic:
by
  simp only [Unit_of_divided_by_X_pow_order, dif_pos]

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R K
inst✝³ : IsDedekindDomain R
inst✝² : IsFractionRing R K
v : HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
x : R
⊢ (HeightOneSpectrum.adicAbv K v) ((algebraMap R K) x) = 1 ↔ x ∉ v.asIdeal

Tactic:
exact v.adicAbv_coe_eq_one_iff (one_lt_absNorm_nnreal v) x

Goal state after: